diff options
| -rw-r--r-- | proofs/logic.ml | 55 | ||||
| -rw-r--r-- | proofs/logic.mli | 5 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 349 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 7 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 221 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 25 | ||||
| -rw-r--r-- | proofs/refiner.ml | 103 | ||||
| -rw-r--r-- | proofs/refiner.mli | 15 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 35 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 11 |
10 files changed, 817 insertions, 9 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a3e387b6e6..db3a6ca18d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -541,3 +541,58 @@ let prim_extractor subfun vl pft = let prim_extractor = Profile.profile3 "prim_extractor" prim_extractor let prim_refiner = Profile.profile3 "prim_refiner" prim_refiner ***) + +(* Pretty-printer *) + +open Printer + +let pr_prim_rule = function + | {name=Intro;newids=[id]} -> + [< 'sTR"Intro " ; print_id id >] + + | {name=Intro_after;newids=[id]} -> + [< 'sTR"intro after " ; print_id id >] + + | {name=Intro_replacing;newids=[id]} -> + [< 'sTR"intro replacing " ; print_id id >] + + | {name=Fix;newids=[f];params=[Num(_,n)]} -> + [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n>] + + | {name=Fix;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> + let rec print_mut = + function (f::lf),((Num(_,n))::ln),(ar::lar) -> + [< print_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar; + print_mut (lf,ln,lar)>] + | _ -> [<>] in + [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n; + 'sTR" with "; print_mut (lf,ln,lar) >] + + | {name=Cofix;newids=[f];terms=[]} -> + [< 'sTR"Cofix "; print_id f >] + + | {name=Cofix;newids=(f::lf);terms=lar} -> + let rec print_mut = + function (f::lf),(ar::lar) -> + [< print_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>] + | _ -> [<>] + in + [< 'sTR"Cofix "; print_id f; 'sTR" with "; print_mut (lf,lar) >] + + | {name=Refine;terms=[c]} -> + [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >] + + | {name=Convert_concl;terms=[c]} -> + [< 'sTR"Change " ; prterm c >] + + | {name=Convert_hyp;hypspecs=[id];terms=[c]} -> + [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; print_id id >] + + | {name=Thin;hypspecs=ids} -> + [< 'sTR"Clear " ; prlist_with_sep pr_spc print_id ids >] + + | {name=Move withdep;hypspecs=[id1;id2]} -> + [< 'sTR (if withdep then "Dependent " else ""); + 'sTR"Move " ; print_id id1; 'sTR " after "; print_id id2 >] + + | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule" diff --git a/proofs/logic.mli b/proofs/logic.mli index 88b632882e..4d1c2de979 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -35,3 +35,8 @@ type refiner_error = exception RefinerError of refiner_error val error_cannot_unify : path_kind -> constr * constr -> 'a + + +(*s Pretty-printer. *) + +val pr_prim_rule : prim_rule -> Pp.std_ppcmds diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml new file mode 100644 index 0000000000..18a9b09a74 --- /dev/null +++ b/proofs/pfedit.ml @@ -0,0 +1,349 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Sign +open Generic +open Term +open Constant +open Evd +open Declare +open Tacmach +open Proof_trees +open Lib + +type proof_topstate = { + top_hyps : var_context * var_context; + top_goal : goal; + top_strength : strength } + +let proof_edits = (Edit.empty() : (string,pftreestate,proof_topstate) Edit.t) + +let list_proofs () = Edit.dom proof_edits + +let msg_proofs use_resume = + match Edit.dom proof_edits with + | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >] + | l -> [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ; + (prlist_with_sep pr_spc pr_str (list_proofs ())) ; 'sTR"." ; + (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >] + else [< >]) + >] + +let undo_default = 12 +let undo_limit = ref undo_default + +(*********************************************************************) +(* Functions for decomposing and modifying the proof state *) +(*********************************************************************) + +let get_state () = + match Edit.read proof_edits with + | None -> errorlabstrm "Pfedit.get_state" + [< 'sTR"No focused proof"; msg_proofs true >] + | Some(_,pfs,ts) -> (pfs,ts) + +let get_topstate () = snd(get_state()) +let get_pftreestate () = fst(get_state()) + +let get_evmap_sign og = + let og = match og with + | Some n -> + let pftree = get_pftreestate () in + Some (nth_goal_of_pftreestate n pftree) + | None -> + try + let pftree = get_pftreestate () in + Some (nth_goal_of_pftreestate 1 pftree) + with UserError _ -> + None + in + match og with + | Some goal -> (project goal, pf_hyps goal) + | _ -> (Evd.empty, Global.var_context()) + +let set_proof s = + try + Edit.focus proof_edits s + with Invalid_argument "Edit.focus" -> + errorlabstrm "Pfedit.set_proof" + [< 'sTR"No such proof" ; (msg_proofs false) >] + +let resume_last () = + match (Edit.last_focused proof_edits) with + | None -> + errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >] + | p -> + Edit.focus proof_edits p + +let get_proof () = + match Edit.read proof_edits with + | None -> + errorlabstrm "Pfedit.get_proof" + [< 'sTR"No focused proof" ; msg_proofs true >] + | Some(na,_,_) -> na + +let add_proof (na,pfs,ts) = + Edit.create proof_edits (na,pfs,ts,Some !undo_limit) + +let del_proof na = + try + Edit.delete proof_edits na + with (UserError ("Edit.delete",_)) -> + errorlabstrm "Pfedit.del_proof" + [< 'sTR"No such proof" ; msg_proofs false >] + +let init_proofs () = Edit.clear proof_edits + +let mutate f = + try + Edit.mutate proof_edits (fun _ pfs -> f pfs) + with Invalid_argument "Edit.mutate" -> + errorlabstrm "Pfedit.mutate" + [< 'sTR"No focused proof" ; msg_proofs true >] + +let rev_mutate f = + try + Edit.mutate proof_edits (fun _ pfs -> f pfs) + with Invalid_argument "Edit.rev_mutate" -> + errorlabstrm "Pfedit.rev_mutate" + [< 'sTR"No focused proof"; msg_proofs true >] + +let start (na,ts) = + let pfs = mk_pftreestate ts.top_goal in + add_proof(na,pfs,ts) + +let restart () = + match Edit.read proof_edits with + | None -> + errorlabstrm "Pfedit.restart" + [< 'sTR"No focused proof to restart" ; msg_proofs true >] + | Some(na,_,ts) -> + del_proof na; + start (na,ts); + set_proof (Some na) + +let proof_prompt () = + match Edit.read proof_edits with + | None -> "Coq < " + | Some(na,_,_) -> na^" < " + +let proof_term () = + extract_pftreestate (get_pftreestate()) + +(* Detect is one has completed a subtree of the initial goal *) +let subtree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate pts) & + not (is_top_pftreestate pts) + +(*********************************************************************) +(* Undo functions *) +(*********************************************************************) + +let set_undo n = + if n>=0 then + undo_limit := n+1 + else + error "Cannot set a negative undo limit" + +let unset_undo () = set_undo undo_default + +let undo n = + try + Edit.undo proof_edits n; + (* needed because the resolution of a subtree is done in 2 steps + then a sequence of undo can lead to a focus on a completely solved + subtree - this solution only works properly if undoing one step *) + if subtree_solved() then Edit.undo proof_edits 1 + with (Invalid_argument "Edit.undo") -> + errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >] + +(*********************************************************************) +(* Saving functions *) +(*********************************************************************) + +let save_named opacity = + let (pfs,ts) = get_state() + and ident = get_proof() in + let {evar_concl=concl} = ts.top_goal + and strength = ts.top_strength in + let pfterm = extract_pftreestate pfs in + declare_constant (id_of_string ident) (*** opacity strength ***) + { const_entry_body = pfterm; const_entry_type = Some concl }; + del_proof ident; + message(ident ^ " is defined") + +let save_anonymous opacity save_ident n = + let (pfs,ts) = get_state() + and ident = get_proof() in + let {evar_concl=concl} = ts.top_goal + and strength = ts.top_strength in + let pfterm = extract_pftreestate pfs in + if ident = "Unnamed_thm" then + declare_constant (id_of_string save_ident) (*** opacity,strength ***) + { const_entry_body = pfterm; const_entry_type = Some concl } + else begin + message("Overriding name " ^ ident ^ " and using " ^ save_ident); + declare_constant (id_of_string save_ident) (*** opacity,strength ***) + { const_entry_body = pfterm; const_entry_type = Some concl } + end; + del_proof ident; + message(save_ident ^ " is defined") + +let save_anonymous_thm opacity id = + save_anonymous opacity id NeverDischarge + +let save_anonymous_remark opacity id = + let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in + save_anonymous opacity id (make_strength path) + +(*********************************************************************) +(* Abort functions *) +(*********************************************************************) + +let refining () = [] <> (Edit.dom proof_edits) + +let abort_goal pn = del_proof pn + +let abort_cur_goal () = del_proof (get_proof ()) + +let abort_goals () = + if refining() then begin + init_proofs(); + message "Current goals aborted" + end else + error "No proof-editing in progress" + +let abort_refine f x = + if refining() then abort_goals(); + f x + (* used to be: error "Must save or abort current goal first" *) + +let reset_name = abort_refine reset_to +(*** TODO +and reset_keeping_name = abort_refine reset_keeping +and reset_section = abort_refine raw_reset_section +and save_state = abort_refine States.raw_save_state +and restore_state = abort_refine States.raw_restore_state +and restore_last_saved_state = abort_refine States.raw_restore_last_saved_state +***) +and reset_all = abort_refine Lib.init + +(***TODO +let reset_prelude () = restore_state "Prelude" +and reset_initial () = restore_state "Initial" +***) + +(*********************************************************************) +(* Modifying the current prooftree *) +(*********************************************************************) + +let start_proof_with_type na str sign fsign concl = + let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in + let ts = { + top_hyps = (sign,fsign); + top_goal = top_goal; + top_strength = str } + in + start(na,ts); + set_proof (Some na) + +let start_proof na str concl_com = + let (sigma,(sign,fsign)) = initial_sigma_assumptions() in + let concl = fconstruct_type sigma sign concl_com in + start_proof_with_type na str sign fsign concl.body + +let start_proof_constr na str concl = + let (sigma,(sign,fsign)) = initial_sigma_assumptions() in + let _ = type_of_type sigma sign concl in + start_proof_with_type na str sign fsign concl + +let solve_nth k tac = + let pft = get_pftreestate() in + if not (List.mem (-1) (cursor_of_pftreestate pft)) then + mutate (solve_nth_pftreestate k tac) + (* ; + let pfs =get_pftreestate() in + let pf = proof_of_pftreestate pfs in + let (pfterm,metamap) = refiner__extract_open_proof pf.goal.hyps pf + in (try typing__control_only_guard empty_evd pfterm + with e -> (undo 1; raise e)); + ()) + *) + else + error "cannot apply a tactic when we are descended behind a tactic-node" + +let by tac = mutate (solve_pftreestate tac) + +let traverse n = rev_mutate (traverse n) + +(* [traverse_to path] + + Traverses the current proof to get to the location specified by + [path]. + + ALGORITHM: + + If the cursor is equal to the path, we are done. + + If the cursor is longer than the path, then traverse to the parent + + If the cursor is equal to the tail of the path, then traverse to + the head of the path, and we are done. + + Otherwise, traverse to the parent, traverse to the tail of the + path, then traverse to the path. + +*) + +let rec nth_cdr = function + | 0 -> (function l -> l) + | n -> (comp List.tl (nth_cdr (n - 1))) + +let rec common_ancestor_equal_length = function + | ((a::l1), (b::l2)) -> + let (prefx,n) as result = (common_ancestor_equal_length (l1,l2)) in + if result = ([],0) then + if a = b then + result + else + (a::prefx),(n + 1) + else + (a::prefx),(n + 1) + | ([], []) -> [],0 + | (_, _) -> anomaly "common_ancestor_equal_length" + +let common_ancestor l1 l2 = + let diff_lengths = (List.length l1) - (List.length l2) in + if diff_lengths > 0 then + let head,tail = chop_list diff_lengths l1 in + let (prefx,n) = common_ancestor_equal_length (tail,l2) in + (head@prefx),n + else if diff_lengths < 0 then + let (prefx,n) = common_ancestor_equal_length + (l1, (nth_cdr (- diff_lengths) l2)) in + prefx,(n - diff_lengths) + else + common_ancestor_equal_length (l1,l2) + +let rec traverse_up = function + | 0 -> (function pf -> pf) + | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf)) + +let rec traverse_down = function + | [] -> (function pf -> pf) + | n::l -> (function pf -> Tacmach.traverse n (traverse_down l pf)) + +let traverse_to path = + let up_and_down path pfs = + let cursor = cursor_of_pftreestate pfs in + let down_list, up_count = common_ancestor path cursor in + traverse_down down_list (traverse_up up_count pfs) + in + rev_mutate (up_and_down path) + +(* traverse the proof tree until it reach the nth subgoal *) +let traverse_nth_goal n = mutate (nth_unproven n) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 2473af0c5b..7a953dff6e 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ open Pp open Sign open Declare open Proof_trees -open Refiner +open Tacmach (*i*) val proof_prompt : unit -> string @@ -32,3 +32,8 @@ val list_proofs : unit -> string list val add_proof : string * pftreestate * proof_topstate -> unit val del_proof : string -> unit val init_proofs : unit -> unit + +val make_focus : int -> unit +val focus : unit -> int +val focused_goal : unit -> int + diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 067162e60e..663aedb44d 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -138,15 +138,9 @@ let status_of_proof pf = pf.status let is_complete_proof pf = pf.status = Complete_proof -let is_leaf_proof pf = - match pf.ref with - | None -> true - | Some _ -> false +let is_leaf_proof pf = (pf.ref = None) -let is_tactic_proof pf = - match pf.subproof with - | Some _ -> true - | None -> false +let is_tactic_proof pf = (pf.subproof <> None) (*******************************************************************) @@ -230,3 +224,214 @@ let rec accessible sigma sp loc = let ctxt_access sigma sp = lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus + +(*********************************************************************) +(* Pretty printing functions *) +(*********************************************************************) + +open Pp +open Printer + +(* Il faudrait parametrer toutes les pr_term, term0, 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 + term0 *) + +let pf_lookup_name_as_renamed hyps ccl s = + Termast.lookup_name_as_renamed (gLOB hyps) ccl s + +let pf_lookup_index_as_renamed ccl n = + Termast.lookup_index_as_renamed ccl n + +let pr_idl idl = prlist_with_sep pr_spc print_id idl + +let pr_goal g = + let sign = context g.evar_env in + let penv = pr_env_opt sign in + let pc = term0_at_top sign 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 pc = term0_at_top (context g.evar_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"Subtree proved!" ; 'fNL >] + | [g] -> + let pg = pr_goal g in v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >] + | g1::rest -> + let rec pr_rec n = function + | [] -> [< >] + | 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_pgm ctxt = match ctxt.pgm with + | None -> [< >] + | Some pgm -> let ppgm = fprterm pgm in [< 'sTR"Realizer " ; ppgm >] + +let pr_ctxt ctxt = + let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >] + +let pr_seq {evar_env=env; evar_concl=cl; evar_info=info} = + let (x,y) as hyps = var_context env in + let sign = List.rev(List.combine x y) in + let pc = pr_ctxt info in + let pdcl = + prlist_with_sep pr_spc + (fun (id,ty) -> hOV 0 [< print_id id; 'sTR" : ";prterm ty.body >]) + sign + in + let pcl = term0_at_top (gLOB hyps) cl in + hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >] + +let prgl gl = + let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in + let pgl = pr_seq gl in + [< 'sTR"[[" ; plc; 'sTR"]" ; pgl ; 'sTR"]" ; 'sPC >] + +let pr_evgl gl = + let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in + let phyps = pr_idl (ids_of_sign (var_context gl.evar_env)) in + let pc = prterm gl.evar_concl in + hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >] + +let pr_evgl_sign gl = + let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in + let ps = pr_sign (var_context gl.evar_env) in + let pc = prterm gl.evar_concl in + hOV 0 [< 'sTR"[[" ; plc ; '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 [< print_id (id_of_existential ev) ; 'sTR"==" ; pe >]) + (Evd.to_list evd) + +let pr_decls decls = pr_evd (ts_it decls) + +let pr_focus accl = pr_idl (List.map id_of_existential (lc_toList accl)) + +let pr_evc evc = + let stamp = ts_stamp evc in + let evc = ts_it evc in + let pe = pr_evd evc.decls in + [< 'sTR"#" ; 'iNT stamp ; 'sTR"[" ; pr_focus evc.focus ; 'sTR"]=" ; pe >] + +let pr_evars = + prlist_with_sep pr_fnl + (fun (ev,evd) -> + let pegl = pr_evgl_sign evd in + [< print_id (id_of_existential ev); 'sTR " : "; pegl >]) + +(* Print an enumerated list of existential variables *) +let rec pr_evars_int i = function + | [] -> [< >] + | (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; + print_id (id_of_existential ev) ; 'sTR " : "; pegl >]); + 'fNL ; pei >] + +let pr_subgoals_existential sigma = function + | [] -> + let exl = Evd.non_instantiated sigma in + if exl = [] then + [< 'sTR"Subtree proved!" ; '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 + | [] -> [< >] + | 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 >] + +open Ast +open Termast +open Pretty + +let ast_of_cvt_bind f = function + | (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])]) + | (Dep id,c) -> ope ("BINDING", [nvar (string_of_id id); + ope ("COMMAND",[(f c)])]) + | (Com,c) -> ope ("BINDING", [ope ("COMMAND",[(f c)])]) + +let rec ast_of_cvt_intro_pattern = function + | IdPat id -> nvar (string_of_id id) + | DisjPat l -> ope ("DISJPATTERN", (List.map ast_of_cvt_intro_pattern l)) + | ConjPat l -> ope ("CONJPATTERN", (List.map ast_of_cvt_intro_pattern l)) + | ListPat l -> ope ("LISTPATTERN", (List.map ast_of_cvt_intro_pattern l)) + +let ast_of_cvt_arg = function + | Identifier id -> nvar (string_of_id id) + | Quoted_string s -> str s + | Integer n -> num n + | Command c -> ope ("COMMAND",[c]) + | Constr c -> + ope ("COMMAND",[bdize false (assumptions_for_print []) c]) + | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl) + | Bindings bl -> ope ("BINDINGS", + List.map (ast_of_cvt_bind (fun x -> x)) bl) + | Cbindings bl -> + ope ("BINDINGS", + List.map + (ast_of_cvt_bind (bdize false (assumptions_for_print []))) bl) + | Tacexp ast -> ope ("TACTIC",[ast]) + | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)]) + | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); + (num n); + ope ("COMMAND",[c])]) + | Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id)); + (ope ("COMMAND",[c]))]) + | Intropattern p -> ast_of_cvt_intro_pattern p + | Letpatterns _ -> failwith "TODO: ast_of_cvt_arg: Letpatterns" diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 7b612ac5fc..6e0f179b0e 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -143,3 +143,28 @@ val get_decls : readable_constraints -> evar_declarations val get_gc : readable_constraints -> global_constraints val remap : readable_constraints -> int * goal -> readable_constraints val ctxt_access : readable_constraints -> int -> bool + + +(*s Pretty printing functions. *) + +(*i*) +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 : global_constraints ->std_ppcmds +val pr_evc : readable_constraints -> std_ppcmds + +val prgl : goal -> std_ppcmds +val pr_seq : goal -> std_ppcmds +val pr_focus : local_constraints -> std_ppcmds +val pr_ctxt : ctxtty -> std_ppcmds +val pr_evars : (int * goal) list -> std_ppcmds +val pr_evars_int : int -> (int * goal) list -> std_ppcmds +val pr_subgoals_existential : evar_declarations -> goal list -> std_ppcmds + +val ast_of_cvt_arg : tactic_arg -> Coqast.t diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 1dc43f4134..dac2d6a61c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -825,3 +825,106 @@ let prev_unproven pts = let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) + + +(* Pretty-printers. *) + +open Pp +open Printer + +let pr_tactic (s,l) = + gentacpr (Ast.ope (s,(List.map ast_of_cvt_arg l))) + +let pr_rule = function + | Prim r -> pr_prim_rule r + | Tactic texp -> hOV 0 (pr_tactic texp) + | Context ctxt -> pr_ctxt ctxt + | Local_constraints lc -> [< 'sTR"Local constraint change" >] + +let thin_sign osign (x,y) = + let com_nsign = List.combine x y in + List.split + (map_succeed (fun (id,ty) -> + if (not (mem_sign osign id)) + or (id,ty) <> (lookup_sign id osign) then + (id,ty) + else failwith "caught") com_nsign) + +let rec print_proof sigma osign pf = + let {evar_env=env; evar_concl=cl; + evar_info=info; evar_body=body} = pf.goal in + let env' = change_hyps (fun sign -> thin_sign osign sign) env in + match pf.ref with + | None -> + hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl; + evar_info=info; evar_body=body} >] + | Some(r,spfl) -> + let sign = var_context env in + hOV 0 [< hOV 0 (pr_seq {evar_env=env'; evar_concl=cl; + evar_info=info; evar_body=body}); + 'sPC ; 'sTR" BY "; + hOV 0 [< pr_rule r >]; 'fNL ; + 'sTR" "; + hOV 0 (prlist_with_sep pr_fnl (print_proof sigma sign) spfl) + >] + +let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>] + +let rec print_script nochange sigma osign pf = + let {evar_env=env; evar_concl=cl} = pf.goal in + let sign = var_context env 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 [< >] else (pr_change pf.goal)); + pr_rule r ; 'sTR"." ; 'fNL ; + prlist_with_sep pr_fnl + (print_script nochange sigma sign) spfl >] + +let rec print_treescript sigma osign pf = + let {evar_env=env; evar_concl=cl} = pf.goal in + let sign = var_context env in + match pf.ref with + | None -> [< >] + | Some(r,spfl) -> + [< pr_rule r ; 'sTR"." ; 'fNL ; + let prsub = + prlist_with_sep pr_fnl (print_treescript sigma sign) spfl + in + if List.length spfl > 1 then + [< 'sTR" "; hOV 0 prsub >] + else + prsub + >] + +let rec print_info_script sigma osign pf = + let {evar_env=env; evar_concl=cl} = pf.goal in + let sign = var_context env in + match pf.ref with + | None -> [< >] + | 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 + diff --git a/proofs/refiner.mli b/proofs/refiner.mli index aa7973ac0e..fa80f4329e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -118,3 +118,18 @@ val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate : global_constraints -> pftreestate -> pftreestate + + +(*s Pretty-printers. *) + +(*i*) +open Pp +(*i*) + +val print_proof : evar_declarations -> var_context -> proof_tree -> std_ppcmds +val pr_rule : rule -> std_ppcmds +val pr_tactic : tactic_expression -> std_ppcmds +val print_script : + bool -> evar_declarations -> var_context -> proof_tree -> std_ppcmds +val print_treescript : + evar_declarations -> var_context -> proof_tree -> std_ppcmds diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 85f2973c03..b70320b81a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -428,3 +428,38 @@ let hide_cbindll_tactic s tac = add_tactic s tacfun; fun l -> vernac_tactic(s,putconstrbinds l) ***) + + +(* Pretty-printers *) + +open Pp +open Printer + +let pr_com sigma goal com = + prterm (rename_bound_var + (ids_of_sign goal.hyps) + (Trad.constr_of_com sigma goal.hyps com)) + +let pr_one_binding sigma goal = function + | (Dep id,com) -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >] + | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >] + | (Com,com) -> [< pr_com sigma goal com >] + +let pr_bindings sigma goal lb = + let prf = pr_one_binding sigma goal in + match lb with + | [] -> [< prlist_with_sep pr_spc prf lb >] + | _ -> [<'sTR"with";'sPC;prlist_with_sep pr_spc prf lb >] + +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) >] + +let pr_glls glls = + hOV 0 [< pr_decls (sig_sig glls) ; 'fNL ; + prlist_with_sep pr_fnl pr_seq (sig_it glls) >] + +let pr_tactic = Refiner.pr_tactic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index be9761efdf..fd4388876a 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -222,3 +222,14 @@ val hide_cbindl_tactic : (constr * (bindOcc * constr) list) hide_combinator val hide_cbindll_tactic : ((constr * (bindOcc * constr) list) list) hide_combinator + +(*s Pretty-printing functions. *) + +(*i*) +open Pp +(*i*) + +val pr_com : 'a Evd.evar_map -> goal -> Coqast.t -> std_ppcmds +val pr_gls : goal sigma -> std_ppcmds +val pr_glls : goal list sigma -> std_ppcmds +val pr_tactic : tactic_expression -> std_ppcmds |