diff options
Diffstat (limited to 'parsing/esyntax.ml')
| -rw-r--r-- | parsing/esyntax.ml | 105 |
1 files changed, 82 insertions, 23 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 9d83c7878..608868ca6 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -13,6 +13,9 @@ open Util open Coqast open Ast open Extend +open Vernacexpr +open Names +open Nametab (*** Syntax keys ***) @@ -74,24 +77,34 @@ let spat_key astp = let se_key se = spat_key se.syn_astpat - (** Syntax entry tables (state of the pretty_printer) **) let from_name_table = ref Gmap.empty let from_key_table = ref Gmapl.empty +let infix_symbols_map = ref Stringmap.empty +let infix_names_map = ref Spmap.empty + (* Summary operations *) -type frozen_t = (string * string, syntax_entry) Gmap.t * - (string * key, syntax_entry) Gmapl.t +type frozen_t = (string * string, astpat syntax_entry) Gmap.t * + (string * key, astpat syntax_entry) Gmapl.t * + section_path Stringmap.t * string list Spmap.t -let freeze () = (!from_name_table, !from_key_table) +let freeze () = + (!from_name_table, !from_key_table, !infix_symbols_map, !infix_names_map) -let unfreeze (fnm,fkm) = +let unfreeze (fnm,fkm,infs,infn) = from_name_table := fnm; - from_key_table := fkm + from_key_table := fkm; + infix_symbols_map := infs; + infix_names_map := infn let init () = from_name_table := Gmap.empty; from_key_table := Gmapl.empty +(* + infix_symbols_map := Stringmap.empty; + infix_names_map := Spmap.empty +*) let find_syntax_entry whatfor gt = let gt_keys = ast_keys gt in @@ -105,7 +118,8 @@ let remove_with_warning name = if Gmap.mem name !from_name_table then begin let se = Gmap.find name !from_name_table in let key = (fst name, se_key se) in - (if !warning_verbose then + if !warning_verbose then + (Options.if_verbose warning ("overriding syntax rule "^(fst name)^":"^(snd name)^".")); from_name_table := Gmap.remove name !from_name_table; from_key_table := Gmapl.remove key se !from_key_table @@ -117,7 +131,7 @@ let add_rule whatfor se = remove_with_warning name; from_name_table := Gmap.add name se !from_name_table; from_key_table := Gmapl.add key se !from_key_table - + let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel @@ -126,6 +140,8 @@ let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel type std_printer = Coqast.t -> std_ppcmds type unparsing_subfunction = string -> tolerability option -> std_printer +type std_constr_printer = Genarg.constr_ast -> std_ppcmds + (* Module of primitive printers *) module Ppprim = struct @@ -136,10 +152,9 @@ module Ppprim = end (* A printer for the tokens. *) -let token_printer stdpr ast = - match ast with - | Id _ | Num _ | Str _ | Path _ -> print_ast ast - | _ -> stdpr ast +let token_printer stdpr = function + | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast + | a -> stdpr a (* Register the primitive printer for "token". It is not used in syntax/PP*.v, * but any ast matching no PP rule is printed with it. *) @@ -148,11 +163,56 @@ let _ = Ppprim.add ("token",token_printer) (* A primitive printer to do "print as" (to specify a length for a string) *) let print_as_printer stdpr = function - | Node (_, "AS", [Num(_,n); Str(_,s)]) -> (stras (n,s)) + | Node (_, "AS", [Num(_,n); Str(_,s)]) -> stras (n,s) | ast -> stdpr ast let _ = Ppprim.add ("print_as",print_as_printer) +(* Handle infix symbols *) + +let find_infix_symbols sp = + try Spmap.find sp !infix_names_map with Not_found -> [] + +let find_infix_name a = + try Stringmap.find a !infix_symbols_map + with Not_found -> anomaly ("Undeclared symbol: "^a) + +let declare_infix_symbol sp s = + let l = find_infix_symbols sp in + infix_names_map := Spmap.add sp (s::l) !infix_names_map; + infix_symbols_map := Stringmap.add s sp !infix_symbols_map + +let meta_pattern m = Pmeta(m,Tany) + +let make_hunks (lp,rp) s e1 e2 = + let n,s = + if is_letter (s.[String.length s -1]) or is_letter (s.[0]) + then 1,s^" " else 0,s + in + [PH (meta_pattern e1, None, lp); + UNP_BRK (n, 1); RO s; + PH (meta_pattern e2, None, rp)] + +let build_syntax (ref,e1,e2,assoc) = + let sp = match ref with + | TrueGlobal r -> Nametab.sp_of_global (Global.env()) r + | SyntacticDef sp -> sp in + let rec find_symbol = function + | [] -> + let s = match ref with + | TrueGlobal r -> + string_of_qualid (shortest_qualid_of_global (Global.env()) r) + | SyntacticDef sp -> string_of_path sp in + UNP_BOX (PpHOVB 0, + [RO "("; RO s; UNP_BRK (1, 1); PH (meta_pattern e1, None, E); + UNP_BRK (1, 1); PH (meta_pattern e2, None, E); RO ")"]) + | a::l -> + if find_infix_name a = sp then + UNP_BOX (PpHOVB 1, make_hunks assoc a e1 e2) + else + find_symbol l + in find_symbol (find_infix_symbols sp) + (* Print the syntax entry. In the unparsing hunks, the tokens are * printed using the token_printer, unless another primitive printer @@ -162,22 +222,21 @@ let print_syntax_entry whatfor sub_pr env se = let rule_prec = (se.syn_id, se.syn_prec) in let rec print_hunk = function | PH(e,externpr,reln) -> - let printer = - match externpr with (* May branch to an other printer *) - | Some c -> - (try (* Test for a primitive printer *) - (Ppprim.map c) (sub_pr whatfor (Some(rule_prec,reln))) - with Not_found -> - token_printer (sub_pr c (Some(rule_prec,reln)))) - | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln))) - in - printer (Ast.pat_sub Ast.dummy_loc env e) + let node = Ast.pat_sub Ast.dummy_loc env e in + let printer = + match externpr with (* May branch to an other printer *) + | Some c -> + (try (* Test for a primitive printer *) Ppprim.map c + with Not_found -> token_printer ) + | _ -> token_printer in + printer (sub_pr whatfor (Some(rule_prec,reln))) node | RO s -> str s | UNP_TAB -> tab () | UNP_FNL -> fnl () | UNP_BRK(n1,n2) -> brk(n1,n2) | UNP_TBRK(n1,n2) -> tbrk(n1,n2) | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist print_hunk sub) + | UNP_INFIX (sp,e1,e2,assoc) -> print_hunk (build_syntax (sp,e1,e2,assoc)) in prlist print_hunk se.syn_hunks |