Reflect.idr

module Reflect

import Decidable.Equality

%access public export
%default total
%language FirstClassReflection

using (xs : List a, ys : List a, gam : List (List a))

  data Elem : a -> List a -> Type where
       Stop : Elem x (x :: xs)
       Pop  : Elem x ys -> Elem x (y :: ys)

-- 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 gam xs -> Expr gam ys -> Expr gam (xs ++ ys)
       Var  : Elem xs gam -> Expr gam xs
       ENil : Expr gam []

-- Reflection of list equalities, indexed over the concrete equality.

  data ListEq : List (List a) -> Type -> Type where
       EqP : Expr gam xs -> Expr gam ys -> ListEq gam (xs = ys)

-- Fully right associative list expressions

  data RExpr : List (List a) -> List a -> Type where
       RApp : RExpr gam xs -> Elem ys gam -> RExpr gam (xs ++ ys)
       RNil : RExpr gam []

-- 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 gam xs -> (xs' ** (RExpr gam 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) ->
                 {gam : List (List a)} -> {xs, ys : List a} ->
                 RExpr gam xs -> RExpr gam ys -> (xs' = xs) -> (ys' = ys) ->
                 (ws' ** (RExpr gam 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 gam xs -> Expr gam 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 gam xs -> (xs' ** (Expr gam 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 gam xs) -> (e' : Expr gam 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 gam ln -> Expr gam 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 gam xs -> Expr gam 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 gam 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 : (gam' : List a) -> Elem x xs -> Elem x (gam' ++ xs)
  weakenElem [] p = p
  weakenElem (g :: gam) p = Pop (weakenElem gam p)

  weaken : (gam' : List (List a)) ->
           Expr gam xs -> Expr (gam' ++ gam) xs
  weaken gam' (App l r) = App (weaken gam' l) (weaken gam' r)
  weaken gam' (Var x) = Var (weakenElem gam' x)
  weaken gam' 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 : (gam : List (List a)) ->
          (xs : List a) -> (gam' ** Expr (gam' ++ gam) xs)
reflectList gam [] = ([] ** ENil)

reflectList gam (x :: xs) with (reflectList gam xs)
     | (gam' ** xs') with (isElem (List.(::) x []) (gam' ++ gam))
        | Just p = (gam' ** App (Var p) xs')
        | Nothing = ([x] :: gam' ** App (Var Stop) (weaken [[x]] xs'))

reflectList gam (xs ++ ys) with (reflectList gam xs)
     | (gam' ** xs') with (reflectList (gam' ++ gam) ys)
         | (gam'' ** ys') = ((gam'' ++ gam') **
                              rewrite (sym (appendAssociative gam'' gam' gam)) in
                                 App (weaken gam'' xs') ys')
reflectList gam t with (isElem t gam)
            | 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) -> (gam : List (List a)) -> (P : Type) -> (gam' ** ListEq (gam' ++ gam) P)
reflectEq a gam (the (List a) xs = the (List a) ys) with (reflectList gam xs)
     | (gam' ** xs')  with (reflectList (gam' ++ gam) ys)
        | (gam'' ** ys') = ((gam'' ++ gam') **
                           rewrite (sym (appendAssociative gam'' gam' gam)) in
                               EqP (weaken gam'' 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 xs2 xs3 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 (snd x)) ItIsJust