8000 Multiple payload types in tokens by proux01 · Pull Request #9815 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Multiple payload types in tokens #9815

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

Merged
merged 3 commits into from
Apr 1, 2019
Merged

Multiple payload types in tokens #9815

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
eadb006
Multiple payload types in tokens
proux01 Feb 17, 2019
ef6c99e
Improve coqpp error message for SELF in anonymous entry
proux01 Mar 24, 2019
d8d3b7a
Add overlay
proux01 Mar 24, 2019
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: 34 additions & 18 deletions coqpp/coqpp_main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,29 +161,33 @@ let is_token s = match string_split s with
| [s] -> is_uident s
| _ -> false

let rec parse_tokens = function
let rec parse_tokens ?(in_anon=false) =
let err_anon () =
if in_anon then
fatal (Printf.sprintf "'SELF' or 'NEXT' illegal in anonymous entry level") in
function
| [GSymbString s] -> SymbToken ("", Some s)
| [GSymbQualid ("QUOTATION", None); GSymbString s] ->
SymbToken ("QUOTATION", Some s)
| [GSymbQualid ("SELF", None)] -> SymbSelf
| [GSymbQualid ("NEXT", None)] -> SymbNext
| [GSymbQualid ("SELF", None)] -> err_anon (); SymbSelf
| [GSymbQualid ("NEXT", None)] -> err_anon (); SymbNext
| [GSymbQualid ("LIST0", None); tkn] ->
SymbList0 (parse_token tkn, None)
SymbList0 (parse_token ~in_anon tkn, None)
| [GSymbQualid ("LIST1", None); tkn] ->
SymbList1 (parse_token tkn, None)
SymbList1 (parse_token ~in_anon tkn, None)
| [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
SymbList0 (parse_token tkn, Some (parse_token tkn'))
SymbList0 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
| [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
SymbList1 (parse_token tkn, Some (parse_token tkn'))
SymbList1 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
| [GSymbQualid ("OPT", None); tkn] ->
SymbOpt (parse_token tkn)
SymbOpt (parse_token ~in_anon tkn)
| [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None)
| [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s)
| [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl)
| [GSymbParen tkns] -> parse_tokens tkns
| [GSymbParen tkns] -> parse_tokens ~in_anon tkns
| [GSymbProd prds] ->
let map p =
let map (pat, tkns) = (pat, parse_tokens tkns) in
let map (pat, tkns) = (pat, parse_tokens ~in_anon:true tkns) in
(List.map map p.gprod_symbs, p.gprod_body)
in
SymbRules (List.map map prds)
Expand All @@ -199,7 +203,7 @@ let rec parse_tokens = function
in
fatal (Printf.sprintf "Invalid token: %s" (db_tokens t))

and parse_token tkn = parse_tokens [tkn]
and parse_token ~in_anon tkn = parse_tokens ~in_anon [tkn]

let print_fun fmt (vars, body) =
let vars = List.rev vars in
Expand All @@ -214,9 +218,20 @@ let print_fun fmt (vars, body) =

(** Meta-program instead of calling Tok.of_pattern here because otherwise
violates value restriction *)
let print_tok fmt (k,o) =
let print_pat fmt = print_opt fmt print_string in
fprintf fmt "(%a,%a)" print_string k print_pat o
let print_tok fmt =
let print_pat fmt = print_opt fmt print_string in
function
| "", Some s -> fprintf fmt "Tok.PKEYWORD (%a)" print_string s
| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
| "INT", s -> fprintf fmt "Tok.PINT (%a)" print_pat s
| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
| "QUOTATION", Some s -> fprintf fmt "Tok.PQUOTATION %a" print_string s
| "EOI", None -> fprintf fmt "Tok.PEOI"
| _ -> failwith "Tok.of_pattern: not a constructor"

let rec print_prod fmt p =
let (vars, tkns) = List.split p.gprod_symbs in
Expand All @@ -225,12 +240,13 @@ let rec print_prod fmt p =

and print_extrule fmt (tkn, vars, body) =
let tkn = List.rev tkn in
fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun (vars, body)
fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body)

and print_symbols fmt = function
and print_symbols ~norec fmt = function
| [] -> fprintf fmt "Extend.Stop"
| tkn :: tkns ->
fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
let c = if norec then "Extend.NextNoRec" else "Extend.Next" in
fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn

and print_symbol fmt tkn = match tkn with
| SymbToken (t, s) ->
Expand All @@ -257,7 +273,7 @@ and print_symbol fmt tkn = match tkn with
let pr fmt (r, body) =
let (vars, tkn) = List.split r in
let tkn = List.rev tkn in
fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
fprintf fmt "Extend.Rules @[(%a,@ (%a))@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
in
let pr fmt rules = print_list fmt pr rules in
fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)
Expand Down
4 changes: 4 additions & 0 deletions dev/ci/user-overlays/09815-token-type.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then
ltac2_CI_REF=token-type
ltac2_CI_GITURL=https://github.com/proux01/ltac2
fi
Loading
0