Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simple let-bindings #234

Merged
merged 8 commits into from
Oct 14, 2024
+660 −132
Merged

Simple let-bindings #234

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
18480aa
Changed -> to . in recursor
AG-something Sep 10, 2024
8550eb9
Added let-binders
AG-something Sep 12, 2024
b9559a2
Added error messages for bad let-bindings
AG-something Sep 12, 2024
79c2d05
Changed equality symbol to :=
AG-something Oct 1, 2024
775f7f8
Merge branch 'main' into dummy-let
Ailrun Oct 2, 2024
4864200
let-binding now works with multiple definitions; added let-binding ve…
Antoine-something Oct 11, 2024
fe8ac70
Replaced -> with . in pretty printer
Antoine-something Oct 13, 2024
103d676
Merge branch 'main' into dummy-let
Ailrun Oct 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 32 additions & 20 deletions driver/Lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion driver/PrettyPrinter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading