created complete grammar

hm.cf

@@ -0,0 +1,32 @@
+layout toplevel ;
+
+entrypoints [Def], Exp ;
+
+token Id ((letter|digit|'_'|'['|']')+) ;
+
+comment "--" ;
+comment "{-" "-}" ;
+
+TypeDef. Def ::= "type" TypeSig1 "|" [Decl] ;
+VarDef.  Def ::= Id ":" TypeSig ":=" Exp ;
+separator Def ";" ;
+
+Decl. Decl ::= Id ":" TypeSig ;
+separator nonempty Decl "|" ;
+
+TypeFun. TypeSig  ::= TypeSig1 "→"  TypeSig ;
+TypeApp. TypeSig1 ::= Id [TypeSig2] ;
+TypeVar. TypeSig2 ::= Id ;
+coercions TypeSig 2;
+
+separator nonempty TypeSig2 "" ;
+
+ExpTyped. Exp  ::= Exp1 ":" TypeSig ;
+ExpAbs.   Exp1 ::= "λ" [Id] "." Exp2 ;
+ExpApp.   Exp2 ::= Exp3 [Exp3] ;
+ExpVar.   Exp3 ::= Id ;
+
+separator nonempty Exp3 "" ;
+coercions Exp 3;
+
+separator nonempty Id "" ;

test

@@ -0,0 +1,59 @@
+-- no pattern matching, instead a recursor is given based on your inductive definition
+-- for example: the following
+
+type List A
+  | nil : List A
+  |	cons  : A → List A → List A
+
+-- will bring the following into scope
+-- rec[List] : B → (A → B → B) → List A → B
+
+-- map could then be written as
+
+map : (A → B) → List A → List B
+ := rec[List] nil (λx xs. cons (f x) xs)
+
+-- one could then define the naturals as follows
+
+type Nat
+  |	zero : Nat
+  |	succ : Nat → Nat
+
+-- defining addition as
+
+add : Nat → Nat → Nat
+ := rec[Nat] (λx. x) (λn f. succ (f n))
+
+-- since                | rec[Nat] : B → (Nat → B → B) → Nat → B
+-- which generalizes to | rec[Nat] : (Nat → Nat) → (Nat → (Nat → Nat) → (Nat → Nat)) → Nat → Nat → Nat
+--                                   ^ adding 0    ^ recursively adding one more     ^ resulting addition type
+
+-- id is used to not add anything, the second function takes the last addition function and adds a layer
+-- of succ onto it, this way it generates a function for adding the right amount.
+
+-- multiplication is defined similairly
+
+mul : Nat → Nat → Nat
+ := rec[Nat] (λx. zero) (λn f. add n (f n))
+
+-- here's an example of a simpler type
+
+type Bool
+  |	true : Bool
+  | false : Bool
+
+not : Bool → Bool
+ := rec[Bool] false true
+
+-- now, let's look at a bit more interesting example
+
+type Expr
+  | num : Nat
+  | add : Expr Expr
+  | mul : Expr Expr
+
+-- this generates the following recursor
+-- rec[Expr] : (Nat → B) → (B → B → B) → (B → B → B) → Expr → B
+
+eval : Expr → Nat
+ := rec[Expr] (λx. x) add mul