From eadb00648127c9a535b533d51189dce41ef16db7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 17 Feb 2019 10:10:22 +0100 Subject: Multiple payload types in tokens Instead of just string (and empty strings for tokens without payload) --- coqpp/coqpp_main.ml | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) (limited to 'coqpp') diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index f4c819eeb6..8657d315f5 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -214,9 +214,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 @@ -225,12 +236,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) -> @@ -257,7 +269,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) -- cgit v1.2.3 From ef6c99e0e2e55b9fe316cc14663df161ebf4a21e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Mar 2019 22:06:44 +0100 Subject: Improve coqpp error message for SELF in anonymous entry Something like "("; [ s = SELF -> { s } ]; ")" in a GRAMMAR EXTEND in a mlg file was causing an error message such as OCAMLOPT f.ml File "f.mlg", line 179, characters 55-67: # not in a semantic rule so line doesn't match anything in the mlg file Error: This expression has type ('a, Extend.mayrec, 'a) Extend.symbol but an expression was expected of type ('a, Extend.norec, 'b) Extend.symbol Type Extend.mayrec is not compatible with type Extend.norec It is now COQPP f.mlg Error: 'SELF' or 'NEXT' illegal in anonymous entry level --- coqpp/coqpp_main.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) (limited to 'coqpp') diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 8657d315f5..baa6c2d64e 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -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) @@ -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 -- cgit v1.2.3