Equality.hs

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module PiSigma.Equality where

import Control.Monad

import PiSigma.Syntax
import PiSigma.Evaluation

class Equal a where
    eq :: Env e => a -> a -> Eval e ()

instance Equal (Clos Term) where
    eq t u = do t' <- eval t
                u' <- eval u
                eq t' u'

eq' :: Env e => Clos (Term,Term) -> Eval e ()
eq' ((t,u),s) = eq (t,s) (u,s)

eqBind :: (Env e,Closure a) =>
          (a -> a -> Eval e ()) ->
          Bind a -> Bind a -> Eval e ()
eqBind eq (x0,c0) (x1,c1) =
  do let s0 = getScope c0
         s1 = getScope c1
     (i,s0') <- decl' x0 s0
     let s1' = extendScope s1 x1 (i,Nothing)
     let c0' = putScope c0 s0'
         c1' = putScope c1 s1'
     eq c0' c1'

instance (Equal a,Closure a) => Equal (Bind a) where
    eq = eqBind eq

instance Equal Val where
    eq (Ne t0) (Ne t1) = eq t0 t1
    eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))
      | ps0 == ps1 = 
        do eq (a0,s0) (a1,s1)
           eq (x0,(b0,s0)) (x1,(b1,s1))
    eq (VLam xt0) (VLam xt1) = eq xt0 xt1
    eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = 
        do eq (t0,s0) (t1,s1)
           eq (u0,s0) (u1,s1)
    eq (VBox b) (VBox b') = eq b b' 
    eq (VLift a) (VLift a') = eq a a'
    eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum
             | otherwise = fail "Different values"

eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()
eqBox (Var x,s) (Var y,s') = 
    do x' <- getId x s
       y' <- getId y s'
       eq x' y'
{-
eqBox (Var x,s) u =
    do x' <- getId x s
       ei <- lookupId x'
       case ei of
         Closure t -> eqBox t u
         Id j -> fail "eqBox: var vs term"
       -- wrong level - this should use functions in Evaluation
       -- have to avoid races: don't unfold the same id twice!
eqBox t u @ (Var _,_) = eqBox u t          
-}
eqBox (Let p t,s) c = fail "eqBox: let not implemented"
{-
    do s' <- evalProg (p,s)
       eqBox (t,s') c
-}
eqBox c c'@(Let p t,s) = eqBox c' c 
eqBox (Q ps (a,(x,b)),s) (Q ps' (a',(x',b')),s')
      | ps == ps' = 
          do eqBox (a,s) (a',s')
             eq (x,Boxed (b,s)) (x',Boxed (b',s'))
eqBox (t :. u,s) (t' :. u',s') =
    do eqBox (t,s) (t',s')
       eqBox (u,s) (u',s')
eqBox (Split t (x,(y,u)),s) (Split t' (x',(y',u')),s') =
    do eqBox (t,s) (t',s')
       eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))
eqBox (Case t bs,s) (Case t' bs',s') =
    do eqBox (t,s) (t',s')
       zipWithM_ (\ (l,t) (l',t') -> 
                      if l==l' then eqBox (t,s) (t',s')
                      else fail "eqBox case") bs bs'
eqBox (Lift t,s) (Lift t',s') = eqBox (t,s) (t',s')
eqBox (Box t,s) (Box t',s') = eqBox (t,s) (t',s')
eqBox (Force t,s) (Force t',s') = eqBox (t,s) (t',s')               
eqBox (t,s) (t',s') | t == t' = return () -- Type, Label, Enum
                    | otherwise = fail "Different terms"
-- TODO: check that it cannot happen that t and t' are syntacically equal but not alpha equivalent!
    
instance Equal Boxed where
    eq (Boxed c) (Boxed c') = eqBox c c'

instance Equal Id where
    eq i0 i1  
        | i0 == i1  = return ()
        | otherwise = do ei0 <- lookupId i0
                         ei1 <- lookupId i1
                         case (ei0,ei1) of
                           (Id j0, Id j1) -> unless (j0 == j1)
                                               (fail "Different variables")
                           (Closure t0, Closure t1) ->
                               letn i0 (Id i0)
                                    (letn i1 (Id i0)
                                          (eq t0 t1))
                           _ -> fail "Variable vs neutral"

instance Equal Ne where
    eq (NVar i0) (NVar i1) = eq i0 i1
    eq (t0 :.. u0) (t1 :.. u1) = 
        do eq t0 t1
           eq u0 u1
    eq (NSplit t0 xyu0) (NSplit t1 xyu1) =
        do eq t0 t1
           eq xyu0 xyu1
    eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =
        do eq t0 t1
           let eqBranches [] [] = return ()
               eqBranches ((l0,u0):lus0) ((l1,u1):lus1) | l0 == l1 =
                 do eq (u0,s0) (u1,s1)
                    eqBranches lus0 lus1
               eqBranches _ _ = fail "Case: branches differ"
           eqBranches lus0 lus1
    eq (NForce t) (NForce t') = eq t t'
    eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")