diff options
author | 2004-07-28 21:54:47 +0000 | |
---|---|---|
committer | 2004-07-28 21:54:47 +0000 | |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /parsing/esyntax.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'parsing/esyntax.ml')
-rw-r--r-- | parsing/esyntax.ml | 276 |
1 files changed, 276 insertions, 0 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml new file mode 100644 index 00000000..6a4758ab --- /dev/null +++ b/parsing/esyntax.ml @@ -0,0 +1,276 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: esyntax.ml,v 1.21.2.1 2004/07/16 19:30:37 herbelin Exp $ *) + +open Pp +open Util +open Names +open Libnames +open Coqast +open Ast +open Extend +open Ppextend +open Names +open Nametab +open Topconstr +open Symbols + +(*** Syntax keys ***) + +(* We define keys for ast and astpats. This is a kind of hash + * function. An ast may have several keys, but astpat only one. The + * idea is that if an ast A matches a pattern P, then the key of P + * is in the set of keys of A. Thus, we can split the syntax entries + * according to the key of the pattern. *) + +type key = + | Cst of Names.constant (* keys for global constants rules *) + | SecVar of Names.variable + | Ind of Names.inductive + | Cstr of Names.constructor + | Nod of string (* keys for other constructed asts rules *) + | Oth (* key for other syntax rules *) + | All (* key for catch-all rules (i.e. with a pattern such as $x .. *) + +let warning_verbose = ref true + +let ast_keys = function + | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) -> + [Cst sl; Nod "APPLIST"; All] + | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) -> + [SecVar s; Nod "APPLIST"; All] + | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl); Num (_,tyi)]) ::_) -> + [Ind (sl,tyi); Nod "APPLIST"; All] + | Node(_,"APPLIST", Node(_,"MUTCONSTRUCT", + [Path (_,sl); Num (_,tyi); Num (_,i)]) ::_) -> + [Cstr ((sl,tyi),i); Nod "APPLIST"; All] + | Node(_,s,_) -> [Nod s; All] + | _ -> [Oth; All] + +let spat_key astp = + match astp with + | Pnode("APPLIST", + Pcons(Pnode("CONST", + Pcons(Pquote(Path (_,sl)),_)), _)) + -> Cst sl + | Pnode("APPLIST", + Pcons(Pnode("SECVAR", + Pcons(Pquote(Nvar (_,s)),_)), _)) + -> SecVar s + | Pnode("APPLIST", + Pcons(Pnode("MUTIND", + Pcons(Pquote(Path (_,sl)), + Pcons(Pquote(Num (_,tyi)),_))), _)) + -> Ind (sl,tyi) + | Pnode("APPLIST", + Pcons(Pnode("MUTCONSTRUCT", + Pcons(Pquote(Path (_,sl)), + Pcons(Pquote(Num (_,tyi)), + Pcons(Pquote(Num (_,i)),_)))), _)) + -> Cstr ((sl,tyi),i) + | Pnode(na,_) -> Nod na + | Pquote ast -> List.hd (ast_keys ast) + | Pmeta _ -> All + | _ -> Oth + +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 + +(* Summary operations *) +type frozen_t = (string * string, astpat syntax_entry) Gmap.t * + (string * key, astpat syntax_entry) Gmapl.t + +let freeze () = + (!from_name_table, !from_key_table) + +let unfreeze (fnm,fkm) = + from_name_table := fnm; + from_key_table := fkm + +let init () = + from_name_table := Gmap.empty; + from_key_table := Gmapl.empty + +let find_syntax_entry whatfor gt = + let gt_keys = ast_keys gt in + let entries = + List.flatten + (List.map (fun k -> Gmapl.find (whatfor,k) !from_key_table) gt_keys) + in + find_all_matches (fun se -> se.syn_astpat) [] gt entries + +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 + (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 + end + +let add_rule whatfor se = + let name = (whatfor,se.syn_id) in + let key = (whatfor, se_key se) in + 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 + + +(* Pretty-printing machinery *) + +type std_printer = Coqast.t -> std_ppcmds +type unparsing_subfunction = string -> tolerability option -> std_printer +type primitive_printer = Coqast.t -> std_ppcmds option + +(* Module of primitive printers *) +module Ppprim = + struct + type t = std_printer -> std_printer + let tab = ref ([] : (string * t) list) + let map a = List.assoc a !tab + let add (a,ppr) = tab := (a,ppr)::!tab + end + +(**********************************************************************) +(* Primitive printers (e.g. for numerals) *) + +(* This is the map associating to a printer the scope it belongs to *) +(* and its ML code *) + +let primitive_printer_tab = + ref (Stringmap.empty : (scope_name * primitive_printer) Stringmap.t) +let declare_primitive_printer s sc pp = + primitive_printer_tab := Stringmap.add s (sc,pp) !primitive_printer_tab +let lookup_primitive_printer s = + Stringmap.find s !primitive_printer_tab + +(* 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. *) +(* +let _ = declare_primitive_printer "token" token_printer +*) + +(* A printer for the tokens. *) +let token_printer stdpr = function + | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast + | a -> stdpr a + +(* Unused ?? +(* A primitive printer to do "print as" (to specify a length for a string) *) +let print_as_printer = function + | Node (_, "AS", [Num(_,n); Str(_,s)]) -> Some (stras (n,s)) + | ast -> None + +let _ = declare_primitive_printer "print_as" default_scope print_as_printer +*) + +(* Handle infix symbols *) + +let pr_parenthesis inherited se strm = + if tolerable_prec inherited se.syn_prec then + strm + else + (str"(" ++ strm ++ str")") + +let print_delimiters inh se strm = function + | None -> pr_parenthesis inh se strm + | Some key -> + let left = "'"^key^":" and right = "'" in + let lspace = + if is_letter (left.[String.length left -1]) then str " " else mt () in + let rspace = + let c = right.[0] in + if is_ident_tail c then str " " else mt () in + hov 0 (str left ++ lspace ++ strm ++ rspace ++ str right) + +(* Print the syntax entry. In the unparsing hunks, the tokens are + * printed using the token_printer, unless another primitive printer + * is specified. *) + +let print_syntax_entry sub_pr scopes env se = + let rec print_hunk rule_prec scopes = function + | PH(e,externpr,reln) -> + let node = Ast.pat_sub 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 scopes (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 rule_prec scopes) sub) + | UNP_SYMBOLIC _ -> anomaly "handled by call_primitive_parser" + in + prlist (print_hunk se.syn_prec scopes) se.syn_hunks + +let call_primitive_parser rec_pr otherwise inherited scopes (se,env) = + try ( + match se.syn_hunks with + | [PH(e,Some c,reln)] -> + (* Test for a primitive printer; may raise Not_found *) + let sc,pr = lookup_primitive_printer c in + (* Look if scope [sc] associated to this printer is OK *) + (match Symbols.availability_of_numeral sc scopes with + | None -> otherwise () + | Some key -> + (* We can use this printer *) + let node = Ast.pat_sub dummy_loc env e in + match pr node with + | Some strm -> print_delimiters inherited se strm key + | None -> otherwise ()) + | [UNP_SYMBOLIC (sc,pat,sub)] -> + (match Symbols.availability_of_notation (sc,pat) scopes with + | None -> otherwise () + | Some (scopt,key) -> + print_delimiters inherited se + (print_syntax_entry rec_pr + (option_fold_right Symbols.push_scope scopt scopes) env + {se with syn_hunks = [sub]}) key) + | _ -> + pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se) + ) + with Not_found -> (* To handle old style printer *) + pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se) + +(* [genprint whatfor dflt inhprec ast] prints out the ast of + * 'universe' whatfor. If the term is not matched by any + * pretty-printing rule, then it will call dflt on it, which is + * responsible for printing out the term (usually #GENTERM...). + * In the case of tactics and commands, dflt also prints + * global constants basenames. *) + +let genprint dflt whatfor inhprec ast = + let rec rec_pr scopes inherited gt = + let entries = find_syntax_entry whatfor gt in + let rec test_rule = function + | se_env::rules -> + call_primitive_parser + rec_pr + (fun () -> test_rule rules) + inherited scopes se_env + | [] -> dflt gt (* No rule found *) + in test_rule entries + in + try + rec_pr (Symbols.current_scopes ()) inhprec ast + with + | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">") + | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">") |