updated readme

README.org

@@ -6,6 +6,7 @@
 * Syntax
 The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. =λ= and =Π= abstractions can be written in the usual ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn't appear in the body as usual.
 
+** Terms
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 #+begin_src
   λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) ⇒ λ (y : β) ⇒ x
@@ -40,6 +41,7 @@ You can also directly bind functions. Here's an example.
 #+end_src
 The syntax for binding functions is just like with definitions.
 
+** Definitions and Axioms
 Definitions and axioms have abstract syntax as shown below.
 #+begin_src
   def <ident> (<ident> : <type>)* : <type>? := <term>;
@@ -57,6 +59,24 @@ Type ascriptions are optional in both definitions and =let= bindings. If include
 
 If the RHS of a definition is =axiom=, then =perga= will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms.
 
+** Sections
+There is a Coq-like section mechanism. You open a section with =section <identifier>= and close it with =end <identifier>=. The identifiers used must match. The identifiers don't serve any purpose beyond organization.
+#+begin_src
+  section Test
+      variable (A B : *);
+      def id (x : A) := x;
+      def const (x : A) (y : B) := id x;
+  end Test
+
+  def id_full (A : *) (x : A) := id A x;
+  def const_full (A B : *) (x : A) (y : B) := const A B x y;
+#+end_src
+In a section, you can add section variables to the context with either =variable= or =hypothesis=. The syntax is the same as function parameters, so you can define multiple variables in one line, and can group section variables of the same type. Then, in the section, any definition using the section variables will be automatically generalized over the section variables that they use. Furthermore, any usage of such section variables (like =id x= in the definition of =const= above) will automatically apply the necessary section variables.
+
+Nested sections are supported, and work as you would expect.
+
+** Comments and preprocessor directives
+
 Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish.
 
 There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include <filepath>= (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. Additionally, =@include= automatically keeps track of what has been included, so duplicate inclusions are skipped, meaning no include guards are necessary.

app/Repl.hs

@@ -23,6 +23,7 @@ data ReplCommand
     | WeakNormalize String
     | Input String
     | LoadFile String
+    | DumpDebug String
     deriving (Show)
 
 parseCommand :: Maybe String -> Maybe ReplCommand
@@ -35,6 +36,7 @@ parseCommand (Just input)
     | ":n " `isPrefixOf` input = Normalize <$> stripPrefix ":n " input
     | ":w " `isPrefixOf` input = WeakNormalize <$> stripPrefix ":w " input
     | ":l " `isPrefixOf` input = LoadFile <$> stripPrefix ":l " input
+    | ":d " `isPrefixOf` input = DumpDebug <$> stripPrefix ":d " input
     | otherwise = Just $ Input input
 
 handleInput :: Env -> String -> InputT IO Env
@@ -46,9 +48,7 @@ handleInput env input =
             Right env' -> pure env'
 
 actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
-actOnParse input action = case parseExpr "repl" (pack input) of
+actOnParse input action = either outputStrLn (action . elaborate) $ parseExpr "repl" (pack input)
-    Left err -> outputStrLn err
-    Right expr -> action $ elaborate expr
 
 printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO ()
 printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env
@@ -78,5 +78,6 @@ repl = do
             Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env
             Just (Normalize input) -> parseActPrint env input normalize >> loop env
             Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env
+            Just (DumpDebug input) -> either outputStrLn (outputStrLn . show) (parseDef "repl" (pack input)) >> loop env
             Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile env filename) >>= either ((>> loop env) . outputStrLn) loop
             Just (Input input) -> handleInput env input >>= loop

examples/logic.pg

@@ -115,21 +115,25 @@ def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :
 
 -- Some logic theorems
 
+section Theorems
+
+    variable (A B C : *);
+
     -- ~(A ∨ B) => ~A ∧ ~B
-def de_morgan1 (A B : *) (h : not (or A B)) : and (not A) (not B) :=
+    def de_morgan1 (h : not (or A B)) : and (not A) (not B) :=
         and_intro (not A) (not B)
             (fun (a : A) => h (or_intro_l A B a))
             (fun (b : B) => h (or_intro_r A B b));
 
     -- ~A ∧ ~B => ~(A ∨ B)
-def de_morgan2 (A B : *) (h : and (not A) (not B)) : not (or A B) :=
+    def de_morgan2 (h : and (not A) (not B)) : not (or A B) :=
         fun (contra : or A B) => 
             or_elim A B false contra
                 (and_elim_l (not A) (not B) h)
                 (and_elim_r (not A) (not B) h);
 
     -- ~A ∨ ~B => ~(A ∧ B)
-def de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
+    def de_morgan3 (h : or (not A) (not B)) : not (and A B) :=
         fun (contra : and A B) =>
             or_elim (not A) (not B) false h
                 (fun (na : not A) => na (and_elim_l A B contra))
@@ -138,19 +142,19 @@ def de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
     -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
 
     -- A ∧ B => B ∧ A
-def and_comm (A B : *) (h : and A B) : and B A :=
+    def and_comm (h : and A B) : and B A :=
         and_intro B A
             (and_elim_r A B h)
             (and_elim_l A B h);
 
     -- A ∨ B => B ∨ A
-def or_comm (A B : *) (h : or A B) : or B A :=
+    def or_comm (h : or A B) : or B A :=
         or_elim A B (or B A) h
             (fun (a : A) => or_intro_r B A a)
             (fun (b : B) => or_intro_l B A b);
 
     -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
-def and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
+    def and_assoc_l (h : and A (and B C)) : and (and A B) C :=
         let (a := (and_elim_l A (and B C) h))
             (bc := (and_elim_r A (and B C) h))
             (b := (and_elim_l B C bc))
@@ -160,7 +164,7 @@ def and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
         end;
 
     -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
-def and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
+    def and_assoc_r (h : and (and A B) C) : and A (and B C) :=
         let (ab := and_elim_l (and A B) C h)
             (a := and_elim_l A B ab)
             (b := and_elim_r A B ab)
@@ -170,7 +174,7 @@ def and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
         end;
 
     -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
-def or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
+    def or_assoc_l (h : or A (or B C)) : or (or A B) C :=
         or_elim A (or B C) (or (or A B) C) h
             (fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
             (fun (g : or B C) =>
@@ -179,7 +183,7 @@ def or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
                     (fun (c : C) => or_intro_r (or A B) C c));
 
     -- (A ∨ B) ∨ C => A ∨ (B ∨ C)
-def or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
+    def or_assoc_r (h : or (or A B) C) : or A (or B C) :=
         or_elim (or A B) C (or A (or B C)) h
             (fun (g : or A B) => 
                 or_elim A B (or A (or B C)) g
@@ -188,7 +192,7 @@ def or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
             (fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
 
     -- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
-def and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :=
+    def and_distrib_l_or (h : and A (or B C)) : or (and A B) (and A C) :=
         or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
             (fun (b : B) => or_intro_l (and A B) (and A C)
                 (and_intro A B (and_elim_l A (or B C) h) b))
@@ -196,7 +200,7 @@ def and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :
                 (and_intro A C (and_elim_l A (or B C) h) c));
 
     -- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
-def and_factor_l_or (A B C : *) (h : or (and A B) (and A C)) : and A (or B C) :=
+    def and_factor_l_or (h : or (and A B) (and A C)) : and A (or B C) :=
         or_elim (and A B) (and A C) (and A (or B C)) h
             (fun (ab : and A B) => and_intro A (or B C)
                 (and_elim_l A B ab)
@@ -207,9 +211,11 @@ def and_factor_l_or (A B C : *) (h : or (and A B) (and A C)) : and A (or B C) :=
 
     -- Thanks Quinn!
     -- A ∨ B => ~B => A
-def disj_syllog (A B : *) (nb : not B) (hor : or A B) : A :=
+    def disj_syllog (nb : not B) (hor : or A B) : A :=
         or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
 
     -- (A => B) => ~B => ~A
-def contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
+    def contrapositive (f : A -> B) (nb : not B) : not A :=
         fun (a : A) => nb (f a);
+
+end Theorems

examples/peano.pg

@@ -155,73 +155,72 @@ def suc_or_zero : forall (n : nat), szc n :=
 -- satisfying 1 and 2. From there we will, with much effort, prove that R is
 -- actually a function satisfying the equations we want it to.
 
+section RecursiveDefs
+
+variable (A : *) (z : A) (fS : nat -> A -> A);
+
 -- {{{ Defining R
 -- Here is condition 1 formally expressed in perga.
-def cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond1 (Q : nat -> A -> *) := Q zero z;
-    Q zero z;
 
 -- Likewise for condition 2.
-def cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond2 (Q : nat -> A -> *) :=
     forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
 
 -- From here we can define R.
-def rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel (x : nat) (y : A) :=
-    forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
+    forall (Q : nat -> A -> *), cond1 Q -> cond2 Q -> Q x y;
 -- }}}
 
 -- {{{ R is total
 def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
 
-def rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
+def rec_rel_cond1 : cond1 rec_rel :=
-    fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;
+    fun (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
 
-def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
+def rec_rel_cond2 : cond2 rec_rel :=
-    fun (n : nat) (y : A) (h : rec_rel A z fS n y)
+    fun (n : nat) (y : A) (h : rec_rel n y)
-        (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
+        (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) =>
         h2 n y (h Q h1 h2);
 
-def rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
+def rec_rel_total : total nat A rec_rel :=
-    let (R           := rec_rel A z fS)
+    let (R           := rec_rel)
         (P (x : nat) := exists A (R x))
-        (c1          := cond1 A z fS)
-        (c2          := cond2 A z fS)
     in
     nat_ind P
-    (exists_intro A (R zero) z (rec_rel_cond1 A z fS))
+    (exists_intro A (R zero) z rec_rel_cond1)
     (fun (n : nat) (IH : P n) =>
         exists_elim A (P (suc n)) (R n) IH
         (fun (y0 : A) (hy : R n y0) =>
-            exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 A z fS n y0 hy)))
+            exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
     end;
+
 -- }}}
 
 -- {{{ Defining R2
-def alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
+def alt_cond1 (x : nat) (y : A) :=
     and (eq nat x zero) (eq A y z);
 
-def cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
+def cond_y2 (x : nat) (y : A)
     (x2 : nat) (y2 : A) :=
-        and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);
+        and (eq A y (fS x2 y2)) (rec_rel x2 y2);
 
-def cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
+def cond_x2 (x : nat) (y : A) (x2 : nat) :=
-    and (pred x x2) (exists A (cond_y2 A z fS x y x2));
+    and (pred x x2) (exists A (cond_y2 x y x2));
 
-def alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
-    exists nat (cond_x2 A z fS x y);
 
-def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
-    or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
 -- }}}
 
 -- {{{ R = R2
 
 -- {{{ R2 ⊆ R
-def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
-    rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
+    let (R   := rec_rel)
-    let (R   := rec_rel A z fS)
+        (R2  := rec_rel_alt)
-        (R2  := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 x y)
-        (ac1 := alt_cond1 A z x y)
+        (ac2 := alt_cond2 x y)
-        (ac2 := alt_cond2 A z fS x y)
     in
         fun (h : R2 x y) =>
             or_elim ac1 ac2 (R x y) h
@@ -229,13 +228,13 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
                 let
                     (x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
                     (yz := and_elim_r (eq nat x zero) (eq A y z) case1)
-                    (a1 := (eq_sym A y z yz) (R zero) (rec_rel_cond1 A z fS))
+                    (a1 := (eq_sym A y z yz) (R zero) rec_rel_cond1)
                 in
                     (eq_sym nat x zero x0) (fun (n : nat) => R n y) a1
                 end)
             (fun (case2 : ac2) =>
-                let (h1 := cond_x2 A z fS x y)
+                let (h1 := cond_x2 x y)
-                    (h2 := cond_y2 A z fS x y)
+                    (h2 := cond_y2 x y)
                 in
                 exists_elim nat (R x y) h1 case2
                 (fun (x2 : nat) (hx2 : h1 x2) =>
@@ -246,7 +245,7 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
                     (fun (y2 : A) (hy2 : h2 x2 y2) =>
                         let (hpreim := and_elim_l (eq A y (fS x2 y2)) (R x2 y2) hy2)
                             (hR     := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2)
-                            (a1     := rec_rel_cond2 A z fS x2 y2 hR)
+                            (a1     := rec_rel_cond2 x2 y2 hR)
                             (a2     := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1)
                         in
                             (eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2
@@ -257,41 +256,36 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
 -- }}}
 
 -- {{{ R ⊆ R2
-def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
+def R2_cond1 : cond1 rec_rel_alt :=
-    or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
+    or_intro_l (alt_cond1 zero z) (alt_cond2 zero z)
     (and_intro (eq nat zero zero) (eq A z z)
         (eq_refl nat zero)
         (eq_refl A z));
 
-def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
+def R2_cond2 : cond2 rec_rel_alt :=
-    let (R  := rec_rel A z fS)
+    let (R  := rec_rel)
-        (R2 := rec_rel_alt A z fS)
+        (R2 := rec_rel_alt)
     in
         fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
         let (x   := suc x2)
             (y   := fS x2 y2)
-            (cx2 := cond_x2 A z fS x y)
+            (cx2 := cond_x2 x y)
-            (cy2 := cond_y2 A z fS x y x2)
+            (cy2 := cond_y2 x y x2)
         in
-            or_intro_r (alt_cond1 A z x y) (alt_cond2 A z fS x y)
+            or_intro_r (alt_cond1 x y) (alt_cond2 x y)
             (exists_intro nat cx2 x2
                 (and_intro (pred x x2) (exists A cy2)
                     (eq_refl nat x)
                     (exists_intro A cy2 y2
                         (and_intro (eq A y y) (R x2 y2)
                             (eq_refl A y)
-                            (R2_sub_R A z fS x2 y2 h)))))
+                            (R2_sub_R x2 y2 h)))))
         end
     end;
 
-def R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+
-    rec_rel A z fS x y -> rec_rel_alt A z fS x y :=
+def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
-    let (R  := rec_rel A z fS)
+    fun (h : rec_rel x y) => h rec_rel_alt R2_cond1 R2_cond2;
-        (R2 := rec_rel_alt A z fS)
-    in
-        fun (h : R x y) =>
-            h R2 (R2_cond1 A z fS) (R2_cond2 A z fS)
-    end;
 -- }}}
 
 -- }}}
@@ -303,13 +297,12 @@ def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
 
 def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
 
-def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
+def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
-    rec_rel_alt A z fS zero y -> eq A y z :=
+    let (R2  := rec_rel_alt)
-    let (R2  := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 zero y)
-        (ac1 := alt_cond1 A z zero y)
+        (ac2 := alt_cond2 zero y)
-        (ac2 := alt_cond2 A z fS zero y)
+        (cx2 := cond_x2 zero y)
-        (cx2 := cond_x2 A z fS zero y)
+        (cy2 := cond_y2 zero y)
-        (cy2 := cond_y2 A z fS zero y)
     in fun (h : R2 zero y) =>
         or_elim ac1 ac2 (eq A y z) h
         (fun (case1 : ac1) => and_elim_r (eq nat zero zero) (eq A y z) case1)
@@ -321,14 +314,13 @@ def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
                 (eq A y z)))
     end;
 
-def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
+def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc x2) y x2) :=
-    rec_rel_alt A z fS (suc x2) y -> exists A (cond_y2 A z fS (suc x2) y x2) :=
+    let (R2   := rec_rel_alt)
-    let (R2   := rec_rel_alt A z fS)
         (x    := suc x2)
