module Reflect
import Decidable.Equality
%default total
using (xs : List a, ys : List a, G : List (List a))
data Elem : a -> List a -> Type where
Stop : Elem x (x :: xs)
Pop : Elem x ys -> Elem x (y :: xs)
-- Expr is a reflection of a list, indexed over the concrete list,
-- and over a set of list variables.
data Expr : List (List a) -> List a -> Type where
App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys)
Var : Elem xs G -> Expr G xs
ENil : Expr G []
-- Reflection of list equalities, indexed over the concrete equality.
data ListEq : List (List a) -> Type -> Type where
EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)
-- Fully right associative list expressions
data RExpr : List (List a) -> List a -> Type where
RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys)
RNil : RExpr G []
-- Convert an expression to a right associative expression, and return
-- a proof that the rewriting has an equal interpretation to the original
-- expression.
-- The idea is that we use this proof to build a proof of equality of
-- list appends
expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))
expr_r ENil = (_ ** (RNil, Refl))
expr_r (Var i) = (_ ** (RApp RNil i, Refl))
expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in
let (yl ** (yr, yprf)) = expr_r ey in
appRExpr _ _ xr yr xprf yprf
where
appRExpr : (xs', ys' : List a) ->
{G : List (List a)} -> {xs, ys : List a} ->
RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
(ws' ** (RExpr G ws', xs' ++ ys' = ws'))
appRExpr x' y' rxs (RApp e i) xprf yprf
= let (xs ** (rec, prf)) = appRExpr _ _ rxs e Refl Refl in
(_ ** (RApp rec i, ?appRExpr1))
appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))
r_expr : RExpr G xs -> Expr G xs
r_expr RNil = ENil
r_expr (RApp xs i) = App (r_expr xs) (Var i)
-- Convert an expression to some other equivalent expression (which
-- just happens to be normalised to right associative form)
reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs'))
reduce e = let (x' ** (e', prf)) = expr_r e in
(x' ** (r_expr e', prf))
-- Build a proof that two expressions are equal. If they are, we'll know
-- that the indices are equal.
eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->
Maybe (e = e')
eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')
eqExpr (App x y) (App x y) | (Just Refl, Just Refl) = Just Refl
eqExpr (App x y) (App x' y') | _ = Nothing
eqExpr (Var i) (Var j) with (prim__syntactic_eq _ _ i j)
eqExpr (Var i) (Var i) | (Just Refl) = Just Refl
eqExpr (Var i) (Var j) | _ = Nothing
eqExpr ENil ENil = Just Refl
eqExpr _ _ = Nothing
-- Given a couple of reflected expressions, try to produce a proof that
-- they are equal
buildProof : {xs : List a} -> {ys : List a} ->
Expr G ln -> Expr G rn ->
(xs = ln) -> (ys = rn) -> Maybe (xs = ys)
buildProof e e' lp rp with (eqExpr e e')
buildProof e e lp rp | Just Refl = ?bp1
buildProof e e' lp rp | Nothing = Nothing
testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)
testEq l r = let (ln ** (l', lPrf)) = reduce l in
let (rn ** (r', rPrf)) = reduce r in
buildProof l' r' lPrf rPrf
-- Given a reflected equality, try to produce a proof that holds
prove : ListEq G t -> Maybe t
prove (EqP xs ys) = testEq xs ys
getJust : (x : Maybe a) -> IsJust x -> a
getJust (Just p) ItIsJust = p
-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
-- (at compile-time only) attempts to construct a proof that its arguments
-- are syntactically equal. We'll find this useful for referring to variables
-- in reflected terms.
isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
isElem x [] = Nothing
isElem x (y :: ys) with (prim__syntactic_eq _ _ x y)
isElem x (x :: ys) | Just Refl = [| Stop |]
isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]
weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)
weakenElem [] p = p
weakenElem (g :: G) p = Pop (weakenElem G p)
weaken : (G' : List (List a)) ->
Expr G xs -> Expr (G' ++ G) xs
weaken G' (App l r) = App (weaken G' l) (weaken G' r)
weaken G' (Var x) = Var (weakenElem G' x)
weaken G' ENil = ENil
-- Now, some reflection magic.
-- %reflection means a function runs on syntax, rather than on constructors.
-- So, 'reflectList' builds a reflected List expression as defined above.
-- It also converts (x :: xs) into a reflected [x] ++ xs So that the above
-- reduction will work the right way.
%reflection
reflectList : (G : List (List a)) ->
(xs : List a) -> (G' ** Expr (G' ++ G) xs)
reflectList G [] = ([] ** ENil)
reflectList G (x :: xs) with (reflectList G xs)
| (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
| Just p = (G' ** App (Var p) xs')
| Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
reflectList G (xs ++ ys) with (reflectList G xs)
| (G' ** xs') with (reflectList (G' ++ G) ys)
| (G'' ** ys') = ((G'' ++ G') **
rewrite (sym (appendAssociative G'' G' G)) in
App (weaken G'' xs') ys')
reflectList G t with (isElem t G)
| Just p = ([] ** Var p)
| Nothing = ([t] ** Var Stop)
-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
-- reflection. Note that it isn't total, and we have to give the element type
-- explicitly because it can't be inferred from P.
-- This is not really a problem - we'll want different reflections for different
-- forms of equality proofs anyway.
%reflection
reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
| (G' ** xs') with (reflectList (G' ++ G) ys)
| (G'' ** ys') = ((G'' ++ G') **
rewrite (sym (appendAssociative G'' G' G)) in
EqP (weaken G'' xs') ys')
-- Need these before we can test it or the reductions won't normalise fully...
---------- Proofs ----------
Reflect.appRExpr1 = proof {
intros;
rewrite sym xprf;
rewrite sym yprf;
rewrite prf;
rewrite sym (appendAssociative xs1 xs2 ys1);
trivial;
}
Reflect.appRExpr2 = proof {
intros;
rewrite xprf;
rewrite sym yprf;
rewrite appendNilRightNeutral x';
trivial;
}
Reflect.bp1 = proof {
intros;
refine Just;
rewrite sym lp;
rewrite sym rp;
trivial;
}
-- "quoteGoal x by p in e" does some magic
-- The effect is to bind x to p applied to the current goal. If 'p' is a
-- reflection function (which is the most likely thing to be useful...)
-- then we can feed the result to the above 'prove' function and pull out
-- the proof, if it exists.
-- The syntax declaration below just gives us an easy way to invoke the
-- prover.
syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
getJust (prove (getProof x)) ItIsJust