Simple let-bindings

driver/Lexer.mll

@@ -40,29 +40,37 @@
     | TYPE _ -> "Type"
     | VAR (_, s) -> s
     | EOF _ -> "<EOF>"
+    | DOT _ -> "."
+    | LET _ -> "let"
+    | IN _ -> "in"
+    | EQ _ -> ":="
 
   let get_range_of_token : token -> (position * position) =
     function
     | ARROW r
-      | AT r
-      | BAR r
-      | COLON r
-      | COMMA r
-      | DARROW r
-      | LPAREN r
-      | RPAREN r
-      | ZERO r
-      | SUCC r
-      | REC r
-      | RETURN r
-      | END r
-      | LAMBDA r
-      | PI r
-      | NAT r
-      | TYPE r
-      | EOF r
-      | INT (r, _)
-      | VAR (r, _) -> r
+    | AT r
+    | BAR r
+    | COLON r
+    | COMMA r
+    | DARROW r
+    | LPAREN r
+    | RPAREN r
+    | ZERO r
+    | SUCC r
+    | REC r
+    | RETURN r
+    | END r
+    | LAMBDA r
+    | PI r
+    | NAT r
+    | TYPE r
+    | EOF r
+    | INT (r, _)
+    | DOT r
+    | LET r
+    | IN r
+    | EQ r
+    | VAR (r, _) -> r
 
   let format_token (f: Format.formatter) (t: token): unit =
     Format.fprintf
@@ -97,8 +105,12 @@ rule read =
   | "Nat" { NAT (get_range lexbuf) }
   | ['0'-'9']+ as lxm { INT (get_range lexbuf, int_of_string lxm) }
   | "Type" { TYPE (get_range lexbuf) }
-  | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) }
   | eof { EOF (get_range lexbuf) }
+  | "." { DOT (get_range lexbuf) }
+  | "let" {LET (get_range lexbuf) }
+  | "in" {IN (get_range lexbuf) }
+  | ":=" {EQ (get_range lexbuf) }
+  | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) }
   | _ as c { failwith (Format.asprintf "@[<v 2>Lexer error:@ @[<v 2>Unexpected character %C@ at %a@]@]@." c format_position lexbuf.lex_start_p) }
 and comment =
   parse

examples/nary.mcl

@@ -5,15 +5,15 @@
       (appNary : forall (n : Nat) (f : Nary (succ n)) (arg : Nat) -> Nary n)
       (n : Nat)
       (f : Nary n)
-    -> (rec n return y -> (forall (g : Nary y) -> Nat)
+    -> (rec n return y . (forall (g : Nary y) -> Nat)
        | zero => toNat
        | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m))
        end) f
 )
 (* Nary definition *)
 (
   fun (n : Nat)
-    -> rec n return y -> Type@0
+    -> rec n return y . Type@0
        | zero => Nat
        | succ m, r => forall (a : Nat) -> r
        end
@@ -23,7 +23,7 @@
 (* appNary definition *)
 (
   fun (n : Nat)
-      (f : rec succ n return y -> Type@0
+      (f : rec succ n return y . Type@0
            | zero => Nat
            | succ m, r => forall (a : Nat) -> r
            end)
@@ -40,7 +40,7 @@
   (
     fun (a : Nat)
         (b : Nat)
-      -> rec a return y -> Nat
+      -> rec a return y . Nat
          | zero => b
          | succ m, r => succ r
          end

examples/simple_let.mcl

@@ -0,0 +1 @@
+let (x : Nat) := zero in succ x : Nat

examples/simple_rec.mcl

@@ -1,4 +1,4 @@
-(fun (x : Nat) -> rec x return y -> Nat
+(fun (x : Nat) -> rec x return y . Nat
   | zero => 1
   | succ n, r => succ r
   end) : forall (x : Nat) -> Nat

examples/vector.mcl

@@ -13,7 +13,7 @@
       (* total head function *)
       (
         fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) ->
-          vecRec A (succ n) vec (fun (l : Nat) -> rec l return r -> Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r -> Type@0 | zero => Nat | succ l, r => A end) -> a)
+          vecRec A (succ n) vec (fun (l : Nat) -> rec l return r . Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r . Type@0 | zero => Nat | succ l, r => A end) -> a)
       )
       (* example vector *)
       (

theories/Frontend/Parser.vy

@@ -10,8 +10,8 @@ Parameter loc : Type.
 
 %token <loc*string> VAR
 %token <loc*nat> INT
-%token <loc> END LAMBDA NAT PI REC RETURN SUCC TYPE ZERO (* keywords *)
-%token <loc> ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" EOF (* symbols *)
+%token <loc> END LAMBDA NAT PI REC RETURN SUCC TYPE ZERO LET IN (* keywords *)
+%token <loc> ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" DOT "." EQ ":=" EOF (* symbols *)
 
 %start <Cst.obj * Cst.obj> prog
 %type <Cst.obj> obj app_obj atomic_obj
@@ -34,16 +34,19 @@ let obj :=
   | ~ = fnbinder; ~ = params; "->"; ~ = obj; { List.fold_left (fun acc arg => fnbinder (fst arg) (snd arg) acc) params obj }
   | ~ = app_obj; <>
 
-  | REC; escr = obj; RETURN; mx = VAR; "->"; em = obj;
+  | REC; escr = obj; RETURN; mx = VAR; "."; em = obj;
     "|"; ZERO; "=>"; ez = obj;
     "|"; SUCC; sx = VAR; ","; sr = VAR; "=>"; ms = obj;
     END; { Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) ms }
   | SUCC; ~ = obj; { Cst.succ obj }
 
+  | LET; p = param; ":="; arg_obj = obj; IN; fun_obj = obj; { Cst.app (Cst.fn (fst p) (snd p) fun_obj) arg_obj }
+
 let app_obj :=
   | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj }
   | ~ = atomic_obj; <>
 
+
 let atomic_obj :=
   | TYPE; "@"; n = INT; { Cst.typ (snd n) }