simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(parser): handle {} properly

Browse source
This commit is contained in:
Simon Cruanes 2022-10-07 21:40:50 -04:00
parent 32d268822d
commit 1bc6f0ef5c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/parser/ast_term.ml
View file

@ -179,8 +179,8 @@ let rec pp_proof out (p : proof) : unit =
and pp_proof_step out (step : proof_step) : unit =
let s = step.view in
Fmt.fprintf out "@[<2>have %s := %a@ proof %a@]" s.name pp_term s.goal
pp_proof s.proof
Fmt.fprintf out "@[<2>have %s := %a@ %a@]" s.name pp_term s.goal pp_proof
s.proof
let pp_decl out (d : decl) =
match d.view with
@ -195,5 +195,5 @@ let pp_decl out (d : decl) =
args pp_tyret () pp_term rhs
| D_hash (name, t) -> Fmt.fprintf out "@[<2>#%s@ %a@];" name pp_term t
| D_theorem { name; goal; proof } ->
Fmt.fprintf out "@[<hv2>theorem %s :=@ %a@ @[<hv2>proof %a@]@];" name
pp_term goal pp_proof proof
Fmt.fprintf out "@[<hv2>theorem %s :=@ %a@ @[<hv>%a@]@];" name pp_term goal
pp_proof proof

2
src/parser/lex.mll
View file

@ -24,6 +24,8 @@ rule token = parse
| ":" { COLON }
| "(" { LPAREN }
| ")" { RPAREN }
| "{" { LBRACE }
| "}" { RBRACE }
| ":=" { EQDEF }
| "->" { ARROW }
| "." { DOT }

5
src/parser/parse_util.ml
View file

@ -8,6 +8,11 @@ module Error = struct
let pp out (self : t) =
Fmt.fprintf out "parse error: %s@ %a" self.msg Loc.pp self.loc
let pp_with_loc ~input out (self : t) =
Fmt.fprintf out "parse error: %s@ %a" self.msg
(Loc.pp_loc ~max_lines:5 ~input)
[ self.loc ]
let to_string = Fmt.to_string pp
end