@@ -0,0 +1,205 @@
1+module Reflect
2+
3+import Decidable.Equality
4+
5+using (xs : List a, ys : List a, G : List (List a))
6+
7+ data Elem : a -> List a -> Type where
8+ Stop : Elem x (x :: xs)
9+ Pop : Elem x ys -> Elem x (y :: xs)
10+
11+-- Expr is a reflection of a list, indexed over the concrete list,
12+-- and over a set of list variables.
13+
14+ data Expr : List (List a) -> List a -> Type where
15+ App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys)
16+ Var : Elem xs G -> Expr G xs
17+ ENil : Expr G []
18+
19+-- Reflection of list equalities, indexed over the concrete equality.
20+
21+ data ListEq : List (List a) -> Type -> Type where
22+ EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)
23+
24+-- Fully right associative list expressions
25+
26+ data RExpr : List (List a) -> List a -> Type where
27+ RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys)
28+ RNil : RExpr G []
29+
30+-- Convert an expression to a right associative expression, and return
31+-- a proof that the rewriting has an equal interpretation to the original
32+-- expression.
33+
34+-- The idea is that we use this proof to build a proof of equality of
35+-- list appends
36+
37+ expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))
38+ expr_r ENil = (_ ** (RNil, refl))
39+ expr_r (Var i) = (_ ** (RApp RNil i, refl))
40+ expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in
41+ let (yl ** (yr, yprf)) = expr_r ey in
42+ appRExpr _ _ xr yr xprf yprf
43+ where
44+ appRExpr : (xs', ys' : List a) ->
45+ RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
46+ (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
47+ appRExpr x' y' rxs (RApp e i) xprf yprf
48+ = let (xs ** (rec, prf)) = appRExpr _ _ rxs e refl refl in
49+ (_ ** (RApp rec i, ?appRExpr1))
50+ appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))
51+
52+ r_expr : RExpr G xs -> Expr G xs
53+ r_expr RNil = ENil
54+ r_expr (RApp xs i) = App (r_expr xs) (Var i)
55+
56+-- Convert an expression to some other equivalent expression (which
57+-- just happens to be normalised to right associative form)
58+
59+ reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs'))
60+ reduce e = let (x' ** (e', prf)) = expr_r e in
61+ (x' ** (r_expr e', prf))
62+
63+-- Build a proof that two expressions are equal. If they are, we'll know
64+-- that the indices are equal.
65+
66+ eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->
67+ Maybe (e = e')
68+ eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')
69+ eqExpr (App x y) (App x y) | (Just refl, Just refl) = Just refl
70+ eqExpr (App x y) (App x' y') | _ = Nothing
71+ eqExpr (Var i) (Var j) with (prim__syntactic_eq _ _ i j)
72+ eqExpr (Var i) (Var i) | (Just refl) = Just refl
73+ eqExpr (Var i) (Var j) | _ = Nothing
74+ eqExpr ENil ENil = Just refl
75+ eqExpr _ _ = Nothing
76+
77+-- Given a couple of reflected expressions, try to produce a proof that
78+-- they are equal
79+
80+ buildProof : {xs : List a} -> {ys : List a} ->
81+ Expr G ln -> Expr G rn ->
82+ (xs = ln) -> (ys = rn) -> Maybe (xs = ys)
83+ buildProof e e' lp rp with (eqExpr e e')
84+ buildProof e e lp rp | Just refl = ?bp1
85+ buildProof e e' lp rp | Nothing = Nothing
86+
87+ testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)
88+ testEq l r = let (ln ** (l', lPrf)) = reduce l in
89+ let (rn ** (r', rPrf)) = reduce r in
90+ buildProof l' r' lPrf rPrf
91+
92+-- Given a reflected equality, try to produce a proof that holds
93+
94+ prove : ListEq G t -> Maybe t
95+ prove (EqP xs ys) = testEq xs ys
96+
97+ getJust : (x : Maybe a) -> IsJust x -> a
98+ getJust (Just p) ItIsJust = p
99+
100+
101+-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
102+-- (at compile-time only) attempts to construct a proof that its arguments
103+-- are syntactically equal. We'll find this useful for referring to variables
104+-- in reflected terms.
105+
106+ isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
107+ isElem x [] = Nothing
108+ isElem x (y :: ys) with (prim__syntactic_eq _ _ x y)
109+ isElem x (x :: ys) | Just refl = [| Stop |]
110+ isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]
111+
112+ weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)
113+ weakenElem [] p = p
114+ weakenElem (g :: G) p = Pop (weakenElem G p)
115+
116+ weaken : (G' : List (List a)) ->
117+ Expr G xs -> Expr (G' ++ G) xs
118+ weaken G' (App l r) = App (weaken G' l) (weaken G' r)
119+ weaken G' (Var x) = Var (weakenElem G' x)
120+ weaken G' ENil = ENil
121+
122+
123+-- Now, some reflection magic.
124+-- %reflection means a function runs on syntax, rather than on constructors.
125+-- So, 'reflectList' builds a reflected List expression as defined above.
126+
127+-- It also converts (x :: xs) into a reflected [x] ++ xs so that the above
128+-- reduction will work the right way.
129+
130+%reflection
131+reflectList : (G : List (List a)) ->
132+ (xs : List a) -> (G' ** Expr (G' ++ G) xs)
133+reflectList G [] = ([] ** ENil)
134+reflectList G (x :: xs) with (reflectList G xs)
135+ | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
136+ | Just p = (G' ** App (Var p) xs')
137+ | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
138+reflectList G (xs ++ ys) with (reflectList G xs)
139+ | (G' ** xs') with (reflectList (G' ++ G) ys)
140+ | (G'' ** ys') = ((G'' ++ G') **
141+ rewrite (sym (appendAssociative G'' G' G)) in
142+ App (weaken G'' xs') ys')
143+reflectList G t with (isElem t G)
144+ | Just p = ([] ** Var p)
145+ | Nothing = ([t] ** Var Stop)
146+
147+
148+-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
149+-- reflection. Note that it isn't total, and we have to give the element type
150+-- explicitly because it can't be inferred from P.
151+
152+-- This is not really a problem - we'll want different reflections for different
153+-- forms of equality proofs anyway.
154+
155+%reflection
156+reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
157+reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
158+ | (G' ** xs') with (reflectList (G' ++ G) ys)
159+ | (G'' ** ys') = ((G'' ++ G') **
160+ rewrite (sym (appendAssociative G'' G' G)) in
161+ EqP (weaken G'' xs') ys')
162+
163+
164+-- Need these before we can test it or the reductions won't normalise fully...
165+
166+---------- Proofs ----------
167+
168+Reflect.appRExpr1 = proof {
169+ intros;
170+ rewrite sym xprf;
171+ rewrite sym yprf;
172+ rewrite prf;
173+ rewrite sym (appendAssociative xs xs2 ys1);
174+ trivial;
175+}
176+
177+Reflect.appRExpr2 = proof {
178+ intros;
179+ rewrite xprf;
180+ rewrite sym yprf;
181+ rewrite appendNilRightNeutral x';
182+ trivial;
183+}
184+
185+Reflect.bp1 = proof {
186+ intros;
187+ refine Just;
188+ rewrite sym lp;
189+ rewrite sym rp;
190+ trivial;
191+}
192+
193+-- "quoteGoal x by p in e" does some magic
194+-- The effect is to bind x to p applied to the current goal. If 'p' is a
195+-- reflection function (which is the most likely thing to be useful...)
196+-- then we can feed the result to the above 'prove' function and pull out
197+-- the proof, if it exists.
198+
199+-- The syntax declaration below just gives us an easy way to invoke the
200+-- prover.
201+
202+syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
203+ getJust (prove (getProof x)) ItIsJust
204+
205+