Moving most of Ltac code to Hightactics.

This is a major step towards the pluginification of Ltac. The one important
file that is out of reach for now is Tacsubst, as it is used in an intricate way
to handle amongst other things auto hints.

6 files changed, 15 insertions, 275 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e5edc74222..6277a8146a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -43,176 +43,6 @@ let inToken : string -> obj =
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (**********************************************************************)
-(* Tactic Notation                                                    *)
-
-let interp_prod_item lev = function
-  | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, nt, (_, sep)) ->
-      let EntryName (etyp, e) = interp_entry_name lev nt sep in
-      GramNonTerminal (loc, etyp, e)
-
-let make_terminal_status = function
-  | GramTerminal s -> Some s
-  | GramNonTerminal _ -> None
-
-let make_fresh_key =
-  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
-  fun () ->
-    let cur = incr id; !id in
-    let lbl = Id.of_string ("_" ^ string_of_int cur) in
-    let kn = Lib.make_kn lbl in
-    let (mp, dir, _) = KerName.repr kn in
-    (** We embed the full path of the kernel name in the label so that the
-        identifier should be unique. This ensures that including two modules
-        together won't confuse the corresponding labels. *)
-    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
-      (ModPath.to_string mp) (DirPath.to_string dir) cur)
-    in
-    KerName.make mp dir (Label.of_id lbl)
-
-type tactic_grammar_obj = {
-  tacobj_key : KerName.t;
-  tacobj_local : locality_flag;
-  tacobj_tacgram : tactic_grammar;
-  tacobj_tacpp : Pptactic.pp_tactic;
-  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
-}
-
-let check_key key =
-  if Tacenv.check_alias key then
-    error "Conflicting tactic notations keys. This can happen when including \
-    twice the same module."
-
-let cache_tactic_notation (_, tobj) =
-  let key = tobj.tacobj_key in
-  let () = check_key key in
-  Tacenv.register_alias key tobj.tacobj_body;
-  Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
-  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
-
-let open_tactic_notation i (_, tobj) =
-  let key = tobj.tacobj_key in
-  if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-let load_tactic_notation i (_, tobj) =
-  let key = tobj.tacobj_key in
-  let () = check_key key in
-  (** Only add the printing and interpretation rules. *)
-  Tacenv.register_alias key tobj.tacobj_body;
-  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
-  if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-let subst_tactic_notation (subst, tobj) =
-  let (ids, body) = tobj.tacobj_body in
-  { tobj with
-    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
-  }
-
-let classify_tactic_notation tacobj = Substitute tacobj
-
-let inTacticGrammar : tactic_grammar_obj -> obj =
-  declare_object {(default_object "TacticGrammar") with
-       open_function = open_tactic_notation;
-       load_function = load_tactic_notation;
-       cache_function = cache_tactic_notation;
-       subst_function = subst_tactic_notation;
-       classify_function = classify_tactic_notation}
-
-let cons_production_parameter = function
-| TacTerm _ -> None
-| TacNonTerm (_, _, (id, _)) -> Some id
-
-let add_tactic_notation (local,n,prods,e) =
-  let ids = List.map_filter cons_production_parameter prods in
-  let prods = List.map (interp_prod_item n) prods in
-  let pprule = {
-    Pptactic.pptac_level = n;
-    pptac_prods = prods;
-  } in
-  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  let parule = {
-    tacgram_level = n;
-    tacgram_prods = prods;
-  } in
-  let tacobj = {
-    tacobj_key = make_fresh_key ();
-    tacobj_local = local;
-    tacobj_tacgram = parule;
-    tacobj_tacpp = pprule;
-    tacobj_body = (ids, tac);
-  } in
-  Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-
-(**********************************************************************)
-(* ML Tactic entries                                                  *)
-
-type ml_tactic_grammar_obj = {
-  mltacobj_name : Tacexpr.ml_tactic_name;
-  (** ML-side unique name *)
-  mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
-  (** Grammar rules generating the ML tactic. *)
-}
-
-exception NonEmptyArgument
-
-(** ML tactic notations whose use can be restricted to an identifier are added
-    as true Ltac entries. *)
-let extend_atomic_tactic name entries =
-  let open Tacexpr in
-  let map_prod prods =
-    let (hd, rem) = match prods with
-    | GramTerminal s :: rem -> (s, rem)
-    | _ -> assert false (** Not handled by the ML extension syntax *)
-    in
-    let empty_value = function
-    | GramTerminal s -> raise NonEmptyArgument
-    | GramNonTerminal (_, typ, e) ->
-      let Genarg.Rawwit wit = typ in
-      let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
-      let default = epsilon_value inj e in
-      match default with
-      | None -> raise NonEmptyArgument
-      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
-    in
-    try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
-  in
-  let entries = List.map map_prod entries in
-  let add_atomic i args = match args with
-  | None -> ()
-  | Some (id, args) ->
-    let args = List.map (fun a -> Tacexp a) args in
-    let entry = { mltac_name = name; mltac_index = i } in
-    let body = TacML (Loc.ghost, entry, args) in
-    Tacenv.register_ltac false false (Names.Id.of_string id) body
-  in
-  List.iteri add_atomic entries
-
-let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
-
-let open_ml_tactic_notation i obj =
-  if Int.equal i 1 then cache_ml_tactic_notation obj
-
-let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
-  declare_object { (default_object "MLTacticGrammar") with
-    open_function = open_ml_tactic_notation;
-    cache_function = cache_ml_tactic_notation;
-    classify_function = (fun o -> Substitute o);
-    subst_function = (fun (_, o) -> o);
-  }
-
-let add_ml_tactic_notation name prods =
-  let obj = {
-    mltacobj_name = name;
-    mltacobj_prod = prods;
-  } in
-  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
-  extend_atomic_tactic name prods
-
-(**********************************************************************)
 (* Printing grammar entries                                           *)
 
 let entry_buf = Buffer.create 64
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 5d01405b27..085cc87c8b 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -15,15 +15,6 @@ open Notation_term
 
 val add_token_obj : string -> unit
 
