0 | module Language.IntrinsicScoping.Variables
  1 |
  2 | import Decidable.Equality
  3 | import Data.Nat
  4 | import Data.Nat.Order
  5 | import Data.SnocList
  6 |
  7 | %default total
  8 |
  9 | ------------------------------------------------------------------------------
 10 | -- De Bruijn indices
 11 | ------------------------------------------------------------------------------
 12 |
 13 | ||| We do not really care about the notion of names used here
 14 | ||| as long as it has a decidable notion of equality.
 15 | ||| String will do for now
 16 | export
 17 | Name : Type
 18 | Name = String
 19 |
 20 | export
 21 | FromString Name where
 22 |   fromString = id
 23 |
 24 | STRING : DecEq String
 25 | STRING = %search
 26 |
 27 | export
 28 | DecEq Name where
 29 |   decEq = decEq @{STRING}
 30 |
 31 | ||| A context of De Bruijn indices is right-to-left.
 32 | ||| Just like in typing rules, newly bound variables are added
 33 | ||| at the most local end with index 0, and all other variables
 34 | ||| see their index shifted by 1.
 35 | public export
 36 | IContext : Type
 37 | IContext = SnocList Name
 38 |
 39 | ||| De Bruijn indices are right-to-left, starting from 0
 40 | public export
 41 | data AtIndex : Nat -> Name -> IContext -> Type where
 42 |   Z : AtIndex 0 nm (g :< nm)
 43 |   S : AtIndex n nm g -> AtIndex (S n) nm (g :< _)
 44 |
 45 | ||| An index is the pairing of its encoding as a natural number
 46 | ||| and the proof it is valid
 47 | public export
 48 | record Index (nm : Name) (ctx : IContext) where
 49 |   constructor MkIndex
 50 |   getIndex : Nat
 51 |   0 validIndex : AtIndex getIndex nm ctx
 52 |
 53 | namespace Index
 54 |
 55 |   public export
 56 |   fresh : Index nm (ctx :< nm)
 57 |   fresh = MkIndex 0 Z
 58 |
 59 |   public export
 60 |   weaken : Index nm ctx -> Index nm (ctx :< _)
 61 |   weaken (MkIndex n p) = MkIndex (S n) (S p)
 62 |
 63 |   export
 64 |   Injective Index.weaken where
 65 |     injective {x = MkIndex m p} {y = MkIndex m p} Refl = Refl
 66 |
 67 |   public export
 68 |   data View : Index nm ctx -> Type where
 69 |     Z : View (Index.fresh {nm, ctx})
 70 |     S : (p : Index nm ctx) -> View (weaken p)
 71 |
 72 |   public export
 73 |   view : (p : Index nm ctx) -> View p
 74 |   view (MkIndex 0 Z) = Z
 75 |   view (MkIndex (S i) (S prf)) = S (MkIndex i prf)
 76 |
 77 |   export
 78 |   isLast : {g : _} -> Index nm ([<x] <+> g) -> Either (nm === x) (Index nm g)
 79 |   isLast {g = [<]} v@_ with (view v)
 80 |     _ | Z = Left Refl
 81 |     _ | S v' = Right v'
 82 |   isLast {g = (sx :< y)} v@_ with (view v)
 83 |     _ | Z = Right fresh
 84 |     _ | S v' = map weaken (isLast v')
 85 |
 86 |   public export
 87 |   delete : {g : IContext} -> Index nm g -> IContext
 88 |   delete v@_ with (view v)
 89 |     delete {g = g :< _} v@_ | Z = g
 90 |     delete {g = _ :< x} v@_ | S n = delete n :< x
 91 |
 92 |   export
 93 |   thicken : (v : Index nm g) -> (v' : Index nm' g) ->
 94 |             Either (nm === nm', v ~=~ v') (Index nm' (delete v))
 95 |   thicken v@_ w@_ with (view v) | (view w)
 96 |     _ | Z | Z = Left (Refl, Refl)
 97 |     _ | Z | S w' = Right w'
 98 |     _ | S _ | Z = Right fresh
 99 |     _ | S v' | S w' with (thicken v' w')
100 |       _ | Left (Refl, p) = Left (Refl, cong weaken p)
101 |       _ | Right res = Right (weaken res)
102 |
103 |   export
104 |   irrelevantAtIndex :
105 |     (p : AtIndex n nm g) ->
106 |     (q : AtIndex n nm' g) ->
107 |     (nm === nm', p ~=~ q)
108 |   irrelevantAtIndex Z Z = (Refl, Refl)
109 |   irrelevantAtIndex (S p) (S q) with (irrelevantAtIndex p q)
110 |     irrelevantAtIndex (S p) (S q) | (Refl, eq) = (Refl, cong S eq)
111 |
112 |   export
113 |   hetEqDec : (v : Index nm g) -> (w : Index nm' g) ->
114 |              Dec (nm === nm', v ~=~ w)
115 |   hetEqDec (MkIndex m p) (MkIndex n q) with (decEq m n)
116 |     _ | No neq = No (\ (Refl, Refl) => neq Refl)
117 |     hetEqDec (MkIndex m p) (MkIndex m q) | Yes Refl
118 |       with 0 (snd (irrelevantAtIndex p q))
119 |       hetEqDec (MkIndex m p) (MkIndex m p) | Yes Refl | Refl = Yes (Refl, Refl)
120 |
121 | ------------------------------------------------------------------------------
122 | -- De Bruijn levels
123 | ------------------------------------------------------------------------------
124 |
125 | ||| A context of De Bruijn levels is left-to-right
126 | ||| Newly bound variables are added at the far end, with index (length ctx).
127 | ||| This has the advantage that all other variables have an unchanged level.
128 | public export
129 | LContext : Type
130 | LContext = List Name
131 |
132 | public export
133 | data AtLevel : Nat -> Name -> LContext -> Type where
134 |   H : {0 ctx : LContext} -> {0 nm : String} ->
135 |       n = length ctx -> AtLevel n nm (nm :: ctx)
136 |   T : {0 ctx : LContext} -> {0 nm : String} ->
137 |       AtLevel n nm ctx -> AtLevel n nm (_ :: ctx)
138 |
139 | levelIsFin : LTE (length ctx) i -> Not (AtLevel i nm ctx)
140 | levelIsFin lte (H Refl) = void (succNotLTEpred lte)
141 | levelIsFin lte (T p) = levelIsFin (lteSuccLeft lte) p
142 |
143 | ||| A level is the pairing of its encoding as a natural number
144 | ||| and the proof it is valid
145 | public export
146 | record Level (nm : Name) (ctx : LContext) where
147 |   constructor MkLevel
148 |   getLevel : Nat
149 |   0 validIndex : AtLevel getLevel nm ctx
150 |
151 | namespace Level
152 |
153 |   export
154 |   weaken : Level nm ctx -> Level nm (_ :: ctx)
155 |   weaken (MkLevel n prf) = MkLevel n (T prf)
156 |
157 |   export
158 |   fresh : {ctx : _} -> Level nm (nm :: ctx)
159 |   fresh = MkLevel (length ctx) (H Refl)
160 |
161 |   public export
162 |   data View : Level nm ctx -> Type where
163 |     Z : View (Level.fresh {nm, ctx})
164 |     S : (p : Level nm ctx) -> View (weaken p)
165 |
166 |   invertH : (prf : AtLevel (length ctx) nm (nm' :: ctx)) ->
167 |             (nm === nm', prf ~=~ H {nm, ctx} Refl)
168 |   invertH (H Refl) = (Refl, Refl)
169 |   invertH (T p) = void (levelIsFin reflexive p)
170 |
171 |   invertT : (prf : AtLevel l nm (nm' :: ctx)) ->
172 |             Not (l === length ctx) ->
173 |             (p' : AtLevel l nm ctx ** prf === T p')
174 |   invertT (H eq) neq = void (neq eq)
175 |   invertT (T p) neq = (p ** Refl)
176 |
177 |   viewAux :
178 |     {l : Nat} -> (0 p : AtLevel l nm (nm' :: ctx)) ->
179 |     (0 p' : AtLevel l nm ctx) -> (0 _ : p === T p') ->
180 |     View (MkLevel l p)
181 |   viewAux .(T p') p' Refl = S (MkLevel l p')
182 |
183 |   public export
184 |   view : {ctx : _} -> (p : Level nm ctx) -> View p
185 |   view  {ctx = nm :: ctx} (MkLevel l p) with (decEq l (length ctx))
186 |     view {ctx = nm :: ctx} (MkLevel .(length ctx) p)
187 |       | Yes Refl with 0 (snd (invertH p))
188 |       view {ctx = nm :: ctx} (MkLevel .(length ctx) .(H Refl))
189 |         | Yes Refl | Refl = Z
190 |     view (MkLevel l p) | No neq = viewAux p _ (snd (invertT p neq))
191 |   view (MkLevel _ (H prf)) impossible
192 |   view (MkLevel _ (T x)) impossible
193 |
194 |   export
195 |   irrelevantAtLevel :
196 |     (p : AtLevel n nm ctx) ->
197 |     (q : AtLevel n nm' ctx) ->
198 |     (nm === nm', p ~=~ q)
199 |   irrelevantAtLevel (H Refl) (H Refl) = (Refl, Refl)
200 |   irrelevantAtLevel (H Refl) (T q) = void (levelIsFin reflexive q)
201 |   irrelevantAtLevel (T p) (H Refl) = void (levelIsFin reflexive p)
202 |   irrelevantAtLevel (T p) (T q) with (irrelevantAtLevel p q)
203 |     irrelevantAtLevel (T p) (T p) | (Refl, Refl) = (Refl, Refl)
204 |
205 |   export
206 |   hetEqDec : (v : Level nm g) -> (w : Level nm' g) ->
207 |              Dec (nm === nm', v ~=~ w)
208 |   hetEqDec (MkLevel m p) (MkLevel n q) with (decEq m n)
209 |     _ | No neq = No (\ (Refl, Refl) => neq Refl)
210 |     hetEqDec (MkLevel m p) (MkLevel m q) | Yes Refl
211 |       with 0 (snd (irrelevantAtLevel p q))
212 |       hetEqDec (MkLevel m p) (MkLevel m p) | Yes Refl | Refl = Yes (Refl, Refl)
213 |
214 | ------------------------------------------------------------------------------
215 | -- Conversion
216 | ------------------------------------------------------------------------------
217 |
218 | public export
219 | rev : List a -> SnocList a
220 | rev [] = [<]
221 | rev (x :: xs) = rev xs :< x
222 |
223 | data Plus : (m, n, p : Nat) -> Type where
224 |   PlusZ : Plus 0 n n
225 |   PlusS : Plus m n p -> Plus (S m) n (S p)
226 |
227 | zeroPlusRight : (m : Nat) -> Plus m 0 m
228 | zeroPlusRight 0 = PlusZ
229 | zeroPlusRight (S m) = PlusS (zeroPlusRight m)
230 |
231 | succPlusRight : Plus m n p -> Plus m (S n) (S p)
232 | succPlusRight PlusZ = PlusZ
233 | succPlusRight (PlusS p) = PlusS (succPlusRight p)
234 |
235 | 0 plusIsGreater : Plus m n p -> LTE n p
236 | plusIsGreater PlusZ = reflexive
237 | plusIsGreater (PlusS prf) = lteSuccRight (plusIsGreater prf)
238 |
239 | levelLT : {ctx : _} -> AtLevel i nm ctx -> LT i (length ctx)
240 | levelLT (H Refl) = reflexive
241 | levelLT (T p) = LTESucc (lteSuccLeft (levelLT p))
242 |
243 | export
244 | lteIsPlus : {n : Nat} -> LTE m n -> Plus (minus n m) m n
245 | lteIsPlus LTEZero = rewrite minusZeroRight n in zeroPlusRight n
246 | lteIsPlus (LTESucc p) = succPlusRight (lteIsPlus p)
247 |
248 | namespace Invariant
249 |
250 |   export
251 |   asIndex : {ls : _} ->
252 |             AtLevel n nm ls ->
253 |             AtIndex (length ls `minus` S n) nm (rev ls)
254 |   asIndex p = go p (lteIsPlus (levelLT p)) where
255 |
256 |     go : forall n, nm, ls, i.
257 |          AtLevel n nm ls ->
258 |          Plus i (S n) (length ls) ->
259 |          AtIndex i nm (rev ls)
260 |     go (H Refl) PlusZ = Z
261 |     go (H Refl) (PlusS prf) = void (succNotLTEpred (plusIsGreater prf))
262 |     go (T p) PlusZ = void (levelIsFin reflexive p)
263 |     go (T p) (PlusS prf) = S (go p prf)
264 |
265 |
266 |
267 | export
268 | asIndex : {ls : _} -> Level nm ls -> Index nm (rev ls)
269 | asIndex (MkLevel n prf) = MkIndex (length ls `minus` S n) (asIndex prf)
270 |