From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- tactics/tacticals.ml | 73 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 49 insertions(+), 24 deletions(-) (limited to 'tactics/tacticals.ml') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 958a205a..596feeec 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -159,8 +159,6 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -open Misctypes - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l) else names else @@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) -let compute_constructor_signatures isrec ((_,k as ity),u) = +let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = match Constr.kind c, recargs with | Prod (_,_,c), recarg::rest -> @@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest | Mrec (_,j) -> - if isrec && Int.equal j k then true :: true :: rest + if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end | LetIn (_,_,_,c), rest -> false :: analrec c rest @@ -263,7 +261,7 @@ let pf_with_evars glsev k gls = tclTHEN (Refiner.tclEVARS evd) (k a) gls let pf_constr_of_global gr k = - pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k + pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k (** Tacticals of Ltac defined directly in term of Proofview *) module New = struct @@ -369,9 +367,36 @@ module New = struct tclTHENSFIRSTn t1 l (tclUNIT()) let tclTHENFIRST t1 t2 = tclTHENFIRSTn t1 [|t2|] + + let tclBINDFIRST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match gls with + | [] -> tclFAIL 0 (str "Expect at least one goal.") + | hd::tl -> + Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclNEWGOALS tl <*> + Proofview.tclUNIT ans + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] + + let option_of_failure f x = try Some (f x) with Failure _ -> None + + let tclBINDLAST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match option_of_failure List.sep_last gls with + | None -> tclFAIL 0 (str "Expect at least one goal.") + | Some (last,firstn) -> + Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun newgls -> + tclEVARMAP >>= fun sigma -> + let firstn = Proofview.Unsafe.undefined sigma firstn in + Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*> + Proofview.tclUNIT ans + let tclTHENS t l = tclINDEPENDENT begin t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) @@ -465,11 +490,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) @@ -479,8 +506,8 @@ module New = struct let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) - | Evd.Evar_defined c -> match Constr.kind c with - | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with + | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to @@ -607,7 +634,7 @@ module New = struct (* 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 ind (c, t) = + rec_flag allnames tac predicate ind (c, t) = Proofview.Goal.enter begin fun gl -> let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -628,15 +655,14 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> Constant.to_string kn - | Var id -> Id.to_string id - | _ -> "\b" + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim + | _ -> mt () in user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures isrec ind in + let branchsigns = compute_constructor_signatures ~rec_flag ind in let brnames = compute_induction_names_gen false branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = @@ -659,7 +685,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.clenv_refine false clenv') + (Clenvtac.clenv_refine clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end @@ -682,7 +708,7 @@ module New = struct let gl_make_elim ind = begin fun gl -> let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, EConstr.of_constr c) + (sigma, c) end let gl_make_case_dep (ind, u) = begin fun gl -> @@ -726,8 +752,8 @@ module New = struct let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with - | None -> true,gl_make_elim - | Some _ -> false,gl_make_case_dep + | NotRecord -> true,gl_make_elim + | FakeRecord | PrimRecord _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) end @@ -742,7 +768,6 @@ module New = struct Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> let (sigma, c) = Evd.fresh_global env sigma ref in - let c = EConstr.of_constr c in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c end -- cgit v1.2.3