diff options
Diffstat (limited to 'parsing/egramcoq.ml')
| -rw-r--r-- | parsing/egramcoq.ml | 110 |
1 files changed, 0 insertions, 110 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 5e89567cc4..f0c12ab8ef 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -224,27 +224,6 @@ let extend_constr_notation (_, ng) = let nb' = extend_constr_pat_notation ng in nb + nb' -(**********************************************************************) -(** Grammar declaration for Tactic Notation (Coq level) *) - -let get_tactic_entry n = - if Int.equal n 0 then - Tactic.simple_tactic, None - else if Int.equal n 5 then - Tactic.binder_tactic, None - else if 1<=n && n<5 then - Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) - else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") - -(**********************************************************************) -(** State of the grammar extensions *) - -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; -} - module GrammarCommand = Dyn.Make(struct end) module GrammarInterp = struct type 'a t = 'a -> int end module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) @@ -260,57 +239,6 @@ let create_grammar_command name interp : _ grammar_command = let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in obj -(** ML Tactic grammar extensions *) - -let add_ml_tactic_entry (name, prods) = - let entry = Tactic.simple_tactic in - let mkact i loc l : raw_tactic_expr = - let open Tacexpr in - let entry = { mltac_name = name; mltac_index = i } in - let map arg = TacGeneric arg in - TacML (loc, entry, List.map map l) - in - let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in - synchronize_level_positions (); - grammar_extend entry None (None, [(None, None, List.rev rules)]); - 1 - -(* Declaration of the tactic grammar rule *) - -let head_is_ident tg = match tg.tacgram_prods with -| GramTerminal _::_ -> true -| _ -> false - -(** Tactic grammar extensions *) - -let add_tactic_entry (kn, tg) = - let entry, pos = get_tactic_entry tg.tacgram_level in - let mkact loc l = - let filter = function - | GramTerminal _ -> None - | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t) - in - let types = List.map_filter filter tg.tacgram_prods in - let map arg t = - (** HACK to handle especially the tactic(...) entry *) - let wit = Genarg.rawwit Constrarg.wit_tactic in - if Genarg.argument_type_eq t (Genarg.unquote wit) then - Tacexp (Genarg.out_gen wit arg) - else - TacGeneric arg - in - let l = List.map2 map l types in - (TacAlias (loc,kn,l):raw_tactic_expr) - in - let () = - if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then - error "Notation for simple tactic must start with an identifier." - in - let rules = make_rule mkact tg.tacgram_prods in - synchronize_level_positions (); - grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - 1 - let extend_grammar tag g = let nb = GrammarInterpMap.find tag !grammar_interp g in grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state @@ -320,15 +248,7 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag = create_grammar_command "Notation" extend_constr_notation -let tactic_grammar = - create_grammar_command "TacticGrammar" add_tactic_entry - -let ml_tactic_grammar = - create_grammar_command "MLTacticGrammar" add_ml_tactic_entry - let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn) -let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn) -let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn) let recover_constr_grammar ntn prec = let filter (_, gram) : notation_grammar option = match gram with @@ -386,33 +306,3 @@ let with_grammar_rule_protection f x = let reraise = Errors.push reraise in let () = unfreeze fs in iraise reraise - -(**********************************************************************) -(** Ltac quotations *) - -let ltac_quotations = ref String.Set.empty - -let create_ltac_quotation name cast (e, l) = - let () = - if String.Set.mem name !ltac_quotations then - failwith ("Ltac quotation " ^ name ^ " already registered") - in - let () = ltac_quotations := String.Set.add name !ltac_quotations in - let entry = match l with - | None -> Aentry (name_of_entry e) - | Some l -> Aentryl (name_of_entry e, l) - in -(* let level = Some "1" in *) - let level = None in - let assoc = None in - let rule = - Next (Next (Next (Next (Next (Stop, - Atoken (Lexer.terminal name)), - Atoken (Lexer.terminal ":")), - Atoken (Lexer.terminal "(")), - entry), - Atoken (Lexer.terminal ")")) - in - let action _ v _ _ _ loc = cast (loc, v) in - let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) |