(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* (goal list * validation) 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 pf_status pf = pf.open_subgoals let is_complete pf = (0 = (pf_status pf)) 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 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] gives [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ; (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] *) let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) (l : proof_tree list) = match nl with | [] -> [] | h::t -> let m,l = list_chop h l in (List.hd fl m) :: (mapshape t (List.tl fl) l) (* [frontier : proof_tree -> goal list * validation] given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals to be solved to complete the proof, and [v] is the corresponding validation *) let rec frontier p = match p.ref with | None -> ([p.goal], (fun lp' -> let p' = List.hd lp' in if p'.goal = p.goal then p' else errorlabstrm "Refiner.frontier" (str"frontier was handed back a ill-formed proof."))) | Some(r,pfl) -> let gll,vl = List.split(List.map frontier pfl) in (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')})) let rec frontier_map_rec f n p = if n < 1 || n > p.open_subgoals then p else match p.ref with | None -> let p' = f p in if p'.goal == p.goal || p'.goal = p.goal then p' else errorlabstrm "Refiner.frontier_map" (str"frontier_map was handed back a ill-formed proof.") | Some(r,pfl) -> let (_,rpfl') = List.fold_left (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')} let frontier_map f n p = let nmax = p.open_subgoals in let n = if n < 0 then nmax + n + 1 else n in if n < 1 || n > nmax then errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); frontier_map_rec f n p let rec frontier_mapi_rec f i p = if p.open_subgoals = 0 then p else match p.ref with | None -> let p' = f i p in if p'.goal == p.goal || p'.goal = p.goal then p' else errorlabstrm "Refiner.frontier_mapi" (str"frontier_mapi was handed back a ill-formed proof.") | Some(r,pfl) -> let (_,rpfl') = List.fold_left (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')} let frontier_mapi f p = frontier_mapi_rec f 1 p (* [list_pf p] is the lists of goals to be solved in order to complete the proof [p] *) let list_pf p = fst (frontier p) 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 } (* Tactics table. *) let tac_tab = Hashtbl.create 17 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 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") (* refiner r is a tactic applying the rule r *) let bad_subproof () = anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") let check_subproof_connection gl spfl = if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) then (bad_subproof (); false) else true 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 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" (* [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 (* 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)) 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 (* [rc_of_pfsigma : proof sigma -> readable_constraints] *) let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal (* [rc_of_glsigma : proof sigma -> readable_constraints] *) let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it (* [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 *) 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 () else !meta_cnt in f in let open_obligations = ref [] in let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf | {ref=Some(Tactic (_,hidden_proof),spfl)} -> let sgl,v = frontier hidden_proof in let flat_proof = v spfl in proof_extractor vl flat_proof | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf | {ref=None;goal=goal} -> let visible_rels = map_succeed (fun id -> try let n = list_index id vl in (n,id) with Not_found -> failwith "caught") (ids_of_named_context 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)) sorted_rels in let abs_concl = List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c) sorted_env goal.evar_concl in let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in let meta = next_meta () in 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" in let pfterm = proof_extractor [] pf in (pfterm, List.rev !open_obligations) (*********************) (* Tacticals *) (*********************) (* unTAC : tactic -> goal sigma -> proof sigma *) let unTAC tac g = let (gl_sigma,v) = tac g in { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma } let unpackage glsig = (ref (glsig.sigma)),glsig.it let repackage r v = {it=v;sigma = !r} let apply_sig_tac r tac g = check_for_interrupt (); (* Breakpoint *) let glsigma,v = tac (repackage r g) in r := glsigma.sigma; (glsigma.it,v) let idtac_valid = function [pf] -> pf | _ -> anomaly "Refiner.idtac_valid" (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} (* identity tactic without any message *) 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 (* 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 (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,s)) let start_tac gls = let (sigr,g) = unpackage gls in (sigr,[g],idtac_valid) let finish_tac (sigr,gl,p) = (repackage sigr gl, p) (* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *) let thensf_tac taci tac (sigr,gs,p) = let n = Array.length taci in let nsg = List.length gs in if nsg apply_sig_tac sigr (if i apply_sig_tac sigr (if i<0 then tac else taci.(i))) (n-nsg) gs) in (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) (* Apply [tac i] on the ith subgoal (no subgoals number check) *) let thensi_tac tac (sigr,gs,p) = let gll,pl = List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) let then_tac tac = thensf_tac [||] tac let non_existent_goal n = errorlabstrm ("No such goal: "^(string_of_int n)) (str"Trying to apply a tactic to a non existent goal") (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from the last goal (i=-1). *) let theni_tac i tac ((_,gl,_) as subgoals) = let nsg = List.length gl in let k = if i < 0 then nsg + i + 1 else i in if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.") else if k >= 1 & k <= nsg then thensf_tac (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC subgoals else non_existent_goal k (* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] to [gls] and applies [t1], ..., [tn] to the [n] first resulting subgoals, and [tac2] to the others subgoals. Raises an error if the number of resulting subgoals is strictly less than [n] *) let tclTHENSFIRSTn tac1 taci tac gls = finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls))) (* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] to [gls] and applies [t1], ..., [tn] to the [n] last resulting subgoals, and [tac2] to the other subgoals. Raises an error if the number of resulting subgoals is strictly less than [n] *) let tclTHENSLASTn tac1 tac taci gls = finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls))) (* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the number of subgoals is *) let tclTHEN_i tac taci gls = finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2 (* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises an error if the number of resulting subgoals is not [n] *) let tclTHENSV tac1 tac2v = tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.") let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) (* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the last resulting subgoal *) let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] (* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC (* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More convenient than [tclTHEN] when [n] is large. *) let rec tclTHENLIST = function [] -> tclIDTAC | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) (* various progress criterions *) let same_goal gl subgoal = (hypotheses subgoal) = (hypotheses gl) & eq_constr (conclusion subgoal) (conclusion gl) let weak_progress gls ptree = (List.length gls.it <> 1) or (not (same_goal (List.hd gls.it) ptree.it)) (* Il y avait ici un ts_eq ........ *) let progress gls ptree = (weak_progress gls ptree) or (not (ptree.sigma == gls.sigma)) (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in if progress (fst rslt) ptree then rslt else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") (* weak_PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged, possibly modifying sigma *) let tclWEAK_PROGRESS tac ptree = let rslt = tac ptree in if weak_progress (fst rslt) ptree then rslt else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.") (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, one of them being identical to the original goal *) let tclNOTSAMEGOAL (tac : tactic) goal = let rslt = tac goal in let gls = (fst rslt).it in if List.exists (same_goal goal.it) gls then errorlabstrm "Refiner.tclNOTSAMEGOAL" (str"Tactic generated a subgoal identical to the original goal.") else rslt (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) | e when catchable_exception e -> check_for_interrupt (); t2 g | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> check_for_interrupt (); t2 g | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) | Stdpp.Exc_located (s,FailError (lvl,s')) -> raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) let tclTRY f = (tclORELSE0 f tclIDTAC) let tclTHENTRY f g = (tclTHEN f (tclTRY g)) (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) let ite_gen tcal tac_if continue tac_else gl= let success=ref false in let tac_if0 gl= let result=tac_if gl in success:=true;result in let tac_else0 e gl= if !success then raise e else tac_else gl in try tcal tac_if0 continue gl with (* Breakpoint *) | e when catchable_exception e -> check_for_interrupt (); tac_else0 e gl | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e -> check_for_interrupt (); tac_else0 e gl | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) | Stdpp.Exc_located (s,FailError (lvl,s')) -> raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) let tclIFTHENELSE=ite_gen tclTHEN (* Idem with tclTHENS and tclTHENSV *) let tclIFTHENSELSE=ite_gen tclTHENS let tclIFTHENSVELSE=ite_gen tclTHENSV (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") (* Try the first thats solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) (* Iteration tacticals *) let tclDO n t = let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); if k = 0 then tclIDTAC else if k = 1 then t else (tclTHEN t (dorec (k-1))) in dorec n (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Repeat on the first subgoal (no failure if no more subgoal) *) let rec tclREPEAT_MAIN t g = (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else tclIDTAC)) tclIDTAC) g (*s Tactics handling a list of goals. *) type validation_list = proof_tree list -> proof_tree list type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list (* Functions working on goal list for correct backtracking in Prolog *) let tclFIRSTLIST = tclFIRST let tclIDTAC_list gls = (gls, fun x -> x) (* first_goal : goal list sigma -> goal sigma *) let first_goal gls = let gl = gls.it and sig_0 = gls.sigma in if gl = [] then error "first_goal"; { it = List.hd gl; sigma = sig_0 } (* goal_goal_list : goal sigma -> goal list sigma *) let goal_goal_list gls = let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 } (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) let apply_tac_list tac glls = let (sigr,lg) = unpackage glls in match lg with | (g1::rest) -> let (gl,p) = apply_sig_tac sigr tac g1 in let n = List.length gl in (repackage sigr (gl@rest), fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest) | _ -> error "apply_tac_list" let then_tactic_list tacl1 tacl2 glls = let (glls1,pl1) = tacl1 glls in let (glls2,pl2) = tacl2 glls1 in (glls2, compose pl1 pl2) (* Transform a tactic_list into a tactic *) let tactic_list_tactic tac gls = let (glres,vl) = tac (goal_goal_list gls) in (glres, compose idtac_valid vl) (* 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 proof-tree remembering how to rebuild the global proof-tree possibly after modification of one of the focused children proof-tree. The number in the stack corresponds to either the selected subtree and the validation is a function from a proof-tree list consisting only of one proof-tree to the global proof-tree or -1 when the move is done behind a registered tactic in which case the validation corresponds to a constant function giving back the original proof-tree. *) type pftreestate = { tpf : proof_tree ; tpfsigma : evar_map; tstack : (int * validation) list } let proof_of_pftreestate pts = pts.tpf let is_top_pftreestate pts = pts.tstack = [] let cursor_of_pftreestate pts = List.map fst pts.tstack let evc_of_pftreestate pts = pts.tpfsigma let top_goal_of_pftreestate pts = { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma } let nth_goal_of_pftreestate n pts = let goals = fst (frontier pts.tpf) in 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]; tstack = tl; tpfsigma = pts.tpfsigma }) | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) (match pts.tpf.ref with | Some (Tactic (_,spf),_) -> let v = (fun pfl -> pts.tpf) in { tpf = spf; tstack = (-1,v)::pts.tstack; tpfsigma = pts.tpfsigma } | _ -> error "traverse: not a tactic-node") | n -> (* when n>0, go to the nth child *) let (npf,v) = descend n pts.tpf in { tpf = npf; tpfsigma = pts.tpfsigma; tstack = (n,v):: pts.tstack } let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc } let app_tac sigr tac p = let (gll,v) = tac {it=p.goal;sigma= !sigr} in sigr := gll.sigma; v (List.map leaf gll.it) (* solve the nth subgoal with tactic tac *) let solve_nth_pftreestate n tac pts = let sigr = ref pts.tpfsigma in let tpf' = frontier_map (app_tac sigr tac) n 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 { tpf = tpf''; tpfsigma = !sigr; tstack = pts.tstack } let solve_pftreestate = solve_nth_pftreestate 1 (* This function implements a poor man's undo at the current goal. This is a gross approximation as it does not attempt to clean correctly the global constraints given in tpfsigma. *) let weak_undo_pftreestate pts = let pf = leaf pts.tpf.goal in { tpf = pf; tpfsigma = pts.tpfsigma; tstack = pts.tstack } (* Gives a new proof (a leaf) of a goal gl *) let mk_pftreestate g = { tpf = leaf g; tstack = []; tpfsigma = Evd.empty } (* Extracts a constr from a proof-tree state ; raises an error if the proof is not complete or the state does not correspond to the head of the proof-tree *) let extract_open_pftreestate pts = extract_open_proof pts.tpfsigma pts.tpf let extract_pftreestate pts = if pts.tstack <> [] then errorlabstrm "extract_pftreestate" (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 if subgoals <> [] then errorlabstrm "extract_proof" (str "Attempt to save an incomplete proof"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env pts.tpfsigma pfterm (*** local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm ***) (* Focus on the first leaf proof in a proof-tree state *) let rec first_unproven pts = let pf = (proof_of_pftreestate pts) in if is_complete_proof pf then errorlabstrm "first_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts else let childnum = list_try_find_i (fun n pf -> if not(is_complete_proof pf) then n else failwith "caught") 1 (children_of_proof pf) in first_unproven (traverse childnum pts) (* Focus on the last leaf proof in a proof-tree state *) let rec last_unproven pts = let pf = proof_of_pftreestate pts in if is_complete_proof pf then errorlabstrm "last_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts else let children = (children_of_proof pf) in let nchilds = List.length children in let childnum = list_try_find_i (fun n pf -> if not(is_complete_proof pf) then n else failwith "caught") 1 (List.rev children) in last_unproven (traverse (nchilds-childnum+1) pts) let rec nth_unproven n pts = let pf = proof_of_pftreestate pts in if is_complete_proof pf then errorlabstrm "nth_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then if n = 1 then pts else errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") else let children = children_of_proof pf in let rec process i k = function | [] -> errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") | pf1::rest -> let k1 = nb_unsolved_goals pf1 in if k1 < k then process (i+1) (k-k1) rest else nth_unproven k (traverse i pts) in process 1 n children let rec node_prev_unproven loc pts = let pf = proof_of_pftreestate pts in match cursor_of_pftreestate pts with | [] -> last_unproven pts | n::l -> if is_complete_proof pf or loc = 1 then node_prev_unproven n (traverse 0 pts) else let child = List.nth (children_of_proof pf) (loc - 2) in if is_complete_proof child then node_prev_unproven (loc - 1) pts else first_unproven (traverse (loc - 1) pts) let rec node_next_unproven loc pts = let pf = proof_of_pftreestate pts in match cursor_of_pftreestate pts with | [] -> first_unproven pts | n::l -> if is_complete_proof pf || loc = (List.length (children_of_proof pf)) then node_next_unproven n (traverse 0 pts) else if is_complete_proof (List.nth (children_of_proof pf) loc) then node_next_unproven (loc + 1) pts else last_unproven(traverse (loc + 1) pts) let next_unproven pts = let pf = proof_of_pftreestate pts in if is_leaf_proof pf then match cursor_of_pftreestate pts with | [] -> error "next_unproven" | n::_ -> node_next_unproven n (traverse 0 pts) else node_next_unproven (List.length (children_of_proof pf)) pts let prev_unproven pts = let pf = proof_of_pftreestate pts in if is_leaf_proof pf then match cursor_of_pftreestate pts with | [] -> error "prev_unproven" | n::_ -> node_prev_unproven n (traverse 0 pts) else node_prev_unproven 1 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 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"") 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"") 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 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 msgnl (hov 0 (str" == " ++ print_subscript (sig_sig gls) sign pf)) with e when catchable_exception e -> msgnl (hov 0 (str "Info failed to apply validation")) end; res