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 {ctx = []} (MkLevel _ _) impossible
192 |
193 |   export
194 |   irrelevantAtLevel :
195 |     (p : AtLevel n nm ctx) ->
196 |     (q : AtLevel n nm' ctx) ->
197 |     (nm === nm', p ~=~ q)
198 |   irrelevantAtLevel (H Refl) (H Refl) = (Refl, Refl)
199 |   irrelevantAtLevel (H Refl) (T q) = void (levelIsFin reflexive q)
200 |   irrelevantAtLevel (T p) (H Refl) = void (levelIsFin reflexive p)
201 |   irrelevantAtLevel (T p) (T q) with (irrelevantAtLevel p q)
202 |     irrelevantAtLevel (T p) (T p) | (Refl, Refl) = (Refl, Refl)
203 |
204 |   export
205 |   hetEqDec : (v : Level nm g) -> (w : Level nm' g) ->
206 |              Dec (nm === nm', v ~=~ w)
207 |   hetEqDec (MkLevel m p) (MkLevel n q) with (decEq m n)
208 |     _ | No neq = No (\ (Refl, Refl) => neq Refl)
209 |     hetEqDec (MkLevel m p) (MkLevel m q) | Yes Refl
210 |       with 0 (snd (irrelevantAtLevel p q))
211 |       hetEqDec (MkLevel m p) (MkLevel m p) | Yes Refl | Refl = Yes (Refl, Refl)
212 |
213 | ------------------------------------------------------------------------------
214 | -- Conversion
215 | ------------------------------------------------------------------------------
216 |
217 | public export
218 | rev : List a -> SnocList a
219 | rev [] = [<]
220 | rev (x :: xs) = rev xs :< x
221 |
222 | data Plus : (m, n, p : Nat) -> Type where
223 |   PlusZ : Plus 0 n n
224 |   PlusS : Plus m n p -> Plus (S m) n (S p)
225 |
226 | zeroPlusRight : (m : Nat) -> Plus m 0 m
227 | zeroPlusRight 0 = PlusZ
228 | zeroPlusRight (S m) = PlusS (zeroPlusRight m)
229 |
230 | succPlusRight : Plus m n p -> Plus m (S n) (S p)
231 | succPlusRight PlusZ = PlusZ
232 | succPlusRight (PlusS p) = PlusS (succPlusRight p)
233 |
234 | 0 plusIsGreater : Plus m n p -> LTE n p
235 | plusIsGreater PlusZ = reflexive
236 | plusIsGreater (PlusS prf) = lteSuccRight (plusIsGreater prf)
237 |
238 | levelLT : {ctx : _} -> AtLevel i nm ctx -> LT i (length ctx)
239 | levelLT (H Refl) = reflexive
240 | levelLT (T p) = LTESucc (lteSuccLeft (levelLT p))
241 |
242 | export
243 | lteIsPlus : {n : Nat} -> LTE m n -> Plus (minus n m) m n
244 | lteIsPlus LTEZero = rewrite minusZeroRight n in zeroPlusRight n
245 | lteIsPlus (LTESucc p) = succPlusRight (lteIsPlus p)
246 |
247 | namespace Invariant
248 |
249 |   export
250 |   asIndex : {ls : _} ->
251 |             AtLevel n nm ls ->
252 |             AtIndex (length ls `minus` S n) nm (rev ls)
253 |   asIndex p = go p (lteIsPlus (levelLT p)) where
254 |
255 |     go : forall n, nm, ls, i.
256 |          AtLevel n nm ls ->
257 |          Plus i (S n) (length ls) ->
258 |          AtIndex i nm (rev ls)
259 |     go (H Refl) PlusZ = Z
260 |     go (H Refl) (PlusS prf) = void (succNotLTEpred (plusIsGreater prf))
261 |     go (T p) PlusZ = void (levelIsFin reflexive p)
262 |     go (T p) (PlusS prf) = S (go p prf)
263 |
264 |
265 |
266 | export
267 | asIndex : {ls : _} -> Level nm ls -> Index nm (rev ls)
268 | asIndex (MkLevel n prf) = MkIndex (length ls `minus` S n) (asIndex prf)
269 |