updated README with changes

README.org

@@ -18,11 +18,11 @@ To be perfectly clear, =λ= abstractions can be written with either "λ" or "fun
 
 =Let= expressions have syntax shown below.
 #+begin_src
-  let ( (<ident> := <expr>) )+ in <expr> end
+  let ( (<ident> (: <type>)? := <expr>) )+ in <expr> end
 #+end_src
 Below is a more concrete example.
 #+begin_src
-  let (a := (and_elim_l A (and B C) h))
+  let (a : 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))
       (c := (and_elim_r B C bc))
@@ -38,19 +38,20 @@ You can also directly bind functions. Here's an example.
 #+end_src
 The syntax for binding functions is just like with definitions.
 
-Definitions have abstract syntax as shown below.
+Definitions and axioms have abstract syntax as shown below.
 #+begin_src
-  <ident> (<ident> : <type>)* : <type>? := <term> | axiom;
+  def <ident> (<ident> : <type>)* : <type>? := <term>;
+  axiom <ident> (<ident> : <type>)* : <type>;
 #+end_src
-(The distinction between =<type>= and =<term>= is for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=). Duplicate definitions are not normally allowed and will result in an error.
+(The distinction between =<type>= and =<term>= is purely for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=). Duplicate definitions are not normally allowed and will result in an error.
 #+begin_src
-  const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x;
+  def const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x;
-  const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
+  def const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
-  const (α β : *) (x : α) (y : β) : α := x;
+  def const (α β : *) (x : α) (y : β) : α := x;
 
-  funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g := axiom;
+  axiom funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g;
 #+end_src
-Type ascriptions are optional. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
+Type ascriptions are optional in both definitions and =let= bindings. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
 
 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.
 
@@ -59,7 +60,7 @@ Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat
 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.
 
 * Usage
-Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. Entering ":t <ident>" prints the type of a particular identifier, while ":v <ident>" prints its value. Entering ":n <expr>" will fully normalize (including unfolding definitions) an expression, while ":w <expr>" will reduce it to weak head normal form. Finally ":l <filepath>" loads a file.
+Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. If you want to see the value of an identifier defined in the environment, you can enter ":v <ident>". Entering ":t <expr>" prints the type of an expression. Entering ":n <expr>" will fully normalize (including unfolding definitions) an expression, while ":w <expr>" will reduce it to weak head normal form. Finally ":l <filepath>" loads a file.
 
 Here's an example session showing the capabilities of the repl.
 #+begin_src text
@@ -160,7 +161,7 @@ This indicates that, when evaluating =Hxy Hx=, it was expecting something of typ
 ** Substantive
 
 *** TODO Sections
-Coq-style sections would be very handy, and probably /relatively/ easy to implement (compared to everything else on this todo list). Upon parsing a definition inside a section, will somehow need to look ahead to see what variables are used to see how I need to modify =binders=, or just make every definition require every section variable as an argument.
+Coq-style sections would be very handy, and probably /relatively/ easy to implement (compared to everything else on this todo list), especially now that we have an [[Multiple levels of AST][intermediate representation]].
 
 *** TODO Inference
 Not decidable, but I might be able to implement some basic unification algorithm, or switch to bidirectional type checking. This isn't super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be handy, especially not at the top level.
@@ -169,7 +170,7 @@ Not decidable, but I might be able to implement some basic unification algorithm
 Much, much more useful than [[Inference][inference]], implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
 
 *** TODO Module System
-A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of =and='s like I currently have; especially painful without [[Implicits][implicits]]) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [[https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf][F-ing modules]] paper is probably a good reference.
+A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of =and='s like I currently have; especially painful without [[Implicits][implicits]]) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [[https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf][F-ing modules]] paper is probably a good reference. Now that I have an [[Multiple levels of AST][intermediate representation]], following in /F-ing modules/'s footsteps and implementing modules purely through elaboration should be possible.
 
 *** DONE Universes?
 Not super necessary, but occasionally extremely useful. Could be fun, idk.
@@ -178,6 +179,8 @@ I was looking into bidirectional typing and came across a description of univers
 
 Also, everything ends up impredicative (no =* : *=, but quantifying over =*i= still leaves you in =*i=), and my implementation of impredicativity feels a little sketchy. There might be paradoxes lurking. It would be easy to switch it over to being predicative, but, without inductive types or at least more built-in types, logical connectives can only be defined impredicatively, so that will have to wait until we have inductive definitions.
 
+I may follow in Coq's footsteps and switch universe hierarchies to something like =* : □ : □₁ : □₂ : □₃ : ...=, where all the =□ᵢ= are predicative and =*= is impredicative (analogous to =Prop= and =Type i=). For now at least, we definitely need at least the lowest sort to be impredicative to allow for impredicative definitions of connectives.
+
 *** TODO Universe polymorphism
 I have [[Universes?][universes]], but without universe polymorphism, they're basically useless, or at least I am unable to find a practical use for them. (When would you want to quantify over e.g. kinds specifically?)
 
@@ -204,8 +207,8 @@ Probably a smart idea.
 *** TODO More incremental parsing/typechecking
 Right now, if there's a failure, everything just stops immediately. More incremental parsing/typechecking could pave the way for more interactivity, e.g. development with holes, an LSP server, etc., not to mention better error messages.
 
-*** TODO Multiple levels of AST
+*** DONE Multiple levels of AST
-Right now, the parsing and typechecking kind of happens all at once on a single syntax representation. As I add fancier and fancier elaboration, it might be a good idea to have multiple syntax representations. So we'd have one level of syntax representing what is actually in the file (modulo some easy elaboration like with function definitions), and through a series of transformations transform it into something like the current =Expr= type with all the information needed for typechecking and all the complex language features removed.
+Added a couple types representing an intermediate representation, as well as a module responsible for elaboration (basically a function from these intermediate types to =Expr=). This /drastically/ simplified the parser, now that it is not responsible for converting to de Bruijn indices, handling the environment, and type checking all in addition to parsing. However, now that type checking is out of the parser, we lost location information for errors, making [[Improve error message][better error messages]] much more important now. I have some ideas for getting location information (and more accurate location information, instead of always pointing to the end of the most relevant definition), which should drastically improve the error messages.
 
 *** TODO Improve type checking algorithm
 I'm proud that I just kinda made up a working type checking algorithm, but it is clearly quite flawed. Even assuming no need to check beta equivalence, I'm pretty sure that this algorithm is approximately exponential in the length of a term, which is pretty terrible. It hasn't been a huge problem, but type checking just the term =R2_sub_R= in [[./examples/peano.pg]] takes about 1.5 seconds. Performance could easily be drastically improved with some memoization, but upgrading to an off-the-shelf bidirectional type checking algorithm seems like a good idea in general. Another problem with my current type checking algorithm is that it is very inflexible (e.g. adding optional return type ascriptions in functions, or type ascriptions in =let= bindings is currently impossible, while trivial to add with bidirectional type checking). I also have no idea how to add [[Inference][type inference]] or [[Implicits][implicits]] with how things are currently structured. A more flexible type checking algorithm, likely together with [[Multiple levels of AST][multiple levels of AST]], makes it seem more possible.

