diff options
65 files changed, 574 insertions, 420 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index f1f65bd8af..f751f4d922 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -209,15 +209,6 @@ let map_evar_info f evi = evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } -let evar_ident_info evi = - match evi.evar_source with - | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id - | _,Evar_kinds.VarInstance id -> id - | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" - | _ -> - let env = reset_with_named_context evi.evar_hyps (Global.env()) in - Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous - (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar @@ -364,11 +355,86 @@ type evar_constraint = conv_pb * Environ.env * constr * constr module EvMap = Evar.Map +module EvNames : +sig + +open Misctypes + +type t + +val empty : t +val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t +val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t +val remove_name_defined : Evar.t -> t -> t +val rename : Evar.t -> Id.t -> t -> t +val reassign_name_defined : Evar.t -> Evar.t -> t -> t +val ident : Evar.t -> t -> Id.t option +val key : Id.t -> t -> Evar.t + +end = +struct + +type t = Id.t EvMap.t * existential_key Idmap.t + +let empty = (EvMap.empty, Idmap.empty) + +let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = + let id = match naming with + | Misctypes.IntroAnonymous -> None + | Misctypes.IntroIdentifier id -> + if Idmap.mem id idtoev then + user_err_loc + (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + Some id + | Misctypes.IntroFresh id -> + let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in + Some id + in + match id with + | None -> names + | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + +let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = + if EvMap.mem evk evtoid then + evar_names + else + add_name_newly_undefined naming evk evi evar_names + +let remove_name_defined evk (evtoid, idtoev as names) = + let id = try Some (EvMap.find evk evtoid) with Not_found -> None in + match id with + | None -> names + | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev) + +let rename evk id (evtoid, idtoev) = + let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in + match id' with + | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + | Some id' -> + if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); + (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) + +let reassign_name_defined evk evk' (evtoid, idtoev as names) = + let id = try Some (EvMap.find evk evtoid) with Not_found -> None in + match id with + | None -> names (** evk' must not be defined *) + | Some id -> + (EvMap.add evk' id (EvMap.remove evk evtoid), + Idmap.add id evk' (Idmap.remove id idtoev)) + +let ident evk (evtoid, _) = + try Some (EvMap.find evk evtoid) with Not_found -> None + +let key id (_, idtoev) = + Idmap.find id idtoev + +end + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; - evar_names : Id.t EvMap.t * existential_key Idmap.t; + evar_names : EvNames.t; (** Universes *) universes : evar_universe_context; (** Conversion problems *) @@ -393,55 +459,15 @@ type evar_map = { (*** Lifting primitive from Evar.Map. ***) -let add_name_newly_undefined naming evk evi (evtoid,idtoev) = - let id = match naming with - | Misctypes.IntroAnonymous -> - let id = evar_ident_info evi in - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) - | Misctypes.IntroIdentifier id -> - let id' = - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - if not (Names.Id.equal id id') then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); - id' - | Misctypes.IntroFresh id -> - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) - -let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = - if EvMap.mem evk evtoid then - evar_names - else - add_name_newly_undefined naming evk evi evar_names - -let remove_name_defined evk (evtoid,idtoev) = - let id = EvMap.find evk evtoid in - (EvMap.remove evk evtoid, Idmap.remove id idtoev) - -let remove_name_possibly_already_defined evk evar_names = - try remove_name_defined evk evar_names - with Not_found -> evar_names - let rename evk id evd = - let (evtoid,idtoev) = evd.evar_names in - let id' = EvMap.find evk evtoid in - if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); - { evd with evar_names = - (EvMap.add evk id evtoid (* overwrite old name *), - Idmap.add id evk (Idmap.remove id' idtoev)) } - -let reassign_name_defined evk evk' (evtoid,idtoev) = - let id = EvMap.find evk evtoid in - (EvMap.add evk' id (EvMap.remove evk evtoid), - Idmap.add id evk' (Idmap.remove id idtoev)) + { evd with evar_names = EvNames.rename evk id evd.evar_names } let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with | Evar_empty -> - let evar_names = add_name_undefined naming e i d.evar_names in + let evar_names = EvNames.add_name_undefined naming e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> - let evar_names = remove_name_possibly_already_defined e d.evar_names in + let evar_names = EvNames.remove_name_defined e d.evar_names in { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } let add d e i = add_with_name d e i @@ -584,7 +610,7 @@ let empty = { last_mods = Evar.Set.empty; metas = Metamap.empty; effects = Safe_typing.empty_private_constants; - evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) + evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; extras = Store.empty; @@ -620,14 +646,8 @@ let add_conv_pb ?(tail=false) pb d = let evar_source evk d = (find d evk).evar_source -let evar_ident evk evd = - try EvMap.find evk (fst evd.evar_names) - with Not_found -> - (* Unnamed (non-dependent) evar *) - add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk)) - -let evar_key id evd = - Idmap.find id (snd evd.evar_names) +let evar_ident evk evd = EvNames.ident evk evd.evar_names +let evar_key id evd = EvNames.key id evd.evar_names let define_aux def undef evk body = let oldinfo = @@ -649,7 +669,7 @@ let define evk body evd = | [] -> evd.last_mods | _ -> Evar.Set.add evk evd.last_mods in - let evar_names = remove_name_defined evk evd.evar_names in + let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } let restrict evk filter ?candidates evd = @@ -659,7 +679,7 @@ let restrict evk filter ?candidates evd = { evar_info with evar_filter = filter; evar_candidates = candidates; evar_extra = Store.empty } in - let evar_names = reassign_name_defined evk evk' evd.evar_names in + let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (mkVar % get_id) ctxt in let body = mkEvar(evk',id_inst) in @@ -1197,7 +1217,34 @@ type unsolvability_explanation = SeveralInstancesFound of int (**********************************************************) (* Pretty-printing *) -let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma) +let pr_evar_suggested_name evk sigma = + let base_id evk' evi = + match evar_ident evk' sigma with + | Some id -> id + | None -> match evi.evar_source with + | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id + | _,Evar_kinds.VarInstance id -> id + | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" + | _ -> + let env = reset_with_named_context evi.evar_hyps (Global.env()) in + Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous + in + let names = EvMap.mapi base_id sigma.undf_evars in + let id = EvMap.find evk names in + let fold evk' id' (seen, n) = + if seen then (seen, n) + else if Evar.equal evk evk' then (true, n) + else if Id.equal id id' then (seen, succ n) + else (seen, n) + in + let (_, n) = EvMap.fold fold names (false, 0) in + if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n)) + +let pr_existential_key sigma evk = match evar_ident evk sigma with +| None -> + str "?" ++ pr_id (pr_evar_suggested_name evk sigma) +| Some id -> + str "?" ++ pr_id id let pr_instance_status (sc,typ) = begin match sc with @@ -1388,7 +1435,7 @@ let pr_evar_list sigma l = h 0 (str (string_of_existential ev) ++ str "==" ++ pr_evar_info evi ++ (if evi.evar_body == Evar_empty - then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}" + then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) in h 0 (prlist_with_sep fnl pr l) diff --git a/engine/evd.mli b/engine/evd.mli index c8753b9c0b..a9ca9a7408 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -246,7 +246,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located (** Convenience function. Wrapper around {!find} to recover the source of an evar in a given evar map. *) -val evar_ident : existential_key -> evar_map -> Id.t +val evar_ident : existential_key -> evar_map -> Id.t option val rename : existential_key -> Id.t -> evar_map -> evar_map @@ -597,6 +597,8 @@ type unsolvability_explanation = SeveralInstancesFound of int val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds +val pr_evar_suggested_name : existential_key -> evar_map -> Id.t + (** {5 Debug pretty-printers} *) val pr_evar_info : evar_info -> Pp.std_ppcmds diff --git a/engine/sigma.ml b/engine/sigma.ml index e886b0d1e7..c25aac0c14 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,6 +36,18 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let new_univ_level_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_univ_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_sort_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + let fresh_sort_in_family ?rigid env sigma s = let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in Sigma (s, sigma, ()) diff --git a/engine/sigma.mli b/engine/sigma.mli index cb948dba59..d7ae2e4ac9 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,6 +66,13 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) +val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Univ.universe_level, 'r) sigma +val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Univ.universe, 'r) sigma +val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Sorts.t, 'r) sigma + val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma val fresh_constant_instance : diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3a8c506cba..3675441353 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -984,7 +984,10 @@ let rec glob_of_pat env sigma = function | PEvar (evk,l) -> let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in let l = Evd.evar_instance_array test (Evd.find sigma evk) l in - let id = Evd.evar_ident evk sigma in + let id = match Evd.evar_ident evk sigma with + | None -> Id.of_string "__" + | Some id -> id + in GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with diff --git a/lib/system.ml b/lib/system.ml index 779e308160..13cfad4aef 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -199,10 +199,12 @@ let is_in_path lpath filename = with Not_found -> false let is_in_system_path filename = - let path = try Sys.getenv "PATH" - with Not_found -> error "system variable PATH not found" in - let lpath = CUnix.path_to_list path in - is_in_path lpath filename + try + let lpath = CUnix.path_to_list (Sys.getenv "PATH") in + is_in_path lpath filename + with Not_found -> + msg_warning (str "system variable PATH not found"); + false let open_trapping_failure name = try open_out_bin name diff --git a/library/universes.ml b/library/universes.ml index 68e422e000..c4eb2afcbb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -954,10 +954,10 @@ let universes_of_constr c = let rec aux s c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.union (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in - LSet.union (Universe.levels u) s + LSet.fold LSet.add (Universe.levels u) s | _ -> fold_constr aux s c in aux LSet.empty c diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 5a49fc8f45..57eb80f5fb 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -250,7 +250,7 @@ module Btauto = struct Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; Tactics.apply (Lazy.force soundness); - Proofview.V82.tactic (Tactics.normalise_vm_in_concl); + Tactics.normalise_vm_in_concl; try_unification env ] | _ -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index e5b68af8e8..b52f156a1b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -48,7 +48,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = sort_of env (ref sigma) c +let sf_of env sigma c = e_sort_of env (ref sigma) c let rec decompose_term env sigma t= match kind_of_term (whd env t) with diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 22a646b3f8..adfcb3e60d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -407,7 +407,7 @@ let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in + let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in let rec aux env avoid subst = function [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> @@ -415,7 +415,7 @@ let concl_refiner metas body gls = let x = id_of_name_using_hdchar env _A Anonymous in let _x = fresh_id avoid x gls in let nenv = Environ.push_named (LocalAssum (_x,_A)) env in - let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in + let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in let nsubst = (n,mkVar _x)::subst in if List.is_empty rest then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 797f43f2a0..0bc40136c5 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Sigma.Notations open Context.Rel.Declaration let compare_instance inst1 inst2= @@ -117,8 +118,10 @@ let mk_open_instance id idc gl m t= let rec aux n avoid env evmap decls = if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in - let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = LocalAssum (Name nid,c) in + let evmap = Sigma.Unsafe.of_evar_map evmap in + let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let evmap = Sigma.to_evar_map evmap in + let decl = LocalAssum (Name nid, c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0e8f7d25c..c05015c538 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -212,6 +212,6 @@ let defined_connectives=lazy let normalize_evaluables= onAllHypsAndConcl (function - None->unfold_in_concl (Lazy.force defined_connectives) + None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) | Some id -> - unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 28982c37fe..c8f8a19e5b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -372,12 +372,12 @@ let isLetIn t = | _ -> false -let h_reduce_with_zeta = - reduce +let h_reduce_with_zeta cl = + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; - }) + }) cl) @@ -708,7 +708,7 @@ let build_proof [ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [Locus.AllOccurrencesBut [1],t] None; + Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); (fun g' -> @@ -1338,7 +1338,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]; + [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); let do_prove = build_proof interactive_proof @@ -1464,7 +1464,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 86abf9e2ef..84a4d910ef 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -114,7 +114,7 @@ let functional_induction with_clean c princl pat = in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) - (Tactics.reduce flag Locusops.allHypsAndConcl) + (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) g else Tacticals.tclIDTAC g in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 56bc4328d1..cdb9c5067f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -368,14 +368,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false ; Genredexpr.rConst = [] } ) - Locusops.onConcl; + Locusops.onConcl); observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -490,15 +490,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -538,12 +538,12 @@ and intros_with_rewrite_aux : tactic = ] g | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -553,12 +553,12 @@ and intros_with_rewrite_aux : tactic = end | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -698,18 +698,18 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; generalize (List.map mkVar ids); thin ids ] else - unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))] + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]) in (* The proof of each branche itself *) let ind_number = ref 0 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 09c5aa5673..046c7aa437 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -276,8 +276,8 @@ let tclUSER tac is_mes l g = if is_mes then observe_tclTHENLIST (str "tclUSER2") [ - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference - (delayed_force Indfun_common.ltof_ref))]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference + (delayed_force Indfun_common.ltof_ref))]); tac ] else tac @@ -562,10 +562,10 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = observe_tclTHENLIST (str "destruct_bounds_aux2")[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; - observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); + observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference infos.func)]); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference infos.func)])); ( observe_tclTHENLIST (str "test")[ list_rewrite true @@ -692,9 +692,8 @@ let mkDestructEq : [generalize new_hyps; (fun g2 -> let changefun patvars = { run = fun sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in - Sigma.Unsafe.of_pair (c, sigma) + let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in + redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) } in Proofview.V82.of_tactic (change_in_concl None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert @@ -904,10 +903,10 @@ let make_rewrite expr_info l hp max = [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ - simpl_iter Locusops.onConcl; + Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference expr_info.func)]); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference expr_info.func)])); (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); @@ -1427,7 +1426,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]); observe_tac (str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 1dd53a3fd8..27daa7e3c6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1170,7 +1170,7 @@ struct let is_prop term = let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in - let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in + let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in Term.is_prop_sort sort in let rec xparse_formula env tg term = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index b740649e98..1f420cf6ae 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -928,15 +928,15 @@ let rec transform p t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - unfold sp_Zminus :: tac,t + Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t | Kapp(Zsucc,[t1]) -> let tac,t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in - unfold sp_Zsucc :: tac,t + Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t | Kapp(Zpred,[t1]) -> let tac,t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in - unfold sp_Zpred :: tac,t + Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t | Kapp(Zmult,[t1;t2]) -> let tac1,t1' = transform (P_APP 1 :: p) t1 and tac2,t2' = transform (P_APP 2 :: p) t2 in @@ -1092,8 +1092,8 @@ let replay_history tactic_normalisation = in Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zle); - Proofview.V82.tactic (simpl_in_concl); + unfold sp_Zle; + simpl_in_concl; intro; (absurd not_sup_sup) ]) [ assumption ; reflexivity ] @@ -1136,10 +1136,10 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - (Proofview.V82.tactic (unfold sp_Zgt)); - (Proofview.V82.tactic simpl_in_concl); + (unfold sp_Zgt); + simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ] + Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] @@ -1161,18 +1161,18 @@ let replay_history tactic_normalisation = [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); Proofview.V82.tactic (clear [aux1;aux2]); - Proofview.V82.tactic (unfold sp_not); + unfold sp_not; (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); Proofview.V82.tactic (mk_then tac); assumption ] ; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ] | EXACT_DIVIDE (e1,k) :: l -> let id = hyp_of_tag e1.id in @@ -1209,8 +1209,8 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> @@ -1330,12 +1330,12 @@ let replay_history tactic_normalisation = (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ]; Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (unfold sp_Zgt); - Proofview.V82.tactic simpl_in_concl; + unfold sp_Zgt; + simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl @@ -1344,9 +1344,9 @@ let replay_history tactic_normalisation = | CONSTANT_NEG(e,k) :: l -> Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]); - Proofview.V82.tactic (unfold sp_Zle); - Proofview.V82.tactic simpl_in_concl; - Proofview.V82.tactic (unfold sp_not); + unfold sp_Zle; + simpl_in_concl; + unfold sp_not; (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); reflexivity @@ -1838,7 +1838,7 @@ let destructure_goal = match destructurate_prop t with | Kapp(Not,[t]) -> (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro) + (Tacticals.New.tclTHEN (unfold sp_not) intro) destructure_hyps) | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 560e6a899e..177c870b3c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list = Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Tactics.normalise_vm_in_concl >> + Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e203b9f651..a67cc7cb87 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -99,10 +99,10 @@ let protect_red map env sigma c = (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; + Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));; (****************************************************************************) @@ -527,8 +527,8 @@ let ring_equality env evd (r,add,mul,opp,req) = match opp with Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.solve_evars env evd setoid in - let op_morph = Typing.solve_evars env evd op_morph in + let setoid = Typing.e_solve_evars env evd setoid in + let op_morph = Typing.e_solve_evars env evd op_morph in (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in @@ -627,7 +627,7 @@ let make_hyp_list env evd lH = (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH (plapp evd coq_nil [|carrier|]) in - let l' = Typing.solve_evars env evd l in + let l' = Typing.e_solve_evars env evd l in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = @@ -753,7 +753,7 @@ let make_term_list env evd carrier rl = let l = List.fold_right (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl (plapp evd coq_nil [|carrier|]) - in Typing.solve_evars env evd l + in Typing.e_solve_evars env evd l let carg = Tacinterp.Value.of_constr let tacarg expr = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index dd58590923..8a55a7aaa5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -28,6 +28,7 @@ open Evarutil open Evarsolve open Evarconv open Evd +open Sigma.Notations open Context.Rel.Declaration (* Pattern-matching errors *) @@ -1955,8 +1956,10 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let sigma,t = match tycon with | Some t -> sigma,t | None -> - let sigma, (t, _) = + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in + let sigma = Sigma.to_evar_map sigma in sigma, t in (* First strategy: we build an "inversion" predicate *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 9d5a6006de..57b273d0d5 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -189,7 +189,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.solve_evars env evdref term) + Typing.e_solve_evars env evdref term) in if isEvar c || isEvar c' then (* Second-order unification needed. *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 67a8f01aa4..c973e1cef3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -528,7 +528,10 @@ let rec detype flags avoid env sigma t = in let id,l = try - let id = Evd.evar_ident evk sigma in + let id = match Evd.evar_ident evk sigma with + | None -> Evd.pr_evar_suggested_name evk sigma + | Some id -> id + in let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 020f998aa7..0a45ae9fd8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1013,7 +1013,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd,ev = new_evar_instance sign !evdref evty ~filter instance in + let evd = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in + let evd = Sigma.to_evar_map evd in evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a65394e17b..3d1822102a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -19,6 +19,7 @@ open Retyping open Reductionops open Evarutil open Pretype_errors +open Sigma.Notations open Context.Rel.Declaration let normalize_evar evd ev = @@ -182,7 +183,9 @@ let restrict_evar_key evd evk filter candidates = let candidates = match candidates with | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in - restrict_evar evd evk filter candidates + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in + (Sigma.to_evar_map sigma, evk) end (* Restrict an applied evar and returns its restriction in the same context *) @@ -580,7 +583,9 @@ let make_projectable_subst aliases sigma evi args = *) let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = - let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let evd = Sigma.to_evar_map evd in let t_in_env = whd_evar evd t_in_env in let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in let ctxt = named_context_of_val sign in @@ -643,8 +648,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in - let evd,ev2_in_sign = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (ev2_in_sign, evd, _) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in + let evd = Sigma.to_evar_map evd in let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 343d3ef903..ab70de0578 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -19,6 +19,7 @@ open Environ open Evd open Reductionops open Pretype_errors +open Sigma.Notations (** Combinators *) @@ -41,7 +42,7 @@ let e_new_global evdref x = evd_comb1 (Evd.fresh_global (Global.env())) evdref x let new_global evd x = - Evd.fresh_global (Global.env()) evd x + Sigma.fresh_global (Global.env()) evd x (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -359,23 +360,19 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) let restrict_evar evd evk filter candidates = + let evd = Sigma.to_evar_map evd in let evd, evk' = Evd.restrict evk filter ?candidates evd in - Evd.declare_future_goal evk' evd, evk' + Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) let new_pure_evar_full evd evi = + let evd = Sigma.to_evar_map evd in let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in - (evd, evk) + Sigma.Unsafe.of_pair (evk, evd) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let default_naming = - if principal then - (* waiting for a more principled approach - (unnamed evars, private names?) *) - Misctypes.IntroFresh (Names.Id.of_string "tmp_goal") - else - Misctypes.IntroAnonymous - in + let evd = Sigma.to_evar_map evd in + let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let evi = { evar_hyps = sign; @@ -391,17 +388,17 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in - (evd,newevk) + Sigma.Unsafe.of_pair (newevk, evd) let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in - (evd,mkEvar (newevk,Array.of_list instance)) + let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + Sigma (mkEvar (newevk,Array.of_list instance), evd, p) (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in let instance = @@ -410,24 +407,26 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let evd = Sigma.to_evar_map evd in - let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in - Sigma.Unsafe.of_pair (c, sigma) +let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in + (Sigma.to_evar_map evd, evk) let new_type_evar env evd ?src ?filter ?naming ?principal rigid = - let evd', s = new_sort_variable rigid evd in - let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in - evd', (e, s) + let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in + let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in + Sigma ((e, s), evd', p +> q) let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in - evdref := evd'; + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in + let sigma = Sigma.to_evar_map sigma in + evdref := sigma; c let new_Type ?(rigid=Evd.univ_flexible) env evd = - let evd', s = new_sort_variable rigid evd in - evd', mkSort s + let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in + Sigma (mkSort s, sigma, p) let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = let evd', s = new_sort_variable rigid !evdref in @@ -526,7 +525,9 @@ let rec check_and_clear_in_constr env evdref err ids c = else let origfilter = Evd.evar_filter evi in let filter = Evd.Filter.apply_subfilter origfilter filter in - let evd,_ = restrict_evar !evdref evk filter None in + let evd = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (_, evd, _) = restrict_evar evd evk filter None in + let evd = Sigma.to_evar_map evd in evdref := evd; (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) let evi = Evd.find !evdref evk in @@ -734,7 +735,10 @@ let define_pure_evar_as_product evd evk = let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in let evd1,(dom,u1) = - new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + (Sigma.to_evar_map evd1, e) + in let evd2,rng = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in @@ -745,7 +749,10 @@ let define_pure_evar_as_product evd evk = else let status = univ_flexible_alg in let evd3, (rng, srng) = - new_type_evar newenv evd1 status ~src ~filter in + let evd1 = Sigma.Unsafe.of_evar_map evd1 in + let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in + (Sigma.to_evar_map evd3, e) + in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng @@ -825,8 +832,8 @@ let define_evar_as_sort env evd (ev,args) = any type has type Type. May cause some trouble, but not so far... *) let judge_of_new_Type evd = - let evd', s = new_univ_variable univ_rigid evd in - evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } + let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in + Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p) (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d87c7ef8d1..bc4c37a918 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -27,12 +27,12 @@ val new_evar : ?principal:bool -> types -> (constr, 'r) Sigma.sigma val new_pure_evar : - named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * evar + ?principal:bool -> types -> (evar, 'r) Sigma.sigma -val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar +val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma (** the same with side-effects *) val e_new_evar : @@ -44,23 +44,23 @@ val e_new_evar : (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - evar_map * (constr * sorts) + (constr * sorts, 'r) Sigma.sigma val e_new_type_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts -val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr +val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr -val restrict_evar : evar_map -> existential_key -> Filter.t -> - constr list option -> evar_map * existential_key +val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> + constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) -val new_global : evar_map -> Globnames.global_reference -> evar_map * constr +val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma val e_new_global : evar_map ref -> Globnames.global_reference -> constr (** Create a fresh evar in a context different from its definition context: @@ -70,11 +70,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + named_context_val -> 'r Sigma.t -> types -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> - constr list -> evar_map * constr + constr list -> (constr, 'r) Sigma.sigma val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list @@ -138,7 +138,7 @@ val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool (** {6 Value/Type constraints} *) -val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment +val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma type type_constraint = types option type val_constraint = constr option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7c91b1a934..5e8c5beb58 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -42,6 +42,7 @@ open Glob_ops open Evarconv open Pattern open Misctypes +open Sigma.Notations open Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint @@ -443,10 +444,13 @@ let pretype_sort evdref = function | GType s -> evd_comb1 judge_of_Type evdref s let new_type_evar env evdref loc = - let e, s = - evd_comb0 (fun evd -> Evarutil.new_type_evar env evd - univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref - in e + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma ((e, _), sigma, _) = + Evarutil.new_type_evar env sigma + univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) + in + evdref := Sigma.to_evar_map sigma; + e let (f_genarg_interp, genarg_interp_hook) = Hook.make () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d7637d1c27..935e18d8dd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -573,7 +573,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = env -> evar_map -> constr -> evar_map * constr +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e65ab83b29..b38252e971 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -108,7 +108,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = env -> evar_map -> constr -> evar_map * constr +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ae224cf0d4..7d2504004f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,6 +23,7 @@ open Reductionops open Cbv open Patternops open Locus +open Sigma.Notations (* Errors *) @@ -389,7 +390,9 @@ let substl_with_function subst sigma constr = if i <= k + Array.length v then match v.(i-k-1) with | (fx, Some (min, ref)) -> - let (sigma, evk) = Evarutil.new_pure_evar venv !evd dummy in + let sigma = Sigma.Unsafe.of_evar_map !evd in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in + let sigma = Sigma.to_evar_map sigma in evd := sigma; minargs := Evar.Map.add evk min !minargs; lift k (mkEvar (evk, [|fx;ref|])) @@ -970,10 +973,12 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = | _ -> mkApp (app', [| a' |])) | _ -> map_constr_with_binders_left_to_right g f acc c -let e_contextually byhead (occs,c) f env sigma t = +let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref 1 in + let sigma = Sigma.to_evar_map sigma in + (** FIXME: we do suspicious things with this evarmap *) let evd = ref sigma in let rec traverse nested (env,c as envc) t = if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t @@ -992,8 +997,8 @@ let e_contextually byhead (occs,c) f env sigma t = (* Skip inner occurrences for stable counting of occurrences *) if locs != [] then ignore (traverse_below (Some (!pos-1)) envc t); - let evm, t = f subst env !evd t in - (evd := evm; t) + let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in + (evd := Sigma.to_evar_map evm; t) end else traverse_below nested envc t @@ -1012,11 +1017,15 @@ let e_contextually byhead (occs,c) f env sigma t = in let t' = traverse None (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; - !evd, t' + Sigma.Unsafe.of_pair (t', !evd) + end } let contextually byhead occs f env sigma t = - let f' subst env sigma t = sigma, f subst env sigma t in - snd (e_contextually byhead occs f' env sigma t) + let f' subst = { e_redfun = begin fun env sigma t -> + Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma + end } in + let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in + c (* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurrence of name. @@ -1135,13 +1144,15 @@ let abstract_scheme env (locc,a) (c, sigma) = let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in mkLambda (na,ta,c'), sigma' -let pattern_occs loccs_trm env sigma c = +let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> + let sigma = Sigma.to_evar_map sigma in let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in try let _ = Typing.unsafe_type_of env sigma abstr_trm in - sigma, applist(abstr_trm, List.map snd loccs_trm) + Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) + end } (* Used in several tactics. *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 6a7248e197..195b21bbf2 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -61,8 +61,7 @@ val unfoldn : val fold_commands : constr list -> reduction_function (** Pattern *) -val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> - evar_map * constr +val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Rem: Lazy strategies are defined in Reduction *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 6c62bd08fc..0faa35c875 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -493,15 +493,18 @@ let is_instance = function let resolvable = Store.field () let set_resolvable s b = - Store.set s resolvable b + if b then Store.remove s resolvable + else Store.set s resolvable () let is_resolvable evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); - Option.default true (Store.get evi.evar_extra resolvable) + Option.is_empty (Store.get evi.evar_extra resolvable) let mark_resolvability_undef b evi = - let t = Store.set evi.evar_extra resolvable b in - { evi with evar_extra = t } + if is_resolvable evi = b then evi + else + let t = set_resolvable evi.evar_extra b in + { evi with evar_extra = t } let mark_resolvability b evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8be28a6202..5347d965b5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -268,7 +268,7 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) -let check env evdref c t = +let e_check env evdref c t = let env = enrich_env env evdref in let j = execute env evdref c in if not (Evarconv.e_cumul env evdref j.uj_type t) then @@ -284,7 +284,7 @@ let unsafe_type_of env evd c = (* Sort of a type *) -let sort_of env evdref c = +let e_sort_of env evdref c = let env = enrich_env env evdref in let j = execute env evdref c in let a = e_type_judgment env evdref j in @@ -311,10 +311,10 @@ let e_type_of ?(refresh=false) env evdref c = c else j.uj_type -let solve_evars env evdref c = +let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) nf_evar !evdref c -let _ = Evarconv.set_solve_evars solve_evars +let _ = Evarconv.set_solve_evars e_solve_evars diff --git a/pretyping/typing.mli b/pretyping/typing.mli index dafd75231a..e524edcca8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -24,16 +24,16 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val check : env -> evar_map ref -> constr -> types -> unit +val e_check : env -> evar_map ref -> constr -> types -> unit (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) -val solve_evars : env -> evar_map ref -> constr -> constr +val e_solve_evars : env -> evar_map ref -> constr -> constr (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6614749d08..e68961da74 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1473,9 +1473,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; diff --git a/printing/printer.ml b/printing/printer.ml index 5f4371f2d0..b89005887f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -403,7 +403,7 @@ let display_name = false (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma)) + if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () (* display the conclusion of a goal *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 84ffee23c1..111a947a9c 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,6 +9,7 @@ open Util open Pp open Term +open Sigma.Notations open Context.Named.Declaration (* This module implements the abstract interface to goals *) @@ -71,7 +72,9 @@ module V82 = struct Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.Unsafe.of_evar_map evars in + let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in let inst = Array.map_of_list (mkVar % get_id) ctxt in @@ -90,7 +93,10 @@ module V82 = struct (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = let id = Evd.evar_ident evk sigma in - Evd.rename evk' id (partial_solution sigma evk c) + let sigma = partial_solution sigma evk c in + match id with + | None -> sigma + | Some id -> Evd.rename evk' id sigma (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = @@ -124,8 +130,10 @@ module V82 = struct let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in - let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = new_sigma; } + let sigma = Sigma.Unsafe.of_evar_map Evd.empty in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in + let sigma = Sigma.to_evar_map sigma in + { Evd.it = evk ; sigma = sigma; } (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ebce25d293..5f4f414a4b 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1085,10 +1085,10 @@ struct let type_hyp (sigma, env) decl = let t = get_type decl in let evdref = ref sigma in - let _ = Typing.sort_of env evdref t in + let _ = Typing.e_sort_of env evdref t in let () = match decl with | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.check env evdref body t + | LocalDef (_,body,_) -> Typing.e_check env evdref body t in (!evdref, Environ.push_named decl env) in @@ -1097,12 +1097,12 @@ struct let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.sort_of env evdref (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in !evdref let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.check env evdref c concl in + let () = Typing.e_check env evdref c concl in !evdref let (pr_constrv,pr_constr) = @@ -1136,7 +1136,10 @@ struct | None -> Evd.define gl.Goal.self c sigma | Some evk -> let id = Evd.evar_ident gl.Goal.self sigma in - Evd.rename evk id (Evd.define gl.Goal.self c sigma) + let sigma = Evd.define gl.Goal.self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma in (** Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 818805a56c..2d886b8e1f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -194,7 +194,7 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let e_red f env evm c = evm, f env evm c +let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl only reduce at the head when an evaluable reference is given, e.g. diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 429bd27742..4afdbf06db 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -18,6 +18,7 @@ open Tacred open Proof_type open Logic open Refiner +open Sigma.Notations open Context.Named.Declaration let re_sig it gc = { it = it; sigma = gc; } @@ -72,7 +73,10 @@ let pf_get_new_ids ids gls = let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c + let (redfun, _) = reduction_of_red_expr (pf_env gls) re in + let sigma = Sigma.Unsafe.of_evar_map (project gls) in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in + (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = diff --git a/stm/stm.ml b/stm/stm.ml index 1503c0f8ab..c4beb60e8f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -513,7 +513,10 @@ end = struct (* {{{ *) let rec fill id = if (get_info id).state = None then fill (Vcs_aux.visit v id).next else copy_info_w_state v id in - fill stop + let v = fill stop in + (* We put in the new dag the first state (since Qed shall run on it, + * see check_task_aux) *) + copy_info_w_state v start let nodes_in_slice ~start ~stop = List.rev (List.map fst (nodes_in_slice ~start ~stop)) @@ -1683,6 +1686,13 @@ let collect_proof keep cur hd brkind id = | _ -> false in let may_pierce_opaque = function | { expr = VernacPrint (PrintName _) } -> true + (* These do not exactly pierce opaque, but are anyway impossible to properly + * delegate *) + | { expr = (VernacDeclareModule _ + | VernacDefineModule _ + | VernacDeclareModuleType _ + | VernacInclude _) } -> true + | { expr = (VernacRequire _ | VernacImport _) } -> true | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in diff --git a/tactics/auto.ml b/tactics/auto.ml index 86b71999b1..761c41da6f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -390,7 +390,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Unfold_nth c -> Proofview.V82.tactic (fun gl -> if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl + tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl else tclFAIL 0 (str"Unbound reference") gl) | Extern tacast -> conclPattern concl p tacast diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 7c05befddd..4855598989 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -245,7 +245,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) - | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) + | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]))) | Extern tacast -> conclPattern concl p tacast in let tac = Proofview.V82.of_tactic (run_hint t tac) in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 6117c8b432..f2d26ec86b 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -198,7 +198,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) + | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in @@ -503,7 +503,7 @@ let autounfolds db occs cls gl = let ids = Idset.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in unfold_option unfolds cls gl + in Proofview.V82.of_tactic (unfold_option unfolds cls) gl let autounfold db cls gl = let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index be4b135974..7c821ddcb5 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -123,7 +123,7 @@ let diseqCase hyps eqonleft = (tclTHEN (intro_using diseq) (tclTHEN (choose_noteq eqonleft) (tclTHEN (rewrite_and_clear (List.rev hyps)) - (tclTHEN (Proofview.V82.tactic red_in_concl) + (tclTHEN (red_in_concl) (tclTHEN (intro_using absurd) (tclTHEN (Simple.apply (mkVar diseq)) (tclTHEN (Extratactics.injHyp absurd) diff --git a/tactics/equality.ml b/tactics/equality.ml index d27dcd82a1..453f81af57 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1609,26 +1609,6 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) -let unfold_body x = - Proofview.Goal.enter { enter = begin fun gl -> - (** We normalize the given hypothesis immediately. *) - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let xval = Context.Named.lookup x hyps |> get_value in - let xval = match xval with - | None -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") - | Some xval -> pf_nf_evar gl xval - in - afterHyp x begin fun aft -> - let hl = List.fold_right (fun d cl -> (get_id d, InHyp) :: cl) aft [] in - let xvar = mkVar x in - let rfun _ _ c = replace_term xvar xval c in - let reducth h = Proofview.V82.tactic (fun gl -> reduct_in_hyp rfun h gl) in - let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in - tclTHENLIST [tclMAP reducth hl; reductc] - end - end } - let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && not (is_global glob_identity eq) diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index f443837a41..2e0996bf5a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -75,7 +75,7 @@ let let_evar name typ = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in - let _ = Typing.sort_of env sigma typ in + let _ = Typing.e_sort_of env sigma typ in let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 930cfebf4c..cdf29e4c62 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -724,8 +724,9 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - change_concl - (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)) + (** FIXME: this looks really wrong. Does anybody really use this tactic? *) + let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in + change_concl c end }; simplest_case a] end } diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b39e34fc1b..6e8e1a6d7e 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -65,8 +65,10 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = let gr = lazy (try_find_global_reference dir s) in - fun (evd,cstrs) -> - let evd, c = Evarutil.new_global evd (Lazy.force gr) in + fun (evd,cstrs) -> + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in + let evd = Sigma.to_evar_map sigma in (evd, cstrs), c (** Utility for dealing with polymorphic applications *) @@ -106,7 +108,7 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in let evdref = ref evars in - let t = Typing.solve_evars env evdref (mkApp (fc, args)) in + let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in (!evdref, cstrs), t let app_poly_nocheck env evars f args = @@ -174,13 +176,17 @@ end) = struct let proper_type = let l = lazy (Lazy.force proper_class).cl_impl in fun (evd,cstrs) -> - let evd, c = Evarutil.new_global evd (Lazy.force l) in + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in + let evd = Sigma.to_evar_map sigma in (evd, cstrs), c let proper_proxy_type = let l = lazy (Lazy.force proper_proxy_class).cl_impl in fun (evd,cstrs) -> - let evd, c = Evarutil.new_global evd (Lazy.force l) in + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in + let evd = Sigma.to_evar_map sigma in (evd, cstrs), c let proper_proof env evars carrier relation x = @@ -349,7 +355,9 @@ end) = struct (try let params, args = Array.chop (Array.length args - 2) args in let env' = Environ.push_rel_context rels env in - let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in + let evars = Sigma.to_evar_map sigma in let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in @@ -409,7 +417,9 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in + let evd = Sigma.to_evar_map sigma in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end @@ -1364,7 +1374,9 @@ module Strategies = let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy = fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in - let evars', t' = rfn env (goalevars evars) t in + let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in + let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in + let evars' = Sigma.to_evar_map sigma in if eq_constr t' t then state, Identity else @@ -1446,7 +1458,7 @@ type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = let evdref = ref sigma in - let sort = Typing.sort_of env evdref concl in + let sort = Typing.e_sort_of env evdref concl in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = @@ -1566,10 +1578,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = convert_concl_no_check newt DEFAULTcast in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in + let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in let opt_beta = match clause with | None -> Proofview.tclUNIT () - | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) + | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp) in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 30a9071fda..2af21fac6e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -805,14 +805,17 @@ let interp_may_eval f ist env sigma = function | ConstrEval (r,c) -> let (sigma,redexp) = interp_red_expr ist env sigma r in let (sigma,c_interp) = f ist env sigma c in - (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp) + let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in + (Sigma.to_evar_map sigma, c) | ConstrContext ((loc,s),c) -> (try let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let evdref = ref sigma in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.solve_evars env evdref c in + let c = Typing.e_solve_evars env evdref c in !evdref , c with | Not_found -> @@ -1967,7 +1970,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in tclTHEN (tclEVARS sigma) - (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) + (Proofview.V82.of_tactic (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))) gl end end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8f30df5c04..f725a06549 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -164,14 +164,13 @@ let _ = let unsafe_intro env store decl b = let open Context.Named.Declaration in 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 decl ctx in let inst = List.map (mkVar % get_id) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (get_id decl)) b in - let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn decl ev, sigma) + let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in + Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) end } let introduction ?(check=true) id = @@ -347,9 +346,7 @@ let rename_hyp repl = let nctx = Environ.val_of_named_context nhyps in let instance = List.map (mkVar % get_id) hyps in 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) + Evarutil.new_evar_instance nctx sigma nconcl ~store instance end } end } @@ -481,7 +478,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr let pf_reduce_decl redfun where decl gl = let open Context.Named.Declaration in - let redfun' = Tacmach.pf_reduce redfun gl in + let redfun' = Tacmach.New.pf_apply redfun gl in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then @@ -560,12 +557,15 @@ let bind_red_expr_occurrences occs nbcl redexp = reduction function either to the conclusion or to a certain hypothesis *) -let reduct_in_concl (redfun,sty) gl = - Proofview.V82.of_tactic (convert_concl_no_check (Tacmach.pf_reduce redfun gl (Tacmach.pf_concl gl)) sty) gl +let reduct_in_concl (redfun,sty) = + Proofview.Goal.nf_enter { enter = begin fun gl -> + convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty + end } -let reduct_in_hyp ?(check=false) redfun (id,where) gl = - Proofview.V82.of_tactic (convert_hyp ~check - (pf_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl)) gl +let reduct_in_hyp ?(check=false) redfun (id,where) = + Proofview.Goal.nf_enter { enter = begin fun gl -> + convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl) + end } let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -578,30 +578,31 @@ let reduct_option ?(check=false) redfun = function let pf_e_reduce_decl redfun where decl gl = let open Context.Named.Declaration in - let sigma = project gl in - let redfun = redfun (pf_env gl) in + let sigma = Proofview.Goal.sigma gl in + let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then errorlabstrm "" (pr_id id ++ str " has no value."); - let sigma, ty' = redfun sigma ty in - sigma, LocalAssum (id,ty') + let Sigma (ty', sigma, p) = redfun sigma ty in + Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> - let sigma, b' = if where != InHypTypeOnly then redfun sigma b else sigma, b in - let sigma, ty' = if where != InHypValueOnly then redfun sigma ty else sigma, ty in - sigma, LocalDef (id,b',ty') - -let e_reduct_in_concl (redfun,sty) gl = - Proofview.V82.of_tactic - (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 (Tacmach.pf_get_hyp gl id) gl in - Proofview.Unsafe.tclEVARS sigma <*> - convert_hyp ~check decl') gl + let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in + let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in + Sigma (LocalDef (id, b', ty'), sigma, p +> q) + +let e_reduct_in_concl (redfun, sty) = + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in + Sigma (convert_concl_no_check c' sty, sigma, p) + end } + +let e_reduct_in_hyp ?(check=false) redfun (id, where) = + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in + Sigma (convert_hyp ~check decl', sigma, p) + end } let e_reduct_option ?(check=false) redfun = function | Some id -> e_reduct_in_hyp ~check (fst redfun) id @@ -613,9 +614,8 @@ let e_reduct_option ?(check=false) redfun = function let e_change_in_concl (redfun,sty) = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - 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) + let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in + Sigma (convert_concl_no_check c sty, sigma, p) end } let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = @@ -624,24 +624,23 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm | LocalAssum (id,ty) -> if where == InHypValueOnly then errorlabstrm "" (pr_id id ++ str " has no value."); - let sigma',ty' = redfun false env sigma ty in - sigma', LocalAssum (id,ty') + let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in + Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> - let sigma',b' = - if where != InHypTypeOnly then redfun true env sigma b else sigma, b + let Sigma (b', sigma, p) = + if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma in - let sigma',ty' = - if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty + let Sigma (ty', sigma, q) = + if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma in - sigma', LocalDef (id,b',ty') + Sigma (LocalDef (id,b',ty'), sigma, p +> q) let e_change_in_hyp redfun (id,where) = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - 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) + let Sigma (c, sigma, p) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + Sigma (convert_hyp c, sigma, p) end } type change_arg = Pattern.patvar_map -> constr Sigma.run @@ -671,32 +670,33 @@ let check_types env sigma mayneedglobalcheck deep newc origc = else sigma (* Now we introduce different instances of the previous tacticals *) -let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = - let sigma = Sigma.Unsafe.of_evar_map sigma in +let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c -> let Sigma (t', sigma, p) = t.run sigma in let sigma = Sigma.to_evar_map sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); - sigma, t' + Sigma.Unsafe.of_pair (t', sigma) +end } (* Use cumulativity only if changing the conclusion not a subterm *) -let change_on_subterm cv_pb deep t where env sigma c = +let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c -> let mayneedglobalcheck = ref false in - let sigma,c = match where with - | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c + let Sigma (c, sigma, p) = match where with + | None -> (change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty)).e_redfun env sigma c | Some occl -> - e_contextually false occl + (e_contextually false occl (fun subst -> - change_and_check Reduction.CONV mayneedglobalcheck true (t subst)) + change_and_check Reduction.CONV mayneedglobalcheck true (t subst))).e_redfun env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env sigma c) + try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; - sigma,c + Sigma (c, sigma, p) +end } let change_in_concl occl t = e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast) @@ -749,14 +749,16 @@ let reduction_clause redexp cl = | OnConcl occs -> (None, bind_red_expr_occurrences occs nbcl redexp)) cl -let reduce redexp cl goal = - let cl = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps goal) cl in +let reduce redexp cl = + Proofview.Goal.enter { enter = begin fun gl -> + let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) 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) -> + let tac = Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check - (Redexpr.reduction_of_red_expr (Tacmach.pf_env goal) redexp) where) redexps in - if check then with_check tac goal else tac goal + (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps in + if check then Proofview.V82.tactic (fun gl -> with_check (Proofview.V82.of_tactic tac) gl) else tac (** FIXME *) + end } (* Unfolding occurrences of a constant *) @@ -811,7 +813,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = else Proofview.tclUNIT () end <*> Proofview.tclORELSE - (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl) + (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> @@ -935,9 +937,9 @@ let lookup_hypothesis_as_renamed_gen red h gl = let rec aux ccl = match lookup_hypothesis_as_renamed env ccl h with | None when red -> - aux - (snd ((fst (Redexpr.reduction_of_red_expr env (Red true))) - env (Sigma.to_evar_map (Proofview.Goal.sigma gl)) ccl)) + let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in + let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in + aux c | x -> x in try aux (Proofview.Goal.concl gl) @@ -1836,7 +1838,7 @@ let check_is_type env ty msg = Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try - let _ = Typing.sort_of env evdref ty in + let _ = Typing.e_sort_of env evdref ty in Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> msg e @@ -1847,10 +1849,10 @@ let check_decl env decl msg = Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try - let _ = Typing.sort_of env evdref ty in + let _ = Typing.e_sort_of env evdref ty in let _ = match decl with | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.check env evdref c ty + | LocalDef (_,c,_) -> Typing.e_check env evdref c ty in Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> @@ -2753,24 +2755,28 @@ let specialize (c,lbind) = (* The two following functions should already exist, but found nowhere *) (* Unfolds x by its definition everywhere *) -let unfold_body x gl = +let unfold_body x = let open Context.Named.Declaration in - let hyps = pf_hyps gl in - let xval = - match Context.Named.lookup x hyps with - | LocalDef (_,xval,_) -> xval - | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") in - let aft = afterHyp x gl in + Proofview.Goal.enter { enter = begin fun gl -> + (** We normalize the given hypothesis immediately. *) + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let xval = match Context.Named.lookup x hyps with + | LocalAssum _ -> errorlabstrm "unfold_body" + (pr_id x ++ str" is not a defined hypothesis.") + | LocalDef (_,xval,_) -> pf_nf_evar gl xval + in + Tacticals.New.afterHyp x begin fun aft -> let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in - tclTHENLIST - [tclMAP (fun h -> reduct_in_hyp rfun h) hl; - reduct_in_concl (rfun,DEFAULTcast)] gl + let reducth h = reduct_in_hyp rfun h in + let reductc = reduct_in_concl (rfun, DEFAULTcast) in + Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc] + end + end } (* Either unfold and clear if defined or simply clear if not a definition *) -let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id]) +let expand_hyp id = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (unfold_body id)) (Proofview.V82.tactic (clear [id])) (*****************************) (* High-level induction *) @@ -3942,7 +3948,7 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr; (* side-conditions in elim (resp case) schemes come last (resp first) *) induct_tac elim; - Proofview.V82.tactic (tclMAP expand_hyp toclear) + Tacticals.New.tclMAP expand_hyp toclear; ]) (Array.map2 (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists)) @@ -3996,7 +4002,7 @@ let induction_without_atomization isrec with_evars elim names lid = if indvars = [] then [List.hd lid_params] else indvars in let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [ (* pattern to make the predicate appear. *) - reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; + Proofview.V82.of_tactic (reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl); (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all possible holes using arguments given by the user (but the functional one). *) @@ -4780,9 +4786,9 @@ module New = struct open Locus let reduce_after_refine = - Proofview.V82.tactic (reduce + reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences }) + {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = Proofview.Refine.refine ?unsafe c <*> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5564b61c37..26ea017696 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -128,44 +128,44 @@ type tactic_reduction = env -> evar_map -> constr -> constr type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg -val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic -val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic -val reduct_in_concl : tactic_reduction * cast_kind -> tactic +val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic +val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic +val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> hyp_location -> unit Proofview.tactic -val red_in_concl : tactic -val red_in_hyp : hyp_location -> tactic -val red_option : goal_location -> tactic -val hnf_in_concl : tactic -val hnf_in_hyp : hyp_location -> tactic -val hnf_option : goal_location -> tactic -val simpl_in_concl : tactic -val simpl_in_hyp : hyp_location -> tactic -val simpl_option : goal_location -> tactic -val normalise_in_concl : tactic -val normalise_in_hyp : hyp_location -> tactic -val normalise_option : goal_location -> tactic -val normalise_vm_in_concl : tactic +val red_in_concl : unit Proofview.tactic +val red_in_hyp : hyp_location -> unit Proofview.tactic +val red_option : goal_location -> unit Proofview.tactic +val hnf_in_concl : unit Proofview.tactic +val hnf_in_hyp : hyp_location -> unit Proofview.tactic +val hnf_option : goal_location -> unit Proofview.tactic +val simpl_in_concl : unit Proofview.tactic +val simpl_in_hyp : hyp_location -> unit Proofview.tactic +val simpl_option : goal_location -> unit Proofview.tactic +val normalise_in_concl : unit Proofview.tactic +val normalise_in_hyp : hyp_location -> unit Proofview.tactic +val normalise_option : goal_location -> unit Proofview.tactic +val normalise_vm_in_concl : unit Proofview.tactic val unfold_in_concl : - (occurrences * evaluable_global_reference) list -> tactic + (occurrences * evaluable_global_reference) list -> unit Proofview.tactic val unfold_in_hyp : - (occurrences * evaluable_global_reference) list -> hyp_location -> tactic + (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic val unfold_option : - (occurrences * evaluable_global_reference) list -> goal_location -> tactic + (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : constr_pattern option -> change_arg -> clause -> tactic val pattern_option : - (occurrences * constr) list -> goal_location -> tactic -val reduce : red_expr -> clause -> tactic -val unfold_constr : global_reference -> tactic + (occurrences * constr) list -> goal_location -> unit Proofview.tactic +val reduce : red_expr -> clause -> unit Proofview.tactic +val unfold_constr : global_reference -> unit Proofview.tactic (** {6 Modification of the local context. } *) val clear : Id.t list -> tactic val clear_body : Id.t list -> unit Proofview.tactic -val unfold_body : Id.t -> tactic +val unfold_body : Id.t -> unit Proofview.tactic val keep : Id.t list -> unit Proofview.tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index ced6d95949..79671ce930 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -56,7 +56,7 @@ Section Finite_nat_set. subst fs1. apply iff_refl. intros H. - eapply counted_list_equal_nth_char. + eapply (counted_list_equal_nth_char _ _ _ _ ?[def]). intros i. destruct (counted_def_nth fs1 i _ ) eqn:H0. (* This was not part of the initial bug report; this is to check that diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 52e1e0ed01..9680d2bbff 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,5 +1,4 @@ -Existential 1 = -?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = ?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b1558dab1c..26eaca8272 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -111,14 +111,14 @@ fun x : option Z => match x with | NONE2 => 0 end : option Z -> Z -fun x : list ?T1 => match x with - | NIL => NONE2 - | (_ :') t => SOME2 t - end - : list ?T1 -> option (list ?T1) +fun x : list ?T => match x with + | NIL => NONE2 + | (_ :') t => SOME2 t + end + : list ?T -> option (list ?T) where -?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1, - x0 cannot be used) +?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1, + x0 cannot be used) s : s 10 diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index c5a393408e..576fbd7c0b 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H fun n : nat => let x := A n : T n in ?y ?y0 : T n : forall n : nat, T n where -?y : [n : nat x := A n : T n |- ?T0 -> T n] -?y0 : [n : nat x := A n : T n |- ?T0] +?y : [n : nat x := A n : T n |- ?T -> T n] +?y0 : [n : nat x := A n : T n |- ?T] fun n : nat => ?y ?y0 : T n : forall n : nat, T n where -?y : [n : nat |- ?T0 -> T n] -?y0 : [n : nat |- ?T0] +?y : [n : nat |- ?T -> T n] +?y0 : [n : nat |- ?T] diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 8fd0394625..56ed89ed86 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -70,7 +70,7 @@ Abort. Goal (forall x y : nat, x = y -> S x = S y) -> True. intros. -einjection (H O) as H0. +einjection (H O ?[y]) as H0. instantiate (y:=O). Abort. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 55b666b723..02e043bc36 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -543,7 +543,7 @@ Qed. Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a): exists x, exists y, X x y. Proof. -intros; eexists; eexists; case H. +intros; eexists; eexists ?[y]; case H. apply (foo ?y). Grab Existential Variables. exact 0. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 9f091e3996..90a60daa66 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -96,21 +96,21 @@ Abort. (* Check that subterm selection does not solve existing evars *) Goal exists x, S x = S 0. -eexists. +eexists ?[x]. Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. Goal exists x, S 0 = S x. -eexists. +eexists ?[x]. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. -do 2 eexists. +eexists ?[n]; eexists ?[p]. destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n). Abort. @@ -426,7 +426,7 @@ destruct b eqn:H. (* Check natural instantiation behavior when the goal has already an evar *) Goal exists x, S x = x. -eexists. +eexists ?[x]. destruct (S _). change (0 = ?x). Abort. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 0755f8bcfd..3d053c2e1b 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -581,7 +581,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTRY ( Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); - Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp)); + simpl_in_hyp (freshz,Locus.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) @@ -725,7 +725,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj None false None (mkVar freshz,NoBindings); - intros; (Proofview.V82.tactic simpl_in_concl); + intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [apply (andb_true_intro()); @@ -902,7 +902,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; - Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref)); + unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all (); assert_by (Name freshH3) diff --git a/toplevel/command.ml b/toplevel/command.ml index 02f29b155f..166fe94ead 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -36,13 +36,14 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr +open Sigma.Notations open Context.Rel.Declaration let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l let rec under_binders env sigma f n c = - if Int.equal n 0 then snd (f env sigma c) else + if Int.equal n 0 then f env sigma c else match kind_of_term c with | Lambda (x,t,c) -> mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) @@ -72,10 +73,14 @@ let red_constant_entry n ce sigma = function | Some red -> let proof_out = ce.const_entry_body in let env = Global.env () in + let (redfun, _) = reduction_of_red_expr env red in + let redfun env sigma c = + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (c, _, _) = redfun.e_redfun env sigma c in + c + in { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out - (fun ((body,ctx),eff) -> - (under_binders env sigma - (fst (reduction_of_red_expr env red)) n body,ctx),eff) } + (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in @@ -1007,7 +1012,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop |]) in - let def = Typing.solve_evars env evdref def in + let def = Typing.e_solve_evars env evdref def in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in @@ -1082,7 +1087,7 @@ let interp_recursive isfix fixl notations = let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in - Typing.solve_evars env evdref app + Typing.e_solve_evars env evdref app with e when Errors.noncritical e -> t in LocalAssum (id,fixprot) :: env' diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4a145481f7..de7ec61c81 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1211,7 +1211,7 @@ let explain_unused_clause env pats = let explain_non_exhaustive env pats = str "Non exhaustive pattern-matching: no clause found for " ++ str (String.plural (List.length pats) "pattern") ++ - spc () ++ hov 0 (pr_sequence pr_cases_pattern pats) + spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) let explain_cannot_infer_predicate env sigma typs = let env = make_all_name_different env in diff --git a/toplevel/record.ml b/toplevel/record.ml index facc8b75d5..4cf81a250c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -24,6 +24,7 @@ open Type_errors open Constrexpr open Constrexpr_ops open Goptions +open Sigma.Notations open Context.Rel.Declaration (********** definition d'un record (structure) **************) @@ -342,11 +343,15 @@ let structure_signature ctx = match l with [] -> Evd.empty | [decl] -> let env = Environ.empty_named_context_val in - let (evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.Unsafe.of_evar_map evm in + let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.to_evar_map evm in evm | decl::tl -> let env = Environ.empty_named_context_val in - let (evm, ev) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.Unsafe.of_evar_map evm in + let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.to_evar_map evm in let new_tl = Util.List.map_i (fun pos decl -> map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8b3e118485..a6a1546ae3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -32,6 +32,7 @@ open Redexpr open Lemmas open Misctypes open Locality +open Sigma.Notations let debug = false let prerr_endline = @@ -1538,7 +1539,12 @@ let vernac_check_may_eval redexp glopt rc = | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in - let redfun env evm c = snd (fst (reduction_of_red_expr env r_interp) env evm c) in + let redfun env evm c = + let (redfun, _) = reduction_of_red_expr env r_interp in + let evm = Sigma.Unsafe.of_evar_map evm in + let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in + c + in msg_notice (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = |