From 9f175bbeb19175a1e422225986f139e8f1a1b56c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 4 May 2018 14:36:18 +0200 Subject: Use evd_combX in Cases. --- engine/evarutil.ml | 10 +++++----- engine/evarutil.mli | 22 +++++++++++++--------- pretyping/cases.ml | 46 +++++++++++++++++++--------------------------- 3 files changed, 37 insertions(+), 41 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 52610f6f3..2b202ef3e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,7 +436,7 @@ let new_pure_evar_full evd evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -463,14 +463,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca in (evd, newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = +let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = let open EConstr in 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 new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -480,7 +480,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [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 env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = +let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -490,7 +490,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = +let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c24660f5b..7dd98bac9 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,10 +25,11 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar_from_context : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * EConstr.t type naming_mode = | KeepUserNameAndRenameExistingButSectionNames @@ -37,25 +38,28 @@ type naming_mode = | FailIfConflict val new_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * Evar.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * Evar.t val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t (** 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:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> rigid -> evar_map * (constr * Sorts.t) val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr @@ -74,10 +78,10 @@ val new_global : evar_map -> GlobRef.t -> evar_map * 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:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> + named_context_val -> evar_map -> types -> constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 84f0aba8c..ee7c39982 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,9 +295,11 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in - evdref := evd; - (e::subst,e::evarl,n+1) + let e = evd_comb1 + (Evarutil.new_evar env ~src:(hole_source n)) + evdref ty' + in + (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) @@ -375,8 +377,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref !lvar tomatch in - let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in - evdref := evd; + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = @@ -399,15 +400,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in - evdref := evd; + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in e -let evd_comb2 f evdref x y = - let (evd',y) = f !evdref x y in - evdref := evd'; - y - let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the term to match and the patterns coerce *) @@ -1019,8 +1014,8 @@ let adjust_impossible_cases pb pred tomatch submat = begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin - let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + let default = evd_comb0 use_unit_judge pb.evdref in + pb.evdref := Evd.define evk default.uj_type !(pb.evdref) end; add_assert_false_case pb tomatch | _ -> @@ -1686,8 +1681,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let evd, ev' = Evarutil.new_evar env !evdref ~src ty in - evdref := evd; + let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1718,8 +1712,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in - evdref := evd; + let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1731,14 +1724,15 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let evd, (impossible_case_type, u) = - new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in - evdref := evd; - (lift (n'-n) impossible_case_type, mkSort u) + let impossible_case_type, u = + evd_comb1 + (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + evdref univ_flexible_alg + in + (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.type_of extenv !evdref t in - evdref := evd; + let tt = evd_comb1 (Typing.type_of extenv) evdref t in (t,tt) in match cumul env !evdref tt (mkSort s) with | None -> anomaly (Pp.str "Build_tycon: should be a type."); @@ -1932,9 +1926,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in - evdref := evd'; - j + evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p | None -> j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) -- cgit v1.2.3