summaryrefslogtreecommitdiff
path: root/proofs/refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refiner.ml')
-rw-r--r--proofs/refiner.ml477
1 files changed, 174 insertions, 303 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 785e6dd4..a1d7e011 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *)
+(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *)
open Pp
open Util
@@ -17,12 +17,10 @@ open Evd
open Sign
open Environ
open Reductionops
-open Instantiate
open Type_errors
open Proof_trees
open Proof_type
open Logic
-open Printer
type transformation_tactic = proof_tree -> (goal list * validation)
@@ -30,10 +28,7 @@ let hypotheses gl = gl.evar_hyps
let conclusion gl = gl.evar_concl
let sig_it x = x.it
-let sig_sig x = x.sigma
-
-
-let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it)
+let project x = x.sigma
let pf_status pf = pf.open_subgoals
@@ -43,21 +38,35 @@ let on_open_proofs f pf = if is_complete pf then pf else f pf
let and_status = List.fold_left (+) 0
-(* Normalizing evars in a goal. Called by tactic Local_constraints
- (i.e. when the sigma of the proof tree changes). Detect if the
- goal is unchanged *)
-let norm_goal sigma gl =
- let red_fun = Evarutil.nf_evar sigma in
- let ncl = red_fun gl.evar_concl in
- let ngl =
- { evar_concl = ncl;
- evar_hyps =
- Sign.fold_named_context
- (fun (d,b,ty) sign ->
- add_named_decl (d, option_app red_fun b, red_fun ty) sign)
- gl.evar_hyps ~init:empty_named_context;
- evar_body = gl.evar_body} in
- if ngl = gl then None else Some ngl
+(* Getting env *)
+
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
+
+
+let descend n p =
+ match p.ref with
+ | None -> error "It is a leaf."
+ | Some(r,pfl) ->
+ if List.length pfl >= n then
+ (match list_chop (n-1) pfl with
+ | left,(wanted::right) ->
+ (wanted,
+ (fun pfl' ->
+ if (List.length pfl' = 1)
+ & (List.hd pfl').goal = wanted.goal
+ then
+ let pf' = List.hd pfl' in
+ let spfl = left@(pf'::right) in
+ let newstatus = and_status (List.map pf_status spfl) in
+ { p with
+ open_subgoals = newstatus;
+ ref = Some(r,spfl) }
+ else
+ error "descend: validation"))
+ | _ -> assert false)
+ else
+ error "Too few subproofs"
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -85,7 +94,7 @@ let rec frontier p =
([p.goal],
(fun lp' ->
let p' = List.hd lp' in
- if p'.goal = p.goal then
+ if Evd.eq_evar_info p'.goal p.goal then
p'
else
errorlabstrm "Refiner.frontier"
@@ -95,9 +104,9 @@ let rec frontier p =
(List.flatten gll,
(fun retpfl ->
let pfl' = mapshape (List.map List.length gll) vl retpfl in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}))
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}))
let rec frontier_map_rec f n p =
@@ -105,7 +114,7 @@ let rec frontier_map_rec f n p =
match p.ref with
| None ->
let p' = f p in
- if p'.goal == p.goal || p'.goal = p.goal then p'
+ if Evd.eq_evar_info p'.goal p.goal then p'
else
errorlabstrm "Refiner.frontier_map"
(str"frontier_map was handed back a ill-formed proof.")
@@ -115,9 +124,9 @@ let rec frontier_map_rec f n p =
(fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
(n,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_map f n p =
let nmax = p.open_subgoals in
@@ -131,7 +140,7 @@ let rec frontier_mapi_rec f i p =
match p.ref with
| None ->
let p' = f i p in
- if p'.goal == p.goal || p'.goal = p.goal then p'
+ if Evd.eq_evar_info p'.goal p.goal then p'
else
errorlabstrm "Refiner.frontier_mapi"
(str"frontier_mapi was handed back a ill-formed proof.")
@@ -141,9 +150,9 @@ let rec frontier_mapi_rec f i p =
(fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
(i,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_mapi f p = frontier_mapi_rec f 1 p
@@ -156,124 +165,87 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
(* leaf g is the canonical incomplete proof of a goal g *)
-let leaf g = {
- open_subgoals = 1;
- goal = g;
- ref = None }
+let leaf g =
+ { open_subgoals = 1;
+ goal = g;
+ ref = None }
-(* Tactics table. *)
+(* refiner r is a tactic applying the rule r *)
-let tac_tab = Hashtbl.create 17
+let check_subproof_connection gl spfl =
+ list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
-let add_tactic s t =
- if Hashtbl.mem tac_tab s then
- errorlabstrm ("Refiner.add_tactic: ")
- (str ("Cannot redeclare tactic "^s));
- Hashtbl.add tac_tab s t
-let overwriting_add_tactic s t =
- if Hashtbl.mem tac_tab s then begin
- Hashtbl.remove tac_tab s;
- warning ("Overwriting definition of tactic "^s)
- end;
- Hashtbl.add tac_tab s t
+let abstract_operation syntax semantics gls =
+ let (sgl_sigma,validation) = semantics gls in
+ let hidden_proof = validation (List.map leaf sgl_sigma.it) in
+ (sgl_sigma,
+ fun spfl ->
+ assert (check_subproof_connection sgl_sigma.it spfl);
+ { open_subgoals = and_status (List.map pf_status spfl);
+ goal = gls.it;
+ ref = Some(Nested(syntax,hidden_proof),spfl)})
-let lookup_tactic s =
- try
- Hashtbl.find tac_tab s
- with Not_found ->
- errorlabstrm "Refiner.lookup_tactic"
- (str"The tactic " ++ str s ++ str" is not installed")
+let abstract_tactic_expr ?(dflt=false) te tacfun gls =
+ abstract_operation (Tactic(te,dflt)) tacfun gls
+let abstract_tactic ?(dflt=false) te =
+ abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
-(* refiner r is a tactic applying the rule r *)
-
-let check_subproof_connection gl spfl =
- list_for_all2eq (fun g pf -> g=pf.goal) gl spfl
-
-let abstract_tactic_expr te tacfun gls =
- let (sgl_sigma,v) = tacfun gls in
- let hidden_proof = v (List.map leaf sgl_sigma.it) in
- (sgl_sigma,
- fun spfl ->
- assert (check_subproof_connection sgl_sigma.it spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = gls.it;
- ref = Some(Tactic(te,hidden_proof),spfl) })
+let abstract_extended_tactic ?(dflt=false) s args =
+ abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
let refiner = function
| Prim pr as r ->
let prim_fun = prim_refiner pr in
- (fun goal_sigma ->
- let sgl = prim_fun goal_sigma.sigma goal_sigma.it in
- ({it=sgl; sigma = goal_sigma.sigma},
- (fun spfl ->
- assert (check_subproof_connection sgl spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = goal_sigma.it;
- ref = Some(r,spfl) })))
-
- | Tactic _ -> failwith "Refiner: should not occur"
+ (fun goal_sigma ->
+ let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
+ ({it=sgl; sigma = sigma'},
+ (fun spfl ->
+ assert (check_subproof_connection sgl spfl);
+ { open_subgoals = and_status (List.map pf_status spfl);
+ goal = goal_sigma.it;
+ ref = Some(r,spfl) })))
+
+
+ | Nested (_,_) | Decl_proof _ ->
+ failwith "Refiner: should not occur"
- (* [Local_constraints lc] makes the local constraints be [lc] and
- normalizes evars *)
-
- | Change_evars as r ->
- (fun goal_sigma ->
- let gl = goal_sigma.it in
- (match norm_goal goal_sigma.sigma gl with
- Some ngl ->
- ({it=[ngl];sigma=goal_sigma.sigma},
- (fun spfl ->
- assert (check_subproof_connection [ngl] spfl);
- { open_subgoals = (List.hd spfl).open_subgoals;
- goal = gl;
- ref = Some(r,spfl) }))
- (* if the evar change does not affect the goal, leave the
- proof tree unchanged *)
- | None -> ({it=[gl];sigma=goal_sigma.sigma},
- (fun spfl ->
- assert (List.length spfl = 1);
- List.hd spfl))))
-
-
-let local_Constraints gl = refiner Change_evars gl
-
-let norm_evar_tac = local_Constraints
+ (* Daimon is a canonical unfinished proof *)
-(*
-let vernac_tactic (s,args) =
- let tacfun = lookup_tactic s args in
- abstract_extra_tactic s args tacfun
-*)
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+ | Daimon ->
+ fun gls ->
+ ({it=[];sigma=gls.sigma},
+ fun spfl ->
+ assert (spfl=[]);
+ { open_subgoals = 0;
+ goal = gls.it;
+ ref = Some(Daimon,[])})
-let abstract_extended_tactic s args =
- abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
-let vernac_tactic (s,args) =
- let tacfun = lookup_tactic s args in
- abstract_extended_tactic s args tacfun
+let local_Constraints gl = refiner (Prim Change_evars) gl
-(* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
-let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
+let norm_evar_tac = local_Constraints
-(* [rc_of_glsigma : proof sigma -> readable_constraints] *)
-let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
+let norm_evar_proof sigma pf =
+ let nf_subgoal i sgl =
+ let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
+ v (List.map leaf gll.it) in
+ frontier_mapi nf_subgoal pf
(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
- takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
- where pfterm is the constr corresponding to the proof
- and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
- where the mi are metavariables numbers, and ci are their types.
- Their proof should be completed in order to complete the initial proof *)
+ takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
+ where pfterm is the constr corresponding to the proof
+ and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
+ where the mi are metavariables numbers, and ci are their types.
+ Their proof should be completed in order to complete the initial proof *)
let extract_open_proof sigma pf =
let next_meta =
let meta_cnt = ref 0 in
let rec f () =
incr meta_cnt;
- if in_dom sigma (existential_of_int !meta_cnt) then f ()
+ if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
else !meta_cnt
in f
in
@@ -281,24 +253,24 @@ let extract_open_proof sigma pf =
let rec proof_extractor vl = function
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
- | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+ | {ref=Some(Nested(_,hidden_proof),spfl)} ->
let sgl,v = frontier hidden_proof in
let flat_proof = v spfl in
proof_extractor vl flat_proof
+
+ | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
- | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
-
- | {ref=None;goal=goal} ->
+ | {ref=(None|Some(Daimon,[]));goal=goal} ->
let visible_rels =
map_succeed
(fun id ->
- try let n = list_index id vl in (n,id)
+ try let n = proof_variable_index id vl in (n,id)
with Not_found -> failwith "caught")
- (ids_of_named_context goal.evar_hyps) in
+ (ids_of_named_context (named_context_of_val goal.evar_hyps)) in
let sorted_rels =
Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
let sorted_env =
- List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps))
+ List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
sorted_rels in
let abs_concl =
List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
@@ -308,7 +280,7 @@ let extract_open_proof sigma pf =
open_obligations := (meta,abs_concl):: !open_obligations;
applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
- | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
+ | _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
in
let pfterm = proof_extractor [] pf in
(pfterm, List.rev !open_obligations)
@@ -345,17 +317,13 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
(* the message printing identity tactic *)
let tclIDTAC_MESSAGE s gls =
- if s = "" then tclIDTAC gls
- else
- begin
- msgnl (str ("Idtac says : "^s)); tclIDTAC gls
- end
+ msg (hov 0 s); tclIDTAC gls
(* General failure tactic *)
let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * string
+exception FailError of int * std_ppcmds
(* The Fail tactic *)
let tclFAIL lvl s g = raise (FailError (lvl,s))
@@ -469,7 +437,7 @@ let rec tclTHENLIST = function
(* various progress criterions *)
let same_goal gl subgoal =
- (hypotheses subgoal) = (hypotheses gl) &
+ eq_named_context_val (hypotheses subgoal) (hypotheses gl) &&
eq_constr (conclusion subgoal) (conclusion gl)
@@ -569,6 +537,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS
let tclIFTHENSVELSE=ite_gen tclTHENSV
+let tclIFTHENTRYELSEMUST tac1 tac2 gl =
+ tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
(* Fails if a tactic did not solve the goal *)
let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
@@ -647,7 +617,6 @@ let tactic_list_tactic tac gls =
-
(* The type of proof-trees state and a few utilities
A proof-tree state is built from a proof-tree, a set of global
constraints, and a stack which allows to navigate inside the
@@ -679,41 +648,19 @@ let nth_goal_of_pftreestate n pts =
try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
with Invalid_argument _ | Failure _ -> non_existent_goal n
-let descend n p =
- match p.ref with
- | None -> error "It is a leaf."
- | Some(r,pfl) ->
- if List.length pfl >= n then
- (match list_chop (n-1) pfl with
- | left,(wanted::right) ->
- (wanted,
- (fun pfl' ->
- if (List.length pfl' = 1)
- & (List.hd pfl').goal = wanted.goal
- then
- let pf' = List.hd pfl' in
- let spfl = left@(pf'::right) in
- let newstatus = and_status (List.map pf_status spfl) in
- { open_subgoals = newstatus;
- goal = p.goal;
- ref = Some(r,spfl) }
- else
- error "descend: validation"))
- | _ -> assert false)
- else
- error "Too few subproofs"
-
let traverse n pts = match n with
| 0 -> (* go to the parent *)
(match pts.tstack with
| [] -> error "traverse: no ancestors"
| (_,v)::tl ->
- { tpf = v [pts.tpf];
+ let pf = v [pts.tpf] in
+ let pf = norm_evar_proof pts.tpfsigma pf in
+ { tpf = pf;
tstack = tl;
tpfsigma = pts.tpfsigma })
| -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
(match pts.tpf.ref with
- | Some (Tactic (_,spf),_) ->
+ | Some (Nested (_,spf),_) ->
let v = (fun pfl -> pts.tpf) in
{ tpf = spf;
tstack = (-1,v)::pts.tstack;
@@ -732,17 +679,23 @@ let app_tac sigr tac p =
sigr := gll.sigma;
v (List.map leaf gll.it)
-(* solve the nth subgoal with tactic tac *)
-let solve_nth_pftreestate n tac pts =
+(* modify proof state at current position *)
+
+let map_pftreestate f pts =
let sigr = ref pts.tpfsigma in
- let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+ let tpf' = f sigr pts.tpf in
let tpf'' =
- if !sigr == pts.tpfsigma then tpf'
- else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
+ if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
{ tpf = tpf'';
tpfsigma = !sigr;
tstack = pts.tstack }
+(* solve the nth subgoal with tactic tac *)
+
+let solve_nth_pftreestate n tac =
+ map_pftreestate
+ (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
+
let solve_pftreestate = solve_nth_pftreestate 1
(* This function implements a poor man's undo at the current goal.
@@ -774,15 +727,16 @@ let extract_pftreestate pts =
(str"Cannot extract from a proof-tree in which we have descended;" ++
spc () ++ str"Please ascend to the root");
let pfterm,subgoals = extract_open_pftreestate pts in
- let exl = Evd.non_instantiated pts.tpfsigma in
+ let exl = Evarutil.non_instantiated pts.tpfsigma in
if subgoals <> [] or exl <> [] then
- errorlabstrm "extract_proof"
- (if subgoals <> [] then
- str "Attempt to save an incomplete proof"
- else
- str "Attempt to save a proof with existential variables still non-instantiated");
+ errorlabstrm "extract_proof"
+ (if subgoals <> [] then
+ str "Attempt to save an incomplete proof"
+ else
+ str "Attempt to save a proof with existential variables still non-instantiated");
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
- strong whd_betaiotaevar env pts.tpfsigma pfterm
+ nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+ (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
(***
local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
***)
@@ -893,137 +847,54 @@ let prev_unproven pts =
let rec top_of_tree pts =
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
+let change_rule f pts =
+ let mark_top _ pt =
+ match pt.ref with
+ Some (oldrule,l) ->
+ {pt with ref=Some (f oldrule,l)}
+ | _ -> invalid_arg "change_rule" in
+ map_pftreestate mark_top pts
+
+let match_rule p pts =
+ match (proof_of_pftreestate pts).ref with
+ Some (r,_) -> p r
+ | None -> false
+
+let rec up_until_matching_rule p pts =
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ if match_rule p one_up then
+ pts
+ else
+ up_until_matching_rule p one_up
-(* Pretty-printers. *)
+let rec up_to_matching_rule p pts =
+ if match_rule p pts then
+ pts
+ else
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ up_to_matching_rule p one_up
-open Pp
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-let pr_tactic = function
- | Tacexpr.TacArg (Tacexpr.Tacexp t) ->
- if !Options.v7 then
- Pptactic.pr_glob_tactic t (*top tactic from tacinterp*)
- else
- Pptacticnew.pr_glob_tactic (Global.env()) t
- | t ->
- if !Options.v7 then
- Pptactic.pr_tactic t
- else
- Pptacticnew.pr_tactic (Global.env()) t
-
-let pr_rule = function
- | Prim r -> hov 0 (pr_prim_rule r)
- | Tactic (texp,_) -> hov 0 (pr_tactic texp)
- | Change_evars ->
- (* This is internal tactic and cannot be replayed at user-level.
- Function pr_rule_dot below is used when we want to hide
- Change_evars *)
- str "Evar change"
-
-(* Does not print change of evars *)
-let pr_rule_dot = function
- | Change_evars -> mt ()
- | r -> pr_rule r ++ str"."
-
-exception Different
-
-(* We remove from the var context of env what is already in osign *)
-let thin_sign osign sign =
- Sign.fold_named_context
- (fun (id,c,ty as d) sign ->
- try
- if Sign.lookup_named id osign = (id,c,ty) then sign
- else raise Different
- with Not_found | Different -> add_named_decl d sign)
- sign ~init:empty_named_context
-
-let rec print_proof sigma osign pf =
- let {evar_hyps=hyps; evar_concl=cl;
- evar_body=body} = pf.goal in
- let hyps' = thin_sign osign hyps in
- match pf.ref with
- | None ->
- hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
- | Some(r,spfl) ->
- hov 0
- (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
- spc () ++ str" BY " ++
- hov 0 (pr_rule r) ++ fnl () ++
- str" " ++
- hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
-)
-
-let pr_change gl =
- (str"Change " ++ prterm_env (Global.env()) gl.evar_concl ++ str".")
-
-let rec print_script nochange sigma osign pf =
- let {evar_hyps=sign; evar_concl=cl} = pf.goal in
- match pf.ref with
- | None ->
- (if nochange then
- (str"<Your Tactic Text here>")
- else
- pr_change pf.goal)
- ++ fnl ()
- | Some(r,spfl) ->
- ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
- pr_rule_dot r ++ fnl () ++
- prlist_with_sep pr_fnl
- (print_script nochange sigma sign) spfl)
-
-let print_treescript nochange sigma _osign pf =
- let rec aux top pf =
- let {evar_hyps=sign; evar_concl=cl} = pf.goal in
- match pf.ref with
- | None ->
- if nochange then
- (str"<Your Tactic Text here>")
- else
- (pr_change pf.goal)
- | Some(r,spfl) ->
- (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
- pr_rule_dot r ++
- match spfl with
- | [] -> mt ()
- | [spf] -> fnl () ++ (if top then mt () else str " ") ++ aux top spf
- | _ -> fnl () ++ str " " ++
- hov 0 (prlist_with_sep fnl (aux false) spfl)
- in hov 0 (aux true pf)
-
-let rec print_info_script sigma osign pf =
- let {evar_hyps=sign; evar_concl=cl} = pf.goal in
- match pf.ref with
- | None -> (mt ())
- | Some(Change_evars,[spf]) ->
- print_info_script sigma osign spf
- | Some(r,spfl) ->
- (pr_rule r ++
- match spfl with
- | [pf1] ->
- if pf1.ref = None then
- (str "." ++ fnl ())
- else
- (str";" ++ brk(1,3) ++
- print_info_script sigma sign pf1)
- | _ -> (str"." ++ fnl () ++
- prlist_with_sep pr_fnl
- (print_info_script sigma sign) spfl))
-
-let format_print_info_script sigma osign pf =
- hov 0 (print_info_script sigma osign pf)
-
-let print_subscript sigma sign pf =
- if is_tactic_proof pf then
- format_print_info_script sigma sign (subproof_of_proof pf)
- else
- format_print_info_script sigma sign pf
+(* Pretty-printers. *)
+
+let pp_info = ref (fun _ _ _ -> assert false)
+let set_info_printer f = pp_info := f
let tclINFO (tac : tactic) gls =
let (sgl,v) as res = tac gls in
begin try
let pf = v (List.map leaf (sig_it sgl)) in
- let sign = (sig_it gls).evar_hyps in
+ let sign = named_context_of_val (sig_it gls).evar_hyps in
msgnl (hov 0 (str" == " ++
- print_subscript (sig_sig gls) sign pf))
+ !pp_info (project gls) sign pf))
with e when catchable_exception e ->
msgnl (hov 0 (str "Info failed to apply validation"))
end;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:30:32 +0000