summaryrefslogtreecommitdiff
path: root/parsing/esyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/esyntax.ml')
-rw-r--r--parsing/esyntax.ml276
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">")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 05:57:27 +0000