Simple let-bindings (#234)

* Changed -> to . in recursor * Added let-binders * Added error messages for bad let-bindings * Changed equality symbol to := * let-binding now works with multiple definitions; added let-binding versions of the big examples (nary and vector); added tests for all the let-binding examples * Replaced -> with . in pretty printer --------- Co-authored-by: AG-something <gaulinantoine@gmail.com> Co-authored-by: Junyoung/"Clare" Jang <jjc9310@gmail.com>
Beluga-lang · Oct 14, 2024 · 9ed1a85 · 9ed1a85
1 parent 1b3c0f2
commit 9ed1a85
Show file tree

Hide file tree

Showing 12 changed files with 660 additions and 132 deletions.
diff --git a/driver/Lexer.mll b/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

diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml
@@ -56,7 +56,7 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
   | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) ->
      let impl f () =
        fprintf f
-         "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ \
+         "@[<hv 0>@[<hov 2>rec %a@ return %s . %a@]@ @[<hov 2>| zero =>@ \
           %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
          format_obj escr mx format_obj em format_obj ez sx sr format_obj es
      in