git.iko.soy/Idris-dev
on d5c8aec help sign in
Idris-dev/test/test030/Reflect.idr
207 lines 7.2 kB history raw
1module Reflect
3import Decidable.Equality
5using (xs : List a, ys : List a, G : List (List a))
7 data Elem : a -> List a -> Type where
8 Stop : Elem x (x :: xs)
9 Pop : Elem x ys -> Elem x (y :: xs)
11-- Expr is a reflection of a list, indexed over the concrete list,
12-- and over a set of list variables.
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 []
19-- Reflection of list equalities, indexed over the concrete equality.
21 data ListEq : List (List a) -> Type -> Type where
22 EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)
24-- Fully right associative list expressions
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 []
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.
34-- The idea is that we use this proof to build a proof of equality of
35-- list appends
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))
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)
56-- Convert an expression to some other equivalent expression (which
57-- just happens to be normalised to right associative form)
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))
63-- Build a proof that two expressions are equal. If they are, we'll know
64-- that the indices are equal.
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
77-- Given a couple of reflected expressions, try to produce a proof that
78-- they are equal
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
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
92-- Given a reflected equality, try to produce a proof that holds
94 prove : ListEq G t -> Maybe t
95 prove (EqP xs ys) = testEq xs ys
97 getJust : (x : Maybe a) -> IsJust x -> a
98 getJust (Just p) ItIsJust = p
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.
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) |]
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)
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
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.
127-- It also converts (x :: xs) into a reflected [x] ++ xs so that the above
128-- reduction will work the right way.
130%reflection
131reflectList : (G : List (List a)) ->
132 (xs : List a) -> (G' ** Expr (G' ++ G) xs)
133reflectList G [] = ([] ** ENil)
135reflectList G (x :: xs) with (reflectList G xs)
136 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
137 | Just p = (G' ** App (Var p) xs')
138 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
140reflectList G (xs ++ ys) with (reflectList G xs)
141 | (G' ** xs') with (reflectList (G' ++ G) ys)
142 | (G'' ** ys') = ((G'' ++ G') **
143 rewrite (sym (appendAssociative G'' G' G)) in
144 App (weaken G'' xs') ys')
145reflectList G t with (isElem t G)
146 | Just p = ([] ** Var p)
147 | Nothing = ([t] ** Var Stop)
150-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
151-- reflection. Note that it isn't total, and we have to give the element type
152-- explicitly because it can't be inferred from P.
154-- This is not really a problem - we'll want different reflections for different
155-- forms of equality proofs anyway.
157%reflection
158reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
159reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
160 | (G' ** xs') with (reflectList (G' ++ G) ys)
161 | (G'' ** ys') = ((G'' ++ G') **
162 rewrite (sym (appendAssociative G'' G' G)) in
163 EqP (weaken G'' xs') ys')
166-- Need these before we can test it or the reductions won't normalise fully...
168---------- Proofs ----------
170Reflect.appRExpr1 = proof {
171 intros;
172 rewrite sym xprf;
173 rewrite sym yprf;
174 rewrite prf;
175 rewrite sym (appendAssociative xs xs2 ys1);
176 trivial;
179Reflect.appRExpr2 = proof {
180 intros;
181 rewrite xprf;
182 rewrite sym yprf;
183 rewrite appendNilRightNeutral x';
184 trivial;
187Reflect.bp1 = proof {
188 intros;
189 refine Just;
190 rewrite sym lp;
191 rewrite sym rp;
192 trivial;
195-- "quoteGoal x by p in e" does some magic
196-- The effect is to bind x to p applied to the current goal. If 'p' is a
197-- reflection function (which is the most likely thing to be useful...)
198-- then we can feed the result to the above 'prove' function and pull out
199-- the proof, if it exists.
201-- The syntax declaration below just gives us an easy way to invoke the
202-- prover.
204syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
205 getJust (prove (getProof x)) ItIsJust