-        (ac1  := alt_cond1 A z x y)
+        (ac1  := alt_cond1 x y)
-        (ac2  := alt_cond2 A z fS x y)
+        (ac2  := alt_cond2 x y)
-        (cx2  := cond_x2 A z fS x y)
+        (cx2  := cond_x2 x y)
-        (cy2  := cond_y2 A z fS x y)
+        (cy2  := cond_y2 x y)
         (goal := exists A (cy2 x2))
     in
         fun (h : R2 x y) =>
@@ -347,31 +339,31 @@ def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
                 end))
     end;
 
-def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
+def R2_functional : fl nat A rec_rel_alt :=
-    let (R    := rec_rel A z fS)
+    let (R    := rec_rel)
-        (R2   := rec_rel_alt A z fS)
+        (R2   := rec_rel_alt)
         (f_in := fl_in nat A R2)
     in nat_ind f_in
         (fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) =>
             eq_trans A y1 z y2
-            (R2_zero A z fS y1 h1)
+            (R2_zero y1 h1)
-            (eq_sym A y2 z (R2_zero A z fS y2 h2)))
+            (eq_sym A y2 z (R2_zero y2 h2)))
         (fun (x2 : nat) (IH : f_in x2) (y1 y2 : A) (h1 : R2 (suc x2) y1) (h2 : R2 (suc x2) y2) =>
             let (x    := suc x2)
-                (cy1  := cond_y2 A z fS x y1 x2)
+                (cy1  := cond_y2 x y1 x2)
-                (cy2  := cond_y2 A z fS x y2 x2)
+                (cy2  := cond_y2 x y2 x2)
                 (goal := eq A y1 y2)
             in
-                exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1)
+                exists_elim A goal cy1 (R2_suc x2 y1 h1)
                 (fun (y12 : A) (h12 : cy1 y12) =>
-                    exists_elim A goal cy2 (R2_suc A z fS x2 y2 h2)
+                    exists_elim A goal cy2 (R2_suc x2 y2 h2)
                     (fun (y22 : A) (h22 : cy2 y22) =>
                         let (y1_preim  := and_elim_l (eq A y1 (fS x2 y12)) (R x2 y12) h12)
                             (y2_preim  := and_elim_l (eq A y2 (fS x2 y22)) (R x2 y22) h22)
                             (R_x2_y12  := and_elim_r (eq A y1 (fS x2 y12)) (R x2 y12) h12)
                             (R_x2_y22  := and_elim_r (eq A y2 (fS x2 y22)) (R x2 y22) h22)
-                            (R2_x2_y12 := R_sub_R2 A z fS x2 y12 R_x2_y12)
+                            (R2_x2_y12 := R_sub_R2 x2 y12 R_x2_y12)
-                            (R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22)
+                            (R2_x2_y22 := R_sub_R2 x2 y22 R_x2_y22)
                             (y12_y22   := IH y12 y22 R2_x2_y12 R2_x2_y22)
                         in
                             eq_trans A y1 (fS x2 y12) y2
@@ -383,21 +375,16 @@ def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A
             end)
     end;
 
-def R_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel A z fS) :=
+def R_functional : fl nat A rec_rel :=
-    let (R   := rec_rel A z fS)
+    fun (n : nat) (y1 y2 : A) (h1 : rec_rel n y1) (h2 : rec_rel n y2) =>
-        (sub := R_sub_R2 A z fS)
+        R2_functional n y1 y2 (R_sub_R2 n y1 h1) (R_sub_R2 n y2 h2);
-    in
-        fun (n : nat) (y1 y2 : A) (h1 : R n y1) (h2 : R n y2) =>
-            R2_functional A z fS n y1 y2 (sub n y1 h1) (sub n y2 h2)
-    end;
 
 -- }}}
 
 -- {{{ Actually defining the function
 
-def rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
+def rec_def (x : nat) : A :=
-    exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
+    exists_elim A A (rec_rel x) (rec_rel_total x) (fun (y : A) (_ : rec_rel x y) => y);
-        (fun (y : A) (_ : rec_rel A z fS x y) => y);
 
 -- }}}
 
