From 21106d4097bcf71e1014be33b77ec64ee015c8f4 Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Sun, 20 Oct 2024 03:20:26 +0800
Subject: [PATCH] fix

---
 Examples/Bool.shitt | 15 +++++++++++++++
 Examples/Exp.shitt  | 20 ++++++++++++++++++++
 Examples/Id.shitt   | 11 +++++++++++
 Examples/Nat.shitt  | 25 +++++++++++++++++++++++++
 src/ShiTT/Check.hs  |  6 +++---
 src/ShiTT/Eval.hs   | 13 ++++++++++---
 6 files changed, 84 insertions(+), 6 deletions(-)
 create mode 100644 Examples/Bool.shitt
 create mode 100644 Examples/Exp.shitt
 create mode 100644 Examples/Id.shitt
 create mode 100644 Examples/Nat.shitt

diff --git a/Examples/Bool.shitt b/Examples/Bool.shitt
new file mode 100644
index 0000000..cedc03d
--- /dev/null
+++ b/Examples/Bool.shitt
@@ -0,0 +1,15 @@
+data Bool : U where 
+| true : ... 
+| false : ...
+
+fun not (_ : Bool) : Bool
+| true = false 
+| false = true
+
+fun and (_ _ : Bool) : Bool 
+| true true = true 
+| _ _ = false 
+
+fun or (_ _ : Bool) : Bool 
+| false false = false 
+| _ _ = true
\ No newline at end of file
diff --git a/Examples/Exp.shitt b/Examples/Exp.shitt
new file mode 100644
index 0000000..90d1e47
--- /dev/null
+++ b/Examples/Exp.shitt
@@ -0,0 +1,20 @@
+#load "Nat.shitt" 
+#load "Bool.shitt"
+
+data Exp : (_ : U) -> U where 
+| nat : (_ : N) -> ... N
+| bool : (_ : Bool) -> ... Bool 
+| andF : ... (Bool -> Bool -> Bool)
+| notF : ... (Bool -> Bool)
+| addF : ... (N -> N -> N)
+| app : {a b : U} (f : Exp (a -> b)) (arg : Exp a) -> ... b
+
+axiom partial fun sorry {A: U} : A 
+
+fun eval {A: U} (e : Exp A) : A 
+| nat x = x 
+| bool b = b 
+| andF = and
+| notF = not 
+| addF = add 
+| app f x = eval f (eval x)
diff --git a/Examples/Id.shitt b/Examples/Id.shitt
new file mode 100644
index 0000000..7313215
--- /dev/null
+++ b/Examples/Id.shitt
@@ -0,0 +1,11 @@
+data Id {A : U} : (x y : A) -> U where 
+| refl : (t : A) -> ... t t 
+
+fun sym {A : U} {x y : A} (p : Id x y) : Id y x where 
+| (refl _) = refl _
+
+fun trans {A : U} {x y z : A} (_ : Id x y) (_ : Id y z) : Id x z where 
+| (refl _) (refl _) = refl _ 
+
+fun cong {A B : U} {x y : A} (f : A -> B) (p : Id x y) : Id (f x) (f y) where 
+| f (refl _) = refl _
diff --git a/Examples/Nat.shitt b/Examples/Nat.shitt
new file mode 100644
index 0000000..146a402
--- /dev/null
+++ b/Examples/Nat.shitt
@@ -0,0 +1,25 @@
+#load "Id.shitt"
+
+data N : U where  
+| zero : ...  
+| succ : (pre : N) -> ...  
+
+fun add (m n : N) : N where  
+| zero n = n
+| (succ m) n = succ (add m n)
+
+fun addAssoc (x y z : N) : Id (add (add x y) z) (add x (add y z)) where 
+| zero y z = refl _
+| (succ x) y z = cong succ (addAssoc x y z) 
+
+fun addIdR (x : N) : Id (add x zero) x where 
+| zero = refl _ 
+| (succ x) = cong succ (addIdR x)
+
+fun addSucc (x y : N) : Id (add (succ x) y) (add x (succ y)) where 
+| zero y = refl _ 
+| (succ x) y = cong succ (addSucc x y)
+
+fun addComm (x y : N) : Id (add x y) (add y x) where 
+| zero y = sym (addIdR _)
+| (succ x) y = trans (cong succ (addComm x y)) (addSucc y x)
diff --git a/src/ShiTT/Check.hs b/src/ShiTT/Check.hs
index d0aa8e5..eb777a5 100644
--- a/src/ShiTT/Check.hs
+++ b/src/ShiTT/Check.hs
@@ -73,7 +73,7 @@ unifySp ctx sp sp' = case (sp, sp') of
   _                      -> throwIO UnifyError
 
 unify :: Context -> Value -> Value -> IO () 
