From 8e10368c387570df13904531bfba05130335ed0e Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 10:08:24 +0000 Subject: Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box Nested was never constructed, while the notion of abstract_tactic_box is obsolete (cf. Refiner.abstract_tactic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/dumptree.ml4 | 7 ------ plugins/xml/proofTree2Xml.ml4 | 51 ------------------------------------------- printing/tactic_printer.ml | 17 +-------------- proofs/proof_type.ml | 6 ++--- proofs/proof_type.mli | 7 ++---- proofs/refiner.ml | 17 ++++----------- proofs/refiner.mli | 6 ++--- tactics/tacinterp.ml | 9 ++------ toplevel/himsg.ml | 19 ++++------------ 9 files changed, 18 insertions(+), 121 deletions(-) diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 623d7c804..c29e4a3b3 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -47,13 +47,6 @@ let pr_proof_instr_xml instr = let pr_rule_xml pr = function | Prim r -> str "" - | Nested(cmpd, subtree) -> - hov 2 (str "" ++ fnl () ++ - begin match cmpd with - Tactic (texp, _) -> pr_tactic_xml texp - end ++ fnl () - ++ pr subtree - ) ++ fnl () ++ str "" | Daimon -> str "" | Decl_proof _ -> str "" ;; diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 033e83410..3831ee9fa 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -113,57 +113,6 @@ Pp.msg_warning (Pp.(++) (Pp.str (List.fold_left (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) - | {PT.goal=goal; - PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} -> - (* [hidden_proof] is the proof of the tactic; *) - (* [nodes] are the proof of the subgoals generated by the tactic; *) - (* [flat_proof] if the proof-tree obtained substituting [nodes] *) - (* for the holes in [hidden_proof] *) - let flat_proof = - Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node - in begin - match tactic_expr with - | Tacexpr.TacArg (_,Tacexpr.Tacexp _) -> - (* We don't need to keep the level of abstraction introduced at *) - (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) - aux flat_proof old_hyps - | _ -> - (****** la tactique employee *) - let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = Pp.string_of_ppcmds (prtac tactic_expr) in - let tacname= first_word tac in - let of_attribute = ("name",tacname)::("script",tac)::of_attribute in - - (****** le but *) - - let concl = Goal.V82.concl sigma goal in - let hyps = Goal.V82.hyps sigma goal in - - let env = Global.env_of_context hyps in - - - let xgoal = - X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in - - let rec build_hyps = - function - | [] -> xgoal - | (id,c,tid)::hyps1 -> - let id' = Names.string_of_id id in - [< build_hyps hyps1; - (X.xml_nempty "Hypothesis" - ["id",idref_of_id id' ; "name",id'] - (constr_to_xml tid sigma env)) - >] in - let old_names = List.map (fun (id,c,tid)->id) old_hyps in - let nhyps = Environ.named_context_of_val hyps in - let new_hyps = - List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in - - X.xml_nempty "Tactic" of_attribute - [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] - end - | {PT.ref=Some(PT.Daimon,_)} -> X.xml_empty "Hidden_open_goal" of_attribute diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml index 87bb89e8d..49d7c21f6 100644 --- a/printing/tactic_printer.ml +++ b/printing/tactic_printer.ml @@ -23,31 +23,16 @@ let pr_tactic = function let pr_rule = function | Prim r -> hov 0 (pr_prim_rule r) - | Nested(cmpd,_) -> - begin - match cmpd with - | Tactic (texp,_) -> hov 0 (pr_tactic texp) - end | Daimon -> str "" | Decl_proof _ -> str "proof" -let uses_default_tac = function - | Nested(Tactic(_,dflt),_) -> dflt - | _ -> false - (* Does not print change of evars *) let pr_rule_dot = function | Prim Change_evars ->str "PC: ch_evars" ++ mt () (* PC: this might be redundant *) - | r -> - pr_rule r ++ if uses_default_tac r then str "..." else str"." + | r -> pr_rule r ++ str"." let pr_rule_dot_fnl = function - | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_) - | TacMutualCofix (true,_,_))),_),_) -> - (* Very big hack to not display hidden tactics in "Theorem with" *) - (* (would not scale!) *) - mt () | Prim Change_evars -> mt () | r -> pr_rule_dot r ++ fnl () diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 1f5ef315b..4652bac2e 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -46,11 +46,10 @@ type proof_tree = { and rule = | Prim of prim_rule - | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon -and compound_rule= +type compound_rule= | Tactic of tactic_expr * bool and tactic_expr = @@ -89,7 +88,7 @@ and tactic_arg = type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref + | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of identifier * glob_tactic_expr | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) @@ -98,4 +97,3 @@ type ltac_trace = (int * Loc.t * ltac_call_kind) list exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn -let abstract_tactic_box = ref (ref None) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 4f7e87ea9..d6081e56c 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -79,11 +79,10 @@ type proof_tree = { and rule = | Prim of prim_rule - | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon -and compound_rule= +type compound_rule= (** the boolean of Tactic tells if the default tactic is used *) | Tactic of tactic_expr * bool @@ -123,7 +122,7 @@ and tactic_arg = type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref + | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of identifier * glob_tactic_expr | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) @@ -131,5 +130,3 @@ type ltac_call_kind = type ltac_trace = (int * Loc.t * ltac_call_kind) list exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn - -val abstract_tactic_box : atomic_tactic_expr option ref ref diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 4f75ffa52..87ba77dc5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -23,18 +23,9 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let abstract_operation syntax semantics = - semantics - -let abstract_tactic_expr ?(dflt=false) te tacfun gls = - abstract_operation (Tactic(te,dflt)) tacfun gls - -let abstract_tactic ?(dflt=false) te = - !abstract_tactic_box := Some te; - abstract_tactic_expr ~dflt (Tacexpr.TacAtom (Loc.ghost,te)) - -let abstract_extended_tactic ?(dflt=false) s args = - abstract_tactic ~dflt (Tacexpr.TacExtend (Loc.ghost, s, args)) +let abstract_tactic_expr ?(dflt=false) te tacfun = tacfun +let abstract_tactic ?(dflt=false) te tacfun = tacfun +let abstract_extended_tactic ?(dflt=false) s args tacfun = tacfun let refiner = function | Prim pr -> @@ -44,7 +35,7 @@ let refiner = function {it=sgl; sigma = sigma'}) - | Nested (_,_) | Decl_proof _ -> + | Decl_proof _ -> failwith "Refiner: should not occur" (* Daimon is a canonical unfinished proof *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index b5fc9ee66..6f11e7115 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -30,9 +30,9 @@ val apply_sig_tac : (** [abstract_tactic tac] hides the (partial) proof produced by [tac] under a single proof node. The boolean tells if the default tactic is used. *) -(* spiwack: currently here for compatibility, abstract_operation - is a second projection *) -val abstract_operation : compound_rule -> tactic -> tactic +(* spiwack: currently here for compatibility, the tactic expression + is discarded and we simply return the tactic. *) + val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic val abstract_extended_tactic : diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0c7d6e0ca..12c970d68 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -227,11 +227,7 @@ let lookup_tactic s = with Not_found -> errorlabstrm "Refiner.lookup_tactic" (str"The tactic " ++ str s ++ str" is not installed.") -(* -let vernac_tactic (s,args) = - let tacfun = lookup_tactic s args in - abstract_extended_tactic s args tacfun -*) + (* Interpretation of extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; @@ -1783,8 +1779,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = and eval_tactic ist = function | TacAtom (loc,t) -> fun gl -> - let box = ref None in abstract_tactic_box := box; - let call = LtacAtomCall (t,box) in + let call = LtacAtomCall t in let tac = (* catch error in the interpretation *) catch_error (push_trace(dloc,call)ist.trace) (interp_atomic ist gl) t in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 141acb3db..c0027ef03 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -996,11 +996,7 @@ let explain_reduction_tactic_error = function let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = - (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in - let tacexpr_differ te te' = - (* NB: The following comparison may raise an exception - since a tacexpr may embed a functional part via a TacExtend *) - try te <> te' with Invalid_argument _ -> false + (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in let pr_call (n,ck) = (match ck with @@ -1009,16 +1005,9 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = | Proof_type.LtacVarCall (id,t) -> quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" - | Proof_type.LtacAtomCall (te,otac) -> quote - (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) - ++ (match !otac with - | Some te' when tacexpr_differ (Obj.magic te') te -> - strbrk " (expanded to " ++ quote - (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te'))) - ++ str ")" - | _ -> mt ()) + | Proof_type.LtacAtomCall te -> + quote (Pptactic.pr_glob_tactic (Global.env()) + (Tacexpr.TacAtom (Loc.ghost,te))) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> let filter = function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in -- cgit v1.2.3