diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 18:34:39 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 18:54:04 +0100 |
commit | 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (patch) | |
tree | 027928408f8e28263edf98a5bd58cd96d43dffca | |
parent | d3653c6da5770dfc4d439639b49193e30172763a (diff) |
Moving Ltac traces to Tacexpr and Tacinterp.
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | intf/tacexpr.mli | 12 | ||||
-rw-r--r-- | proofs/proof_type.ml | 52 | ||||
-rw-r--r-- | proofs/proof_type.mli | 16 | ||||
-rw-r--r-- | proofs/proofs.mllib | 1 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
-rw-r--r-- | tactics/tacsubst.mli | 4 | ||||
-rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
-rw-r--r-- | toplevel/himsg.ml | 22 | ||||
-rw-r--r-- | toplevel/himsg.mli | 2 |
12 files changed, 35 insertions, 83 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 39e4b1cdb..34bde1ac2 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -174,7 +174,6 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Proof_type Goal Miscprint Logic diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f2a567c00..b1dc174d4 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -394,3 +394,15 @@ type tactic_arg = type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen + +(** Traces *) + +type ltac_call_kind = + | LtacMLCall of glob_tactic_expr + | LtacNotationCall of KerName.t + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr + | LtacVarCall of Id.t * glob_tactic_expr + | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + +type ltac_trace = (Loc.t * ltac_call_kind) list diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index dd2c7b253..000000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i*) -open Evd -open Names -open Term -open Tacexpr -open Glob_term -open Nametab -open Misctypes -(*i*) - -(* This module defines the structure of proof tree and the tactic type. So, it - is used by Proof_tree and Refiner *) - -(** Types of goals, tactics, rules ... *) - -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma - -type prim_rule = - | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int - | Cofix of Id.t * (Id.t * constr) list * int - | Refine of constr - | Thin of Id.t list - | Move of Id.t * Id.t move_location - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -(** Ltac traces *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index aa05f58ab..b4c9dae2a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -57,19 +57,3 @@ type rule = prim_rule type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -(** Ltac traces *) - -(** TODO: Move those definitions somewhere sensible *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -val ltac_trace_info : ltac_trace Exninfo.t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 1bd701cb9..47a637575 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,7 +2,6 @@ Miscprint Goal Evar_refiner Proof_using -Proof_type Proof_errors Logic Proofview diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index bf5f9ddc8..82252610a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,6 +44,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +let ltac_trace_info = Tacsubst.ltac_trace_info + let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in match Val.eq t (val_tag wit) with diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index c5da3494c..31327873e 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -14,6 +14,8 @@ open Genarg open Redexpr open Misctypes +val ltac_trace_info : ltac_trace Exninfo.t + module Value : sig type t = Val.t diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 55941c1ca..17cb8ad19 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -18,6 +18,8 @@ open Genredexpr open Patternops open Pretyping +let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () + (** Substitution of tactics at module closing time *) (** For generic arguments, we declare and store substitutions diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli index c1bf27257..8b686c5ce 100644 --- a/tactics/tacsubst.mli +++ b/tactics/tacsubst.mli @@ -11,6 +11,10 @@ open Mod_subst open Genarg open Misctypes +(** TODO: Move those definitions somewhere sensible *) + +val ltac_trace_info : ltac_trace Exninfo.t + (** Substitution of tactics at module closing time *) val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 600683d35..91ef45393 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -120,7 +120,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, let err = Errors.make_anomaly msg in Util.iraise (err, info) in - let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in + let ltac_trace = Exninfo.get info Tacsubst.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with | None -> e diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index de7ec61c8..1af09dd84 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1247,9 +1247,9 @@ let explain_reduction_tactic_error = function let is_defined_ltac trace = let rec aux = function - | (_, Proof_type.LtacNameCall f) :: tail -> + | (_, Tacexpr.LtacNameCall f) :: tail -> not (Tacenv.is_ltac_for_ml_tactic f) - | (_, Proof_type.LtacAtomCall _) :: tail -> + | (_, Tacexpr.LtacAtomCall _) :: tail -> false | _ :: tail -> aux tail | [] -> false in @@ -1258,17 +1258,17 @@ let is_defined_ltac trace = let explain_ltac_call_trace last trace loc = let calls = last :: List.rev_map snd trace in let pr_call ck = match ck with - | Proof_type.LtacNotationCall kn -> quote (KerName.print kn) - | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) - | Proof_type.LtacMLCall t -> + | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn) + | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) + | Tacexpr.LtacMLCall t -> quote (Pptactic.pr_glob_tactic (Global.env()) t) - | Proof_type.LtacVarCall (id,t) -> + | Tacexpr.LtacVarCall (id,t) -> quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" - | Proof_type.LtacAtomCall te -> + | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.ghost,te))) - | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> quote (pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ @@ -1282,7 +1282,7 @@ let explain_ltac_call_trace last trace loc = | [] -> mt () | _ -> let kind_of_last_call = match List.last calls with - | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed." + | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed." | _ -> ", last call failed." in hov 0 (str "In nested Ltac calls to " ++ @@ -1290,9 +1290,9 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Proof_type.LtacNameCall f as tac) :: _ + | (_,Tacexpr.LtacNameCall f as tac) :: _ when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac) + | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) :: _ -> [tac] | t :: tail -> t :: aux tail | [] -> [] in diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 3ef98380b..50bbd15c6 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -37,7 +37,7 @@ val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds val extract_ltac_trace : - Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t + Tacexpr.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t val explain_module_error : Modops.module_typing_error -> std_ppcmds |