app/Main.hs

@@ -1,7 +1,7 @@
 module Main where
 
-import Eval (Env, emptyEnv)
+import qualified Data.Map.Strict as M
-import Parser (handleFile)
+import Program (handleAndParseFile)
 import Repl
 
 main :: IO ()
@@ -9,8 +9,8 @@ main = do
     args <- getArgs
     case args of
         [] -> void repl
-        files -> handleFiles emptyEnv files
+        files -> handleFiles files
 
-handleFiles :: Env -> [String] -> IO ()
+handleFiles :: [String] -> IO ()
-handleFiles _ [] = putTextLn "success!"
+handleFiles [] = putTextLn "success!"
-handleFiles env (file : rest) = runExceptT (handleFile env file) >>= either putStrLn (`handleFiles` rest)
+handleFiles (file : rest) = runExceptT (handleAndParseFile M.empty file) >>= either putStrLn (const $ handleFiles rest)

app/Repl.hs

@@ -4,10 +4,12 @@ import Check (findType)
 import Data.List (stripPrefix)
 import qualified Data.Map.Strict as M
 import Data.Text (pack)
+import Elaborator
 import Errors (Result)
 import Eval
 import Expr
 import Parser
+import Program
 import System.Console.Haskeline
 import System.Directory (createDirectoryIfMissing, getHomeDirectory)
 import System.FilePath ((</>))
@@ -37,21 +39,22 @@ parseCommand (Just input)
 
 handleInput :: Env -> String -> InputT IO Env
 handleInput env input =
-    let (res, env') = parseDefEmpty env (pack input)
+    case parseDef "repl" (pack input) of
-     in case res of
+        Left err -> outputStrLn err >> pure env
-            Left err -> outputStrLn err >> pure env'
+        Right irDef -> case evalDef env irDef of
-            Right () -> pure env'
+            Left err -> outputStrLn (toString err) >> pure env
+            Right env' -> pure env'
 
-actOnParse :: Env -> String -> (Expr -> InputT IO ()) -> InputT IO ()
+actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
-actOnParse env input action = case parseExpr env (pack input) of
+actOnParse input action = case parseExpr "repl" (pack input) of
     Left err -> outputStrLn err
-    Right expr -> action expr
+    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
 
 parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO ()
-parseActPrint env input action = actOnParse env input (printErrorOrResult env action)
+parseActPrint env input action = actOnParse input (printErrorOrResult env action)
 
 lookupAct :: Env -> String -> (Definition -> InputT IO ()) -> InputT IO ()
 lookupAct env input action = maybe (outputStrLn $ "'" ++ input ++ "' unbound") action $ M.lookup (pack input) env
@@ -75,5 +78,5 @@ 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 (LoadFile filename) -> lift (runExceptT $ handleFile env filename) >>= either ((>> loop env) . outputStrLn) loop
+            Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile env filename) >>= either ((>> loop env) . outputStrLn) loop
             Just (Input input) -> handleInput env input >>= loop

examples/algebra.pg

@@ -13,64 +13,64 @@
 -- I'd always strongly recommend including the type ascriptions for theorems
 
 -- a unary operation on a set `A` is a function `A -> A`
-unop (A : *) := A -> A;
+def unop (A : *) := A -> A;
 
 -- a binary operation on a set `A` is a function `A -> A -> A`
-binop (A : *) := A -> A -> A;
+def binop (A : *) := A -> A -> A;
 
 -- a binary operation is associative if ...
-assoc (A : *) (op : binop A) :=
+def assoc (A : *) (op : binop A) :=
     forall (a b c : A), eq A (op a (op b c)) (op (op a b) c);
 
 -- an element `e : A` is a left identity with respect to binop `op` if `∀ a, e * a = a`
-id_l (A : *) (op : binop A) (e : A) :=
+def id_l (A : *) (op : binop A) (e : A) :=
     forall (a : A), eq A (op e a) a;
 
 -- likewise for right identity
-id_r (A : *) (op : binop A) (e : A) :=
+def id_r (A : *) (op : binop A) (e : A) :=
     forall (a : A), eq A (op a e) a;
 
 -- an element is an identity element if it is both a left and right identity
-id (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e);
+def id (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e);
 
 -- b is a left inverse for a if `b * a = e`
 -- NOTE: we don't require `e` to be an identity in this definition.
 --       this definition is purely for convenience's sake