@@ -415,39 +402,30 @@ axiom definite_description (A : *) (P : A -> *) (h : exists A P) :
     P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
 
 -- Now we can use this axiom to prove that R n (rec_def n).
-def rec_def_sat (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : rec_rel A z fS x (rec_def A z fS x) :=
+def rec_def_sat (x : nat) : rec_rel x (rec_def x) :=
-    definite_description A (rec_rel A z fS x) (rec_rel_total A z fS x);
+    definite_description A (rec_rel x) (rec_rel_total x);
 
-def eq1 (A : *) (z : A) (f : nat -> A) := eq A (f zero) z;
+def eq1 (f : nat -> A) := eq A (f zero) z;
 
-def eq2 (A : *) (z : A) (fS : nat -> A -> A) (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
+def eq2 (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
 
 -- f zero = z
-def rec_def_sat_zero (A : *) (z : A) (fS : nat -> A -> A) : eq1 A z (rec_def A z fS) :=
+def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
-    let (f := rec_def A z fS) in
-        R_functional A z fS zero (f zero) z
-        (rec_def_sat A z fS zero)
-        (rec_rel_cond1 A z fS)
-    end;
 
 -- f n = y -> f (suc n) = fS n y
-def rec_def_sat_suc (A : *) (z : A) (fS : nat -> A -> A) : eq2 A z fS (rec_def A z fS) :=
+def rec_def_sat_suc : eq2 rec_def :=
     fun (n : nat) =>
-        let (R     := rec_rel A z fS)
+        let (y     := rec_def n)
-            (f     := rec_def A z fS)
+            (RSnfy := rec_rel_cond2 n y (rec_def_sat n))
-            (y     := f n)
-            (Rf    := rec_def_sat A z fS)
-            (RSnfy := rec_rel_cond2 A z fS n y (Rf n))
         in
-            R_functional A z fS (suc n) (f (suc n)) (fS n y) (Rf (suc n)) RSnfy 
+            R_functional (suc n) (rec_def (suc n)) (fS n y) (rec_def_sat (suc n)) RSnfy 
         end;
 
 -- }}}
 
 -- {{{ The function satisfying these equations is unique
 
-def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A)
+def rec_def_unique (fS : nat -> A -> A) (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
-    (h1f : eq1 A z f) (h2f : eq2 A z fS f) (h1g : eq1 A z g) (h2g : eq2 A z fS g)
     : forall (n : nat), eq A (f n) (g n) :=
         nat_ind (fun (n : nat) => eq A (f n) (g n))
         -- base case: f 0 = g 0
@@ -470,6 +448,8 @@ def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A)
 
 -- }}}
 
