aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml230
1 files changed, 229 insertions, 1 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c331eea6f..06a1cc812 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -25,6 +25,10 @@ open Libnames
open Extend
open Nametab
open Ppconstr
+open Evd
+open Proof_type
+open Refiner
+open Pfedit
let emacs_str s = if !Options.print_emacs then s else ""
@@ -124,7 +128,8 @@ let prterm t = prterm_env (Global.env()) t
let prtype t = prtype_env (Global.env()) t
let prjudge j = prjudge_env (Global.env()) j
-let _ = Termops.set_print_constr prterm
+let _ = Termops.set_print_constr prterm_env
+(*let _ = Tactic_debug.set_pattern_printer pr_pattern_env*)
let pr_constant env cst = prterm_env env (mkConst cst)
let pr_existential env ev = prterm_env env (mkEvar ev)
@@ -250,3 +255,226 @@ let pr_context_of env = match Options.print_hyps_limit () with
| None -> hv 0 (pr_context_unlimited env)
| Some n -> hv 0 (pr_context_limit n env)
+
+(* display complete goal *)
+let 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
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
+
+(* display the conclusion of a goal *)
+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
+
+(* display evar type: a context and a type *)
+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"]")
+
+(* 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
+
+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
+
+(* Print open subgoals. Checks for uninstantiated existential variables *)
+let pr_subgoals sigma = function
+ | [] ->
+ let exl = Evarutil.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 ())
+
+
+let pr_subgoals_of_pfts pfts =
+ let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in
+ let sigma = (top_goal_of_pftreestate pfts).sigma in
+ pr_subgoals 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))
+
+(* Elementary tactics *)
+
+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 " ++ print_constr t)
+ else
+ (str"Cut " ++ print_constr 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" : " ++ print_constr 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" : " ++ print_constr 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 print_constr c
+
+ | Convert_concl c ->
+ (str"Change " ++ print_constr c)
+
+ | Convert_hyp (id,None,t) ->
+ (str"Change " ++ print_constr t ++ spc () ++ str"in " ++ pr_id id)
+
+ | Convert_hyp (id,Some c,t) ->
+ (str"Change " ++ print_constr 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 " ++ print_constr t)
+ else
+ (str"cut " ++ print_constr 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" : " ++ print_constr 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" : " ++ print_constr 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 print_constr c
+
+ | Convert_concl c ->
+ (str"change " ++ print_constr c)
+
+ | Convert_hyp (id,None,t) ->
+ (str"change " ++ print_constr t ++ spc () ++ str"in " ++ pr_id id)
+
+ | Convert_hyp (id,Some c,t) ->
+ (str"change " ++ print_constr 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:20:45 +0000