-inv_l (A : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e;
+def inv_l (A : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e;
 
 -- likewise for right inverse
-inv_r (A : *) (op : binop A) (e : A) (a b : A) := eq A (op a b) e;
+def inv_r (A : *) (op : binop A) (e : A) (a b : A) := eq A (op a b) e;
 
 -- and full-on inverse
-inv (A : *) (op : binop A) (e : A) (a b : A) := and (inv_l A op e a b) (inv_r A op e a b);
+def inv (A : *) (op : binop A) (e : A) (a b : A) := and (inv_l A op e a b) (inv_r A op e a b);
 
 -- --------------------------------------------------------------------------------------------------------------
 -- |                                      ALGEBRAIC STRUCTURES                                                  |
 -- --------------------------------------------------------------------------------------------------------------
 
 -- a set `S` with binary operation `op` is a semigroup if its operation is associative
-semigroup (S : *) (op : binop S) : * := assoc S op;
+def semigroup (S : *) (op : binop S) : * := assoc S op;
 
 -- a set `M` with binary operation `op` and element `e` is a monoid 
-monoid (M : *) (op : binop M) (e : M) : * :=
+def monoid (M : *) (op : binop M) (e : M) : * :=
     and (semigroup M op) (id M op e);
 
 -- some "getters" for `monoid` so we don't have to do a bunch of very verbose
 -- and-eliminations every time we want to use something
-id_lm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_l M op e :=
+def id_lm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_l M op e :=
     and_elim_l (id_l M op e) (id_r M op e)
         (and_elim_r (semigroup M op) (id M op e) Hmonoid);
 
-id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_r M op e :=
+def id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_r M op e :=
     and_elim_r (id_l M op e) (id_r M op e)
         (and_elim_r (semigroup M op) (id M op e) Hmonoid);
 
-assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : assoc M op :=
+def assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : assoc M op :=
     and_elim_l (semigroup M op) (id M op e) Hmonoid;
 
 -- now we can prove that, for any monoid, if `a` is a left identity, then it
 -- must be "the" identity
-monoid_id_l_implies_identity
+def monoid_id_l_implies_identity
     (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e)
     (a : M) (H : id_l M op a) : eq M a e :=
         -- WTS a = a * e = e
@@ -86,7 +86,7 @@ monoid_id_l_implies_identity
             (H e);
 
 -- the analogous result for right identities
-monoid_id_r_implies_identity
+def monoid_id_r_implies_identity
     (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e)
     (a : M) (H : id_r M op a) : eq M a e :=
         -- this time, we'll show `a = e * a = e`
@@ -102,36 +102,36 @@ monoid_id_r_implies_identity
   
 
 -- groups are just monoids with inverses
-has_inverses (G : *) (op : binop G) (e : G) (i : unop G) : * :=
+def has_inverses (G : *) (op : binop G) (e : G) (i : unop G) : * :=
     forall (a : G), inv G op e a (i a);
 
-group (G : *) (op : binop G) (e : G) (i : unop G) : * :=
+def group (G : *) (op : binop G) (e : G) (i : unop G) : * :=
     and (monoid G op e)
         (has_inverses G op e i);
 
 -- more "getters"
-monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e :=
+def monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e :=
     and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup;
 
-assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op :=
+def assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op :=
     assoc_m G op e (monoid_g G op e i Hgroup);
 
-id_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_l G op e :=
+def id_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_l G op e :=
     id_lm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup);
 
-id_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_r G op e :=
+def id_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_r G op e :=
     id_rm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup);
 
-inv_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)  : forall (a : G), inv G op e a (i a) :=
+def inv_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)  : forall (a : G), inv G op e a (i a) :=
     and_elim_r (monoid G op e) (has_inverses G op e i) Hgroup;
 
-inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_l G op e a (i a) :=
+def inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_l G op e a (i a) :=
     and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);
 
-inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
+def inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
     and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);
 
-left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) :=
+def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) :=
     -- b = b * e
     --   = b * (a * a^-1)
     --   = (b * a) * a^-1

examples/classical.pg

@@ -2,23 +2,23 @@
 
 -- excluded middle!
 -- P ∨ ~P
-em (P : *) : or (P) (not P) := axiom;
+axiom em (P : *) : or P (not P);
 
 -- ~~P => P
-dne (P : *) (nnp : not (not P)) : P :=
+def dne (P : *) (nnp : not (not P)) : P :=
     or_elim P (not P) P (em P)
         (fun (p : P) => p)
         (fun (np : not P) => nnp np P);
 
 -- ((P => Q) => P) => P
-peirce (P Q : *) (h : (P -> Q) -> P) : P :=
+def peirce (P Q : *) (h : (P -> Q) -> P) : P :=
     or_elim P (not P) P (em P)
         (fun (p : P) => p)
         (fun (np : not P) => h (fun (p : P) => np p Q));
 
 
 -- ~(A ∧ B) => ~A ∨ ~B
