add start of Quox.Equal

src/Quox.idr

@@ -1,7 +1,11 @@
 module Quox
 
+import public Quox.Name
 import public Quox.Syntax
+import public Quox.Equal
+import public Quox.Error
 import public Quox.Pretty
+-- import public Quox.Typechecker
 
 import Data.Nat
 import Data.Vect

src/Quox/Equal.idr

@@ -0,0 +1,126 @@
+module Quox.Equal
+
+import public Quox.Syntax
+import Quox.Error
+
+%default total
+
+
+public export
+data Error =
+  Clash  SomeTerm SomeTerm
+| ClashU Universe Universe
+| ClashQ Qty      Qty
+
+private %inline
+clashT' : Term d n -> Term d n -> Error
+clashT' = Clash `on` some2
+
+private %inline
+clashE' : Elim d n -> Elim d n -> Error
+clashE' = clashT' `on` E
+
+parameters {auto _ : MonadThrow Error m}
+  private %inline
+  clashT : Term d n -> Term d n -> m a
+  clashT = throw .: clashT'
+
+  private %inline
+  clashE : Elim d n -> Elim d n -> m a
+  clashE = clashT `on` E
+
+  private %inline
+  eq : Eq a => (a -> a -> Error) -> a -> a -> m ()
+  eq err a b = unless (a == b) $ throw $ err a b
+
+  mutual
+    private covering
+    equalTN' : DSubst d 0 -> (s, t : Term d n) ->
+               (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
+
+    equalTN' _ (TYPE k) (TYPE l) _ _ =
+      eq ClashU k l
+    equalTN' _ s@(TYPE _) t _ _ = clashT s t
+
+    equalTN' th (Pi qtm1 qty1 _ arg1 res1) (Pi qtm2 qty2 _ arg2 res2) _ _ = do
+      eq ClashQ qtm1 qtm2
+      eq ClashQ qty1 qty2
+      equalTS th arg1 arg2
+      equalTS th res1 res2
+    equalTN' _ s@(Pi {}) t _ _ = clashT s t
+
+    -- [todo] eta
+    equalTN' th (Lam _ body1) (Lam _ body2) _ _ =
+      equalTS th body1 body2
+    equalTN' _ s@(Lam {}) t _ _ = clashT s t
+
+    equalTN' th (E e) (E f) ps pt = equalES th e f
+    equalTN' _ s@(E _) t _ _ = clashT s t
+
+    equalTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
+    equalTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
+
+    private covering
+    equalEN' : DSubst d 0 -> (e, f : Elim d n) ->
+               (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
+
+    equalEN' _ (F x) (F y) _ _ = do
+      eq (clashE' `on` F {d = 0, n = 0}) x y
+    equalEN' _ e@(F _) f _ _ = clashE e f
+
+    equalEN' _ (B i) (B j) _ _ = do
+      eq (clashE' `on` B {d = 0}) i j
+    equalEN' _ e@(B _) f _ _ = clashE e f
+
+    equalEN' th (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
+      equalES th fun1 fun2
+      equalTS th arg1 arg2
+    equalEN' _ e@(_ :@ _) f _ _ = clashE e f
+
+    equalEN' th (tm1 :# ty1) (tm2 :# ty2) _ _ = do
+      equalTS th tm1 tm2
+      equalTS th ty1 ty2
+    equalEN' _ e@(_ :# _) f _ _ = clashE e f
+
+    equalEN' _ (CloE  {}) _ pe _ = void $ pe IsCloE
+    equalEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
+
+
+    private covering %inline
+    equalTN : DSubst d 0 -> NonRedexTerm d n -> NonRedexTerm d n -> m ()
+    equalTN th s t = equalTN' th s.fst t.fst s.snd t.snd
+
+    private covering %inline
+    equalEN : DSubst d 0 -> NonRedexElim d n -> NonRedexElim d n -> m ()
+    equalEN th e f = equalEN' th e.fst f.fst e.snd f.snd
+
+
+    export covering %inline
+    equalTS : DSubst d 0 -> Term d n -> Term d n -> m ()
+    equalTS th s t = equalTN th (whnfT s) (whnfT t)
+
+    export covering %inline
+    equalES : DSubst d 0 -> Elim d n -> Elim d n -> m ()
+    equalES th e f = equalEN th (whnfE e) (whnfE f)
+
+
+  export covering %inline
+  equalT : DimEq d -> Term d n -> Term d n -> m ()
+  equalT eqs s t =
+    let s' = whnfT s; t' = whnfT t in
+    for_ (splits eqs) $ \th => equalTN th s' t'
+
+  export covering %inline
+  equalE : DimEq d -> Elim d n -> Elim d n -> m ()
+  equalE eqs e f =
+    let e' = whnfE e; f' = whnfE f in
+    for_ (splits eqs) $ \th => equalEN th e' f'
+
+
+  export covering %inline
+  equalT0 : Term 0 n -> Term 0 n -> m ()
+  equalT0 = equalT zeroEq
+
+  export covering %inline
+  equalE0 : Elim 0 n -> Elim 0 n -> m ()
+  equalE0 = equalE zeroEq