-(** Adding a tactic notation in the environment *)
-
-val add_tactic_notation :
-  locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
-    unit
-
-val add_ml_tactic_notation : ml_tactic_name ->
-  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
-
 (** Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 44c83be46c..b2fc456d07 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -323,8 +323,7 @@ let get_info x =
 
 let assumption_message = Declare.assumption_message
 
-let (set_default_tactic, get_default_tactic, print_default_tactic) = 
-  Tactic_option.declare_tactic_option "Program tactic"
+let default_tactic = ref (Proofview.tclUNIT ())
 
 (* true = All transparent, false = Opaque if possible *)
 let proofs_transparency = ref true
@@ -895,7 +894,7 @@ let rec solve_obligation prg num tac =
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
   let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
             Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
-  let _ = Pfedit.by (snd (get_default_tactic ())) in
+  let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
@@ -924,7 +923,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      | None ->
 		  match obl.obl_tac with
 		  | Some t -> t
-		  | None -> snd (get_default_tactic ())
+		  | None -> !default_tactic
 	    in
 	    let evd = Evd.from_ctx !prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index e257da0161..3e99f5760b 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -54,10 +54,8 @@ type progress = (* Resolution status of a program *)
   | Remain of int  (* n obligations remaining *)
   | Dependent (* Dependent on other definitions *)
   | Defined of global_reference (* Defined as id *)
-      
-val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * unit Proofview.tactic
-val print_default_tactic : unit -> Pp.std_ppcmds
+
+val default_tactic : unit Proofview.tactic ref
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ba5eb3f7d..bdd52d5be0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -20,7 +20,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Tacinterp
 open Command
 open Goptions
 open Libnames
@@ -34,6 +33,9 @@ open Misctypes
 open Locality
 open Sigma.Notations
 
+(** TODO: make this function independent of Ltac *)
+let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
+
 let debug = false
 let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
@@ -471,7 +473,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
           | None -> None
           | Some r ->
 	      let (evc,env)= get_current_context () in
- 		Some (snd (interp_redexp env evc r)) in
+ 		Some (snd (Hook.get f_interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l lettop =
@@ -912,81 +914,6 @@ let vernac_restore_state file =
 (************)
 (* Commands *)
 
-type tacdef_kind =
-  | NewTac of Id.t
-  | UpdateTac of Nametab.ltac_constant
-
-let is_defined_tac kn =
-  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
-
-let register_ltac local tacl =
-  let map tactic_body =
-    match tactic_body with
-    | TacticDefinition ((loc,id), body) ->
-        let kn = Lib.make_kn id in
-        let id_pp = pr_id id in
-        let () = if is_defined_tac kn then
-          Errors.user_err_loc (loc, "",
-            str "There is already an Ltac named " ++ id_pp ++ str".")
-        in
-        let is_primitive =
-          try
-            match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
-            | Tacexpr.TacArg _ -> false
-            | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
-          with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
-        in
-        let () = if is_primitive then
-          msg_warning (str "The Ltac name " ++ id_pp ++
-            str " may be unusable because of a conflict with a notation.")
-        in
-        NewTac id, body
-    | TacticRedefinition (ident, body) ->
-        let loc = loc_of_reference ident in
-        let kn =
-          try Nametab.locate_tactic (snd (qualid_of_reference ident))
-          with Not_found ->
-            Errors.user_err_loc (loc, "",
-                        str "There is no Ltac named " ++ pr_reference ident ++ str ".")
-        in
-        UpdateTac kn, body
-  in
-  let rfun = List.map map tacl in
-  let recvars =
-    let fold accu (op, _) = match op with
-    | UpdateTac _ -> accu
-    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
-    in
-    List.fold_left fold [] rfun
-  in
-  let ist = Tacintern.make_empty_glob_sign () in
-  let map (name, body) =
-    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
-    (name, body)
-  in
-  let defs () =
-    (** Register locally the tactic to handle recursivity. This function affects
-        the whole environment, so that we transactify it afterwards. *)
-    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
-    let () = List.iter iter_rec recvars in
-    List.map map rfun
-  in
-  let defs = Future.transactify defs () in
-  let iter (def, tac) = match def with
-  | NewTac id ->
-    Tacenv.register_ltac false local id tac;
-    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
-  | UpdateTac kn ->
-    Tacenv.redefine_ltac local kn tac;
-    let name = Nametab.shortest_qualid_of_tactic kn in
-    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
-  in
-  List.iter iter defs
-
-let vernac_declare_tactic_definition locality def =
-  let local = make_module_locality locality in
-  register_ltac local def
-
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in
   Hints.create_hint_db local id full_transparent_state b
@@ -1500,8 +1427,7 @@ let vernac_check_may_eval redexp glopt rc =
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
-        Tacintern.dump_glob_red_expr r;
-        let (sigma',r_interp) = interp_redexp env sigma' r in
+        let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
 	let redfun env evm c =
           let (redfun, _) = reduction_of_red_expr env r_interp in
           let evm = Sigma.Unsafe.of_evar_map evm in
@@ -1512,7 +1438,7 @@ let vernac_check_may_eval redexp glopt rc =
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
-  declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r))
+  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
@@ -1580,7 +1506,6 @@ let vernac_print = function
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
@@ -1820,8 +1745,6 @@ let interp ?proof ~loc locality poly c =
   | VernacError e -> raise e
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) ->
-      Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)
   | VernacSyntaxExtension (local,sl) ->
       vernac_syntax_extension locality local sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
@@ -1899,8 +1822,6 @@ let interp ?proof ~loc locality poly c =
   | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
 
   (* Commands *)
-  | VernacDeclareTacticDefinition def ->
-      vernac_declare_tactic_definition locality def
   | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
   | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
   | VernacHints (local,dbnames,hints) ->
@@ -1976,15 +1897,13 @@ let check_vernac_supports_locality c l =
   match l, c with
   | None, _ -> ()
   | Some _, (
-      VernacTacticNotation _
-    | VernacOpenCloseScope _
+      VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacDeclareMLModule _
-    | VernacDeclareTacticDefinition _
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
     | VernacSyntacticDefinition _
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4a59b1299b..4e7fa4a087 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -61,3 +61,6 @@ val vernac_end_proof :
 val with_fail : bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
+
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+  Evd.evar_map * Redexpr.red_expr) Hook.t