@@ -9,7 +9,7 @@ using (xs : List a, ys : List a, G : List (List a))
9 Stop : Elem x (x :: xs)
9 Stop : Elem x (x :: xs)
10 Pop : Elem x ys -> Elem x (y :: xs)
10 Pop : Elem x ys -> Elem x (y :: xs)
12−-- Expr is a Reflection of a list, indexed over the concrete list,
12+-- Expr is a reflection of a list, indexed over the concrete list,
13-- and over a set of list variables.
13-- and over a set of list variables.
15 data Expr : List (List a) -> List a -> Type where
15 data Expr : List (List a) -> List a -> Type where
@@ -76,7 +76,7 @@ using (xs : List a, ys : List a, G : List (List a))
76 eqExpr ENil ENil = Just Refl
76 eqExpr ENil ENil = Just Refl
77 eqExpr _ _ = Nothing
77 eqExpr _ _ = Nothing
79−-- Given a couple of Reflected expressions, try to produce a proof that
79+-- Given a couple of reflected expressions, try to produce a proof that
80-- they are equal
80-- they are equal
82 buildProof : {xs : List a} -> {ys : List a} ->
82 buildProof : {xs : List a} -> {ys : List a} ->
@@ -91,7 +91,7 @@ using (xs : List a, ys : List a, G : List (List a))
91 let (rn ** (r', rPrf)) = reduce r in
91 let (rn ** (r', rPrf)) = reduce r in
92 buildProof l' r' lPrf rPrf
92 buildProof l' r' lPrf rPrf
94−-- Given a Reflected equality, try to produce a proof that holds
94+-- Given a reflected equality, try to produce a proof that holds
96 prove : ListEq G t -> Maybe t
96 prove : ListEq G t -> Maybe t
97 prove (EqP xs ys) = testEq xs ys
97 prove (EqP xs ys) = testEq xs ys
@@ -103,7 +103,7 @@ using (xs : List a, ys : List a, G : List (List a))
103-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
103-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
104-- (at compile-time only) attempts to construct a proof that its arguments
104-- (at compile-time only) attempts to construct a proof that its arguments
105-- are syntactically equal. We'll find this useful for referring to variables
105-- are syntactically equal. We'll find this useful for referring to variables
106−-- in Reflected terms.
106+-- in reflected terms.
108 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
108 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
109 isElem x [] = Nothing
109 isElem x [] = Nothing
@@ -122,44 +122,44 @@ using (xs : List a, ys : List a, G : List (List a))
122 weaken G' ENil = ENil
122 weaken G' ENil = ENil
125−-- Now, some Reflection magic.
125+-- Now, some reflection magic.
126−-- %Reflection means a function runs on syntax, rather than on constructors.
126+-- %reflection means a function runs on syntax, rather than on constructors.
127−-- So, 'ReflectList' builds a Reflected List expression as defined above.
127+-- So, 'reflectList' builds a reflected List expression as defined above.
129−-- It also converts (x :: xs) into a Reflected [x] ++ xs so that the above
129+-- It also converts (x :: xs) into a reflected [x] ++ xs So that the above
130-- reduction will work the right way.
130-- reduction will work the right way.
132−%Reflection
132+%reflection
133−ReflectList : (G : List (List a)) ->
133+reflectList : (G : List (List a)) ->
134 (xs : List a) -> (G' ** Expr (G' ++ G) xs)
134 (xs : List a) -> (G' ** Expr (G' ++ G) xs)
135−ReflectList G [] = ([] ** ENil)
135+reflectList G [] = ([] ** ENil)
137−ReflectList G (x :: xs) with (ReflectList G xs)
137+reflectList G (x :: xs) with (reflectList G xs)
138 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
138 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
139 | Just p = (G' ** App (Var p) xs')
139 | Just p = (G' ** App (Var p) xs')
140 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
140 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
142−ReflectList G (xs ++ ys) with (ReflectList G xs)
142+reflectList G (xs ++ ys) with (reflectList G xs)
143− | (G' ** xs') with (ReflectList (G' ++ G) ys)
143+ | (G' ** xs') with (reflectList (G' ++ G) ys)
144 | (G'' ** ys') = ((G'' ++ G') **
144 | (G'' ** ys') = ((G'' ++ G') **
145 rewrite (sym (appendAssociative G'' G' G)) in
145 rewrite (sym (appendAssociative G'' G' G)) in
146 App (weaken G'' xs') ys')
146 App (weaken G'' xs') ys')
147−ReflectList G t with (isElem t G)
147+reflectList G t with (isElem t G)
148 | Just p = ([] ** Var p)
148 | Just p = ([] ** Var p)
149 | Nothing = ([t] ** Var Stop)
149 | Nothing = ([t] ** Var Stop)
152−-- Similarly, ReflectEq converts an equality proof on Lists into the ListEq
152+-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
153−-- Reflection. Note that it isn't total, and we have to give the element type
153+-- reflection. Note that it isn't total, and we have to give the element type
154-- explicitly because it can't be inferred from P.
154-- explicitly because it can't be inferred from P.
156−-- This is not really a problem - we'll want different Reflections for different
156+-- This is not really a problem - we'll want different reflections for different
157-- forms of equality proofs anyway.
157-- forms of equality proofs anyway.
159−%Reflection
159+%reflection
160−ReflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
160+reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
161−ReflectEq a G (the (List a) xs = the (List a) ys) with (ReflectList G xs)
161+reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
162− | (G' ** xs') with (ReflectList (G' ++ G) ys)
162+ | (G' ** xs') with (reflectList (G' ++ G) ys)
163 | (G'' ** ys') = ((G'' ++ G') **
163 | (G'' ** ys') = ((G'' ++ G') **
164 rewrite (sym (appendAssociative G'' G' G)) in
164 rewrite (sym (appendAssociative G'' G' G)) in
165 EqP (weaken G'' xs') ys')
165 EqP (weaken G'' xs') ys')
@@ -196,14 +196,14 @@ Reflect.bp1 = proof {
197-- "quoteGoal x by p in e" does some magic
197-- "quoteGoal x by p in e" does some magic
198-- The effect is to bind x to p applied to the current goal. If 'p' is a
198-- The effect is to bind x to p applied to the current goal. If 'p' is a
199−-- Reflection function (which is the most likely thing to be useful...)
199+-- reflection function (which is the most likely thing to be useful...)
200-- then we can feed the result to the above 'prove' function and pull out
200-- then we can feed the result to the above 'prove' function and pull out
201-- the proof, if it exists.
201-- the proof, if it exists.
203-- The syntax declaration below just gives us an easy way to invoke the
203-- The syntax declaration below just gives us an easy way to invoke the
204-- prover.
204-- prover.
206−syntax AssocProof [ty] = quoteGoal x by ReflectEq ty [] in
206+syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
207 getJust (prove (getProof x)) ItIsJust
207 getJust (prove (getProof x)) ItIsJust