aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml256
1 files changed, 255 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4625cc84b..ee89b55a8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -50,7 +50,6 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL
let tclFAIL_lazy = Refiner.tclFAIL_lazy
let tclDO = Refiner.tclDO
-let tclTIMEOUT = Refiner.tclTIMEOUT
let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
let tclPROGRESS = Refiner.tclPROGRESS
let tclSHOWHYPS = Refiner.tclSHOWHYPS
@@ -367,3 +366,258 @@ let make_case_branch_assumptions ba gl =
let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
+
+(** Tacticals of Ltac defined directly in term of Proofview *)
+module New = struct
+ open Proofview
+ open Proofview.Notations
+
+ let tclTHEN t1 t2 =
+ t1 <*> tclEXTEND [] t2 []
+
+ let tclFAIL lvl msg =
+ tclZERO (Refiner.FailError (lvl,lazy msg))
+
+ let catch_failerror e =
+ try
+ Refiner.catch_failerror e;
+ tclUNIT ()
+ with e -> tclZERO e
+ let tclORELSE0 t1 t2 =
+ tclORELSE
+ t1
+ begin fun e ->
+ catch_failerror e <*> t2
+ end
+ let tclORELSE t1 t2 =
+ tclORELSE0 (tclPROGRESS t1) t2
+
+ let tclTHENS3PARTS t1 l1 repeat l2 =
+ t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2)
+ let tclTHENSFIRSTn t1 l repeat =
+ tclTHENS3PARTS t1 l repeat [||]
+ let tclTHENFIRSTn t1 l =
+ tclTHENSFIRSTn t1 l (tclUNIT())
+ let tclTHENFIRST t1 t2 =
+ t1 <*> tclFOCUS 1 1 t2
+ let tclTHENLASTn t1 l =
+ t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l)
+ let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
+ let tclTHENS t l =
+ t <*> tclDISPATCH l
+ let tclTHENLIST l =
+ List.fold_left tclTHEN (tclUNIT()) l
+
+
+ (* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+ let tclMAP tacfun l =
+ List.fold_right (fun x -> (tclTHEN (tacfun x))) l (tclUNIT())
+
+ let tclTRY t =
+ tclORELSE0 t (tclUNIT ())
+
+ let tclIFTHENELSE t1 t2 t3 =
+ tclIFCATCH t1
+ (fun () -> tclEXTEND [] t2 [])
+ (fun _ -> t3)
+ let tclIFTHENSVELSE t1 a t3 =
+ tclIFCATCH t1
+ (fun () -> tclDISPATCH (Array.to_list a))
+ (fun _ -> t3)
+ let tclIFTHENTRYELSEMUST t1 t2 =
+ tclIFTHENELSE t1 (tclTRY t2) t2
+
+ (* Try the first tactic that does not fail in a list of tactics *)
+ let rec tclFIRST = function
+ | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic."))
+ | t::rest -> tclORELSE0 t (tclFIRST rest)
+
+ let rec tclFIRST_PROGRESS_ON tac = function
+ | [] -> tclFAIL 0 (str "No applicable tactic")
+ | [a] -> tac a (* so that returned failure is the one from last item *)
+ | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl)
+
+ let rec tclDO n t =
+ if n < 0 then
+ tclZERO (Errors.UserError (
+ "Refiner.tclDO",
+ str"Wrong argument : Do needs a positive integer.")
+ )
+ else if n = 0 then tclUNIT ()
+ else if n = 1 then t
+ else tclTHEN t (tclDO (n-1) t)
+
+ let rec tclREPEAT0 t =
+ tclIFCATCH t
+ (fun () -> tclEXTEND [] (tclREPEAT0 t) [])
+ (fun _ -> tclUNIT ())
+ let tclREPEAT t =
+ tclREPEAT0 (tclPROGRESS t)
+ let rec tclREPEAT_MAIN0 t =
+ tclIFCATCH t
+ (fun () -> tclFOCUS 1 1 (tclREPEAT_MAIN0 t))
+ (fun _ -> tclUNIT ())
+ let tclREPEAT_MAIN t =
+ tclREPEAT_MAIN0 (tclPROGRESS t)
+
+ let tclCOMPLETE t =
+ t >= fun res ->
+ (tclEXTEND
+ []
+ (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
+ []
+ ) <*>
+ tclUNIT res
+
+ (* Try the first thats solves the current goal *)
+ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
+
+
+ let tclWITHHOLES accept_unresolved_holes tac sigma x =
+ tclEVARMAP >= fun sigma_initial ->
+ if sigma == sigma_initial then tac x
+ else
+ let check_evars env new_sigma sigma initial_sigma =
+ try
+ Refiner.check_evars env new_sigma sigma initial_sigma;
+ tclUNIT ()
+ with e ->
+ tclZERO e
+ in
+ let check_evars_if =
+ if not accept_unresolved_holes then
+ tclEVARMAP >= fun sigma_final ->
+ tclENV >= fun env ->
+ check_evars env sigma_final sigma sigma_initial
+ else
+ tclUNIT ()
+ in
+ Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if
+
+ let nthDecl m =
+ Goal.hyps >- fun hyps ->
+ let hyps = Environ.named_context_of_val hyps in
+ try Goal.return (List.nth hyps (m-1))
+ with Failure _ -> error "No such assumption."
+
+ let nthHypId m = nthDecl m >- fun (id,_,_) -> Goal.return id
+ let nthHyp m = nthHypId m >- fun id -> Goal.return (mkVar id)
+
+ let onNthHypId m tac =
+ nthHypId m >>- tac
+ let onNthHyp m tac =
+ nthHyp m >>- tac
+
+ let onLastHypId = onNthHypId 1
+ let onLastHyp = onNthHyp 1
+
+ let onNthDecl m tac = nthDecl m >>- tac
+ let onLastDecl = onNthDecl 1
+
+ let ifOnHyp pred tac1 tac2 id =
+ Tacmach.New.pf_get_hyp_typ id >>- fun typ ->
+ if pred (id,typ) then
+ tac1 id
+ else
+ tac2 id
+
+ let fullGoal =
+ Tacmach.New.pf_ids_of_hyps >- fun hyps ->
+ Goal.return (None :: List.map Option.make hyps)
+
+ let tryAllHyps tac =
+ Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+ tclFIRST_PROGRESS_ON tac hyps
+ let tryAllHypsAndConcl tac =
+ fullGoal >>- fun fullGoal ->
+ tclFIRST_PROGRESS_ON tac fullGoal
+
+ let onClause tac cl =
+ Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+ tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
+
+ (* Find the right elimination suffix corresponding to the sort of the goal *)
+ (* c should be of type A1->.. An->B with B an inductive definition *)
+ let general_elim_then_using mk_elim
+ isrec allnames tac predicate (indbindings,elimbindings)
+ ind indclause =
+ Tacmach.New.of_old (mk_elim ind) >>- fun elim ->
+ (* applying elimination_scheme just a little modified *)
+ let indclause' = clenv_match_args indbindings indclause in
+ Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+ Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) >>- fun elimclause ->
+ let indmv =
+ match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
+ | Meta mv -> mv
+ | _ -> anomaly (str"elimination")
+ in
+ let pmv =
+ let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
+ match kind_of_term p with
+ | Meta p -> p
+ | _ ->
+ let name_elim =
+ match kind_of_term elim with
+ | Const kn -> string_of_con kn
+ | Var id -> string_of_id id
+ | _ -> "\b"
+ in
+ error ("The elimination combinator " ^ name_elim ^ " is unknown.")
+ in
+ let elimclause' = clenv_fchain indmv elimclause indclause' in
+ let elimclause' = clenv_match_args elimbindings elimclause' in
+ let branchsigns = compute_construtor_signatures isrec ind in
+ let brnames = compute_induction_names (Array.length branchsigns) allnames in
+ let after_tac ce i =
+ let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in
+ let ba = { branchsign = branchsigns.(i);
+ branchnames = brnames.(i);
+ nassums =
+ List.fold_left
+ (fun acc b -> if b then acc+2 else acc+1)
+ 0 branchsigns.(i);
+ branchnum = i+1;
+ ity = ind;
+ largs = List.map (clenv_nf_meta ce) largs;
+ pred = clenv_nf_meta ce hd }
+ in
+ tac ba
+ in
+ let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in
+ let elimclause' =
+ match predicate with
+ | None -> elimclause'
+ | Some p ->
+ clenv_unify ~flags:Unification.elim_flags
+ Reduction.CONV (mkMeta pmv) p elimclause'
+ in
+ new_elim_res_pf_THEN_i elimclause' branchtacs
+
+ let elimination_then_using tac predicate bindings c =
+ Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>- fun (ind,t) ->
+ Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>- fun indclause ->
+ let isrec,mkelim =
+ if (Global.lookup_mind (fst ind)).mind_record
+ then false,gl_make_case_dep
+ else true,gl_make_elim
+ in
+ general_elim_then_using mkelim isrec
+ None tac predicate bindings ind indclause
+
+ let case_then_using =
+ general_elim_then_using gl_make_case_dep false
+
+ let case_nodep_then_using =
+ general_elim_then_using gl_make_case_nodep false
+
+
+ let elimination_then tac = elimination_then_using tac None
+
+ let elim_on_ba tac ba =
+ Tacmach.New.of_old (make_elim_branch_assumptions ba) >>- fun branches ->
+ tac branches
+
+ let case_on_ba tac ba =
+ Tacmach.New.of_old (make_case_branch_assumptions ba) >>- fun branches ->
+ tac branches
+end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 01:47:14 +0000