
   0 | ||| Fresh lists, a variant of Catarina Coquand's contexts in "A
   1 | ||| Formalised Proof of the Soundness and Completeness of a Simply
   2 | ||| Typed Lambda-Calculus with Explicit Substitutions"
   3 | |||
   4 | ||| Based directly on Agda's fresh lists:
   5 | ||| http://agda.github.io/agda-stdlib/Data.List.Fresh.html
   6 | module Data.List.Fresh
   7 | 
   8 | import public Data.So
   9 | 
  10 | %hide Builtin.infixr.(#)
  11 | 
  12 | %default total
  13 | 
  14 | -- Boolean "relation"
  15 | public export
  16 | BRel : Type -> Type
  17 | BRel a = a -> a -> Bool
  18 | 
  19 | export infix 4 #, ##, #?
  20 | 
  21 | public export
  22 | data FreshList : (a : Type) -> (neq : BRel a) -> Type
  23 | 
  24 | -- The boolean version
  25 | public export
  26 | (##) : {neq : BRel a} -> (x : a) -> (xs : FreshList a neq) -> Bool
  27 | -- The type version
  28 | public export
  29 | (#) : {neq : BRel a} -> (x : a) -> (xs : FreshList a neq) -> Type
  30 | 
  31 | public export
  32 | data FreshList : (a : Type) -> (neq : BRel a) -> Type where
  33 |   Nil  : FreshList a neq
  34 |   (::) : (x : a) -> (xs : FreshList a neq) ->
  35 |          {auto 0 fresh : x # xs} ->
  36 |          FreshList a neq
  37 | 
  38 | %name FreshList xs, ys, zs
  39 | 
  40 | x ##    []     = True
  41 | x ## (y :: xs) = (x `neq` y) && (x ## xs)
  42 | 
  43 | x # xs = So (x ## xs)
  44 | 
  45 | namespace FreshList1
  46 | 
  47 |   public export
  48 |   data FreshList1 : (a : Type) -> (neq : BRel a) -> Type where
  49 |     (::) : (x : a) -> (xs : FreshList a neq) ->
  50 |            {auto 0 fresh : x # xs} ->
  51 |            FreshList1 a neq
  52 | 
  53 | parameters
  54 |   {0 A : Type} {0 Aneq : BRel A}
  55 |   {0 B : Type} {0 Bneq : BRel B}
  56 |   (F : A -> B)
  57 |   (Injectivity : (x,y : A) -> So (x `Aneq` y) -> So (F x `Bneq` F y))
  58 | 
  59 |   public export
  60 |   map : FreshList A Aneq -> FreshList B Bneq
  61 | 
  62 |   public export
  63 |   0 mapFreshness : {x : A} -> (ys : FreshList A Aneq) ->
  64 |                    x # ys -> F x # map ys
  65 | 
  66 |   map     []              = []
  67 |   map ((x :: xs) {fresh}) = (F x :: map xs) {fresh = mapFreshness xs fresh}
  68 | 
  69 |   mapFreshness    []              _
  70 |     = Oh
  71 |   mapFreshness (y :: ys) p
  72 |     = let (x_fresh_y, x_fresh_ys) = soAnd p in
  73 |       andSo (Injectivity _ _ x_fresh_y, mapFreshness ys x_fresh_ys)
  74 | 
  75 | namespace View
  76 |   public export
  77 |   data Empty : FreshList a neq -> Type where
  78 |     Nil : Empty Nil
  79 | 
  80 |   public export
  81 |   data NonEmpty : FreshList a neq -> Type where
  82 |     IsNonEmpty : NonEmpty ((x :: xs) {fresh})
  83 | 
  84 | public export
  85 | length : FreshList a neq -> Nat
  86 | length [] = 0
  87 | length (x :: xs) = 1 + length xs
  88 | 
  89 | public export
  90 | fromMaybe : Maybe a -> FreshList a neq
  91 | fromMaybe Nothing  = []
  92 | fromMaybe (Just x) = [x]
  93 | 
  94 | -- I don't include replicate since freshness ought not to be
  95 | -- reflexive, but feel free to add it if you need it
  96 | 
  97 | public export
  98 | uncons : FreshList a neq -> Maybe (a , FreshList a neq)
  99 | uncons    []     = Nothing
 100 | uncons (x :: xs) = Just (x, xs)
 101 | 
 102 | public export
 103 | toFreshList1 : FreshList a neq -> Maybe (FreshList1 a neq)
 104 | toFreshList1    []     = Nothing
 105 | toFreshList1 (x :: xs) = Just (x :: xs)
 106 | 
 107 | public export
 108 | head : (xs : FreshList a neq) -> (isNonEmpty : NonEmpty xs) => a
 109 | head (x :: xs) {isNonEmpty = IsNonEmpty} = x
 110 | 
 111 | public export
 112 | tail : (xs : FreshList a neq) -> (isNonEmpty : NonEmpty xs) => FreshList a neq
 113 | tail (x :: xs) {isNonEmpty = IsNonEmpty} = xs
 114 | 
 115 | public export
 116 | 0 (.freshness) : (xs : FreshList a neq) -> (isNonEmpty : NonEmpty xs) =>
 117 |                  head xs # tail xs
 118 | (((x :: xs) {fresh}).freshness) {isNonEmpty = IsNonEmpty} = fresh
 119 | 
 120 | -- Freshness lemmata
 121 | parameters (0 x : a) (ys : FreshList a neq) {auto isNonEmpty : NonEmpty ys}
 122 |   public export
 123 |   0 headFreshness : x # ys -> So (x `neq` head ys)
 124 | 
 125 |   public export
 126 |   0 tailFreshness : x # ys -> x # (tail ys)
 127 | 
 128 | headFreshness x (y :: ys) {isNonEmpty = IsNonEmpty} freshness
 129 |   = fst (soAnd freshness)
 130 | tailFreshness x (y :: ys) {isNonEmpty = IsNonEmpty} freshness
 131 |   = snd (soAnd freshness)
 132 | 
 133 | public export
 134 | take : Nat -> FreshList a neq -> FreshList a neq
 135 | public export
 136 | 0 takeFreshness : (n : Nat) -> (xs : FreshList a neq) -> y # xs -> y # take n xs
 137 | 
 138 | take 0     xs                  = []
 139 | take (S n)     []              = []
 140 | take (S n) ((x :: xs) {fresh}) = (x :: take n xs) {fresh = takeFreshness n xs fresh}
 141 | 
 142 | takeFreshness  0          xs  fresh = Oh
 143 | takeFreshness (S n)    []     fresh = Oh
 144 | takeFreshness (S n) (x :: xs) fresh =
 145 |   let (y_neq_x, y_fresh_xs) = soAnd fresh in
 146 |   andSo (y_neq_x, takeFreshness n xs y_fresh_xs)
 147 | 
 148 | public export
 149 | drop : Nat -> FreshList a neq -> FreshList a neq
 150 | drop 0           xs  = xs
 151 | drop (S n)    []     = []
 152 | drop (S n) (x :: xs) = drop n xs
 153 | 
 154 | -- The Agda lib has more general takeWhile, dropWhile, filter
 155 | -- involving decidable predicts, but we follow the Idris stdlib and
 156 | -- use the special case for Bool
 157 | 
 158 | public export
 159 | takeWhile : (pred : a -> Bool) -> FreshList a neq -> FreshList a neq
 160 | public export
 161 | 0 takeWhileFreshness : (pred : a -> Bool) -> (xs : FreshList a neq) ->
 162 |   y # xs -> y # takeWhile pred xs
 163 | 
 164 | takeWhile pred     []              = []
 165 | takeWhile pred ((x :: xs) {fresh}) = case pred x of
 166 |   True  => (x :: takeWhile pred xs) {fresh = takeWhileFreshness pred xs fresh}
 167 |   False => []
 168 | 
 169 | takeWhileFreshness  pred []           fresh
 170 |   = Oh
 171 | takeWhileFreshness  pred (x :: xs) fresh with (pred x)
 172 |  takeWhileFreshness pred (x :: xs) fresh | True
 173 |   = let (y_fresh_x, y_fresh_xs) = soAnd fresh in
 174 |     andSo (y_fresh_x, takeWhileFreshness pred xs y_fresh_xs)
 175 |  takeWhileFreshness pred (x :: xs) fresh | False
 176 |   = Oh
 177 | 
 178 | public export
 179 | dropWhile : (pred : a -> Bool) -> FreshList a neq -> FreshList a neq
 180 | 
 181 | public export
 182 | 0 dropWhileFreshness : (pred : a -> Bool) -> (xs : FreshList a neq) ->
 183 |   y # xs -> y # dropWhile pred xs
 184 | 
 185 | 
 186 | dropWhile pred     []              = []
 187 | dropWhile pred ((x :: xs) {fresh}) = case pred x of
 188 |   True  => (x :: dropWhile pred xs) {fresh = dropWhileFreshness pred xs fresh}
 189 |   False => []
 190 | 
 191 | dropWhileFreshness  pred    []     fresh = Oh
 192 | dropWhileFreshness  pred (x :: xs) fresh with (pred x)
 193 |  dropWhileFreshness pred (x :: xs) fresh | False
 194 |    = Oh
 195 |  dropWhileFreshness pred (x :: xs) fresh | True
 196 |    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
 197 |      andSo (y_neq_x, dropWhileFreshness pred xs y_fresh_xs)
 198 | 
 199 | public export
 200 | filter : (pred : a -> Bool) -> FreshList a neq -> FreshList a neq
 201 | public export
 202 | 0 filterFreshness : (pred : a -> Bool) -> (xs : FreshList a neq) ->
 203 |   y # xs -> y # filter pred xs
 204 | 
 205 | filter pred     []              = []
 206 | filter pred ((x :: xs) {fresh}) = case pred x of
 207 |   False => filter pred xs
 208 |   True  => (x :: filter pred xs) {fresh = filterFreshness pred xs fresh}
 209 | 
 210 | filterFreshness  pred    []     fresh = Oh
 211 | filterFreshness  pred (x :: xs) fresh with (pred x)
 212 |  filterFreshness pred (x :: xs) fresh | False
 213 |    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
 214 |      filterFreshness pred xs y_fresh_xs
 215 |  filterFreshness pred (x :: xs) fresh | True
 216 |    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
 217 |      andSo (y_neq_x, filterFreshness pred xs y_fresh_xs)
 218 | 
 219 | -- Todo: move `decSo : (b : Bool) -> Dec (So b)` to base
 220 | public export
 221 | decideFreshness : {neq : BRel a} ->
 222 |                   (x : a) -> (ys : FreshList a neq) ->
 223 |                   Dec (x # ys)
 224 | decideFreshness x ys with (x ## ys)
 225 |   decideFreshness x ys | True  = Yes Oh
 226 |   decideFreshness x ys | False = No absurd
 227 | 
 228 | public export
 229 | foldl : (f : b -> a -> b) -> b -> FreshList a neq -> b
 230 | foldl f x [] = x
 231 | foldl f x (y :: ys) = foldl f (x `f` y) ys
 232 | 
 233 | public export
 234 | foldr : (f : a -> b -> b) -> b -> FreshList a neq -> b
 235 | foldr f x [] = x
 236 | foldr f x (val :: vals) = (val `f` foldr f x vals)
 237 | 
 238 | namespace String
 239 |   public export
 240 |   (##) : BRel String
 241 |   s ## t = (s /= t)
 242 | 
 243 | namespace Aux
 244 |   public export
 245 |   FreshSnoc : {a : Type} -> {neq : BRel a} -> SnocList a -> FreshList a neq -> Type
 246 | 
 247 | public export
 248 | castAux : (sx : SnocList a) -> (xs : FreshList a neq) ->
 249 |   {auto 0 fresh : FreshSnoc {neq} sx xs} -> FreshList a neq
 250 | 
 251 | namespace Aux
 252 | 
 253 |   FreshSnoc [<] xs = ()
 254 |   FreshSnoc (sx :< x) xs = (fresh : x # xs ** FreshSnoc sx ((x :: xs) {fresh}))
 255 | 
 256 | castAux     [<]   xs = xs
 257 | castAux (sx :< x) xs {fresh}
 258 |   = castAux sx ((x :: xs) {fresh = fresh.fst}) {fresh = fresh.snd}
 259 | 
 260 | public export
 261 | Fresh : {a : Type} -> {neq : BRel a} -> SnocList a -> Type
 262 | Fresh {neq} sx = FreshSnoc {neq} sx []
 263 | 
 264 | public export
 265 | cast : (sx : SnocList a) -> {auto 0 fresh : Fresh {neq} sx} -> FreshList a neq
 266 | cast sx = castAux sx []
 267 |