aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml11
-rw-r--r--proofs/logic.ml130
-rw-r--r--proofs/logic.mli5
-rw-r--r--proofs/pfedit.ml26
-rw-r--r--proofs/pfedit.mli5
-rw-r--r--proofs/proof_trees.ml152
-rw-r--r--proofs/proof_trees.mli14
-rw-r--r--proofs/refiner.ml131
-rw-r--r--proofs/refiner.mli10
-rw-r--r--proofs/tacmach.ml6
-rw-r--r--proofs/tacmach.mli11
-rw-r--r--proofs/tactic_debug.ml27
-rw-r--r--proofs/tactic_debug.mli7
13 files changed, 42 insertions, 493 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index aa2ff18ce..07c3aca83 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -48,13 +48,10 @@ let clenv_cast_meta clenv =
match kind_of_term (strip_outer_cast u) with
| Meta mv ->
(try
- match Metamap.find mv (metas_of clenv.env) with
- | Cltyp b ->
- let b' = clenv_nf_meta clenv b.rebus in
- if occur_meta b' then u else mkCast (mkMeta mv, b')
- | Clval(_) -> u
- with Not_found ->
- u)
+ let b = Typing.meta_type clenv.env mv in
+ if occur_meta b then u
+ else mkCast (mkMeta mv, b)
+ with Not_found -> u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
| Case(ci,p,c,br) ->
mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e7af07dfe..8aa732fe3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -655,133 +655,3 @@ let prim_extractor subfun vl pft =
| None-> error "prim_extractor handed incomplete proof"
-(* Pretty-printer *)
-
-open Printer
-
-let prterm x = prterm_env (Global.env()) x
-
-let pr_prim_rule_v7 = function
- | Intro id ->
- str"Intro " ++ pr_id id
-
- | Intro_replacing id ->
- (str"intro replacing " ++ pr_id id)
-
- | Cut (b,id,t) ->
- if b then
- (str"Assert " ++ prterm t)
- else
- (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
-
- | FixRule (f,n,[]) ->
- (str"Fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others) ->
- let rec print_mut = function
- | (f,n,ar)::oth ->
- pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
- | [] -> mt () in
- (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
- str" with " ++ print_mut others)
-
- | Cofix (f,[]) ->
- (str"Cofix " ++ pr_id f)
-
- | Cofix (f,others) ->
- let rec print_mut = function
- | (f,ar)::oth ->
- (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
- | [] -> mt () in
- (str"Cofix " ++ pr_id f ++ str" with " ++ print_mut others)
-
- | Refine c ->
- str(if occur_meta c then "Refine " else "Exact ") ++
- Constrextern.with_meta_as_hole prterm c
-
- | Convert_concl c ->
- (str"Change " ++ prterm c)
-
- | Convert_hyp (id,None,t) ->
- (str"Change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id)
-
- | Convert_hyp (id,Some c,t) ->
- (str"Change " ++ prterm c ++ spc () ++ str"in "
- ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")")
-
- | Thin ids ->
- (str"Clear " ++ prlist_with_sep pr_spc pr_id ids)
-
- | ThinBody ids ->
- (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids)
-
- | Move (withdep,id1,id2) ->
- (str (if withdep then "Dependent " else "") ++
- str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2)
-
- | Rename (id1,id2) ->
- (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
-
-let pr_prim_rule_v8 = function
- | Intro id ->
- str"intro " ++ pr_id id
-
- | Intro_replacing id ->
- (str"intro replacing " ++ pr_id id)
-
- | Cut (b,id,t) ->
- if b then
- (str"assert " ++ prterm t)
- else
- (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
-
- | FixRule (f,n,[]) ->
- (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others) ->
- let rec print_mut = function
- | (f,n,ar)::oth ->
- pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
- | [] -> mt () in
- (str"fix " ++ pr_id f ++ str"/" ++ int n ++
- str" with " ++ print_mut others)
-
- | Cofix (f,[]) ->
- (str"cofix " ++ pr_id f)
-
- | Cofix (f,others) ->
- let rec print_mut = function
- | (f,ar)::oth ->
- (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
- | [] -> mt () in
- (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
-
- | Refine c ->
- str(if occur_meta c then "refine " else "exact ") ++
- Constrextern.with_meta_as_hole prterm c
-
- | Convert_concl c ->
- (str"change " ++ prterm c)
-
- | Convert_hyp (id,None,t) ->
- (str"change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id)
-
- | Convert_hyp (id,Some c,t) ->
- (str"change " ++ prterm c ++ spc () ++ str"in "
- ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")")
-
- | Thin ids ->
- (str"clear " ++ prlist_with_sep pr_spc pr_id ids)
-
- | ThinBody ids ->
- (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids)
-
- | Move (withdep,id1,id2) ->
- (str (if withdep then "dependent " else "") ++
- str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2)
-
- | Rename (id1,id2) ->
- (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
-
-let pr_prim_rule t =
- if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0a641e975..561c26a7f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -60,8 +60,3 @@ type refiner_error =
exception RefinerError of refiner_error
val catchable_exception : exn -> bool
-
-
-(*s Pretty-printer. *)
-
-val pr_prim_rule : prim_rule -> Pp.std_ppcmds
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 11f4c956d..2e6946f72 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -305,29 +305,3 @@ let focused_goal () = let n = !focus_n in if n=0 then 1 else n
let reset_top_of_tree () =
let pts = get_pftreestate () in
if not (is_top_pftreestate pts) then mutate top_of_tree
-
-(** Printers *)
-
-let pr_subgoals_of_pfts pfts =
- let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in
- let sigma = project (top_goal_of_pftreestate pfts) in
- pr_subgoals_existential sigma gls
-
-let pr_open_subgoals () =
- let pfts = get_pftreestate () in
- match focus() with
- | 0 ->
- pr_subgoals_of_pfts pfts
- | n ->
- let pf = proof_of_pftreestate pfts in
- let gls = fst (frontier pf) in
- assert (n > List.length gls);
- if List.length gls < 2 then
- pr_subgoal n gls
- else
- v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
- pr_subgoal n gls)
-
-let pr_nth_open_subgoal n =
- let pf = proof_of_pftreestate (get_pftreestate ()) in
- pr_subgoal n (fst (frontier pf))
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index de84d04a3..b0aacd86c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -176,8 +176,3 @@ val traverse_prev_unproven : unit -> unit
proof and goal management, as it is done, for instance in pcoq *)
val traverse_to : int list -> unit
val mutate : (pftreestate -> pftreestate) -> unit
-
-(** Printers *)
-
-val pr_open_subgoals : unit -> std_ppcmds
-val pr_nth_open_subgoal : int -> std_ppcmds
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 445e19967..73cc5d273 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -66,10 +66,6 @@ let is_tactic_proof pf = match pf.ref with
| _ -> false
-(*******************************************************************)
-(* Constraints for existential variables *)
-(*******************************************************************)
-
let pf_lookup_name_as_renamed env ccl s =
Detyping.lookup_name_as_renamed env ccl s
@@ -81,154 +77,12 @@ let pf_lookup_index_as_renamed env ccl n =
(*********************************************************************)
open Pp
-open Printer
-
-(* Il faudrait parametrer toutes les pr_term, term_env, etc. par la
- strategie de renommage choisie pour Termast (en particulier, il
- faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par
- Intros Until fonctionne exactement comme on affiche le but avec
- term_env *)
-
-let pf_lookup_name_as_renamed hyps ccl s =
- Detyping.lookup_name_as_renamed hyps ccl s
-let pf_lookup_index_as_renamed ccl n =
- Detyping.lookup_index_as_renamed ccl n
-
-let pr_idl idl = prlist_with_sep pr_spc pr_id idl
-
-let pr_goal g =
+let db_pr_goal g =
let env = evar_env g in
- let penv = pr_context_of env in
- let pc = prterm_env_at_top env g.evar_concl in
+ let penv = print_named_context env in
+ let pc = print_constr_env env g.evar_concl in
str" " ++ hv 0 (penv ++ fnl () ++
- str (emacs_str (String.make 1 (Char.chr 253))) ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
-let pr_concl n g =
- let env = evar_env g in
- let pc = prterm_env_at_top env g.evar_concl in
- str (emacs_str (String.make 1 (Char.chr 253))) ++
- str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc
-
-(* print the subgoals but write Subtree proved! even in case some existential
- variables remain unsolved, pr_subgoals_existential is a safer version
- of pr_subgoals *)
-
-let pr_subgoals = function
- | [] -> (str"Proof completed." ++ fnl ())
- | [g] ->
- let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
- | g1::rest ->
- let rec pr_rec n = function
- | [] -> (mt ())
- | g::rest ->
- let pg = pr_concl n g in
- let prest = pr_rec (n+1) rest in
- (cut () ++ pg ++ prest)
- in
- let pg1 = pr_goal g1 in
- let pgr = pr_rec 2 rest in
- v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr)
-
-let pr_subgoal n =
- let rec prrec p = function
- | [] -> error "No such goal"
- | g::rest ->
- if p = 1 then
- let pg = pr_goal g in
- v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
- else
- prrec (p-1) rest
- in
- prrec n
-
-let pr_seq evd =
- let env = evar_env evd
- and cl = evd.evar_concl
- in
- let pdcl = pr_named_context_of env in
- let pcl = prterm_env_at_top env cl in
- hov 0 (pdcl ++ spc () ++ hov 0 (str"|- " ++ pcl))
-
-let prgl gl =
- let pgl = pr_seq gl in
- (str"[" ++ pgl ++ str"]" ++ spc ())
-
-let pr_evgl gl =
- let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in
- let pc = prterm gl.evar_concl in
- hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]")
-
-let pr_evgl_sign gl =
- let ps = pr_named_context_of (evar_env gl) in
- let pc = prterm gl.evar_concl in
- hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]")
-
-(* evd.evgoal.lc seems to be printed twice *)
-let pr_decl evd =
- let pevgl = pr_evgl evd in
- let pb =
- match evd.evar_body with
- | Evar_empty -> (fnl ())
- | Evar_defined c -> let pc = prterm c in (str" => " ++ pc ++ fnl ())
- in
- h 0 (pevgl ++ pb)
-
-let pr_evd evd =
- prlist_with_sep pr_fnl
- (fun (ev,evd) ->
- let pe = pr_decl evd in
- h 0 (str (string_of_existential ev) ++ str"==" ++ pe))
- (Evd.to_list evd)
-
-let pr_decls decls = pr_evd decls
-
-let pr_evc evc =
- let pe = pr_evd evc.sigma in
- (pe)
-
-let pr_evars =
- prlist_with_sep pr_fnl
- (fun (ev,evd) ->
- let pegl = pr_evgl_sign evd in
- (str (string_of_existential ev) ++ str " : " ++ pegl))
-
-(* Print an enumerated list of existential variables *)
-let rec pr_evars_int i = function
- | [] -> (mt ())
- | (ev,evd)::rest ->
- let pegl = pr_evgl_sign evd in
- let pei = pr_evars_int (i+1) rest in
- (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
- str (string_of_existential ev) ++ str " : " ++ pegl)) ++
- fnl () ++ pei
-
-(* Equivalent to pr_subgoals but start from the prooftree and
- check for uninstantiated existential variables *)
-
-let pr_subgoals_existential sigma = function
- | [] ->
- let exl = non_instantiated sigma in
- if exl = [] then
- (str"Proof completed." ++ fnl ())
- else
- let pei = pr_evars_int 1 exl in
- (str "No more subgoals but non-instantiated existential " ++
- str "variables :" ++fnl () ++ (hov 0 pei))
- | [g] ->
- let pg = pr_goal g in
- v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
- | g1::rest ->
- let rec pr_rec n = function
- | [] -> (mt ())
- | g::rest ->
- let pc = pr_concl n g in
- let prest = pr_rec (n+1) rest in
- (cut () ++ pc ++ prest)
- in
- let pg1 = pr_goal g1 in
- let prest = pr_rec 2 rest in
- v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
- ++ pg1 ++ prest ++ fnl ())
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 12f82b7f4..73a6bd9a8 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -43,16 +43,4 @@ val pf_lookup_index_as_renamed : env -> constr -> int -> int option
open Pp
(*i*)
-val pr_goal : goal -> std_ppcmds
-val pr_subgoals : goal list -> std_ppcmds
-val pr_subgoal : int -> goal list -> std_ppcmds
-
-val pr_decl : goal -> std_ppcmds
-val pr_decls : evar_map -> std_ppcmds
-val pr_evc : named_context sigma -> std_ppcmds
-
-val prgl : goal -> std_ppcmds
-val pr_seq : goal -> std_ppcmds
-val pr_evars : (existential_key * goal) list -> std_ppcmds
-val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds
-val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
+val db_pr_goal : goal -> std_ppcmds
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index acdc302af..1cd343e38 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -884,129 +884,13 @@ let rec top_of_tree pts =
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
+
(* Pretty-printers. *)
-open Pp
-
-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 " ++ Printer.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)
-
-(* printed by Show Script command *)
-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
+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
@@ -1014,11 +898,8 @@ let tclINFO (tac : tactic) gls =
let pf = v (List.map leaf (sig_it sgl)) in
let sign = (sig_it gls).evar_hyps in
msgnl (hov 0 (str" == " ++
- print_subscript (sig_sig gls) sign pf))
+ !pp_info (sig_sig gls) sign pf))
with e when catchable_exception e ->
msgnl (hov 0 (str "Info failed to apply validation"))
end;
res
-
-(* Change evars *)
-let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 8e39e0181..5dc61aa1b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -200,11 +200,5 @@ val change_constraints_pftreestate
(*i*)
open Pp
(*i*)
-
-val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
-val pr_rule : rule -> std_ppcmds
-val pr_tactic : tactic_expr -> std_ppcmds
-val print_script :
- bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
-val print_treescript :
- bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+val set_info_printer :
+ (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0ea076edd..85e885a13 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -246,9 +246,9 @@ let rec pr_list f = function
| a::l1 -> (f a) ++ pr_list f l1
let pr_gls gls =
- hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls))
+ hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
let pr_glls glls =
- hov 0 (pr_decls (sig_sig glls) ++ fnl () ++
- prlist_with_sep pr_fnl pr_seq (sig_it glls))
+ hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+ prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 4793924d7..4fbc102cc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -172,11 +172,6 @@ val tactic_list_tactic : tactic_list -> tactic
val tclFIRSTLIST : tactic_list list -> tactic_list
val tclIDTAC_list : tactic_list
-(*s Pretty-printing functions. *)
-
-(*i*)
-open Pp
-(*i*)
-
-val pr_gls : goal sigma -> std_ppcmds
-val pr_glls : goal list sigma -> std_ppcmds
+(*s Pretty-printing functions (debug only). *)
+val pr_gls : goal sigma -> Pp.std_ppcmds
+val pr_glls : goal list sigma -> Pp.std_ppcmds
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index cfa65119f..5daa10fc7 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -9,13 +9,15 @@
open Names
open Constrextern
open Pp
-open Pptactic
-open Printer
open Tacexpr
open Termops
-let pr_glob_tactic x =
- (if !Options.v7 then pr_glob_tactic else Pptacticnew.pr_glob_tactic (Global.env())) x
+let prtac = ref (fun _ -> assert false)
+let set_tactic_printer f = prtac := f
+let prmatchpatt = ref (fun _ _ -> assert false)
+let set_match_pattern_printer f = prmatchpatt := f
+let prmatchrl = ref (fun _ -> assert false)
+let set_match_rule_printer f = prmatchrl := f
(* This module intends to be a beginning of debugger for tactic expressions.
Currently, it is quite simple and we can hope to have, in the future, a more
@@ -31,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt())
(* Prints the goal *)
let db_pr_goal g =
- msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g))
+ msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Tacmach.sig_it g))
(* Prints the commands *)
let help () =
@@ -45,7 +47,7 @@ let help () =
let goal_com g tac =
begin
db_pr_goal g;
- msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ())
+ msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
end
(* Gives the number of a run command *)
@@ -106,15 +108,14 @@ let debug_prompt lev g tac f =
(* Prints a constr *)
let db_constr debug env c =
if debug <> DebugOff & !skip = 0 then
- msgnl (str "Evaluated term: " ++ prterm_env env c)
+ msgnl (str "Evaluated term: " ++ print_constr_env env c)
(* Prints the pattern rule *)
let db_pattern_rule debug num r =
if debug <> DebugOff & !skip = 0 then
begin
msgnl (str "Pattern rule " ++ int num ++ str ":");
- msgnl (str "|" ++ spc () ++
- pr_match_rule false Printer.pr_pattern pr_glob_tactic r)
+ msgnl (str "|" ++ spc () ++ !prmatchrl r)
end
(* Prints the hypothesis pattern identifier if it exists *)
@@ -127,12 +128,12 @@ let db_matched_hyp debug env (id,c) ido =
if debug <> DebugOff & !skip = 0 then
msgnl (str "Hypothesis " ++
str ((Names.string_of_id id)^(hyp_bound ido)^
- " has been matched: ") ++ prterm_env env c)
+ " has been matched: ") ++ print_constr_env env c)
(* Prints the matched conclusion *)
let db_matched_concl debug env c =
if debug <> DebugOff & !skip = 0 then
- msgnl (str "Conclusion has been matched: " ++ prterm_env env c)
+ msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
(* Prints a success message when the goal has been matched *)
let db_mc_pattern_success debug =
@@ -150,9 +151,7 @@ let db_hyp_pattern_failure debug env (na,hyp) =
if debug <> DebugOff & !skip = 0 then
msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
" cannot match: ") ++
- pr_match_pattern
- (Printer.pr_pattern_env env (names_of_rel_context env))
- hyp)
+ !prmatchpatt env hyp)
(* Prints a matching failure message for a rule *)
let db_matching_failure debug =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 034e36d93..27536dfa9 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -20,6 +20,13 @@ open Term
Currently, it is quite simple and we can hope to have, in the future, a more
complete panel of commands dedicated to a proof assistant framework *)
+val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
+val set_match_pattern_printer :
+ (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
+val set_match_rule_printer :
+ ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+ unit
+
(* Debug information *)
type debug_info =
| DebugOn of int
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 03:18:45 +0000