+end RecursiveDefs
+
 -- }}}
 
 -- Now we can safely define addition.

lib/Elaborator.hs

@@ -1,13 +1,174 @@
+{-# LANGUAGE TupleSections #-}
+
 module Elaborator where
 
-import Data.List (elemIndex)
+import Data.List (elemIndex, lookup)
+import qualified Data.Set as S
 import Expr (Expr)
 import qualified Expr as E
-import IR (IRExpr)
+import IR (IRDef (..), IRExpr, IRProgram, IRSectionDef (..))
 import qualified IR as I
+import Relude.Extra.Lens
 
 type Binders = [Text]
 
+data SectionContext = SectionContext
+    { sectionDefs :: [(Text, [(Text, IRExpr)])] -- name and list of variables and their types it depends on
+    , sectionVars :: [(Text, IRExpr)] -- variables and their types
+    }
+
+type ElabMonad = State SectionContext
+
+lookupDefInCtxt :: Text -> SectionContext -> Maybe [(Text, IRExpr)]
+lookupDefInCtxt def (SectionContext defs _) = lookup def defs
+
+-- looks up a definition in the context and gives a list of the variables and
+-- their types that it depends on
+lookupDef :: Text -> ElabMonad (Maybe [(Text, IRExpr)])
+lookupDef def = lookupDefInCtxt def <$> get
+
+lookupVarInCtxt :: Text -> SectionContext -> Maybe IRExpr
+lookupVarInCtxt var = lookup var . sectionVars
+
+-- looks up a variable in the context and returns its type
+lookupVar :: Text -> ElabMonad (Maybe IRExpr)
+lookupVar var = lookupVarInCtxt var <$> get
+
+sectionDefsL :: Lens' SectionContext [(Text, [(Text, IRExpr)])]
+sectionDefsL = lens sectionDefs setter
+  where
+    setter ctxt newDefs = ctxt{sectionDefs = newDefs}
+
+sectionVarsL :: Lens' SectionContext [(Text, IRExpr)]
+sectionVarsL = lens sectionVars setter
+  where
+    setter ctxt newVars = ctxt{sectionVars = newVars}
+
+saveState :: ElabMonad a -> ElabMonad a
+saveState action = get >>= (action <*) . put
+
+debugIRExpr :: IRExpr -> String
+debugIRExpr = E.prettyS . elaborate
+
+debugIRDef :: IRDef -> String
+debugIRDef (Def name (Just ty) body) = "def " ++ toString name ++ " : " ++ debugIRExpr ty ++ " := " ++ debugIRExpr body ++ ";"
+debugIRDef (Def name Nothing body) = "def " ++ toString name ++ " := " ++ debugIRExpr body ++ ";"
+debugIRDef (Axiom name typ) = "axiom " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
+
+debugIRSectionDef :: IRSectionDef -> String
+debugIRSectionDef (Variable name typ) = "variable " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
+debugIRSectionDef (Section name _) = "section " ++ toString name ++ ";"
+debugIRSectionDef (IRDef def) = debugIRDef def
+
+elabSection :: Text -> [IRSectionDef] -> ElabMonad [IRDef]
+elabSection _name contents = saveState $ concat <$> forM contents elabDef
+
+elabProgram :: IRProgram -> [IRDef]
+elabProgram prog = evalState (elabSection "" prog) (SectionContext [] [])
+
+pushVariable :: Text -> IRExpr -> SectionContext -> SectionContext
+pushVariable name ty (SectionContext defs vars) = SectionContext defs ((name, ty) : vars)
+
+pushDefinition :: Text -> [(Text, IRExpr)] -> SectionContext -> SectionContext
+pushDefinition name defVars (SectionContext defs vars) = SectionContext ((name, defVars) : defs) vars
+
+removeName :: Text -> ElabMonad ()
+removeName name = do 
+    modify $ over sectionDefsL (filter ((/= name) . fst))
+    modify $ over sectionVarsL (filter ((/= name) . fst))
+
+extendVars :: Set (Text, IRExpr) -> ElabMonad (Set (Text, IRExpr))
+extendVars vars = do
+    vars' <- foldr S.union S.empty <$> traverse (usedVars . snd) (S.toList vars)
+    if vars' `S.isSubsetOf` vars
+        then pure vars
+        else extendVars (vars `S.union` vars')
+
+organize :: Set (Text, IRExpr) -> ElabMonad [(Text, IRExpr)]
+organize found = do
+    vars <- gets sectionVars
+    pure $ reverse [var | var <- vars, var `S.member` found]
+
+-- find all the section variables used in an expression
+usedVars :: IRExpr -> ElabMonad (Set (Text, IRExpr))
+usedVars (I.Var name) = do
+    varDeps <- maybe S.empty (S.singleton . (name,)) <$> lookupVar name
+    defDeps <- maybe S.empty S.fromList <$> lookupDef name
+    pure $ varDeps `S.union` defDeps
+usedVars I.Star = pure S.empty
+usedVars (I.Level _) = pure S.empty
+usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n
+usedVars (I.Abs name ty ascr body) = saveState $ do
+    ty' <- usedVars ty
+    ascr' <- traverse usedVars ascr
+    removeName name
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+usedVars (I.Pi name ty ascr body) = saveState $ do
+    ty' <- usedVars ty
+    ascr' <- traverse usedVars ascr
+    removeName name
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+usedVars (I.Let name ascr value body) = saveState $ do
+    ty' <- usedVars value
+    ascr' <- traverse usedVars ascr
+    removeName name
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+
+-- traverse the body of a definition, adding the necessary section arguments to
+-- any definitions made within the section
+traverseBody :: IRExpr -> ElabMonad IRExpr
+traverseBody (I.Var name) = do
+    mdeps <- lookupDef name
+    case mdeps of
+        Nothing -> pure $ I.Var name
+        Just deps -> pure $ foldl' (\acc newVar -> I.App acc (I.Var $ fst newVar)) (I.Var name) deps
+traverseBody I.Star = pure I.Star
+traverseBody (I.Level k) = pure $ I.Level k
+traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n
+traverseBody (I.Abs name ty ascr body) = saveState $ do
+    ty' <- traverseBody ty
+    ascr' <- traverse traverseBody ascr
+    removeName name
+    I.Abs name ty' ascr' <$> traverseBody body
+traverseBody (I.Pi name ty ascr body) = saveState $ do
+    ty' <- traverseBody ty
+    ascr' <- traverse traverseBody ascr
+    removeName name
+    I.Pi name ty' ascr' <$> traverseBody body
+traverseBody (I.Let name ascr value body) = saveState $ do
+    ascr' <- traverse traverseBody ascr
+    value' <- traverseBody value
+    removeName name
+    I.Let name ascr' value' <$> traverseBody body
+
+mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
+mkPi (param, typ) = I.Pi param typ Nothing
+
+mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr
+mkAbs (param, typ) = I.Abs param typ Nothing
+
+generalizeType :: IRExpr -> [(Text, IRExpr)] -> IRExpr
+generalizeType = foldr mkPi
+
+generalizeVal :: IRExpr -> [(Text, IRExpr)] -> IRExpr
+generalizeVal = foldr mkAbs
+
+elabDef :: IRSectionDef -> ElabMonad [IRDef]
+elabDef (IRDef (Def name ty body)) = do
+    tyVars <- fromMaybe S.empty <$> traverse usedVars ty
+    bodyVars <- usedVars body
+    totalVars <- extendVars (tyVars `S.union` bodyVars) >>= organize
+    newBody <- traverseBody body
+    newType <- traverse traverseBody ty
+    modify $ pushDefinition name totalVars
+    pure [Def name (flip generalizeType totalVars <$> newType) (generalizeVal newBody totalVars)]
+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 (Variable name ty) = [] <$ modify' (pushVariable name ty)
+
 saveBinders :: State Binders a -> State Binders a
 saveBinders action = do
     binders <- get
@@ -18,10 +179,6 @@ saveBinders action = do
 elaborate :: IRExpr -> Expr
 elaborate ir = evalState (elaborate' ir) []
   where
-    helper :: (Monad m) => Maybe a -> (a -> m b) -> m (Maybe b)
-    helper Nothing _ = pure Nothing
-    helper (Just x) f = Just <$> f x
-
     elaborate' :: IRExpr -> State Binders Expr
     elaborate' (I.Var n) = do
         binders <- get
@@ -31,12 +188,12 @@ elaborate ir = evalState (elaborate' ir) []
     elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
     elaborate' (I.Abs x t a b) = saveBinders $ do
         t' <- elaborate' t
-        a' <- helper a elaborate'
+        a' <- traverse elaborate' a
         modify (x :)
         E.Abs x t' a' <$> elaborate' b
     elaborate' (I.Pi x t a b) = saveBinders $ do
         t' <- elaborate' t
-        a' <- helper a elaborate'
+        a' <- traverse elaborate' a
         modify (x :)
         E.Pi x t' a' <$> elaborate' b
     elaborate' (I.Let name Nothing val body) = saveBinders $ do

lib/Errors.hs

@@ -9,6 +9,7 @@ data Error
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
+    | EmptySection Text
     deriving (Eq, Ord)
 
 instance ToText Error where
@@ -18,6 +19,7 @@ instance ToText Error where
     toText (NotEquivalent a a' e) = "Cannot unify '" <> pretty a <> "' with '" <> pretty a' <> "' when evaluating '" <> pretty e <> "'"
     toText (PNMissingType x) = "Axiom '" <> x <> "' missing type ascription"
     toText (DuplicateDefinition n) = "'" <> n <> "' already defined"
+    toText (EmptySection var) = "Tried to declare variable " <> var <> " without a section"
 
 instance ToString Error where
     toString = toString . toText

lib/Expr.hs

@@ -143,12 +143,12 @@ helper k e@(Pi{}) = if k > 2 then parenthesize res else res
   where
     (params, body) = collectPis e
     grouped = showParamGroup <$> groupParams params
-    res = "∏ " <> unwords grouped <> " . " <> pretty body
+    res = "∏ " <> unwords grouped <> " , " <> pretty body
 helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
   where
     (params, body) = collectLambdas e
     grouped = showParamGroup <$> groupParams params
-    res = "λ " <> unwords grouped <> " . " <> pretty body
+    res = "λ " <> unwords grouped <> " => " <> pretty body
 helper _ e@(Let{}) = res
   where
     (binds, body) = collectLets e

lib/IR.hs

@@ -30,6 +30,18 @@ data IRExpr
         }
     deriving (Show, Eq, Ord)
 
+data IRSectionDef
+    = Section
+        { sectionName :: Text
+        , sectionContents :: [IRSectionDef]
+        }
+    | Variable
+        { variableName :: Text
+        , variableType :: IRExpr
+        }
+    | IRDef IRDef
+    deriving (Show, Eq, Ord)
+
 data IRDef
     = Def
         { defName :: Text
@@ -40,5 +52,6 @@ data IRDef
         { axiomName :: Text
         , axiomAscription :: IRExpr
         }
+    deriving (Show, Eq, Ord)
 
-type IRProgram = [IRDef]
+type IRProgram = [IRSectionDef]

lib/Parser.hs

@@ -34,10 +34,7 @@ eat :: Text -> Parser ()
 eat = void . lexeme . chunk
 
 keywords :: [Text]
-keywords = ["forall", "let", "in", "end", "fun", "def", "axiom"]
+keywords = ["forall", "let", "in", "end", "fun", "def", "axiom", "section", "variable", "hypothesis"]
-
-reservedChars :: [Char]
-reservedChars = "();:"
 
 pIdentifier :: Parser Text
 pIdentifier = try $ label "identifier" $ lexeme $ do
@@ -158,29 +155,6 @@ pNumSort = lexeme $ pSquare >> Level <$> (L.decimal <|> subscriptInt)
 pSort :: Parser IRExpr
 pSort = lexeme $ pStar <|> try pNumSort <|> pSquare
 
-pAxiom :: Parser IRDef
-pAxiom = lexeme $ label "axiom" $ do
-    eat "axiom"
-    ident <- pIdentifier
-    params <- pManyParams
-    ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
-    eat ";"
-    pure $ Axiom ident ascription
-
-pDef :: Parser IRDef
-pDef = lexeme $ label "definition" $ do
-    eat "def"
-    ident <- pIdentifier
-    params <- pManyParams
-    ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
-    eat ":="
-    body <- pIRExpr
-    eat ";"
-    pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
-
-pIRDef :: Parser IRDef
-pIRDef = pAxiom <|> pDef
-
 pTerm :: Parser IRExpr
 pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
 
@@ -193,8 +167,47 @@ pIRExpr = lexeme $ try pArrow <|> pAppTerm
 pAscription :: Parser IRExpr
 pAscription = lexeme $ try $ eat ":" >> label "type" pIRExpr
 
+pAxiom :: Parser IRDef
+pAxiom = lexeme $ label "axiom" $ do
+    eat "axiom"
+    ident <- pIdentifier
+    params <- pManyParams
+    ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
+    eat ";"
+    pure $ Axiom ident ascription
+
+pVariable :: Parser [IRSectionDef]
+pVariable = lexeme $ label "variable declaration" $ do
+    eat "variable" <|> eat "hypothesis"
+    vars <- pManyParams
+    eat ";"
+    pure $ uncurry Variable <$> vars
+
+pDef :: Parser IRDef
+pDef = lexeme $ label "definition" $ do
+    eat "def"
+    ident <- pIdentifier
+    params <- pManyParams
+    ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
+    eat ":="
+    body <- pIRExpr
+    eat ";"
+    pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
+
+pSection :: Parser IRSectionDef
+pSection = lexeme $ label "section" $ do
+    eat "section"
+    secLabel <- pIdentifier
+    body <- concat <$> many pIRDef
+    eat "end"
+    void $ lexeme $ chunk secLabel
+    pure $ Section secLabel body
+
+pIRDef :: Parser [IRSectionDef]
+pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection)
+
 pIRProgram :: Parser IRProgram
-pIRProgram = skipSpace >> some pIRDef
+pIRProgram = skipSpace >> concat <$> some pIRDef
 
 parserWrapper :: Parser a -> String -> Text -> Either String a
 parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
@@ -203,7 +216,7 @@ parseProgram :: String -> Text -> Either String IRProgram
 parseProgram = parserWrapper pIRProgram
 
 parseDef :: String -> Text -> Either String IRDef
-parseDef = parserWrapper pIRDef
+parseDef = parserWrapper (pAxiom <|> pDef)
 
 parseExpr :: String -> Text -> Either String IRExpr
 parseExpr = parserWrapper pIRExpr

lib/Program.hs

@@ -41,7 +41,7 @@ evalDef :: Env -> IRDef -> Result Env
 evalDef = flip (execStateT . handleDef)
 
 handleProgram :: Env -> IRProgram -> Result Env
-handleProgram env = flip execStateT env . mapM_ handleDef
+handleProgram env = flip execStateT env . mapM_ handleDef . elabProgram
 
 handleAndParseProgram :: Env -> String -> Text -> Either String Env
 handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input