-de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
+def de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
     or_elim A (not A) (or (not A) (not B)) (em A)
         (fun (a : A) =>
             or_elim B (not B) (or (not A) (not B)) (em B)

examples/computation.pg

@@ -1,22 +1,24 @@
+@include logic.pg
+
 -- without recursion, computation is kind of hard
 -- we can, however, define natural numbers using the Church encoding and do
 -- computation with them
 
 -- the natural number `n` is encoded as the function taking any function
 -- `A -> A` and repeating it `n` times
-nat : * := forall (A : *), (A -> A) -> A -> A;
+def nat : * := forall (A : *), (A -> A) -> A -> A;
 
 -- zero is the constant function
-zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
+def zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
 
 -- `suc n` composes one more `f` than `n`
-suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
+def suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
 
 -- addition can be encoded as usual
-plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
+def plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
 
 -- likewise for multiplication
-times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
+def times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
 
 -- unforunately, it is impossible to prove induction on Church numerals,
 -- which makes it really hard to prove standard theorems, or do anything really.
@@ -24,16 +26,16 @@ times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m
 -- but we can still do computations with Church numerals
 
 -- first some abbreviations for numbers will be handy
-one   : nat := suc zero;
+def one   : nat := suc zero;
-two   : nat := suc one;
+def two   : nat := suc one;
-three : nat := suc two;
+def three : nat := suc two;
-four  : nat := suc three;
+def four  : nat := suc three;
-five  : nat := suc four;
+def five  : nat := suc four;
-six   : nat := suc five;
+def six   : nat := suc five;
-seven : nat := suc six;
+def seven : nat := suc six;
-eight : nat := suc seven;
+def eight : nat := suc seven;
-nine  : nat := suc eight;
+def nine  : nat := suc eight;
-ten   : nat := suc nine;
+def ten   : nat := suc nine;
 
 -- now we can do a bunch of computations, even at the type level
 -- the way we can do this is by defining equality (see <examples/logic.pg> for
@@ -42,23 +44,12 @@ ten   : nat := suc nine;
 -- then perga will only accept our proof if `plus one one` and `two` are beta
 -- equivalent
 
--- first we do need a definition of equality
-eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
-eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
-eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
-    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
-eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
-    Hyz P (Hxy P Hx);
-eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
-  fun (P : B -> *) (Hfx : P (f x)) =>
-      H (fun (a : A) => P (f a)) Hfx;
-
 -- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
 -- proof that `1 + 1 = 2`
-one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
+def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
 
 -- we can likewise compute 2 + 2
-two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
+def two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
 
 -- even multiplication works
-two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;
+def two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;

examples/logic.pg

@@ -1,44 +1,44 @@
 -- False
 
-false : * := forall (A : *), A;
+def false : * := forall (A : *), A;
 
 -- no introduction rule
 
 -- elimination rule
-false_elim (A : *) (contra : false) : A := contra A;
+def false_elim (A : *) (contra : false) : A := contra A;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Negation
 
-not (A : *) : * := A -> false;
+def not (A : *) : * := A -> false;
 
 -- introduction rule (kinda just the definition)
-not_intro (A : *) (h : A -> false) : not A := h;
+def not_intro (A : *) (h : A -> false) : not A := h;
 
 -- elimination rule
-not_elim (A B : *) (a : A) (na : not A) : B := na a B;
+def not_elim (A B : *) (a : A) (na : not A) : B := na a B;
 
 -- can introduce double negation (can't eliminate it as that isn't constructive)
-double_neg_intro (A : *) (a : A) : not (not A) :=
+def double_neg_intro (A : *) (a : A) : not (not A) :=
     fun (notA : not A) => notA a;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Conjunction
 
-and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
+def and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
 
 -- introduction rule
-and_intro (A B : *) (a : A) (b : B) : and A B :=
+def and_intro (A B : *) (a : A) (b : B) : and A B :=
     fun (C : *) (H : A -> B -> C) => H a b;
 
 -- left elimination rule
-and_elim_l (A B : *) (ab : and A B) : A :=
+def and_elim_l (A B : *) (ab : and A B) : A :=
     ab A (fun (a : A) (b : B) => a);
 
 -- right elimination rule
-and_elim_r (A B : *) (ab : and A B) : B :=
+def and_elim_r (A B : *) (ab : and A B) : B :=
     ab B (fun (a : A) (b : B) => b);
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -46,18 +46,18 @@ and_elim_r (A B : *) (ab : and A B) : B :=
 -- Disjunction
 
 -- 2nd order disjunction
-or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
+def or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
 
 -- left introduction rule
-or_intro_l (A B : *) (a : A) : or A B :=
+def or_intro_l (A B : *) (a : A) : or A B :=
     fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
 
 -- right introduction rule
-or_intro_r (A B : *) (b : B) : or A B :=
+def or_intro_r (A B : *) (b : B) : or A B :=
     fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
 
 -- elimination rule (kinda just the definition)
-or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
+def or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
     ab C ha hb;
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -65,14 +65,14 @@ or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
 -- Existential
 
 -- 2nd order existential
-exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
+def exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
 
 -- introduction rule
-exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
+def exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
     fun (C : *) (g : forall (x : A), P x -> C) => g a h;
 
 -- elimination rule (kinda just the definition)
-exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
+def exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
     ex_a B h;
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -80,34 +80,34 @@ exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a
 -- Universal
 
 -- 2nd order universal (just ∏, including it for completeness)
-all (A : *) (P : A -> *) : * := forall (a : A), P a;
+def all (A : *) (P : A -> *) : * := forall (a : A), P a;
 
 -- introduction rule
-all_intro (A : *) (P : A -> *) (h : forall (a : A), P a) : all A P := h;
+def all_intro (A : *) (P : A -> *) (h : forall (a : A), P a) : all A P := h;
 
 -- elimination rule
-all_elim (A : *) (P : A -> *) (h_all : all A P) (a : A) : P a := h_all a;
+def all_elim (A : *) (P : A -> *) (h_all : all A P) (a : A) : P a := h_all a;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Equality
 
 -- 2nd order Leibniz equality
-eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
 
 -- equality is reflexive
-eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
 
 -- equality is symmetric
-eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
+def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
     Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
 
 -- equality is transitive
-eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
+def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
     Hyz P (Hxy P Hx);
 
 -- equality is a universal congruence
-eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
   fun (P : B -> *) (Hfx : P (f x)) =>
       H (fun (a : A) => P (f a)) Hfx;
 
@@ -116,20 +116,20 @@ eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
 -- Some logic theorems
 
 -- ~(A ∨ B) => ~A ∧ ~B
-de_morgan1 (A B : *) (h : not (or A B)) : and (not A) (not B) :=
+def de_morgan1 (A B : *) (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)
-de_morgan2 (A B : *) (h : and (not A) (not B)) : not (or A B) :=
+def de_morgan2 (A B : *) (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)
-de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
+def de_morgan3 (A B : *) (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 +138,19 @@ 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
-and_comm (A B : *) (h : and A B) : and B A :=
+def and_comm (A B : *) (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
-or_comm (A B : *) (h : or A B) : or B A :=
+def or_comm (A B : *) (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
-and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
+def and_assoc_l (A B C : *) (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 +160,7 @@ and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
     end;
 
 -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
-and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
+def and_assoc_r (A B C : *) (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 +170,7 @@ and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
     end;
 
 -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
-or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
+def or_assoc_l (A B C : *) (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 +179,7 @@ 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)
-or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
+def or_assoc_r (A B C : *) (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 +188,7 @@ 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
-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 (A B C : *) (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 +196,7 @@ 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)
-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 (A B C : *) (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 +207,9 @@ 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
-disj_syllog (A B : *) (nb : not B) (hor : or A B) : A :=
+def disj_syllog (A B : *) (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
-contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
+def contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
     fun (a : A) => nb (f a);

examples/peano.pg

@@ -5,7 +5,7 @@
 @include logic.pg
 @include algebra.pg
 
-comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
+def comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
   g (f x);
 
 -- }}}
@@ -24,7 +24,7 @@ comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
 -- defined is a value of the asserted type. For example, we will use the axiom
 -- system to assert the existence of a type of natural numbers
 
-nat : * := axiom;
+axiom nat : *;
 
 -- As you can imagine, this can be risky. For instance, there's nothing stopping
 -- us from saying
@@ -47,21 +47,21 @@ nat : * := axiom;
 -- (https://en.wikipedia.org/wiki/Peano_axioms).
 
 -- axiom 1: 0 is a natural number
-zero : nat := axiom;
+axiom zero : nat;
 
 -- axiom 6: For every n, S n is a natural number.
-suc (n : nat) : nat := axiom;
+axiom suc (n : nat) : nat;
 
 -- axiom 7: If S n = S m, then n = m.
-suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m := axiom;
+axiom suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m;
 
 -- axiom 8: No successor of any natural number is zero.
-suc_nonzero : forall (n : nat), not (eq nat (suc n) zero) := axiom;
+axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);
 
 -- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
 -- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
-nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
+axiom nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
-    -> forall (n : nat), P n := axiom;
+    -> forall (n : nat), P n;
 
 -- }}}
 
@@ -77,27 +77,27 @@ nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
 -- long and complicated really quickly.
 
 -- Some abbreviations for common numbers.
-one   : nat := suc zero;
+def one   : nat := suc zero;
-two   : nat := suc one;
+def two   : nat := suc one;
-three : nat := suc two;
+def three : nat := suc two;
-four  : nat := suc three;
+def four  : nat := suc three;
-five  : nat := suc four;
+def five  : nat := suc four;
 
 -- First, the predecessor of n is m if n = suc m.
-pred (n m : nat) : * := eq nat n (suc m);
+def pred (n m : nat) : * := eq nat n (suc m);
 
 -- Our claim is a disjunction, whose first option is that n = 0.
-szc_l (n : nat) := eq nat n zero;
+def szc_l (n : nat) := eq nat n zero;
 
 -- The second option is that n has a predecessor.
-szc_r (n : nat) := exists nat (pred n);
+def szc_r (n : nat) := exists nat (pred n);
 
 -- So the claim we are trying to prove is that either one of the above options
 -- holds for every n.
-szc (n : nat) := or (szc_l n) (szc_r n);
+def szc (n : nat) := or (szc_l n) (szc_r n);
 
 -- And here's our proof!
-suc_or_zero : forall (n : nat), szc n :=
+def suc_or_zero : forall (n : nat), szc n :=
     -- We will prove this by induction.
     nat_ind szc
         -- For the base case, the first option holds, i.e. 0 = 0
@@ -157,30 +157,30 @@ suc_or_zero : forall (n : nat), szc n :=
 
 -- {{{ Defining R
 -- Here is condition 1 formally expressed in perga.
-cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
     Q zero z;
 
 -- Likewise for condition 2.
-cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
     forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
 
 -- From here we can define R.
-rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
     forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
 -- }}}
 
 -- {{{ R is total
-total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
+def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
 
-rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
+def rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
     fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;
 
-rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
+def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
     fun (n : nat) (y : A) (h : rec_rel A z fS n y)
         (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
         h2 n y (h Q h1 h2);
 
-rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
+def rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
     let (R := rec_rel A z fS)
         (P (x : nat) := exists A (R x))
         (c1 := cond1 A z fS)
@@ -196,27 +196,27 @@ rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS
 -- }}}
 
 -- {{{ Defining R2
-alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
+def alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
     and (eq nat x zero) (eq A y z);
 
-cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
+def cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
     (x2 : nat) (y2 : A) :=
         and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);
 
-cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
+def cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
     and (pred x x2) (exists A (cond_y2 A z fS x y x2));
 
-alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
     exists nat (cond_x2 A z fS x y);
 
-rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
     or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
 -- }}}
 
 -- {{{ R = R2
 
 -- {{{ R2 ⊆ R
-R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
     rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
     let (R := rec_rel A z fS)
         (R2 := rec_rel_alt A z fS)
@@ -257,13 +257,13 @@ R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
 -- }}}
 
 -- {{{ R ⊆ R2
-R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
+def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
     or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
     (and_intro (eq nat zero zero) (eq A z z)
         (eq_refl nat zero)
         (eq_refl A z));
 
-R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
+def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
     let (R := rec_rel A z fS)
         (R2 := rec_rel_alt A z fS)
     in
@@ -284,7 +284,7 @@ R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS
         end
     end;
 
-R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+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 :=
     let (R := rec_rel A z fS)
         (R2 := rec_rel_alt A z fS)
@@ -298,12 +298,12 @@ R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
 
 -- {{{ R2 (hence R) is functional
 
-fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
+def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
     R x y1 -> R x y2 -> eq B y1 y2;
 
-fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
+def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
 
-R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
+def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
     rec_rel_alt A z fS zero y -> eq A y z :=
     let (R2 := rec_rel_alt A z fS)
         (ac1 := alt_cond1 A z zero y)
@@ -321,7 +321,7 @@ R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
                 (eq A y z)))
     end;
 
-R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
+def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
     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 A z fS)
         (x := suc x2)
@@ -347,7 +347,7 @@ R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
                 end))
     end;
 
-R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
+def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
     let (R := rec_rel A z fS)
         (R2 := rec_rel_alt A z fS)
         (f_in := fl_in nat A R2)
@@ -385,7 +385,7 @@ R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z f
 
 -- }}}
 
-rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
+def rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
     exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
         (fun (y : A) (_ : rec_rel A z fS x y) => y);
 

lib/Check.hs

@@ -49,7 +49,12 @@ findType g (Pi _ a b) = do
     i <- findLevel g a
     j <- findLevel (incIndices a : map incIndices g) b
     pure $ Level $ max (i - 1) j -- This feels very sketchy, but certainly adds impredicativity
-findType g (Let _ v b) = findType g (subst 0 v b)
+findType g (Let _ Nothing v b) = findType g (subst 0 v b)
+findType g e@(Let _ (Just t) v b) = do
+    res <- findType g (subst 0 v b)
+    equiv <- betaEquiv t res
+    unless equiv $ throwError $ NotEquivalent t res e
+    pure t
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env

lib/Elaborator.hs

@@ -0,0 +1,43 @@
+module Elaborator where
+
+import Data.List (elemIndex)
+import Expr (Expr)
+import qualified Expr as E
+import IR (IRExpr)
+import qualified IR as I
+
+type Binders = [Text]
+
+saveBinders :: State Binders a -> State Binders a
+saveBinders action = do
+    binders <- get
+    res <- action
+    put binders
+    pure res
+
+elaborate :: IRExpr -> Expr
+elaborate ir = evalState (elaborate' ir) []
+  where
+    elaborate' :: IRExpr -> State Binders Expr
+    elaborate' (I.Var n) = do
+        binders <- get
+        pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+    elaborate' (I.Level level) = pure $ E.Level level
+    elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
+    elaborate' (I.Abs x t b) = saveBinders $ do
+        t' <- elaborate' t
+        modify (x :)
+        E.Abs x t' <$> elaborate' b
+    elaborate' (I.Pi x t b) = saveBinders $ do
+        t' <- elaborate' t
+        modify (x :)
+        E.Pi x t' <$> elaborate' b
+    elaborate' (I.Let name Nothing val body) = saveBinders $ do
+        val' <- elaborate' val
+        modify (name :)
+        E.Let name Nothing val' <$> elaborate' body
+    elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
+        val' <- elaborate' val
+        ty' <- elaborate' ty
+        modify (name :)
+        E.Let name (Just ty') val' <$> elaborate' body

lib/Eval.hs

@@ -10,9 +10,6 @@ import Relude.Extra.Lens
 
 data Definition = Def {_ty :: Expr, _val :: Expr}
 
-makeDef :: Expr -> Expr -> Definition
-makeDef typ value = Def{_ty = typ, _val = value}
-
 tyL :: Lens' Definition Expr
 tyL = lens _ty setter
   where
@@ -46,7 +43,7 @@ subst _ _ (Level i) = Level i
 subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
-subst k s (Let x v b) = Let x (subst k s v) (subst (k + 1) (incIndices s) b)
+subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
 
 envLookupVal :: Text -> ReaderT Env Result Expr
 envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
@@ -63,7 +60,7 @@ whnf (App m n) = do
         then pure $ App m n
         else whnf $ App m' n
 whnf (Free n) = envLookupVal n >>= whnf
-whnf (Let _ v b) = whnf $ subst 0 v b
+whnf (Let _ _ v b) = whnf $ subst 0 v b
 whnf e = pure e
 
 reduce :: Expr -> ReaderT Env Result Expr
@@ -72,7 +69,7 @@ reduce (App m n) = App <$> reduce m <*> reduce n
 reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
-reduce (Let _ v b) = pure $ subst 0 v b
+reduce (Let _ _ v b) = pure $ subst 0 v b
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -91,19 +88,22 @@ betaEquiv e1 e2
         case (e1', e2') of
             (Var k1 _, Var k2 _) -> pure $ k1 == k2
             (Free n, Free m) -> pure $ n == m
-            (Axiom n, Axiom m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
+            (Axiom n, Axiom m) -> pure $ n == m
             (Level i, Level j) -> pure $ i == j
             (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
-            (Let _ v b, e) -> betaEquiv (subst 0 v b) e
+            (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
-            (e, Let _ v b) -> betaEquiv (subst 0 v b) e
+            (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible or false
 
-checkBeta :: Env -> Expr -> Expr -> Result Bool
+checkBeta :: Env -> Expr -> Expr -> Expr -> Result ()
-checkBeta env e1 e2 = runReaderT (betaEquiv e1 e2) env
+checkBeta env e1 e2 ctxt = case runReaderT (betaEquiv e1 e2) env of
+    Left err -> Left err
+    Right False -> Left $ NotEquivalent e1 e2 ctxt
+    Right True -> Right ()
 
 isSortPure :: Expr -> Bool
 isSortPure (Level _) = True

lib/Expr.hs

@@ -8,18 +8,18 @@ data Expr where
     App :: Expr -> Expr -> Expr
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
-    Let :: Text -> Expr -> Expr -> Expr
+    Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
     deriving (Show, Ord)
 
 instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
     (Free s) == (Free t) = s == t
-    (Axiom a) == (Axiom b) = a == b
+    (Axiom s) == (Axiom t) = s == t
     (Level i) == (Level j) = i == j
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
-    (Let _ v1 b1) == (Let _ v2 b2) = v1 == v2 && b1 == b2
+    (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
     _ == _ = False
 
 occursFree :: Integer -> Expr -> Bool
@@ -30,7 +30,7 @@ occursFree _ (Level _) = False
 occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
-occursFree n (Let _ v b) = occursFree n v || occursFree (n + 1) b
+occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
 
 shiftIndices :: Integer -> Integer -> Expr -> Expr
 shiftIndices d c (Var x k)
@@ -42,7 +42,7 @@ shiftIndices _ _ (Level i) = Level i
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
-shiftIndices d c (Let x v b) = Let x (shiftIndices d c v) (shiftIndices d (c + 1) b)
+shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
 
 incIndices :: Expr -> Expr
 incIndices = shiftIndices 1 0
@@ -63,7 +63,7 @@ collectLambdas (Abs x ty body) = ((x, ty) : params, final)
 collectLambdas e = ([], e)
 
 collectLets :: Expr -> ([Binding], Expr)
-collectLets (Let x val body) = ((x, params', val') : bindings, final)
+collectLets (Let x _ val body) = ((x, params', val') : bindings, final)
   where
     (bindings, final) = collectLets body
     (params, val') = collectLambdas val

lib/IR.hs

@@ -0,0 +1,41 @@
+module IR where
+
+type Param = (Text, IRExpr)
+
+data IRExpr
+    = Var {varName :: Text}
+    | Level {level :: Integer}
+    | App
+        { appFunc :: IRExpr
+        , appArg :: IRExpr
+        }
+    | Abs
+        { absParamName :: Text
+        , absParamType :: IRExpr
+        , absBody :: IRExpr
+        }
+    | Pi
+        { piParamName :: Text
+        , piParamType :: IRExpr
+        , piBody :: IRExpr
+        }
+    | Let
+        { letVarName :: Text
+        , letAscription :: Maybe IRExpr
+        , letValue :: IRExpr
+        , letBody :: IRExpr
+        }
+    deriving (Show, Eq, Ord)
+
+data IRDef
+    = Def
+        { defName :: Text
+        , defAscription :: Maybe IRExpr
+        , defBody :: IRExpr
+        }
+    | Axiom
+        { axiomName :: Text
+        , axiomAscription :: IRExpr
+        }
+
+type IRProgram = [IRDef]

lib/Parser.hs

@@ -1,37 +1,21 @@
-{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE TupleSections #-}
 
-module Parser (parseDef, parseDefEmpty, parseExpr, parseProgram, handleFile) where
+module Parser where
 
-import Check
 import Control.Monad.Except
-import Data.List (elemIndex, foldl, foldl1)
+import Data.List (foldl1)
-import qualified Data.Map.Strict as M
 import qualified Data.Text as T
 import Errors (Error (..))
-import Eval
+import IR
-import Expr (Expr (..), incIndices)
 import Preprocessor
-import Relude.Extra.Lens
+import Text.Megaparsec (Parsec, ShowErrorComponent (..), between, choice, chunk, errorBundlePretty, label, runParser, try)
-import Text.Megaparsec (ParsecT, ShowErrorComponent (..), between, choice, chunk, customFailure, errorBundlePretty, label, runParserT, try)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
-data InnerState = IS {_binders :: [Text], _env :: Env}
-
-bindsL :: Lens' InnerState [Text]
-bindsL = lens _binders setter
-  where
-    setter (IS{_env}) new = IS{_env, _binders = new}
-
-envL :: Lens' InnerState Env
-envL = lens _env setter
-  where
-    setter (IS{_binders}) new = IS{_env = new, _binders}
-
 newtype TypeError = TE Error
     deriving (Eq, Ord)
 
-type Parser = ParsecT TypeError Text (State InnerState)
+type Parser = Parsec TypeError Text
 
 instance ShowErrorComponent TypeError where
     showErrorComponent (TE e) = toString e
@@ -50,7 +34,10 @@ eat :: Text -> Parser ()
 eat = void . lexeme . chunk
 
 keywords :: [Text]
-keywords = ["forall", "let", "in", "end", "fun"]
+keywords = ["forall", "let", "in", "end", "fun", "def", "axiom"]
+
+reservedChars :: [Char]
+reservedChars = "();:"
 
 pIdentifier :: Parser Text
 pIdentifier = try $ label "identifier" $ lexeme $ do
@@ -62,178 +49,135 @@ pIdentifier = try $ label "identifier" $ lexeme $ do
             "Reserved word: " ++ T.unpack ident
     pure ident
 
-pVar :: Parser Expr
+pVar :: Parser IRExpr
-pVar = label "variable" $ lexeme $ do
+pVar = label "variable" $ lexeme $ Var <$> pIdentifier
-    name <- pIdentifier
-    binders <- view bindsL <$> get
-    pure $ Var name . fromIntegral <$> elemIndex name binders ?: Free name
 
 defChoice :: NonEmpty Text -> Parser ()
 defChoice options = lexeme $ label (T.unpack $ head options) $ void $ choice $ fmap chunk options
 
-pParamGroup :: Parser [(Text, Expr)]
+pParamGroup :: Parser [Param]
 pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
     idents <- some pIdentifier
     eat ":"
-    ty <- pExpr
+    ty <- pIRExpr
-    modify $ over bindsL $ flip (foldl $ flip (:)) idents
+    pure $ map (,ty) idents
-    pure $ zip idents (iterate incIndices ty)
 
-pSomeParams :: Parser [(Text, Expr)]
+pSomeParams :: Parser [Param]
 pSomeParams = lexeme $ concat <$> some pParamGroup
 
-pManyParams :: Parser [(Text, Expr)]
+pManyParams :: Parser [Param]
 pManyParams = lexeme $ concat <$> many pParamGroup
 
-withBinders :: Parser a -> Parser a
+pLAbs :: Parser IRExpr
-withBinders parser = do
+pLAbs = lexeme $ label "λ-abstraction" $ do
-    oldBinders <- view bindsL <$> get
-    result <- parser
-    modify $ set bindsL oldBinders
-    pure result
-
-pLAbs :: Parser Expr
-pLAbs = lexeme $ label "λ-abstraction" $ withBinders $ do
     _ <- defChoice $ "λ" :| ["fun"]
     params <- pSomeParams
     _ <- defChoice $ "=>" :| ["⇒"]
-    body <- pExpr
+    body <- pIRExpr
     pure $ foldr (uncurry Abs) body params
 
-pPAbs :: Parser Expr
+pPAbs :: Parser IRExpr
-pPAbs = lexeme $ label "Π-abstraction" $ withBinders $ do
+pPAbs = lexeme $ label "Π-abstraction" $ do
     _ <- defChoice $ "∏" :| ["forall", "∀"]
     params <- pSomeParams
     eat ","
-    body <- pExpr
+    body <- pIRExpr
     pure $ foldr (uncurry Pi) body params
 
-pBinding :: Parser (Text, Expr)
+pBinding :: Parser (Text, Maybe IRExpr, IRExpr)
 pBinding = lexeme $ label "binding" $ do
-    env <- get
     eat "("
     ident <- pIdentifier
     params <- pManyParams
+    ascription <- optional pAscription
     eat ":="
-    value <- pExpr
+    value <- pIRExpr
     eat ")"
-    put env
+    pure
-    modify $ over bindsL (ident :)
+        ( ident
-    pure (ident, foldr (uncurry Abs) value params)
+        , flip (foldr (uncurry Pi)) params <$> ascription
+        , foldr (uncurry Abs) value params
+        )
 
-pLet :: Parser Expr
+pLet :: Parser IRExpr
-pLet = lexeme $ label "let expression" $ withBinders $ do
+pLet = lexeme $ label "let expression" $ do
     eat "let"
     bindings <- some pBinding
     eat "in"
-    body <- try pExpr
+    body <- try pIRExpr
     eat "end"
-    pure $ foldr (uncurry Let) body bindings
+    pure $ foldr letTuple body bindings
+  where
+    letTuple :: (Text, Maybe IRExpr, IRExpr) -> IRExpr -> IRExpr
+    letTuple (name, ascription, value) = Let name ascription value
 
-pArrow :: Parser Expr
+pArrow :: Parser IRExpr
 pArrow = lexeme $ label "->" $ do
     a <- pAppTerm
     _ <- defChoice $ "->" :| ["→"]
-    Pi "" a . incIndices <$> pExpr
+    Pi "" a <$> pIRExpr
 
-pApp :: Parser Expr
+pApp :: Parser IRExpr
 pApp = lexeme $ foldl1 App <$> some pTerm
 
-pStar :: Parser Expr
+pStar :: Parser IRExpr
 pStar = lexeme $ Level 0 <$ eat "*"
 
-pNumSort :: Parser Expr
+pNumSort :: Parser IRExpr
 pNumSort = lexeme $ label "sort" $ eat "*" >> Level <$> L.decimal
 
-pSort :: Parser Expr
+pSort :: Parser IRExpr
-pSort = try pNumSort <|> pStar
+pSort = lexeme $ try pNumSort <|> pStar
 
-checkAscription :: Text -> Expr -> Maybe Expr -> Parser ()
+pAxiom :: Parser IRDef
-checkAscription ident value massert = do
+pAxiom = lexeme $ label "axiom" $ do
-    env <- get
-    ty <- either (customFailure . TE) pure (checkType (env ^. envL) value)
-    case massert of
-        Nothing -> updateStateDefinition ident ty value
-        Just assert -> do
-            equiv <- either (customFailure . TE) pure (checkBeta (env ^. envL) ty assert)
-            unless equiv $ customFailure $ TE $ NotEquivalent ty assert value
-            updateStateDefinition ident assert value
-
-updateStateDefinition :: Text -> Expr -> Expr -> Parser ()
-updateStateDefinition ident ty value = do
-    env <- get
-    when (M.member ident (env ^. envL)) (customFailure $ TE $ DuplicateDefinition ident)
-    modify $ over envL $ M.insert ident $ makeDef ty value
-
-pAxiom :: Text -> Maybe Expr -> Parser ()
-pAxiom ident Nothing = customFailure $ TE $ PNMissingType ident
-pAxiom ident (Just ascription) = do
     eat "axiom"
-    eat ";"
-    updateStateDefinition ident ascription (Axiom ident)
-
-pBody :: [(Text, Expr)] -> Text -> Maybe Expr -> Parser ()
-pBody params ident ascription = do
-    value <- flip (foldr (uncurry Abs)) params <$> pExpr
-    checkAscription ident value ascription
-    eat ";"
-
-pDef :: Parser ()
-pDef = lexeme $ label "definition" $ withBinders $ do
-    skipSpace
     ident <- pIdentifier
     params <- pManyParams
-    ascription <- fmap (flip (foldr (uncurry Pi)) params) <$> pAscription
+    ascription <- fmap (flip (foldr (uncurry Pi)) 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 (uncurry Pi)) params) <$> optional pAscription
     eat ":="
-    choice [pAxiom ident ascription, pBody params ident ascription]
+    body <- pIRExpr
+    eat ";"
+    pure $ Def ident ascription $ foldr (uncurry Abs) body params
 
-pTerm :: Parser Expr
+pIRDef :: Parser IRDef
-pTerm =
+pIRDef = pAxiom <|> pDef
-    lexeme $
-        label "term" $
-            choice
-                [ between (char '(') (char ')') pExpr
-                , pSort
-                , pVar
-                ]
 
-pAppTerm :: Parser Expr
+pTerm :: Parser IRExpr
-pAppTerm =
+pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
-    lexeme $
-        choice
-            [ pLAbs
-            , pPAbs
-            , pLet
-            , pApp
-            ]
 
-pExpr :: Parser Expr
+pAppTerm :: Parser IRExpr
-pExpr = lexeme $ try pArrow <|> pAppTerm
+pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
 
-pAscription :: Parser (Maybe Expr)
+pIRExpr :: Parser IRExpr
-pAscription = lexeme $ optional $ try $ defChoice (pure ":") >> label "type" pExpr
+pIRExpr = lexeme $ try pArrow <|> pAppTerm
 
-pProgram :: Parser Env
+pAscription :: Parser IRExpr
-pProgram = lexeme $ skipSpace >> many pDef >> _env <$> get
+pAscription = lexeme $ try $ eat ":" >> label "type" pIRExpr
 
-emptyBinders :: Env -> InnerState
+pIRProgram :: Parser IRProgram
-emptyBinders env = IS{_binders = [], _env = env}
+pIRProgram = skipSpace >> some pIRDef
 
-parseDef :: Text -> State Env (Either String ())
+parserWrapper :: Parser a -> String -> Text -> Either String a
-parseDef input = do
+parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
-    env <- get
-    let (output, IS{_env}) = runState (runParserT pDef "" input) (emptyBinders env)
-    put _env
-    pure $ first errorBundlePretty output
 
-parseExpr :: Env -> Text -> Either String Expr
+parseProgram :: String -> Text -> Either String IRProgram
-parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) $ emptyBinders env
+parseProgram = parserWrapper pIRProgram
 
-parseDefEmpty :: Env -> Text -> (Either String (), Env)
+parseDef :: String -> Text -> Either String IRDef
-parseDefEmpty env input = runState (parseDef input) env
+parseDef = parserWrapper pIRDef
 
-parseProgram :: Env -> Text -> Either String Env
+parseExpr :: String -> Text -> Either String IRExpr
-parseProgram initial input = first errorBundlePretty $ evalState (runParserT pProgram "" input) $ emptyBinders initial
+parseExpr = parserWrapper pIRExpr
 
-handleFile :: Env -> String -> ExceptT String IO Env
+handleFile :: String -> ExceptT String IO IRProgram
-handleFile initial filename = (toString `withExceptT` runPreprocessor filename) >>= liftEither . parseProgram initial
+handleFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . parseProgram filename

lib/Program.hs

@@ -0,0 +1,49 @@
+module Program where
+
+import Check
+import Control.Monad.Except
+import qualified Data.Map.Strict as M
+import Elaborator
+import Errors
+import Eval (Env, checkBeta)
+import qualified Eval
+import Expr (Expr)
+import qualified Expr
+import IR
+import Parser (parseProgram)
+import Preprocessor (runPreprocessor)
+
+insertDef :: Text -> Expr -> Expr -> Env -> Env
+insertDef name ty body = M.insert name (Eval.Def ty body)
+
+handleDef :: IRDef -> StateT Env Result ()
+handleDef (Axiom name ty) = do
+    env <- get
+    _ <- liftEither $ checkType env $ elaborate ty
+    modify $ insertDef name (elaborate ty) (Expr.Axiom name)
+handleDef (Def name Nothing irBody) = do
+    env <- get
+    ty <- liftEither $ checkType env body
+    modify $ insertDef name ty body
+  where
+    body = elaborate irBody
+handleDef (Def name (Just irTy) irBody) = do
+    env <- get
+    ty' <- liftEither $ checkType env body
+    liftEither $ checkBeta env ty ty' body
+    modify $ insertDef name ty' body
+  where
+    body = elaborate irBody
+    ty = elaborate irTy
+
+evalDef :: Env -> IRDef -> Result Env
+evalDef = flip (execStateT . handleDef)
+
+handleProgram :: Env -> IRProgram -> Result Env
+handleProgram env = flip execStateT env . mapM_ handleDef
+
+handleAndParseProgram :: Env -> String -> Text -> Either String Env
+handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input
+
+handleAndParseFile :: Env -> String -> ExceptT String IO Env
+handleAndParseFile env filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram env filename

perga.cabal

@@ -26,25 +26,30 @@ common warnings
 library perga-lib
     import:             warnings
     exposed-modules:    Check
-                        Parser
+                        Elaborator
-                        Expr
-                        Eval
                         Errors
+                        Eval
+                        Expr
+                        IR
+                        Parser
                         Preprocessor
+                        Program
 
     hs-source-dirs:     lib
     build-depends:      base ^>=4.19.1.0
                       , relude
-                      , mtl
-                      , megaparsec
-                      , parser-combinators
                       , filepath
+                      , megaparsec
+                      , mtl
+                      , parser-combinators
     mixins:             base hiding (Prelude)
                       , relude (Relude as Prelude)
                       , relude
     default-language:   Haskell2010
     default-extensions: OverloadedStrings
                       , GADTs
+                      , DuplicateRecordFields
+                      , OverloadedRecordDot
 
 executable perga
     import:             warnings
@@ -53,11 +58,11 @@ executable perga
 
     build-depends:      base ^>=4.19.1.0
                       , relude
-                      , perga-lib
-                      , haskeline
-                      , mtl
                       , directory
                       , filepath
+                      , haskeline
+                      , mtl
+                      , perga-lib
     mixins:             base hiding (Prelude)
                       , relude (Relude as Prelude)
                       , relude