module Reflect

import Decidable.Equality

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) ->
                 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 xs 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