diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 815 |
1 files changed, 459 insertions, 356 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0b920066f..289d5109a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -26,7 +26,7 @@ open Evd open Pfedit open Tacred open Genredexpr -open Tacmach +open Tacmach.New open Logic open Clenv open Refiner @@ -43,6 +43,7 @@ open Locus open Locusops open Misctypes open Proofview.Notations +open Sigma.Notations let nb_prod x = let rec count n c = @@ -57,7 +58,7 @@ let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost -let typ_of = Retyping.get_type_of +let typ_of env sigma c = Retyping.get_type_of env (Sigma.to_evar_map sigma) c open Goptions @@ -126,6 +127,19 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } +(* Shrinking of abstract proofs. *) + +let shrink_abstract = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "shrinking of abstracted proofs"; + optkey = ["Shrink"; "Abstract"]; + optread = (fun () -> !shrink_abstract) ; + optwrite = (fun b -> shrink_abstract := b) } + (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -144,7 +158,7 @@ let _ = optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; - optread = (fun () -> !bracketing_last_or_and_intro_pattern) ; + optread = (fun () -> !bracketing_last_or_and_intro_pattern); optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } (*********************************************) @@ -158,21 +172,22 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store (id, c, t) b = - Proofview.Refine.refine ~unsafe:true begin fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in let ctx = named_context_val env in let nctx = push_named_context_val (id, c, t) ctx in let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar id) b in let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in - sigma, mkNamedLambda_or_LetIn (id, c, t) ev - end + Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma) + end } let introduction ?(check=true) id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in @@ -184,51 +199,55 @@ let introduction ?(check=true) id = | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b | LetIn (_, c, t, b) -> unsafe_intro env store (id, Some c, t) b | _ -> raise (RefinerError IntroNeedsProduct) - end + end } let refine = Tacmach.refine let convert_concl ?(check=true) ty k = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in - Proofview.Refine.refine ~unsafe:true begin fun sigma -> - let sigma = + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let Sigma ((), sigma, p) = if check then begin + let sigma = Sigma.to_evar_map sigma in ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; - sigma - end else sigma in - let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ~store ty in - (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty)) - end - end + Sigma.Unsafe.of_pair ((), sigma) + end else Sigma.here () sigma in + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in + let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in + Sigma (ans, sigma, p +> q) + end } + end } let convert_hyp ?(check=true) d = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.raw_concl gl in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in - Proofview.Refine.refine ~unsafe:true (fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty) - end + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Evarutil.new_evar env sigma ~principal:true ~store ty + end } + end } let convert_concl_no_check = convert_concl ~check:false let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> try let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in Proofview.Unsafe.tclEVARS sigma with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") -end +end } let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y @@ -261,7 +280,7 @@ let error_replacing_dependency env sigma id err = errorlabstrm "" (replacing_dependency_msg env sigma id err) let thin l gl = - try thin l gl + try Tacmach.thin l gl with Evarutil.ClearDependencyError (id,err) -> error_clear_dependency (pf_env gl) (project gl) id err @@ -300,7 +319,7 @@ let rename_hyp repl = match dom with | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -332,10 +351,12 @@ let rename_hyp repl = let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in let instance = List.map (fun (id, _, _) -> mkVar id) hyps in - Proofview.Refine.refine ~unsafe:true begin fun sigma -> - Evarutil.new_evar_instance nctx sigma nconcl ~store instance - end - end + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in + Sigma.Unsafe.of_pair (c, sigma) + end } + end } (**************************************************************) (* Fresh names *) @@ -380,7 +401,7 @@ let find_name mayrepl decl naming gl = match naming with | NamingAvoid idl -> (* this case must be compatible with [find_intro_names] below. *) let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> @@ -396,16 +417,16 @@ let find_name mayrepl decl naming gl = match naming with (**************************************************************) let assert_before_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENLAST (Proofview.V82.tactic (fun gl -> - try internal_cut b id t gl + try Tacmach.internal_cut b id t gl with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) @@ -414,16 +435,16 @@ let assert_before na = assert_before_gen false (naming_of_name na) let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id)) let assert_after_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (fun gl -> - try internal_cut_rev b id t gl + try Tacmach.internal_cut_rev b id t gl with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) @@ -460,7 +481,7 @@ let cofix ido gl = match ido with type tactic_reduction = env -> evar_map -> constr -> constr let pf_reduce_decl redfun where (id,c,ty) gl = - let redfun' = pf_reduce redfun gl in + let redfun' = Tacmach.pf_reduce redfun gl in match c with | None -> if where == InHypValueOnly then @@ -540,11 +561,11 @@ let bind_red_expr_occurrences occs nbcl redexp = certain hypothesis *) let reduct_in_concl (redfun,sty) gl = - Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl + Proofview.V82.of_tactic (convert_concl_no_check (Tacmach.pf_reduce redfun gl (Tacmach.pf_concl gl)) sty) gl let reduct_in_hyp ?(check=false) redfun (id,where) gl = Proofview.V82.of_tactic (convert_hyp ~check - (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl + (pf_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl)) gl let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -571,13 +592,13 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl = let e_reduct_in_concl (redfun,sty) gl = Proofview.V82.of_tactic - (let sigma, c' = (pf_apply redfun gl (pf_concl gl)) in + (let sigma, c' = (Tacmach.pf_apply redfun gl (Tacmach.pf_concl gl)) in Proofview.Unsafe.tclEVARS sigma <*> convert_concl_no_check c' sty) gl let e_reduct_in_hyp ?(check=false) redfun (id,where) gl = Proofview.V82.of_tactic - (let sigma, decl' = pf_e_reduce_decl redfun where (pf_get_hyp gl id) gl in + (let sigma, decl' = pf_e_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl in Proofview.Unsafe.tclEVARS sigma <*> convert_hyp ~check decl') gl @@ -588,17 +609,12 @@ let e_reduct_option ?(check=false) redfun = function (** Versions with evars to maintain the unification of universes resulting from conversions. *) -let tclWITHEVARS f k = - Proofview.Goal.enter begin fun gl -> - let evm, c' = f gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k c') - end - let e_change_in_concl (redfun,sty) = - tclWITHEVARS - (fun gl -> redfun (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) - (Proofview.Goal.raw_concl gl)) - (fun c -> convert_concl_no_check c sty) + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in + Sigma.Unsafe.of_pair (convert_concl_no_check c sty, sigma) + end } let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma = match c with @@ -617,11 +633,12 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma', (id,Some b',ty') let e_change_in_hyp redfun (id,where) = - tclWITHEVARS - (fun gl -> e_pf_change_decl redfun where - (Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl)) - (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)) - convert_hyp + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> + let sigma = Sigma.to_evar_map sigma in + let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let sigma, c = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + Sigma.Unsafe.of_pair (convert_hyp c, sigma) + end } type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr @@ -683,7 +700,7 @@ let change_option occl t = function | None -> change_in_concl occl t let change chg c cls gl = - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in + let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in Proofview.V82.of_tactic (Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> change_option (bind_change_occurrences occs chg) c (Some (id,where)) @@ -724,12 +741,12 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl goal = - let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in + let cl = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in let tac = tclMAP (fun (where,redexp) -> e_reduct_option ~check - (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in + (Redexpr.reduction_of_red_expr (Tacmach.pf_env goal) redexp) where) redexps in if check then with_check tac goal else tac goal (* Unfolding occurrences of a constant *) @@ -766,9 +783,9 @@ let build_intro_tac id dest tac = match dest with Proofview.V82.tactic (move_hyp id dest); tac id] let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = nf_evar (Proofview.Goal.sigma gl) concl in + let concl = nf_evar (Tacmach.New.project gl) concl in match kind_of_term concl with | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> let name = find_name false (name,None,t) name_flag gl in @@ -792,7 +809,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end - end + end } let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false @@ -856,14 +873,14 @@ let get_previous_hyp_position id gl = aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let intro_replacing id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let next_hyp = get_next_hyp_position id gl in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (thin_for_replacing [id]); introduction id; Proofview.V82.tactic (move_hyp id next_hyp); ] - end + end } (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' @@ -875,7 +892,7 @@ let intro_replacing id = (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -884,16 +901,16 @@ let intros_possibly_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) - end + end } (* This version assumes that replacement is actually possible *) let intros_replacing ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Proofview.V82.tactic (thin_for_replacing ids)) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) - end + end } (* User-level introduction tactics *) @@ -911,7 +928,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = env (project gl) ccl)) | x -> x in - try aux (pf_concl gl) + try aux (Tacmach.pf_concl gl) with Redelimination -> None let is_quantified_hypothesis id g = @@ -937,10 +954,10 @@ let depth_of_quantified_hypothesis red h gl = str".") let intros_until_gen red h = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in Tacticals.New.tclDO n (if red then introf else intro) - end + end } let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) @@ -948,7 +965,7 @@ let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true -let tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl +let tclCHECKVAR id gl = ignore (Tacmach.pf_get_hyp gl id); tclIDTAC gl let try_intros_until_id_check id = Tacticals.New.tclORELSE (intros_until_id id) (Proofview.V82.tactic (tclCHECKVAR id)) @@ -963,12 +980,15 @@ let rec intros_move = function Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false) (intros_move rest) +let run_delayed env sigma c = + Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma } + (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> - let (sigma',cbl) = f env sigma in + let (cbl, sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') @@ -978,20 +998,20 @@ let onOpenInductionArg env sigma tac = function (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let pending = (sigma,sigma) in tac clear_flag (pending,(c,NoBindings)) - end)) + end })) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + (Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let pending = (sigma,sigma) in tac clear_flag (pending,(mkVar id,NoBindings)) - end) + end }) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -1016,9 +1036,9 @@ let map_induction_arg f = function (****************************************) let cut c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_nf_concl gl in let is_sort = try @@ -1034,15 +1054,15 @@ let cut c = let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = local_strong whd_betaiota sigma c in - Proofview.Refine.refine ~unsafe:true begin fun h -> - let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in - let (h, x) = Evarutil.new_evar env h c in + Proofview.Refine.refine ~unsafe:true { run = begin fun h -> + let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in + let Sigma (x, h, q) = Evarutil.new_evar env h c in let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - (h, mkApp (f, [|x|])) - end + Sigma (mkApp (f, [|x|]), h, p +> q) + end } else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") - end + end } let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in @@ -1086,7 +1106,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) if not with_evars && occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Proofview.V82.tactic (refine_no_check new_hyp_prf) in + let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN @@ -1151,12 +1171,12 @@ let enforce_prop_bound_names rename tac = mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t') | _ -> print_int i; Pp.msg (print_constr t); assert false in let rename_branch i = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in change_concl (aux env sigma i t) - end in + end } in (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) tac (Array.map rename_branch nn) @@ -1171,9 +1191,9 @@ let rec contract_letin_in_lam_header c = let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = @@ -1184,7 +1204,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) - end + end } (* * Elimination tactic with bindings and using an arbitrary @@ -1201,20 +1221,20 @@ type eliminator = { } let general_elim_clause_gen elimtac indclause elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in let elimt = Retyping.get_type_of env sigma elimc in let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause - end + end } let general_elim with_evars clear_flag (c, lbindc) elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in @@ -1222,14 +1242,14 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) - end + end } (* Case analysis tactics *) let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in let t = Retyping.get_type_of env sigma c in let (mind,_) = reduce_to_quantified_ind env sigma t in @@ -1239,11 +1259,13 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + let tac = (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let general_case_analysis with_evars clear_flag (c,lbindc as cx) = match kind_of_term c with @@ -1276,11 +1298,13 @@ let find_eliminator c gl = let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> - let evd, elim = find_eliminator c gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) + (Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> + let sigma, elim = find_eliminator c gl in + let tac = (general_elim with_evars clear_flag cx elim) - end) + in + Sigma.Unsafe.of_pair (tac, sigma) + end }) begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default @@ -1325,9 +1349,9 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta (nth_arg i elimclause.templval.rebus) in @@ -1348,7 +1372,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) - end + end } let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1403,9 +1427,9 @@ let make_projection env sigma params cstr sign elim i n c u = in elim let descend_in_conjunctions avoid tac (err, info) c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in try let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in @@ -1424,9 +1448,9 @@ let descend_in_conjunctions avoid tac (err, info) c = NotADefinedRecordUseScheme (snd elim) in Tacticals.New.tclFIRST (List.init n (fun i -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match make_projection env sigma params cstr sign elim i n c u with | None -> Tacticals.New.tclFAIL 0 (mt()) | Some (p,pt) -> @@ -1435,31 +1459,32 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end)) + end })) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err - end + end } (****************************************************) (* Resolution tactics *) (****************************************************) let solve_remaining_apply_goals = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> if !apply_solve_class_goals then try let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let evd = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in - if Typeclasses.is_class_type sigma concl then - let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS evd') - (Proofview.V82.tactic (refine_no_check c')) - else Proofview.tclUNIT () - with Not_found -> Proofview.tclUNIT () - else Proofview.tclUNIT () - end + if Typeclasses.is_class_type evd concl then + let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in + let tac = + (Proofview.V82.tactic (Tacmach.refine_no_check c')) + in + Sigma.Unsafe.of_pair (tac, evd') + else Sigma.here (Proofview.tclUNIT ()) sigma + with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma + else Sigma.here (Proofview.tclUNIT ()) sigma + end } let tclORELSEOPT t k = Proofview.tclORELSE t @@ -1470,7 +1495,7 @@ let tclORELSEOPT t k = | Some tac -> tac) let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in @@ -1479,9 +1504,9 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) step. *) let concl_nprod = nb_prod concl in let rec try_main_apply with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = @@ -1533,14 +1558,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) | PretypeError _|RefinerError _|UserError _|Failure _ -> Some (try_red_apply thm_ty0 (e, info)) | _ -> None) - end + end } in Tacticals.New.tclTHENLIST [ try_main_apply with_destruct c; solve_remaining_apply_goals; apply_clear_request clear_flag (use_clear_hyp_by_default ()) c ] - end + end } let rec apply_with_bindings_gen b e = function | [] -> Proofview.tclUNIT () @@ -1552,13 +1577,13 @@ let rec apply_with_bindings_gen b e = function let apply_with_delayed_bindings_gen b e l = let one k (loc, f) = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma, cb = f env sigma in + let (cb, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES e (general_apply b b e k (loc,cb)) sigma - end + end } in let rec aux = function | [] -> Proofview.tclUNIT () @@ -1621,18 +1646,18 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) = let apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,(d,lbind))) tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (Anonymous,None,t') naming gl in let rec aux idstoclear with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in try let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause @@ -1647,22 +1672,22 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) - end + end } in aux [] with_destruct d - end + end } let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,f)) tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let sigma, c = f env sigma in + let sigma = Tacmach.New.project gl in + let (c, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,c)) tac) sigma - end + end } (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1682,20 +1707,20 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam *) let cut_and_apply c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in - Proofview.Refine.refine begin fun sigma -> + Proofview.Refine.refine { run = begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in - let (sigma, f) = Evarutil.new_evar env sigma typ in - let (sigma, x) = Evarutil.new_evar env sigma c1 in + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in let ans = mkApp (f, [|mkApp (c, [|x|])|]) in - (sigma, ans) - end + Sigma (ans, sigma, p +> q) + end } | _ -> error "lapply needs a non-dependent product." - end + end } (********************************************************************) (* Exact tactics *) @@ -1708,29 +1733,31 @@ let cut_and_apply c = (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) let new_exact_no_check c = - Proofview.Refine.refine ~unsafe:true (fun h -> (h, c)) + Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } let exact_check c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in - Proofview.Unsafe.tclEVARS sigma <*> + let tac = Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } -let exact_no_check = refine_no_check +let exact_no_check = Tacmach.refine_no_check let vm_cast_no_check c gl = - let concl = pf_concl gl in - refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl + let concl = Tacmach.pf_concl gl in + Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl let exact_proof c gl = - let c,ctx = Constrintern.interp_casted_constr (pf_env gl) (project gl) c (pf_concl gl) - in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl + let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl) + in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl let assumption = let rec arec gl only_eq = function @@ -1741,7 +1768,7 @@ let assumption = else Tacticals.New.tclZEROMSG (str "No such assumption.") | (id, c, t)::rest -> let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = if only_eq then (sigma, Constr.equal t concl) else @@ -1750,13 +1777,13 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id)) + Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar id) h } else arec gl only_eq rest in - let assumption_tac gl = + let assumption_tac = { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in arec gl true hyps - in + end } in Proofview.Goal.nf_enter assumption_tac (*****************************************************************) @@ -1799,7 +1826,7 @@ let check_decl env (_, c, ty) msg = msg e let clear_body ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let ctx = named_context env in @@ -1832,10 +1859,10 @@ let clear_body ids = check_is_type env concl msg in check_hyps <*> check_concl <*> - Proofview.Refine.refine ~unsafe:true begin fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma concl - end - end + end } + end } let clear_wildcards ids = Proofview.V82.tactic (tclMAP (fun (loc,id) gl -> @@ -1865,7 +1892,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in + let clause = Tacmach.pf_apply make_clenv_binding g (c,Tacmach.pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1882,20 +1909,20 @@ let specialize (c,lbind) g = tclEVARS clause.evd, term in match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with - | Var id when Id.List.mem id (pf_ids_of_hyps g) -> + | Var id when Id.List.mem id (Tacmach.pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (Tacmach.pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (Tacmach.pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) let keep hyps = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let cl,_ = @@ -1908,7 +1935,7 @@ let keep hyps = ~init:([],[]) (Proofview.Goal.env gl) in Proofview.V82.tactic (fun gl -> thin cl gl) - end + end } (************************) (* Introduction tactics *) @@ -1925,7 +1952,7 @@ let check_number_of_constructors expctdnumopt i nconstr = if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let cl = Tacmach.New.pf_nf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -1935,16 +1962,19 @@ let constructor_tac with_evars expctdnumopt i lbind = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; - let sigma, cons = Evd.fresh_constructor_instance - (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in + let Sigma (cons, sigma, p) = Sigma.fresh_constructor_instance + (Proofview.Goal.env gl) sigma (fst mind, i) in let cons = mkConstructU cons in let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in + let tac = (Tacticals.New.tclTHENLIST - [Proofview.Unsafe.tclEVARS sigma; + [ convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) - end + in + Sigma (tac, sigma, p) + end } let one_constructor i lbind = constructor_tac false None i lbind @@ -1961,7 +1991,7 @@ let rec tclANY tac = function let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let cl = Tacmach.New.pf_nf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -1971,7 +2001,7 @@ let any_constructor with_evars tacopt = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; tclANY tac (List.interval 1 nconstr) - end + end } let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -2022,7 +2052,7 @@ let my_find_eq_data_decompose gl t = | Constr_matching.PatternMatchingFailure -> None let intro_decomp_eq loc l thin tac id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2033,10 +2063,10 @@ let intro_decomp_eq loc l thin tac id = (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") - end + end } let intro_or_and_pattern loc bracketed ll thin tac id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2047,7 +2077,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id = (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id]))) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv (Array.of_list ll)) - end + end } let rewrite_hyp assert_style l2r id = let rew_on l2r = @@ -2055,7 +2085,7 @@ let rewrite_hyp assert_style l2r id = let subst_on l2r x rhs = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in @@ -2077,7 +2107,7 @@ let rewrite_hyp assert_style l2r id = Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) | _ -> Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) - end + end } let rec prepare_naming loc = function | IntroIdentifier id -> NamingMustBe (loc,id) @@ -2213,10 +2243,10 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with Proofview.tclUNIT () (* apply_in_once do a replacement *) else Proofview.V82.tactic (clear [id]) in - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma,c = f env sigma in + let (c, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES false (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) @@ -2225,7 +2255,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) (tac thin None [])) sigma - end + end } and prepare_intros_loc loc dft destopt = function | IntroNaming ipat -> @@ -2288,7 +2318,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars let tac (naming,lemma) tac id = apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) else get_previous_hyp_position id gl in @@ -2299,7 +2329,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id - end + end } (* if sidecond_first then @@ -2310,7 +2340,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars *) let apply_in simple with_evars clear_flag id lemmas ipat = - let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, fun _ sigma -> sigma, l)) lemmas in + let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in general_apply_in false simple simple with_evars clear_flag id lemmas ipat let apply_delayed_in simple with_evars clear_flag id lemmas ipat = @@ -2341,11 +2371,10 @@ let decode_hyp = function *) let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in let t = match ty with Some t -> t | _ -> typ_of env sigma c in - let eq_tac gl = match with_eq with + let Sigma ((newcl, eq_tac), sigma, p) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl @@ -2353,26 +2382,31 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = | IntroIdentifier id -> id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env sigma eqdata.eq in - let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in + let sigma = Sigma.to_evar_map sigma in let sigma, _ = Typing.type_of env sigma term in - sigma, term, + let ans = term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) (clear_body [heq;id]) + in + Sigma.Unsafe.of_pair (ans, sigma) | None -> - (sigma, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in - let (sigma,newcl,eq_tac) = eq_tac gl in - Tacticals.New.tclTHENLIST - [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check newcl DEFAULTcast; + Sigma.here (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) sigma + in + let tac = + Tacticals.New.tclTHENLIST + [ convert_concl_no_check newcl DEFAULTcast; intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ] - end + in + Sigma (tac, sigma, p) + end } let insert_before decls lasthyp env = match lasthyp with @@ -2400,55 +2434,55 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env sigma eqdata.eq in - let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in - let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in - (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) + let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in + Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) | None -> let newenv = insert_before [id,body,t] lastlhyp env in - let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in - (sigma,mkNamedLetIn id c t x) + let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in + Sigma (mkNamedLetIn id c t x, sigma, p) let letin_tac with_eq id c ty occs = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let abs = AbstractExact (id,c,ty,occs,true) in let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in (* We keep the original term to match *) - letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty - end + let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in + Sigma.here tac sigma + end } let letin_pat_tac with_eq id c occs = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in - let sigma,c = match res with + let Sigma (c, sigma, p) = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c - | Some (sigma,c) -> (sigma,c) in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) + | Some res -> res in + let tac = (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) - end + in + Sigma (tac, sigma, p) + end } (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *) let forward b usetac ipat c = match usetac with | None -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in let hd = head_ident c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (Proofview.V82.tactic (exact_no_check c)) - end + end } | Some tac -> if b then Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac @@ -2478,25 +2512,25 @@ let apply_type hdcty argl gl = let bring_hyps hyps = if List.is_empty hyps then Tacticals.New.tclIDTAC else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (instance_from_named_context hyps) in - Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = + Proofview.Refine.refine { run = begin fun sigma -> + let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in - (sigma, (mkApp (ev, args))) - end - end + Sigma (mkApp (ev, args), sigma, p) + end } + end } let revert hyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) - end + end } (* Compute a name for a generalization *) @@ -2530,9 +2564,9 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_unsafe_type_of gl c in - let env = pf_env gl in - generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl + let t = Tacmach.pf_unsafe_type_of gl c in + let env = Tacmach.pf_env gl in + generalize_goal_gen env (Tacmach.pf_ids_of_hyps gl) i o t cl let generalize_dep ?(with_let=false) c gl = let env = pf_env gl in @@ -2554,11 +2588,11 @@ let generalize_dep ?(with_let=false) c gl = -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in let body = if with_let then match kind_of_term c with - | Var id -> pi2 (pf_get_hyp gl id) + | Var id -> pi2 (Tacmach.pf_get_hyp gl id) | _ -> None else None in @@ -2575,17 +2609,17 @@ let generalize_dep ?(with_let=false) c gl = let generalize_gen_let lconstr gl = let newcl, evd = List.fold_right_i (generalize_goal gl) 0 lconstr - (pf_concl gl,project gl) + (Tacmach.pf_concl gl,Tacmach.project gl) in tclTHEN (tclEVARS evd) (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> if Option.is_empty b then Some c else None) lconstr)) gl let new_generalize_gen_let lconstr = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in let (newcl, sigma), args = @@ -2596,12 +2630,14 @@ let new_generalize_gen_let lconstr = generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar env sigma newcl in - (sigma, (applist (ev, args))) - end - end + let tac = + Proofview.Refine.refine { run = begin fun sigma -> + let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in + Sigma ((applist (ev, args)), sigma, p) + end } + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let generalize_gen lconstr = generalize_gen_let (List.map (fun ((occs,c),na) -> @@ -2695,7 +2731,7 @@ let check_unused_names names = (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names) + (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names) let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -2775,7 +2811,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = match ra with | (RecArg,deprec,recvarname) :: (IndArg,depind,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (recpat,names) = match names with | [loc,IntroNaming (IntroIdentifier id) as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in @@ -2783,37 +2819,37 @@ let induct_discharge dests avoid' tac (avoid,ra) names = | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [recpat] (fun ids thin -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin) - end) - end + end }) + end } | (IndArg,dep,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) - end + end } | (RecArg,dep,recvarname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | (OtherArg,dep,_) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | [] -> check_unused_names names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) @@ -2827,7 +2863,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in @@ -2876,7 +2912,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (atomize_one (i-1) (mkVar x::args) (x::avoid)) in atomize_one (List.length argl) [] [] - end + end } (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps @@ -3187,11 +3223,11 @@ let mk_term_eq env sigma ty t ty' t' = let make_abstract_generalize gl id concl dep ctx body c eqs args refls = let meta = Evarutil.new_meta() in let eqslen = List.length eqs in - let term, typ = mkVar id, pf_get_hyp_typ gl id in + let term, typ = mkVar id, Tacmach.pf_get_hyp_typ gl id in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) let abshypeq, abshypt = if dep then - let eq, refl = mk_term_eq (push_rel_context ctx (pf_env gl)) (project gl) (lift 1 c) (mkRel 1) typ term in + let eq, refl = mk_term_eq (push_rel_context ctx (Tacmach.pf_env gl)) (Tacmach.project gl) (lift 1 c) (mkRel 1) typ term in mkProd (Anonymous, eq, lift 1 concl), [| refl |] else concl, [||] in @@ -3252,9 +3288,9 @@ let is_defined_variable env id = match lookup_named id env with | (_, Some _, _) -> true let abstract_args gl generalize_vars dep id defined f args = - let sigma = project gl in - let env = pf_env gl in - let concl = pf_concl gl in + let sigma = Tacmach.project gl in + let env = Tacmach.pf_env gl in + let concl = Tacmach.pf_concl gl in let dep = dep || dependent (mkVar id) concl in let avoid = ref [] in let get_id name = @@ -3272,7 +3308,7 @@ let abstract_args gl generalize_vars dep id defined f args = let rel, c = Reductionops.splay_prod_n env sigma 1 prod in List.hd rel, c in - let argty = pf_unsafe_type_of gl arg in + let argty = Tacmach.pf_unsafe_type_of gl arg in let ty = (* refresh_universes_strict *) ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3313,7 +3349,7 @@ let abstract_args gl generalize_vars dep id defined f args = in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (Tacmach.pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3322,13 +3358,13 @@ let abstract_args gl generalize_vars dep id defined f args = hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars else [] in - let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in + let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls, dep, succ (List.length ctx), vars) else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.jmeq_module_name; let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in @@ -3360,15 +3396,15 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) - end + end } let rec compare_upto_variables x y = if (isVar x || isRel x) && (isVar y || isRel y) then true else compare_constr compare_upto_variables x y let specialize_eqs id gl = - let env = pf_env gl in - let ty = pf_get_hyp_typ gl id in + let env = Tacmach.pf_env gl in + let ty = Tacmach.pf_get_hyp_typ gl id in let evars = ref (project gl) in let unif env evars c1 c2 = compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 @@ -3643,7 +3679,7 @@ let guess_elim isrec dep s hyp0 gl = let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess + Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3688,7 +3724,7 @@ let is_functional_induction elimc gl = let get_eliminator elim dep s gl = match elim with | ElimUsing (elim,indsign) -> - Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign + Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in @@ -3711,10 +3747,10 @@ let recolle_clenv i params args elimclause gl = let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in (* parameters correspond to first elts of lid. *) let clauses_params = - List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i)) + List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(i)) 0 params in let clauses_args = - List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(k+i)) + List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(k+i)) 0 args in let clauses = clauses_params@clauses_args in (* iteration of clenv_fchain with all infos we have. *) @@ -3741,7 +3777,7 @@ let induction_tac with_evars params indvars elim gl = let elimc = contract_letin_in_lam_header elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in let elimclause = - pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in + Tacmach.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in (* elimclause' is built from elimclause by instanciating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) @@ -3753,9 +3789,9 @@ let induction_tac with_evars params indvars elim gl = induction applies with the induction hypotheses *) let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let concl = Tacmach.New.pf_nf_concl gl in let statuslists,lhyp0,toclear,deps,avoid,dep = cook_sign hyp0 inhyps indvars env in let dep = dep || Option.cata (fun id -> occur_var env id concl) false hyp0 in @@ -3766,9 +3802,9 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in let names = compute_induction_names (Array.length indsign) names in + let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; (* Generalize dependent hyps (but not args) *) if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr); (* side-conditions in elim (resp case) schemes come last (resp first) *) @@ -3778,15 +3814,17 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = (Array.map2 (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists)) indsign names) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim))) - end + end } let msg_not_right_number_induction_arguments scheme = str"Not the right number of induction arguments (expected " ++ @@ -3803,7 +3841,7 @@ let msg_not_right_number_induction_arguments scheme = must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac *) let induction_without_atomization isrec with_evars elim names lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in let nargs_indarg_farg = scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in @@ -3834,11 +3872,11 @@ let induction_without_atomization isrec with_evars elim names lid = ]) in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context None [] elim indvars names induct_tac - end + end } (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls gl = - if occur_var (pf_env gl) id (pf_concl gl) && + if occur_var (Tacmach.pf_env gl) id (Tacmach.pf_concl gl) && cls.concl_occs == NoOccurrences then errorlabstrm "" (str "Conclusion must be mentioned: it depends on " ++ pr_id id @@ -3856,6 +3894,7 @@ let clear_unselected_context id inhyps cls gl = | None -> tclIDTAC gl let use_bindings env sigma elim must_be_closed (c,lbind) typ = + let sigma = Sigma.to_evar_map sigma in let typ = if elim == None then (* w/o an scheme, the term has to be applied at least until @@ -3877,7 +3916,8 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = if must_be_closed && occur_meta (clenv_value indclause) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) - pose_all_metas_as_evars env indclause.evd (clenv_value indclause) + let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in + Sigma.Unsafe.of_pair (c, sigma) with e when catchable_exception e -> try find_clause (try_red_product env sigma typ) with Redelimination -> raise e in @@ -3895,6 +3935,7 @@ let check_expected_type env sigma (elimc,bl) elimt = fun t -> Evarconv.e_cumul env (ref sigma) t u let check_enough_applied env sigma elim = + let sigma = Sigma.to_evar_map sigma in (* A heuristic to decide whether the induction arg is enough applied *) match elim with | None -> @@ -3902,7 +3943,7 @@ let check_enough_applied env sigma elim = fun u -> let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t | Some elimc -> - let elimt = typ_of env sigma (fst elimc) in + let elimt = Retyping.get_type_of env sigma (fst elimc) in let scheme = compute_elim_sig ~elimc elimt in match scheme.indref with | None -> @@ -3915,13 +3956,12 @@ let check_enough_applied env sigma elim = let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.raw_concl gl in let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in - let (sigma',c) = use_bindings env sigma elim false (c0,lbind) t0 in + let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with @@ -3931,7 +3971,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in - let (sigma,c0) = finish_evar_resolution ~flags env sigma (pending,c0) in + let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in + let tac = (if isrec then (* Historically, induction has side conditions last *) Tacticals.New.tclTHENFIRST @@ -3939,12 +3980,13 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* and destruct has side conditions first *) Tacticals.New.tclTHENLAST) (Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; - Proofview.Refine.refine ~unsafe:true (fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> let b = not with_evars && with_eq != None in - let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in - let t = Retyping.get_type_of env sigma c in - mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)); + let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in + let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in + let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in + Sigma (ans, sigma, p +> q) + end }; Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable); if is_arg_pure_hyp then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0])) @@ -3952,19 +3994,24 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) tac + in + Sigma (tac, sigma, q) - | Some (sigma',c) -> + | Some (Sigma (c, sigma', q)) -> (* pattern found *) let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) let env = reset_with_named_context sign env in + let tac = Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma'; - Proofview.Refine.refine ~unsafe:true (fun sigma -> - mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None); + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None + end }; tac ] - end + in + Sigma (tac, sigma', p +> q) + end } let has_generic_occurrences_but_goal cls id env ccl = clause_with_generic_context_selection cls && @@ -3976,11 +4023,12 @@ let induction_gen clear_flag isrec with_evars elim let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ccl = Proofview.Goal.raw_concl gl in let cls = Option.default allHypsAndConcl cls in + let sigma = Sigma.Unsafe.of_evar_map sigma in let t = typ_of env sigma c in let is_arg_pure_hyp = isVar c && not (mem_named_context (destVar c) (Global.named_context())) @@ -4011,7 +4059,7 @@ let induction_gen clear_flag isrec with_evars elim isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) - end + end } (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4036,7 +4084,7 @@ let induction_gen_l isrec with_evars elim names lc = atomize_list l' | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4047,7 +4095,7 @@ let induction_gen_l isrec with_evars elim names lc = Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') - end in + end } in Tacticals.New.tclTHENLIST [ (atomize_list lc); @@ -4064,18 +4112,21 @@ let induction_destruct isrec with_evars (lc,elim) = match lc with | [] -> assert false (* ensured by syntax, but if called inside caml? *) | [c,(eqname,names as allnames),cls] -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match elim with | Some elim when is_functional_induction elim gl -> (* Standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) if not (Option.is_empty cls) then error "'in' clause not supported here."; let finish_evar_resolution f = - let (sigma',(c,lbind)) = f env sigma in + let ((c, lbind), sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in - snd (finish_evar_resolution env sigma' (pending,c)),lbind in + let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in + (c, lbind) + in let c = map_induction_arg finish_evar_resolution c in onInductionArg (fun _clear_flag (c,lbind) -> @@ -4086,11 +4137,11 @@ let induction_destruct isrec with_evars (lc,elim) = (* standard induction *) onOpenInductionArg env sigma (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c - end + end } | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match elim with | None -> (* Several arguments, without "using" clause *) @@ -4104,20 +4155,23 @@ let induction_destruct isrec with_evars (lc,elim) = (onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag isrec with_evars None (a,b) cl) a) (Tacticals.New.tclMAP (fun (a,b,cl) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a - end) l) + end }) l) | Some elim -> (* Several induction hyps with induction scheme *) let finish_evar_resolution f = - let (sigma',(c,lbind)) = f env sigma in + let ((c, lbind), sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in if lbind != NoBindings then error "'with' clause not supported here."; - snd (finish_evar_resolution env sigma' (pending,c)) in + let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in + c + in let lc = List.map (on_pi1 (map_induction_arg finish_evar_resolution)) lc in let newlc = List.map (fun (x,(eqn,names),cls) -> @@ -4134,7 +4188,7 @@ let induction_destruct isrec with_evars (lc,elim) = error "'as' clause with multiple arguments and 'using' clause can only occur last."; let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc - end + end } let induction ev clr c l e = induction_gen clr true ev e @@ -4176,7 +4230,7 @@ let simple_destruct = function *) let elim_scheme_type elim t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in match kind_of_term (last_arg clause.templval.rebus) with | Meta mv -> @@ -4186,23 +4240,23 @@ let elim_scheme_type elim t = (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type") - end + end } let elim_type t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) - end + Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) + end } let case_type t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl) in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) - end + Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) + end } (************************************************) @@ -4215,14 +4269,14 @@ let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make () let maybe_betadeltaiota_concl allowred gl = let concl = Tacmach.New.pf_nf_concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in if not allowred then concl else let env = Proofview.Goal.env gl in whd_betadeltaiota env sigma concl let reflexivity_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4230,7 +4284,7 @@ let reflexivity_red allowred = match match_with_equality_type concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings - end + end } let reflexivity = Proofview.tclORELSE @@ -4272,7 +4326,7 @@ let match_with_equation c = Proofview.tclZERO NoEquationFound let symmetry_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4284,7 +4338,7 @@ let symmetry_red allowred = (convert_concl_no_check concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind - end + end } let symmetry = Proofview.tclORELSE @@ -4298,7 +4352,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE @@ -4316,7 +4370,7 @@ let symmetry_in id = | NoEquationFound -> Hook.get forward_setoid_symmetry_in id | e -> Proofview.tclZERO ~info e end - end + end } let intros_symmetry = Tacticals.New.onClause @@ -4341,7 +4395,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4349,7 +4403,7 @@ let prove_transitivity hdcncl eq_kind t = mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), @@ -4361,10 +4415,10 @@ let prove_transitivity hdcncl eq_kind t = [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; assumption ])) - end + end } let transitivity_red allowred t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4381,7 +4435,7 @@ let transitivity_red allowred t = match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") | Some t -> prove_transitivity eq eq_kind t - end + end } let transitivity_gen t = Proofview.tclORELSE @@ -4407,14 +4461,58 @@ let interpretable_as_section_decl evd d1 d2 = match d2,d1 with e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 | (_,None,t1), (_,_,t2) -> e_eq_constr_univs evd t1 t2 +let rec decompose len c t accu = + if len = 0 then (c, t, accu) + else match kind_of_term c, kind_of_term t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t ((na, None, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t ((na, Some b, u) :: accu) + | _ -> assert false + +let rec shrink ctx sign c t accu = match ctx, sign with +| [], [] -> (c, t, accu) +| p :: ctx, (id, _, _) :: sign -> + if noccurn 1 c then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = mkLambda_or_LetIn p c in + let t = mkProd_or_LetIn p t in + let accu = match p with + | (_, None, _) -> mkVar id :: accu + | (_, Some _, _) -> accu + in + shrink ctx sign c t accu +| _ -> assert false + +let shrink_entry sign const = + let open Entries in + let typ = match const.const_entry_type with + | None -> assert false + | Some t -> t + in + (** The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.const_entry_body) in + let ((body, uctx), eff) = Future.force const.const_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + let const = { const with + const_entry_body = Future.from_val ((body, uctx), eff); + const_entry_type = Some typ; + } in + (const, args) + let abstract_subproof id gk tac = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let current_sign = Global.named_context() and global_sign = Proofview.Goal.hyps gl in - let evdref = ref (Proofview.Goal.sigma gl) in + let sigma = Sigma.to_evar_map sigma in + let evdref = ref sigma in let sign,secsign = List.fold_right (fun (id,_,_ as d) (s1,s2) -> @@ -4448,6 +4546,10 @@ let abstract_subproof id gk tac = let (_, info) = Errors.push src in iraise (e, info) in + let const, args = + if !shrink_abstract then shrink_entry sign const + else (const, List.rev (instance_from_named_context sign)) + in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in (** ppedrot: seems legit to have abstracted subproofs as local*) @@ -4459,14 +4561,13 @@ let abstract_subproof id gk tac = let eff = private_con_of_con (Global.safe_env ()) cst in let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in - let args = List.rev (instance_from_named_context sign) in let solve = - Proofview.Unsafe.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in - if not safe then Proofview.mark_as_unsafe <*> solve else solve - end + let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in + Sigma.Unsafe.of_pair (tac, evd) + end } let anon_id = Id.of_string "anonymous" @@ -4486,7 +4587,7 @@ let tclABSTRACT name_op tac = abstract_subproof s gk tac let unify ?(state=full_transparent_state) x y = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> try let core_flags = { (default_unify_flags ()).core_unify_flags with @@ -4498,10 +4599,12 @@ let unify ?(state=full_transparent_state) x y = merge_unify_flags = core_flags; subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } in - let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y - in Proofview.Unsafe.tclEVARS evd - with e when Errors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Not unifiable") - end + let sigma = Sigma.to_evar_map sigma in + let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in + Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma) + with e when Errors.noncritical e -> + Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma + end } module Simple = struct (** Simplified version of some of the above tactics *) |