From 513344627bbdf4d822ca93156d2e2943408ec50d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 21 Oct 2015 17:42:00 +0200 Subject: Turn Pcoq into a regular ML file. --- parsing/pcoq.ml | 814 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ parsing/pcoq.ml4 | 814 ------------------------------------------------------- 2 files changed, 814 insertions(+), 814 deletions(-) create mode 100644 parsing/pcoq.ml delete mode 100644 parsing/pcoq.ml4 diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml new file mode 100644 index 0000000000..48dc1372ce --- /dev/null +++ b/parsing/pcoq.ml @@ -0,0 +1,814 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* grammar_object G.entry +end + +module Gramobj : Gramobj = +struct + type grammar_object = Obj.t + let weaken_entry e = Obj.magic e +end + +(** Grammar entries with associated types *) + +type entry_type = argument_type +type grammar_object = Gramobj.grammar_object +type typed_entry = argument_type * grammar_object G.entry +let in_typed_entry t e = (t,Gramobj.weaken_entry e) +let type_of_typed_entry (t,e) = t +let object_of_typed_entry (t,e) = e +let weaken_entry x = Gramobj.weaken_entry x + +module type Gramtypes = +sig + val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry + val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry +end + +module Gramtypes : Gramtypes = +struct + let inGramObj rawwit = in_typed_entry (unquote rawwit) + let outGramObj (a:'a raw_abstract_argument_type) o = + if not (argument_type_eq (type_of_typed_entry o) (unquote a)) + then anomaly ~label:"outGramObj" (str "wrong type"); + (* downcast from grammar_object *) + Obj.magic (object_of_typed_entry o) +end + +open Gramtypes + +(** Grammar extensions *) + +(** NB: [extend_statment = + gram_position option * single_extend_statment list] + and [single_extend_statment = + string option * gram_assoc option * production_rule list] + and [production_rule = symbol list * action] + + In [single_extend_statement], first two parameters are name and + assoc iff a level is created *) + +(** Type of reinitialization data *) +type gram_reinit = gram_assoc * gram_position + +type ext_kind = + | ByGrammar of + grammar_object G.entry + * gram_reinit option (** for reinitialization if ever needed *) + * G.extend_statment + | ByEXTEND of (unit -> unit) * (unit -> unit) + +(** The list of extensions *) + +let camlp4_state = ref [] + +(** Deletion *) + +let grammar_delete e reinit (pos,rls) = + List.iter + (fun (n,ass,lev) -> + List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) + (List.rev rls); + match reinit with + | Some (a,ext) -> + let lev = match Option.map Compat.to_coq_position pos with + | Some (Level n) -> n + | _ -> assert false + in + maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + | None -> () + +(** The apparent parser of Coq; encapsulate G to keep track + of the extensions. *) + +module Gram = + struct + include G + let extend e = + maybe_curry + (fun ext -> + camlp4_state := + (ByEXTEND ((fun () -> grammar_delete e None ext), + (fun () -> maybe_uncurry (G.extend e) ext))) + :: !camlp4_state; + maybe_uncurry (G.extend e) ext) + let delete_rule e pil = + (* spiwack: if you use load an ML module which contains GDELETE_RULE + in a section, God kills a kitty. As it would corrupt remove_grammars. + There does not seem to be a good way to undo a delete rule. As deleting + takes fewer arguments than extending. The production rule isn't returned + by delete_rule. If we could retrieve the necessary information, then + ByEXTEND provides just the framework we need to allow this in section. + I'm not entirely sure it makes sense, but at least it would be more correct. + *) + G.delete_rule e pil + end + +(** This extension command is used by the Grammar constr *) + +let grammar_extend e reinit ext = + camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) ext + +(** Remove extensions + + [n] is the number of extended entries (not the number of Grammar commands!) + to remove. *) + +let rec remove_grammars n = + if n>0 then + (match !camlp4_state with + | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") + | ByGrammar(g,reinit,ext)::t -> + let f (a,b) = (of_coq_assoc a, of_coq_position b) in + grammar_delete g (Option.map f reinit) ext; + camlp4_state := t; + remove_grammars (n-1) + | ByEXTEND (undo,redo)::t -> + undo(); + camlp4_state := t; + remove_grammars n; + redo(); + camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + +let make_rule r = [None, None, r] + +(** An entry that checks we reached the end of the input. *) + +let eoi_entry en = + let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in + let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in + let act = Gram.action (fun _ x loc -> x) in + maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + e + +let map_entry f en = + let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in + let symbs = [Symbols.snterm (Gram.Entry.obj en)] in + let act = Gram.action (fun x loc -> f x) in + maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + e + +(* Parse a string, does NOT check if the entire string was read + (use eoi_entry) *) + +let parse_string f x = + let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) + +type gram_universe = string * (string, typed_entry) Hashtbl.t + +let trace = ref false + +(* The univ_tab is not part of the state. It contains all the grammars that + exist or have existed before in the session. *) + +let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t) + +let create_univ s = + let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u + +let uprim = create_univ "prim" +let uconstr = create_univ "constr" +let utactic = create_univ "tactic" +let uvernac = create_univ "vernac" + +let get_univ s = + try + Hashtbl.find univ_tab s + with Not_found -> + anomaly (Pp.str ("Unknown grammar universe: "^s)) + +let get_entry (u, utab) s = Hashtbl.find utab s + +let new_entry etyp (u, utab) s = + if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); + let ename = u ^ ":" ^ s in + let e = in_typed_entry etyp (Gram.entry_create ename) in + Hashtbl.add utab s e; e + +let create_entry (u, utab) s etyp = + try + let e = Hashtbl.find utab s in + if not (argument_type_eq (type_of_typed_entry e) etyp) then + failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); + e + with Not_found -> + new_entry etyp (u, utab) s + +let create_constr_entry s = + outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType) + +let create_generic_entry s wit = + outGramObj wit (create_entry utactic s (unquote wit)) + +(* [make_gen_entry] builds entries extensible by giving its name (a string) *) +(* For entries extensible only via the ML name, Gram.entry_create is enough *) + +let make_gen_entry (u,univ) rawwit s = + let e = Gram.entry_create (u ^ ":" ^ s) in + Hashtbl.add univ s (inGramObj rawwit e); e + +(* Initial grammar entries *) + +module Prim = + struct + let gec_gen x = make_gen_entry uprim x + + (* Entries that can be referred via the string -> Gram.entry table *) + (* Typically for tactic or vernac extensions *) + let preident = gec_gen (rawwit wit_pre_ident) "preident" + let ident = gec_gen (rawwit wit_ident) "ident" + let natural = gec_gen (rawwit wit_int) "natural" + let integer = gec_gen (rawwit wit_int) "integer" + let bigint = Gram.entry_create "Prim.bigint" + let string = gec_gen (rawwit wit_string) "string" + let reference = make_gen_entry uprim (rawwit wit_ref) "reference" + let by_notation = Gram.entry_create "by_notation" + let smart_global = Gram.entry_create "smart_global" + + (* parsed like ident but interpreted as a term *) + let var = gec_gen (rawwit wit_var) "var" + + let name = Gram.entry_create "Prim.name" + let identref = Gram.entry_create "Prim.identref" + let pattern_ident = Gram.entry_create "pattern_ident" + let pattern_identref = Gram.entry_create "pattern_identref" + + (* A synonym of ident - maybe ident will be located one day *) + let base_ident = Gram.entry_create "Prim.base_ident" + + let qualid = Gram.entry_create "Prim.qualid" + let fullyqualid = Gram.entry_create "Prim.fullyqualid" + let dirpath = Gram.entry_create "Prim.dirpath" + + let ne_string = Gram.entry_create "Prim.ne_string" + let ne_lstring = Gram.entry_create "Prim.ne_lstring" + + end + +module Constr = + struct + let gec_constr = make_gen_entry uconstr (rawwit wit_constr) + + (* Entries that can be referred via the string -> Gram.entry table *) + let constr = gec_constr "constr" + let operconstr = gec_constr "operconstr" + let constr_eoi = eoi_entry constr + let lconstr = gec_constr "lconstr" + let binder_constr = create_constr_entry "binder_constr" + let ident = make_gen_entry uconstr (rawwit wit_ident) "ident" + let global = make_gen_entry uconstr (rawwit wit_ref) "global" + let sort = make_gen_entry uconstr (rawwit wit_sort) "sort" + let pattern = Gram.entry_create "constr:pattern" + let constr_pattern = gec_constr "constr_pattern" + let lconstr_pattern = gec_constr "lconstr_pattern" + let closed_binder = Gram.entry_create "constr:closed_binder" + let binder = Gram.entry_create "constr:binder" + let binders = Gram.entry_create "constr:binders" + let open_binders = Gram.entry_create "constr:open_binders" + let binders_fixannot = Gram.entry_create "constr:binders_fixannot" + let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" + let record_declaration = Gram.entry_create "constr:record_declaration" + let appl_arg = Gram.entry_create "constr:appl_arg" + end + +module Module = + struct + let module_expr = Gram.entry_create "module_expr" + let module_type = Gram.entry_create "module_type" + end + +module Tactic = + struct + (* Main entry for extensions *) + let simple_tactic = Gram.entry_create "tactic:simple_tactic" + + (* Entries that can be referred via the string -> Gram.entry table *) + (* Typically for tactic user extensions *) + let open_constr = + make_gen_entry utactic (rawwit wit_open_constr) "open_constr" + let constr_with_bindings = + make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" + let bindings = + make_gen_entry utactic (rawwit wit_bindings) "bindings" + let hypident = Gram.entry_create "hypident" + let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let uconstr = + make_gen_entry utactic (rawwit wit_uconstr) "uconstr" + let quantified_hypothesis = + make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis" + let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var" + let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr" + let simple_intropattern = + make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern" + let clause_dft_concl = + make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause" + + + (* Main entries for ltac *) + let tactic_arg = Gram.entry_create "tactic:tactic_arg" + let tactic_expr = Gram.entry_create "tactic:tactic_expr" + let binder_tactic = Gram.entry_create "tactic:binder_tactic" + + let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic" + + (* Main entry for quotations *) + let tactic_eoi = eoi_entry tactic + + (* For Ltac definition *) + let tacdef_body = Gram.entry_create "tactic:tacdef_body" + + end + +module Vernac_ = + struct + let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + + (* The different kinds of vernacular commands *) + let gallina = gec_vernac "gallina" + let gallina_ext = gec_vernac "gallina_ext" + let command = gec_vernac "command" + let syntax = gec_vernac "syntax_command" + let vernac = gec_vernac "Vernac.vernac" + let vernac_eoi = eoi_entry vernac + let rec_definition = gec_vernac "Vernac.rec_definition" + (* Main vernac entry *) + let main_entry = Gram.entry_create "vernac" + + let () = + let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in + let act_eoi = Gram.action (fun _ loc -> None) in + let rule = [ + ([ Symbols.stoken Tok.EOI ], act_eoi); + ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac ); + ] in + maybe_uncurry (Gram.extend main_entry) (None, make_rule rule) + + end + +let main_entry = Vernac_.main_entry + +(**********************************************************************) +(* This determines (depending on the associativity of the current + level and on the expected associativity) if a reference to constr_n is + a reference to the current level (to be translated into "SELF" on the + left border and into "constr LEVEL n" elsewhere), to the level below + (to be translated into "NEXT") or to an below wrt associativity (to be + translated in camlp4 into "constr" without level) or to another level + (to be translated into "constr LEVEL n") + + The boolean is true if the entry was existing _and_ empty; this to + circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + converse of the extension mechanism *) + +let constr_level = string_of_int + +let default_levels = + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.RightA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_pattern_levels = + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 11,Extend.LeftA,false; + 10,Extend.RightA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let level_stack = + ref [(default_levels, default_pattern_levels)] + +(* At a same level, LeftA takes precedence over RightA and NoneA *) +(* In case, several associativity exists for a level, we make two levels, *) +(* first LeftA, then RightA and NoneA together *) + +let admissible_assoc = function + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false + | Extend.RightA, Some Extend.LeftA -> false + | _ -> true + +let create_assoc = function + | None -> Extend.RightA + | Some a -> a + +let error_level_assoc p current expected = + let pr_assoc = function + | Extend.LeftA -> str "left" + | Extend.RightA -> str "right" + | Extend.NonA -> str "non" in + errorlabstrm "" + (str "Level " ++ int p ++ str " is already declared " ++ + pr_assoc current ++ str " associative while it is now expected to be " ++ + pr_assoc expected ++ str " associative.") + +let create_pos = function + | None -> Extend.First + | Some lev -> Extend.After (constr_level lev) + +let find_position_gen forpat ensure assoc lev = + let ccurrent,pcurrent as current = List.hd !level_stack in + match lev with + | None -> + level_stack := current :: !level_stack; + None, None, None, None + | Some n -> + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = + if forpat then (ccurrent, add_level None pcurrent) + else (add_level None ccurrent, pcurrent) in + level_stack := updated:: !level_stack; + let assoc = create_assoc assoc in + begin match !init with + | None -> + (* Create the entry *) + Some (create_pos !after), Some assoc, Some (constr_level n), None + | _ -> + (* The reinit flag has been updated *) + Some (Extend.Level (constr_level n)), None, None, !init + end + with + (* Nothing has changed *) + Exit -> + level_stack := current :: !level_stack; + (* Just inherit the existing associativity and name (None) *) + Some (Extend.Level (constr_level n)), None, None, None + +let remove_levels n = + level_stack := List.skipn n !level_stack + +let rec list_mem_assoc_triple x = function + | [] -> false + | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l + +let register_empty_levels forpat levels = + let filter n = + try + let levels = (if forpat then snd else fst) (List.hd !level_stack) in + if not (list_mem_assoc_triple n levels) then + Some (find_position_gen forpat true None (Some n)) + else None + with Failure _ -> None + in + List.map_filter filter levels + +let find_position forpat assoc level = + find_position_gen forpat false assoc level + +(* Synchronise the stack of level updates *) +let synchronize_level_positions () = + let _ = find_position true None None in () + +(**********************************************************************) +(* Binding constr entry keys to entries *) + +(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp4_assoc = function + | Some Extend.NonA | Some Extend.RightA -> Extend.RightA + | None | Some Extend.LeftA -> Extend.LeftA + +let assoc_eq al ar = match al, ar with +| Extend.NonA, Extend.NonA +| Extend.RightA, Extend.RightA +| Extend.LeftA, Extend.LeftA -> true +| _, _ -> false + +(* [adjust_level assoc from prod] where [assoc] and [from] are the name + and associativity of the level where to add the rule; the meaning of + the result is + + None = SELF + Some None = NEXT + Some (Some (n,cur)) = constr LEVEL n + s.t. if [cur] is set then [n] is the same as the [from] level *) +let adjust_level assoc from = function +(* Associativity is None means force the level *) + | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) +(* Compute production name on the right side *) + (* If NonA or LeftA on the right-hand side, set to NEXT *) + | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) -> + Some None + (* If RightA on the right-hand side, set to the explicit (current) level *) + | (NumLevel n,BorderProd (Right,Some Extend.RightA)) -> + Some (Some (n,true)) +(* Compute production name on the left side *) + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None + (* If the expected assoc is the current one, set to SELF *) + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> + None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (NumLevel n,BorderProd (Left,Some a)) -> + begin match a with + | Extend.LeftA -> Some (Some (n, true)) + | _ -> Some None + end + (* None means NEXT *) + | (NextLevel,_) -> Some None +(* Compute production name elsewhere *) + | (NumLevel n,InternalProd) -> + match from with + | ETConstr (p,()) when Int.equal p (n + 1) -> Some None + | ETConstr (p,()) -> Some (Some (n, Int.equal n p)) + | _ -> Some (Some (n,false)) + +let compute_entry allow_create adjust forpat = function + | ETConstr (n,q) -> + (if forpat then weaken_entry Constr.pattern + else weaken_entry Constr.operconstr), + adjust (n,q), false + | ETName -> weaken_entry Prim.name, None, false + | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") + | ETBinder false -> weaken_entry Constr.binder, None, false + | ETBinderList (true,tkl) -> + let () = match tkl with [] -> () | _ -> assert false in + weaken_entry Constr.open_binders, None, false + | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") + | ETBigint -> weaken_entry Prim.bigint, None, false + | ETReference -> weaken_entry Constr.global, None, false + | ETPattern -> weaken_entry Constr.pattern, None, false + | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") + | ETOther (u,n) -> + let u = get_univ u in + let e = + try get_entry u n + with Not_found when allow_create -> create_entry u n ConstrArgType in + object_of_typed_entry e, None, true + +(* This computes the name of the level where to add a new rule *) +let interp_constr_entry_key forpat = function + | ETConstr(200,()) when not forpat -> + weaken_entry Constr.binder_constr, None + | e -> + let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in + (e, level) + +(* This computes the name to give to a production knowing the name and + associativity of the level where it must be added *) +let interp_constr_prod_entry_key ass from forpat en = + compute_entry false (adjust_level ass from) forpat en + +(**********************************************************************) +(* Binding constr entry keys to symbols *) + +let is_self from e = + match from, e with + ETConstr(n,()), ETConstr(NumLevel n', + BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false + | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n' + | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint + | ETPattern, ETPattern) -> true + | ETOther(s1,s2), ETOther(s1',s2') -> + String.equal s1 s1' && String.equal s2 s2' + | _ -> false + +let is_binder_level from e = + match from, e with + ETConstr(200,()), + ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true + | _ -> false + +let make_sep_rules tkl = + Gram.srules' + [List.map gram_token_of_token tkl, + List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl + (Gram.action (fun loc -> ()))] + +let rec symbol_of_constr_prod_entry_key assoc from forpat typ = + if is_binder_level from typ then + if forpat then + Symbols.snterml (Gram.Entry.obj Constr.pattern,"200") + else + Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200") + else if is_self from typ then + Symbols.sself + else + match typ with + | ETConstrList (typ',[]) -> + Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) + | ETConstrList (typ',tkl) -> + Symbols.slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), + make_sep_rules tkl) + | ETBinderList (false,[]) -> + Symbols.slist1 + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) + | ETBinderList (false,tkl) -> + Symbols.slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), + make_sep_rules tkl) + + | _ -> + match interp_constr_prod_entry_key assoc from forpat typ with + | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj) + | (eobj,Some None,_) -> Symbols.snext + | (eobj,Some (Some (lev,cur)),_) -> + Symbols.snterml (Gram.Entry.obj eobj,constr_level lev) + +(** Binding general entry keys to symbol *) + +let rec symbol_of_prod_entry_key = function + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Amodifiers s -> + Gram.srules' + [([], Gram.action (fun _loc -> [])); + ([gram_token_of_string "("; + Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string ","); + gram_token_of_string ")"], + Gram.action (fun _ l _ _loc -> l))] + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Atactic 5 -> Symbols.snterm (Gram.Entry.obj Tactic.binder_tactic) + | Atactic n -> + Symbols.snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) + | Agram s -> + let e = + try + (** ppedrot: we should always generate Agram entries which have already + been registered, so this should not fail. *) + let (u, s) = match String.split ':' s with + | u :: s :: [] -> (u, s) + | _ -> raise Not_found + in + get_entry (get_univ u) s + with Not_found -> + Errors.anomaly (str "Unregistered grammar entry: " ++ str s) + in + Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) + | Aentry (u,s) -> + let e = get_entry (get_univ u) s in + Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) + +let level_of_snterml e = int_of_string (Symbols.snterml_level e) + +(**********************************************************************) +(* Interpret entry names of the form "ne_constr_list" as entry keys *) + +let coincide s pat off = + let len = String.length pat in + let break = ref true in + let i = ref 0 in + while !break && !i < len do + let c = Char.code s.[off + !i] in + let d = Char.code pat.[!i] in + break := Int.equal c d; + incr i + done; + !break + +let tactic_level s = + if Int.equal (String.length s) 7 && coincide s "tactic" 0 then + let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) + else None + else None + +let type_of_entry u s = + type_of_typed_entry (get_entry u s) + +let rec interp_entry_name static up_level s sep = + let l = String.length s in + if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then + let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in + ListArgType t, Alist1 g + else if l > 12 && coincide s "ne_" 0 && + coincide s "_list_sep" (l-9) then + let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in + ListArgType t, Alist1sep (g,sep) + else if l > 5 && coincide s "_list" (l-5) then + let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in + ListArgType t, Alist0 g + else if l > 9 && coincide s "_list_sep" (l-9) then + let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in + ListArgType t, Alist0sep (g,sep) + else if l > 4 && coincide s "_opt" (l-4) then + let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in + OptArgType t, Aopt g + else if l > 5 && coincide s "_mods" (l-5) then + let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in + ListArgType t, Amodifiers g + else + let s = match s with "hyp" -> "var" | _ -> s in + let check_lvl n = match up_level with + | None -> false + | Some m -> Int.equal m n + && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) + && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) + in + let t, se = + match tactic_level s with + | Some n -> + (** Quite ad-hoc *) + let t = unquote (rawwit wit_tactic) in + let se = + if check_lvl n then Aself + else if check_lvl (n + 1) then Anext + else Atactic n + in + (Some t, se) + | None -> + try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found -> + try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found -> + try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found -> + if static then + error ("Unknown entry "^s^".") + else + None, Aentry ("",s) in + let t = + match t with + | Some t -> t + | None -> ExtraArgType s in + t, se + +let list_entry_names () = + let add_entry key (entry, _) accu = (key, entry) :: accu in + let ans = Hashtbl.fold add_entry (snd uprim) [] in + let ans = Hashtbl.fold add_entry (snd uconstr) ans in + Hashtbl.fold add_entry (snd utactic) ans diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 deleted file mode 100644 index 48dc1372ce..0000000000 --- a/parsing/pcoq.ml4 +++ /dev/null @@ -1,814 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* grammar_object G.entry -end - -module Gramobj : Gramobj = -struct - type grammar_object = Obj.t - let weaken_entry e = Obj.magic e -end - -(** Grammar entries with associated types *) - -type entry_type = argument_type -type grammar_object = Gramobj.grammar_object -type typed_entry = argument_type * grammar_object G.entry -let in_typed_entry t e = (t,Gramobj.weaken_entry e) -let type_of_typed_entry (t,e) = t -let object_of_typed_entry (t,e) = e -let weaken_entry x = Gramobj.weaken_entry x - -module type Gramtypes = -sig - val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry - val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry -end - -module Gramtypes : Gramtypes = -struct - let inGramObj rawwit = in_typed_entry (unquote rawwit) - let outGramObj (a:'a raw_abstract_argument_type) o = - if not (argument_type_eq (type_of_typed_entry o) (unquote a)) - then anomaly ~label:"outGramObj" (str "wrong type"); - (* downcast from grammar_object *) - Obj.magic (object_of_typed_entry o) -end - -open Gramtypes - -(** Grammar extensions *) - -(** NB: [extend_statment = - gram_position option * single_extend_statment list] - and [single_extend_statment = - string option * gram_assoc option * production_rule list] - and [production_rule = symbol list * action] - - In [single_extend_statement], first two parameters are name and - assoc iff a level is created *) - -(** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position - -type ext_kind = - | ByGrammar of - grammar_object G.entry - * gram_reinit option (** for reinitialization if ever needed *) - * G.extend_statment - | ByEXTEND of (unit -> unit) * (unit -> unit) - -(** The list of extensions *) - -let camlp4_state = ref [] - -(** Deletion *) - -let grammar_delete e reinit (pos,rls) = - List.iter - (fun (n,ass,lev) -> - List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) - (List.rev rls); - match reinit with - | Some (a,ext) -> - let lev = match Option.map Compat.to_coq_position pos with - | Some (Level n) -> n - | _ -> assert false - in - maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) - | None -> () - -(** The apparent parser of Coq; encapsulate G to keep track - of the extensions. *) - -module Gram = - struct - include G - let extend e = - maybe_curry - (fun ext -> - camlp4_state := - (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> maybe_uncurry (G.extend e) ext))) - :: !camlp4_state; - maybe_uncurry (G.extend e) ext) - let delete_rule e pil = - (* spiwack: if you use load an ML module which contains GDELETE_RULE - in a section, God kills a kitty. As it would corrupt remove_grammars. - There does not seem to be a good way to undo a delete rule. As deleting - takes fewer arguments than extending. The production rule isn't returned - by delete_rule. If we could retrieve the necessary information, then - ByEXTEND provides just the framework we need to allow this in section. - I'm not entirely sure it makes sense, but at least it would be more correct. - *) - G.delete_rule e pil - end - -(** This extension command is used by the Grammar constr *) - -let grammar_extend e reinit ext = - camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; - camlp4_verbose (maybe_uncurry (G.extend e)) ext - -(** Remove extensions - - [n] is the number of extended entries (not the number of Grammar commands!) - to remove. *) - -let rec remove_grammars n = - if n>0 then - (match !camlp4_state with - | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") - | ByGrammar(g,reinit,ext)::t -> - let f (a,b) = (of_coq_assoc a, of_coq_position b) in - grammar_delete g (Option.map f reinit) ext; - camlp4_state := t; - remove_grammars (n-1) - | ByEXTEND (undo,redo)::t -> - undo(); - camlp4_state := t; - remove_grammars n; - redo(); - camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) - -let make_rule r = [None, None, r] - -(** An entry that checks we reached the end of the input. *) - -let eoi_entry en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in - let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in - let act = Gram.action (fun _ x loc -> x) in - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); - e - -let map_entry f en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in - let symbs = [Symbols.snterm (Gram.Entry.obj en)] in - let act = Gram.action (fun x loc -> f x) in - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); - e - -(* Parse a string, does NOT check if the entire string was read - (use eoi_entry) *) - -let parse_string f x = - let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) - -type gram_universe = string * (string, typed_entry) Hashtbl.t - -let trace = ref false - -(* The univ_tab is not part of the state. It contains all the grammars that - exist or have existed before in the session. *) - -let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t) - -let create_univ s = - let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u - -let uprim = create_univ "prim" -let uconstr = create_univ "constr" -let utactic = create_univ "tactic" -let uvernac = create_univ "vernac" - -let get_univ s = - try - Hashtbl.find univ_tab s - with Not_found -> - anomaly (Pp.str ("Unknown grammar universe: "^s)) - -let get_entry (u, utab) s = Hashtbl.find utab s - -let new_entry etyp (u, utab) s = - if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); - let ename = u ^ ":" ^ s in - let e = in_typed_entry etyp (Gram.entry_create ename) in - Hashtbl.add utab s e; e - -let create_entry (u, utab) s etyp = - try - let e = Hashtbl.find utab s in - if not (argument_type_eq (type_of_typed_entry e) etyp) then - failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); - e - with Not_found -> - new_entry etyp (u, utab) s - -let create_constr_entry s = - outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType) - -let create_generic_entry s wit = - outGramObj wit (create_entry utactic s (unquote wit)) - -(* [make_gen_entry] builds entries extensible by giving its name (a string) *) -(* For entries extensible only via the ML name, Gram.entry_create is enough *) - -let make_gen_entry (u,univ) rawwit s = - let e = Gram.entry_create (u ^ ":" ^ s) in - Hashtbl.add univ s (inGramObj rawwit e); e - -(* Initial grammar entries *) - -module Prim = - struct - let gec_gen x = make_gen_entry uprim x - - (* Entries that can be referred via the string -> Gram.entry table *) - (* Typically for tactic or vernac extensions *) - let preident = gec_gen (rawwit wit_pre_ident) "preident" - let ident = gec_gen (rawwit wit_ident) "ident" - let natural = gec_gen (rawwit wit_int) "natural" - let integer = gec_gen (rawwit wit_int) "integer" - let bigint = Gram.entry_create "Prim.bigint" - let string = gec_gen (rawwit wit_string) "string" - let reference = make_gen_entry uprim (rawwit wit_ref) "reference" - let by_notation = Gram.entry_create "by_notation" - let smart_global = Gram.entry_create "smart_global" - - (* parsed like ident but interpreted as a term *) - let var = gec_gen (rawwit wit_var) "var" - - let name = Gram.entry_create "Prim.name" - let identref = Gram.entry_create "Prim.identref" - let pattern_ident = Gram.entry_create "pattern_ident" - let pattern_identref = Gram.entry_create "pattern_identref" - - (* A synonym of ident - maybe ident will be located one day *) - let base_ident = Gram.entry_create "Prim.base_ident" - - let qualid = Gram.entry_create "Prim.qualid" - let fullyqualid = Gram.entry_create "Prim.fullyqualid" - let dirpath = Gram.entry_create "Prim.dirpath" - - let ne_string = Gram.entry_create "Prim.ne_string" - let ne_lstring = Gram.entry_create "Prim.ne_lstring" - - end - -module Constr = - struct - let gec_constr = make_gen_entry uconstr (rawwit wit_constr) - - (* Entries that can be referred via the string -> Gram.entry table *) - let constr = gec_constr "constr" - let operconstr = gec_constr "operconstr" - let constr_eoi = eoi_entry constr - let lconstr = gec_constr "lconstr" - let binder_constr = create_constr_entry "binder_constr" - let ident = make_gen_entry uconstr (rawwit wit_ident) "ident" - let global = make_gen_entry uconstr (rawwit wit_ref) "global" - let sort = make_gen_entry uconstr (rawwit wit_sort) "sort" - let pattern = Gram.entry_create "constr:pattern" - let constr_pattern = gec_constr "constr_pattern" - let lconstr_pattern = gec_constr "lconstr_pattern" - let closed_binder = Gram.entry_create "constr:closed_binder" - let binder = Gram.entry_create "constr:binder" - let binders = Gram.entry_create "constr:binders" - let open_binders = Gram.entry_create "constr:open_binders" - let binders_fixannot = Gram.entry_create "constr:binders_fixannot" - let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" - let record_declaration = Gram.entry_create "constr:record_declaration" - let appl_arg = Gram.entry_create "constr:appl_arg" - end - -module Module = - struct - let module_expr = Gram.entry_create "module_expr" - let module_type = Gram.entry_create "module_type" - end - -module Tactic = - struct - (* Main entry for extensions *) - let simple_tactic = Gram.entry_create "tactic:simple_tactic" - - (* Entries that can be referred via the string -> Gram.entry table *) - (* Typically for tactic user extensions *) - let open_constr = - make_gen_entry utactic (rawwit wit_open_constr) "open_constr" - let constr_with_bindings = - make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" - let bindings = - make_gen_entry utactic (rawwit wit_bindings) "bindings" - let hypident = Gram.entry_create "hypident" - let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" - let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" - let uconstr = - make_gen_entry utactic (rawwit wit_uconstr) "uconstr" - let quantified_hypothesis = - make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis" - let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var" - let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr" - let simple_intropattern = - make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern" - let clause_dft_concl = - make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause" - - - (* Main entries for ltac *) - let tactic_arg = Gram.entry_create "tactic:tactic_arg" - let tactic_expr = Gram.entry_create "tactic:tactic_expr" - let binder_tactic = Gram.entry_create "tactic:binder_tactic" - - let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic" - - (* Main entry for quotations *) - let tactic_eoi = eoi_entry tactic - - (* For Ltac definition *) - let tacdef_body = Gram.entry_create "tactic:tacdef_body" - - end - -module Vernac_ = - struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) - - (* The different kinds of vernacular commands *) - let gallina = gec_vernac "gallina" - let gallina_ext = gec_vernac "gallina_ext" - let command = gec_vernac "command" - let syntax = gec_vernac "syntax_command" - let vernac = gec_vernac "Vernac.vernac" - let vernac_eoi = eoi_entry vernac - let rec_definition = gec_vernac "Vernac.rec_definition" - (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" - - let () = - let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in - let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac ); - ] in - maybe_uncurry (Gram.extend main_entry) (None, make_rule rule) - - end - -let main_entry = Vernac_.main_entry - -(**********************************************************************) -(* This determines (depending on the associativity of the current - level and on the expected associativity) if a reference to constr_n is - a reference to the current level (to be translated into "SELF" on the - left border and into "constr LEVEL n" elsewhere), to the level below - (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level - (to be translated into "constr LEVEL n") - - The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the - converse of the extension mechanism *) - -let constr_level = string_of_int - -let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 10,Extend.RightA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 11,Extend.LeftA,false; - 10,Extend.RightA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let level_stack = - ref [(default_levels, default_pattern_levels)] - -(* At a same level, LeftA takes precedence over RightA and NoneA *) -(* In case, several associativity exists for a level, we make two levels, *) -(* first LeftA, then RightA and NoneA together *) - -let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false - | _ -> true - -let create_assoc = function - | None -> Extend.RightA - | Some a -> a - -let error_level_assoc p current expected = - let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in - errorlabstrm "" - (str "Level " ++ int p ++ str " is already declared " ++ - pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative.") - -let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) - -let find_position_gen forpat ensure assoc lev = - let ccurrent,pcurrent as current = List.hd !level_stack in - match lev with - | None -> - level_stack := current :: !level_stack; - None, None, None, None - | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = - if forpat then (ccurrent, add_level None pcurrent) - else (add_level None ccurrent, pcurrent) in - level_stack := updated:: !level_stack; - let assoc = create_assoc assoc in - begin match !init with - | None -> - (* Create the entry *) - Some (create_pos !after), Some assoc, Some (constr_level n), None - | _ -> - (* The reinit flag has been updated *) - Some (Extend.Level (constr_level n)), None, None, !init - end - with - (* Nothing has changed *) - Exit -> - level_stack := current :: !level_stack; - (* Just inherit the existing associativity and name (None) *) - Some (Extend.Level (constr_level n)), None, None, None - -let remove_levels n = - level_stack := List.skipn n !level_stack - -let rec list_mem_assoc_triple x = function - | [] -> false - | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l - -let register_empty_levels forpat levels = - let filter n = - try - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - if not (list_mem_assoc_triple n levels) then - Some (find_position_gen forpat true None (Some n)) - else None - with Failure _ -> None - in - List.map_filter filter levels - -let find_position forpat assoc level = - find_position_gen forpat false assoc level - -(* Synchronise the stack of level updates *) -let synchronize_level_positions () = - let _ = find_position true None None in () - -(**********************************************************************) -(* Binding constr entry keys to entries *) - -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function - | Some Extend.NonA | Some Extend.RightA -> Extend.RightA - | None | Some Extend.LeftA -> Extend.LeftA - -let assoc_eq al ar = match al, ar with -| Extend.NonA, Extend.NonA -| Extend.RightA, Extend.RightA -| Extend.LeftA, Extend.LeftA -> true -| _, _ -> false - -(* [adjust_level assoc from prod] where [assoc] and [from] are the name - and associativity of the level where to add the rule; the meaning of - the result is - - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function -(* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) -(* Compute production name on the right side *) - (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) -> - Some None - (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some Extend.RightA)) -> - Some (Some (n,true)) -(* Compute production name on the left side *) - (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None - (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> - None - (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | Extend.LeftA -> Some (Some (n, true)) - | _ -> Some None - end - (* None means NEXT *) - | (NextLevel,_) -> Some None -(* Compute production name elsewhere *) - | (NumLevel n,InternalProd) -> - match from with - | ETConstr (p,()) when Int.equal p (n + 1) -> Some None - | ETConstr (p,()) -> Some (Some (n, Int.equal n p)) - | _ -> Some (Some (n,false)) - -let compute_entry allow_create adjust forpat = function - | ETConstr (n,q) -> - (if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr), - adjust (n,q), false - | ETName -> weaken_entry Prim.name, None, false - | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") - | ETBinder false -> weaken_entry Constr.binder, None, false - | ETBinderList (true,tkl) -> - let () = match tkl with [] -> () | _ -> assert false in - weaken_entry Constr.open_binders, None, false - | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") - | ETBigint -> weaken_entry Prim.bigint, None, false - | ETReference -> weaken_entry Constr.global, None, false - | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") - | ETOther (u,n) -> - let u = get_univ u in - let e = - try get_entry u n - with Not_found when allow_create -> create_entry u n ConstrArgType in - object_of_typed_entry e, None, true - -(* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key forpat = function - | ETConstr(200,()) when not forpat -> - weaken_entry Constr.binder_constr, None - | e -> - let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in - (e, level) - -(* This computes the name to give to a production knowing the name and - associativity of the level where it must be added *) -let interp_constr_prod_entry_key ass from forpat en = - compute_entry false (adjust_level ass from) forpat en - -(**********************************************************************) -(* Binding constr entry keys to symbols *) - -let is_self from e = - match from, e with - ETConstr(n,()), ETConstr(NumLevel n', - BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false - | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n' - | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint - | ETPattern, ETPattern) -> true - | ETOther(s1,s2), ETOther(s1',s2') -> - String.equal s1 s1' && String.equal s2 s2' - | _ -> false - -let is_binder_level from e = - match from, e with - ETConstr(200,()), - ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true - | _ -> false - -let make_sep_rules tkl = - Gram.srules' - [List.map gram_token_of_token tkl, - List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl - (Gram.action (fun loc -> ()))] - -let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - if is_binder_level from typ then - if forpat then - Symbols.snterml (Gram.Entry.obj Constr.pattern,"200") - else - Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200") - else if is_self from typ then - Symbols.sself - else - match typ with - | ETConstrList (typ',[]) -> - Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) - | ETBinderList (false,[]) -> - Symbols.slist1 - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) - | ETBinderList (false,tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) - - | _ -> - match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj) - | (eobj,Some None,_) -> Symbols.snext - | (eobj,Some (Some (lev,cur)),_) -> - Symbols.snterml (Gram.Entry.obj eobj,constr_level lev) - -(** Binding general entry keys to symbol *) - -let rec symbol_of_prod_entry_key = function - | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) - | Amodifiers s -> - Gram.srules' - [([], Gram.action (fun _loc -> [])); - ([gram_token_of_string "("; - Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string ","); - gram_token_of_string ")"], - Gram.action (fun _ l _ _loc -> l))] - | Aself -> Symbols.sself - | Anext -> Symbols.snext - | Atactic 5 -> Symbols.snterm (Gram.Entry.obj Tactic.binder_tactic) - | Atactic n -> - Symbols.snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) - | Agram s -> - let e = - try - (** ppedrot: we should always generate Agram entries which have already - been registered, so this should not fail. *) - let (u, s) = match String.split ':' s with - | u :: s :: [] -> (u, s) - | _ -> raise Not_found - in - get_entry (get_univ u) s - with Not_found -> - Errors.anomaly (str "Unregistered grammar entry: " ++ str s) - in - Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) - | Aentry (u,s) -> - let e = get_entry (get_univ u) s in - Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) - -let level_of_snterml e = int_of_string (Symbols.snterml_level e) - -(**********************************************************************) -(* Interpret entry names of the form "ne_constr_list" as entry keys *) - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - -let tactic_level s = - if Int.equal (String.length s) 7 && coincide s "tactic" 0 then - let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) - else None - else None - -let type_of_entry u s = - type_of_typed_entry (get_entry u s) - -let rec interp_entry_name static up_level s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in - ListArgType t, Alist1 g - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in - ListArgType t, Alist1sep (g,sep) - else if l > 5 && coincide s "_list" (l-5) then - let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in - ListArgType t, Alist0 g - else if l > 9 && coincide s "_list_sep" (l-9) then - let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in - ListArgType t, Alist0sep (g,sep) - else if l > 4 && coincide s "_opt" (l-4) then - let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in - OptArgType t, Aopt g - else if l > 5 && coincide s "_mods" (l-5) then - let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in - ListArgType t, Amodifiers g - else - let s = match s with "hyp" -> "var" | _ -> s in - let check_lvl n = match up_level with - | None -> false - | Some m -> Int.equal m n - && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) - && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) - in - let t, se = - match tactic_level s with - | Some n -> - (** Quite ad-hoc *) - let t = unquote (rawwit wit_tactic) in - let se = - if check_lvl n then Aself - else if check_lvl (n + 1) then Anext - else Atactic n - in - (Some t, se) - | None -> - try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found -> - try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found -> - try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found -> - if static then - error ("Unknown entry "^s^".") - else - None, Aentry ("",s) in - let t = - match t with - | Some t -> t - | None -> ExtraArgType s in - t, se - -let list_entry_names () = - let add_entry key (entry, _) accu = (key, entry) :: accu in - let ans = Hashtbl.fold add_entry (snd uprim) [] in - let ans = Hashtbl.fold add_entry (snd uconstr) ans in - Hashtbl.fold add_entry (snd utactic) ans -- cgit v1.2.3