-unify ctx (force ctx -> t) (force ctx -> u) = -- trace ("UNIFYING: " ++ show t ++ " WITH " ++ show u) $ 
+unify ctx (refresh ctx -> t) (refresh ctx -> u) = -- trace ("UNIFYING: " ++ show t ++ " WITH " ++ show u) $ 
   case (t, u) of 
   ---
   (VU, VU) -> pure ()
@@ -88,9 +88,9 @@ unify ctx (force ctx -> t) (force ctx -> u) = -- trace ("UNIFYING: " ++ show t +
     unify (ctx <: freeVar x') (t @ x := VVar x') (vApp ctx t' (VVar x') i)
   ---
   (VPi x i a b, VPi x' i' a' b') | i == i' -> do 
-    let y = freshName ctx x 
+    let fre = freshName ctx x 
     unify ctx a a'
-    unify (ctx <: freeVar x') (b @ x := VVar y) (b' @ x' := VVar y)
+    unify (ctx <: freeVar fre) (b @ x := VVar fre) (b' @ x' := VVar fre)
   ---
   (VCon con sp, VCon con' sp') | con == con' -> unifySp ctx sp sp' 
   ---
diff --git a/src/ShiTT/Eval.hs b/src/ShiTT/Eval.hs
index a621799..a2c2c9a 100644
--- a/src/ShiTT/Eval.hs
+++ b/src/ShiTT/Eval.hs
@@ -26,16 +26,21 @@ instance Show Value where
         VLam x Expl b -> inParen $ "lambda " ++ x ++ ". "   ++ pp True (b @ x := VVar x)
         VLam x Impl b -> inParen $ "lambda {" ++ x ++ "}. " ++ pp True (b @ x := VVar x)
         VRig x sp -> if null sp then remove_infix x else inParen $ x ++ ppSp sp
-        VCon x sp -> {-"!con!" ++ -}pp is_top (VRig x sp)
+        VCon x sp -> pp is_top (VRig x sp)
         VFlex m sp -> pp is_top (VRig ('?':show m) sp)
-        VFunc x sp -> {- "!fun!" ++ -}pp is_top (VRig x.funName sp)
-        VPatVar x sp -> {- "!pat!" ++ -}pp is_top (VRig x sp)
+        VFunc x sp -> pp is_top (VRig x.funName sp)
+        VPatVar x sp -> pp is_top (VRig x sp)
         VPi x Expl t b -> inParen $ "Pi (" ++ x ++ ":" ++ pp True t ++ "). " ++ pp True (b @ x := VVar x)
         VPi x Impl t b -> inParen $ "Pi {" ++ x ++ ":" ++ pp True t ++ "}. " ++ pp True (b @ x := VVar x)
         VU -> "U"
         where paren x = '(' : x ++ ")"
               inParen x = if is_top then x else paren x
 
+-- For debug
+-- deriving instance Show Value 
+-- instance Show Closure where 
+--   show (Closure _ b) = show b 
+
 instance Show Context where 
   show ctx = "\n- env:" ++ show ctx.env ++ "\n- typ:" ++ show ctx.types ++ "\n- sig:" ++ show ctx.decls
 
@@ -80,6 +85,8 @@ eval ctx@(env -> env) = \case
   Meta m              -> vMeta m
   ---
   PatVar x            -> case M.lookup x env of 
+    Just (VPatVar y []) 
+      | y /= x -> eval ctx (PatVar y) 
     Just v -> v 
     Nothing 
       | head x == '*' -> VPatVar x []