@@ -6,7 +6,7 @@ import Decidable.Equality
66%default total
77%language FirstClassReflection
88
9−using (xs : List a, ys : List a, G : List (List a))
9+using (xs : List a, ys : List a, gam : List (List a))
1010
1111 data Elem : a -> List a -> Type where
1212 Stop : Elem x (x :: xs)
@@ -16,20 +16,20 @@ using (xs : List a, ys : List a, G : List (List a))
1616-- and over a set of list variables.
1717
1818 data Expr : List (List a) -> List a -> Type where
19− App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys)
20− Var : Elem xs G -> Expr G xs
21− ENil : Expr G []
19+ App : Expr gam xs -> Expr gam ys -> Expr gam (xs ++ ys)
20+ Var : Elem xs gam -> Expr gam xs
21+ ENil : Expr gam []
2222
2323-- Reflection of list equalities, indexed over the concrete equality.
2424
2525 data ListEq : List (List a) -> Type -> Type where
26− EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)
26+ EqP : Expr gam xs -> Expr gam ys -> ListEq gam (xs = ys)
2727
2828-- Fully right associative list expressions
2929
3030 data RExpr : List (List a) -> List a -> Type where
31− RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys)
32− RNil : RExpr G []
31+ RApp : RExpr gam xs -> Elem ys gam -> RExpr gam (xs ++ ys)
32+ RNil : RExpr gam []
3333
3434-- Convert an expression to a right associative expression, and return
3535-- a proof that the rewriting has an equal interpretation to the original
@@ -38,7 +38,7 @@ using (xs : List a, ys : List a, G : List (List a))
3838-- The idea is that we use this proof to build a proof of equality of
3939-- list appends
4040
41− expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))
41+ expr_r : Expr gam xs -> (xs' ** (RExpr gam xs', xs = xs'))
4242 expr_r ENil = (_ ** (RNil, Refl))
4343 expr_r (Var i) = (_ ** (RApp RNil i, Refl))
4444 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in
@@ -46,29 +46,29 @@ using (xs : List a, ys : List a, G : List (List a))
4646 appRExpr _ _ xr yr xprf yprf
4747 where
4848 appRExpr : (xs', ys' : List a) ->
49− {G : List (List a)} -> {xs, ys : List a} ->
50− RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
51− (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
49+ {gam : List (List a)} -> {xs, ys : List a} ->
50+ RExpr gam xs -> RExpr gam ys -> (xs' = xs) -> (ys' = ys) ->
51+ (ws' ** (RExpr gam ws', xs' ++ ys' = ws'))
5252 appRExpr x' y' rxs (RApp e i) xprf yprf
5353 = let (xs ** (rec, prf)) = appRExpr _ _ rxs e Refl Refl in
5454 (_ ** (RApp rec i, ?appRExpr1))
5555 appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))
5656
57− r_expr : RExpr G xs -> Expr G xs
57+ r_expr : RExpr gam xs -> Expr gam xs
5858 r_expr RNil = ENil
5959 r_expr (RApp xs i) = App (r_expr xs) (Var i)
6060
6161-- Convert an expression to some other equivalent expression (which
6262-- just happens to be normalised to right associative form)
6363
64− reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs'))
64+ reduce : Expr gam xs -> (xs' ** (Expr gam xs', xs = xs'))
6565 reduce e = let (x' ** (e', prf)) = expr_r e in
6666 (x' ** (r_expr e', prf))
6767
6868-- Build a proof that two expressions are equal. If they are, we'll know
6969-- that the indices are equal.
7070
71− eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->
71+ eqExpr : (e : Expr gam xs) -> (e' : Expr gam ys) ->
7272 Maybe (e = e')
7373 eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')
7474 eqExpr (App x y) (App x y) | (Just Refl, Just Refl) = Just Refl
@@ -83,20 +83,20 @@ using (xs : List a, ys : List a, G : List (List a))
8383-- they are equal
8484
8585 buildProof : {xs : List a} -> {ys : List a} ->
86− Expr G ln -> Expr G rn ->
86+ Expr gam ln -> Expr gam rn ->
8787 (xs = ln) -> (ys = rn) -> Maybe (xs = ys)
8888 buildProof e e' lp rp with (eqExpr e e')
8989 buildProof e e lp rp | Just Refl = ?bp1
9090 buildProof e e' lp rp | Nothing = Nothing
9191
92− testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)
92+ testEq : Expr gam xs -> Expr gam ys -> Maybe (xs = ys)
9393 testEq l r = let (ln ** (l', lPrf)) = reduce l in
9494 let (rn ** (r', rPrf)) = reduce r in
9595 buildProof l' r' lPrf rPrf
9696
9797-- Given a reflected equality, try to produce a proof that holds
9898
99− prove : ListEq G t -> Maybe t
99+ prove : ListEq gam t -> Maybe t
100100 prove (EqP xs ys) = testEq xs ys
101101
102102 getJust : (x : Maybe a) -> IsJust x -> a
@@ -114,15 +114,15 @@ using (xs : List a, ys : List a, G : List (List a))
114114 isElem x (x :: ys) | Just Refl = [| Stop |]
115115 isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]
116116
117− weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)
117+ weakenElem : (gam' : List a) -> Elem x xs -> Elem x (gam' ++ xs)
118118 weakenElem [] p = p
119− weakenElem (g :: G) p = Pop (weakenElem G p)
119+ weakenElem (g :: gam) p = Pop (weakenElem gam p)
120120
121− weaken : (G' : List (List a)) ->
122− Expr G xs -> Expr (G' ++ G) xs
123− weaken G' (App l r) = App (weaken G' l) (weaken G' r)
124− weaken G' (Var x) = Var (weakenElem G' x)
125− weaken G' ENil = ENil
121+ weaken : (gam' : List (List a)) ->
122+ Expr gam xs -> Expr (gam' ++ gam) xs
123+ weaken gam' (App l r) = App (weaken gam' l) (weaken gam' r)
124+ weaken gam' (Var x) = Var (weakenElem gam' x)
125+ weaken gam' ENil = ENil
126126
127127
128128-- Now, some reflection magic.
@@ -133,21 +133,21 @@ using (xs : List a, ys : List a, G : List (List a))
133133-- reduction will work the right way.
134134
135135%reflection
136−reflectList : (G : List (List a)) ->
137− (xs : List a) -> (G' ** Expr (G' ++ G) xs)
138−reflectList G [] = ([] ** ENil)
139−
140−reflectList G (x :: xs) with (reflectList G xs)
141− | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
142− | Just p = (G' ** App (Var p) xs')
143− | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
144−
145−reflectList G (xs ++ ys) with (reflectList G xs)
146− | (G' ** xs') with (reflectList (G' ++ G) ys)
147− | (G'' ** ys') = ((G'' ++ G') **
148− rewrite (sym (appendAssociative G'' G' G)) in
149− App (weaken G'' xs') ys')
150−reflectList G t with (isElem t G)
136+reflectList : (gam : List (List a)) ->
137+ (xs : List a) -> (gam' ** Expr (gam' ++ gam) xs)
138+reflectList gam [] = ([] ** ENil)
139+
140+reflectList gam (x :: xs) with (reflectList gam xs)
141+ | (gam' ** xs') with (isElem (List.(::) x []) (gam' ++ gam))
142+ | Just p = (gam' ** App (Var p) xs')
143+ | Nothing = ([x] :: gam' ** App (Var Stop) (weaken [[x]] xs'))
144+
145+reflectList gam (xs ++ ys) with (reflectList gam xs)
146+ | (gam' ** xs') with (reflectList (gam' ++ gam) ys)
147+ | (gam'' ** ys') = ((gam'' ++ gam') **
148+ rewrite (sym (appendAssociative gam'' gam' gam)) in
149+ App (weaken gam'' xs') ys')
150+reflectList gam t with (isElem t gam)
151151 | Just p = ([] ** Var p)
152152 | Nothing = ([t] ** Var Stop)
153153
@@ -160,12 +160,12 @@ reflectList G t with (isElem t G)
160160-- forms of equality proofs anyway.
161161
162162%reflection
163−reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
164−reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
165− | (G' ** xs') with (reflectList (G' ++ G) ys)
166− | (G'' ** ys') = ((G'' ++ G') **
167− rewrite (sym (appendAssociative G'' G' G)) in
168− EqP (weaken G'' xs') ys')
163+reflectEq : (a : Type) -> (gam : List (List a)) -> (P : Type) -> (gam' ** ListEq (gam' ++ gam) P)
164+reflectEq a gam (the (List a) xs = the (List a) ys) with (reflectList gam xs)
165+ | (gam' ** xs') with (reflectList (gam' ++ gam) ys)
166+ | (gam'' ** ys') = ((gam'' ++ gam') **
167+ rewrite (sym (appendAssociative gam'' gam' gam)) in
168+ EqP (weaken gam'' xs') ys')
169169
170170
171171-- Need these before we can test it or the reductions won't normalise fully...