From fbfd8891bb53155da92cab3d589d233d1f02efa2 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Sun, 8 Dec 2024 19:37:56 -0800
Subject: [PATCH] solved #16

---
 examples/category.pg | 37 +++++++++++++++++++++++++++++++++++++
 examples/logic.pg    | 20 ++++++++++++++++++++
 lib/Elaborator.hs    | 19 +++++++++++++++++--
 lib/Eval.hs          |  6 ------
 4 files changed, 74 insertions(+), 8 deletions(-)
 create mode 100644 examples/category.pg

diff --git a/examples/category.pg b/examples/category.pg
new file mode 100644
index 0000000..5bb5f72
--- /dev/null
+++ b/examples/category.pg
@@ -0,0 +1,37 @@
+@include logic.pg
+
+section Category
+    variable
+        (Obj  : *)
+        (Hom  : Obj -> Obj -> *)
+        (id   : forall (A     : Obj), Hom A A)
+        (comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C);
+
+    hypothesis
+        (id_l  : forall (A B     : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f)
+        (id_r  : forall (A B     : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f)
+        (assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D),
+            eq (Hom A D)
+                (comp A B D f (comp B C D g h))
+                (comp A C D (comp A B C f g) h));
+
+    def initial  (A : Obj) := forall (B : Obj), exists_uniq (Hom A B) (fun (f : Hom A B) => true);
+    def terminal (A : Obj) := forall (B : Obj), exists_uniq (Hom B A) (fun (f : Hom B A) => true);
+
+    section Inverses
+        variable
+            (A B : Obj)
+            (f : Hom A B)
+            (g : Hom B A);
+
+        def inv_l := eq (Hom A A) (comp A B A f g) (id A);
+        def inv_r := eq (Hom B B) (comp B A B g f) (id B);
+
+        def inv := and inv_l inv_r;
+    end Inverses
+
+    def isomorphic (A B : Obj) :=
+        exists (Hom A B) (fun (f : Hom A B) =>
+            exists (Hom B A) (fun (g : Hom B A) => 
+                inv A B f g));
+end Category
diff --git a/examples/logic.pg b/examples/logic.pg
index 3fd95a9..d90a909 100644
--- a/examples/logic.pg
+++ b/examples/logic.pg
@@ -9,6 +9,14 @@ def false_elim (A : *) (contra : false) : A := contra A;
 
 -- --------------------------------------------------------------------------------------------------------------
 
+-- True
+
+def true : * := forall (A : *), A -> A;
+
+def true_intro : true := fun (A : *) (x : A) => x;
+
+-- --------------------------------------------------------------------------------------------------------------
+
 -- Negation
 
 def not (A : *) : * := A -> false;
@@ -113,6 +121,18 @@ def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :
 
 -- --------------------------------------------------------------------------------------------------------------
 
+-- unique existence
+def exists_uniq (A : *) (P : A -> *) : * :=
+    exists A (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y));
+
+def exists_uniq_elim (A B : *) (P : A -> *) (ex_a : exists_uniq A P) (h : forall (a : A), P a -> (forall (y : A), P y -> eq A a y) -> B) : B :=
+    exists_elim A B (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y)) ex_a
+    (fun (a : A) (h2 : and (P a) (forall (y : A), P y -> eq A a y)) =>
+        h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2)
+            (and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2));
+
+-- --------------------------------------------------------------------------------------------------------------
+
 -- Some logic theorems
 
 section Theorems
diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs
index f79472e..8f85180 100644
--- a/lib/Elaborator.hs
+++ b/lib/Elaborator.hs
@@ -44,11 +44,26 @@ sectionVarsL = lens sectionVars setter
   where
     setter ctxt newVars = ctxt{sectionVars = newVars}
 
+saveStateSection :: ElabMonad a -> ElabMonad a
+saveStateSection action = do
+    (SectionContext _ oldVars) <- get
+    res <- action
+    (SectionContext newDefs _) <- get
+    put (SectionContext (mapMaybe (usesFrom oldVars) newDefs) oldVars)
+    pure res
+  where
+    usesFrom :: [(Text, IRExpr)] -> (Text, [(Text, IRExpr)]) -> Maybe (Text, [(Text, IRExpr)])
+    usesFrom vars (name, uses) =
+        let newUses = filter (`elem` vars) uses
+         in if null newUses
+                then Nothing
+                else Just (name, newUses)
+
 saveState :: ElabMonad a -> ElabMonad a
 saveState action = get >>= (action <*) . put
 
 elabSection :: Text -> [IRSectionDef] -> ElabMonad [IRDef]
-elabSection _name contents = saveState $ concat <$> forM contents elabDef
+elabSection _name contents = saveStateSection $ concat <$> forM contents elabDef
 
 elabProgram :: IRProgram -> [IRDef]
 elabProgram prog = evalState (elabSection "" prog) (SectionContext [] [])
@@ -155,7 +170,7 @@ elabDef (IRDef (Axiom name ty)) = do
     vars <- usedVars ty >>= extendVars >>= organize
     modify $ pushDefinition name vars
     pure [Axiom name (generalizeType ty vars)]
-elabDef (Section name contents) = saveState $ elabSection name contents
+elabDef (Section name contents) = saveStateSection $ elabSection name contents
 elabDef (Variable name ty) = [] <$ pushVariable name ty
 
 saveBinders :: State Binders a -> State Binders a
diff --git a/lib/Eval.hs b/lib/Eval.hs
index 7239d0b..df79b16 100644
--- a/lib/Eval.hs
+++ b/lib/Eval.hs
@@ -80,12 +80,6 @@ normalize e = do
         then pure e
         else normalize e'
 
--- betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
--- betaEquiv e1 e2 = do
---     e1' <- normalize e1
---     e2' <- normalize e2
---     pure $ e1' == e2'
-
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
 betaEquiv e1 e2
     | e1 == e2 = pure True