From 886a9c2fb25e32bd87b3fce38023b3e701134d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 27 Dec 2017 20:22:23 +0100 Subject: [econstr] Continue consolidation of EConstr API under `interp`. This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag. --- interp/constrintern.ml | 46 ++++++++--------- interp/constrintern.mli | 39 +++++++-------- interp/declare.ml | 8 +-- interp/impargs.ml | 128 ++++++++++++++++++++++++------------------------ interp/impargs.mli | 6 +-- interp/modintern.ml | 7 ++- interp/notation.ml | 59 ++++++++++++---------- interp/notation.mli | 6 +-- 8 files changed, 152 insertions(+), 147 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d03aa3552..9053cdc24 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -184,14 +184,14 @@ let compute_explicitable_implicit imps = function (* Unable to know in advance what the implicit arguments will be *) [] -let compute_internalization_data env ty typ impl = - let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in +let compute_internalization_data env sigma ty typ impl = + let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in let expls_impl = compute_explicitable_implicit impl ty in - (ty, expls_impl, impl, compute_arguments_scope typ) + (ty, expls_impl, impl, compute_arguments_scope sigma typ) -let compute_internalization_env env ?(impls=empty_internalization_env) ty = +let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 - (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) + (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map) impls (**********************************************************************) @@ -2207,9 +2207,9 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty -let scope_of_type_kind = function +let scope_of_type_kind sigma = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ) + | OfType typ -> compute_type_scope sigma typ | WithoutTypeConstraint -> None let empty_ltac_sign = { @@ -2218,19 +2218,17 @@ let empty_ltac_sign = { ltac_extra = Genintern.Store.empty; } -let intern_gen kind env +let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = - let tmp_scope = scope_of_type_kind kind in + let tmp_scope = scope_of_type_kind sigma kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} pattern_mode (ltacvars, Id.Map.empty) c -let intern_constr env c = intern_gen WithoutTypeConstraint env c - -let intern_type env c = intern_gen IsType env c - +let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c +let intern_type env sigma c = intern_gen IsType env sigma c let intern_pattern globalenv patt = try intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt @@ -2245,7 +2243,7 @@ let intern_pattern globalenv patt = (* All evars resolved *) let interp_gen kind env sigma ?(impls=empty_internalization_env) c = - let c = intern_gen kind ~impls env c in + let c = intern_gen kind ~impls env sigma c in understand ~expected_type:kind env sigma c let interp_constr env sigma ?(impls=empty_internalization_env) c = @@ -2260,13 +2258,13 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) let interp_open_constr env sigma c = - understand_tcc env sigma (intern_constr env c) + understand_tcc env sigma (intern_constr env sigma c) (* Not all evars expected to be resolved and computation of implicit args *) let interp_constr_evars_gen_impls env sigma ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls env c in + let c = intern_gen expected_type ~impls env sigma c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in let sigma, c = understand_tcc env sigma ~expected_type c in sigma, (c, imps) @@ -2283,7 +2281,7 @@ let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c = (* Not all evars expected to be resolved, with side-effect on evars *) let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls env c in + let c = intern_gen expected_type ~impls env sigma c in understand_tcc env sigma ~expected_type c let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = @@ -2297,9 +2295,9 @@ let interp_type_evars env sigma ?(impls=empty_internalization_env) c = (* Miscellaneous *) -let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = +let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~pattern_mode:true ~ltacvars env c in + ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = @@ -2323,16 +2321,14 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* Interpret binders and contexts *) let interp_binder env sigma na t = - let t = intern_gen IsType env t in + let t = intern_gen IsType env sigma t in let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in understand ~expected_type:IsType env sigma t' -let interp_binder_evars env evdref na t = - let t = intern_gen IsType env t in +let interp_binder_evars env sigma na t = + let t = intern_gen IsType env sigma t in let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in - let evd, c = understand_tcc env !evdref ~expected_type:IsType t' in - evdref := evd; - c + understand_tcc env sigma ~expected_type:IsType t' let my_intern_constr env lvar acc c = internalize env acc false lvar c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 7411fb84b..563230b59 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -7,17 +7,17 @@ (************************************************************************) open Names -open Constr open Evd open Environ +open Misctypes open Libnames open Globnames open Glob_term open Pattern +open EConstr open Constrexpr open Notation_term open Pretyping -open Misctypes (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) @@ -58,10 +58,10 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env -val compute_internalization_data : env -> var_internalization_type -> +val compute_internalization_data : env -> evar_map -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> +val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env @@ -78,11 +78,10 @@ val empty_ltac_sign : ltac_sign (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : env -> constr_expr -> glob_constr - -val intern_type : env -> constr_expr -> glob_constr +val intern_constr : env -> evar_map -> constr_expr -> glob_constr +val intern_type : env -> evar_map -> constr_expr -> glob_constr -val intern_gen : typing_constraint -> env -> +val intern_gen : typing_constraint -> env -> evar_map -> ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr @@ -100,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context + constr_expr -> types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -108,37 +107,37 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr + ?impls:internalization_env -> constr_expr -> evar_map * constr val interp_casted_constr_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr + ?impls:internalization_env -> constr_expr -> types -> evar_map * constr val interp_type_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types + ?impls:internalization_env -> constr_expr -> evar_map * types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - evar_map * (EConstr.constr * Impargs.manual_implicits) + evar_map * (constr * Impargs.manual_implicits) val interp_casted_constr_evars_impls : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> EConstr.types -> - evar_map * (EConstr.constr * Impargs.manual_implicits) + ?impls:internalization_env -> constr_expr -> types -> + evar_map * (constr * Impargs.manual_implicits) val interp_type_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - evar_map * (EConstr.types * Impargs.manual_implicits) + evar_map * (types * Impargs.manual_implicits) (** Interprets constr patterns *) val intern_constr_pattern : - env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) @@ -152,14 +151,14 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types +val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * types (** Interpret contexts: returns extended env and context *) val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map -> local_binder_expr list -> - evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)) + evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) diff --git a/interp/declare.ml b/interp/declare.ml index dfa84f278..f6d7b45c3 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -135,7 +135,7 @@ let set_declare_scheme f = declare_scheme := f let update_tables c = declare_constant_implicits c; Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c) + Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) let register_side_effect (c, role) = let o = inConstant { @@ -275,7 +275,7 @@ let inVariable : variable_obj -> obj = let declare_variable id obj = let oname = add_leaf id (inVariable (Inr (id,obj))) in declare_var_implicits id; - Notation.declare_ref_arguments_scope (VarRef id); + Notation.declare_ref_arguments_scope Evd.empty (VarRef id); Heads.declare_head (EvalVarRef id); oname @@ -283,9 +283,9 @@ let declare_variable id obj = let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope (IndRef (kn,i)); + Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); for j=1 to List.length lc do - Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); done) mie.mind_entry_inds let inductive_names sp kn mie = diff --git a/interp/impargs.ml b/interp/impargs.ml index ed1cd5276..6767af6d8 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -7,21 +7,20 @@ (************************************************************************) open CErrors +open Pp open Util open Names -open Globnames open Constr -open Reduction +open Globnames open Declarations -open Environ -open Libobject +open Decl_kinds open Lib -open Pp -open Constrexpr +open Libobject +open EConstr open Termops +open Reductionops +open Constrexpr open Namegen -open Decl_kinds -open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -165,8 +164,8 @@ let update pos rig (na,st) = in na, Some e (* modified is_rigid_reference with a truncated env *) -let is_flexible_reference env bound depth f = - match kind f with +let is_flexible_reference env sigma bound depth f = + match kind sigma f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true | Rel n -> (* since local definitions have been expanded *) false @@ -174,102 +173,101 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - env |> Environ.lookup_named id |> is_local_def + env |> Environ.lookup_named id |> NamedDecl.is_local_def | Ind _ | Construct _ -> false | _ -> true let push_lift d (e,n) = (push_rel d e,n+1) -let is_reversible_pattern bound depth f l = - isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) && - Array.for_all (fun c -> isRel c && destRel c < depth) l && +let is_reversible_pattern sigma bound depth f l = + isRel sigma f && let n = destRel sigma f in (n < bound+depth) && (n >= depth) && + Array.for_all (fun c -> isRel sigma c && destRel sigma c < depth) l && Array.distinct l (* Precondition: rels in env are for inductive types only *) -let add_free_rels_until strict strongly_strict revpat bound env m pos acc = +let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc = let rec frec rig (env,depth as ed) c = - let hd = if strict then whd_all env c else c in + let hd = if strict then whd_all env sigma c else c in let c = if strongly_strict then hd else c in - match kind hd with + match kind sigma hd with | Rel n when (n < bound+depth) && (n >= depth) -> let i = bound + depth - n - 1 in acc.(i) <- update pos rig acc.(i) - | App (f,l) when revpat && is_reversible_pattern bound depth f l -> - let i = bound + depth - destRel f - 1 in + | App (f,l) when revpat && is_reversible_pattern sigma bound depth f l -> + let i = bound + depth - EConstr.destRel sigma f - 1 in acc.(i) <- update pos rig acc.(i) - | App (f,_) when rig && is_flexible_reference env bound depth f -> + | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c + iter_constr_with_full_binders sigma push_lift (frec false) ed c | Proj (p,c) when rig -> if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c + iter_constr_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c + iter_constr_with_full_binders sigma push_lift (frec false) ed c | Evar _ -> () | _ -> - iter_constr_with_full_binders push_lift (frec rig) ed c + iter_constr_with_full_binders sigma push_lift (frec rig) ed c in - let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in + let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc -let rec is_rigid_head t = match kind t with +let rec is_rigid_head sigma t = match kind sigma t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true - | Case (_,_,f,_) -> is_rigid_head f + | Case (_,_,f,_) -> is_rigid_head sigma f | Proj (p,c) -> true | App (f,args) -> - (match kind f with - | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) - | _ -> is_rigid_head f) + (match kind sigma f with + | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i))) + | _ -> is_rigid_head sigma f) | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ | Prod _ | Meta _ | Cast _ -> assert false (* calcule la liste des arguments implicites *) let find_displayed_name_in all avoid na (env, b) = - let b = EConstr.of_constr b in let envnames_b = (env, b) in let flag = RenamingElsewhereFor envnames_b in if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b else compute_displayed_name_in Evd.empty flag avoid na b -let compute_implicits_gen strict strongly_strict revpat contextual all env t = +let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) = let rigid = ref true in let open Context.Rel.Declaration in - let rec aux env avoid n names t = - let t = whd_all env t in - match kind t with + let rec aux env avoid n names (t : EConstr.t) = + let t = whd_all env sigma t in + match kind sigma t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in - add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) + add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) | _ -> - rigid := is_rigid_head t; + rigid := is_rigid_head sigma t; let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in if contextual then - add_free_rels_until strict strongly_strict revpat n env t Conclusion v + add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v else v in - match kind (whd_all env t) with + match kind sigma (whd_all env sigma t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] -let compute_implicits_flags env f all t = +let compute_implicits_flags env sigma f all t = compute_implicits_gen (f.strict || f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env t + f.reversible_pattern f.contextual all env sigma t -let compute_auto_implicits env flags enriching t = - if enriching then compute_implicits_flags env flags true t - else compute_implicits_gen false false false true true env t +let compute_auto_implicits env sigma flags enriching t = + if enriching then compute_implicits_flags env sigma flags true t + else compute_implicits_gen false false false true true env sigma t -let compute_implicits_names env t = - let _, impls = compute_implicits_gen false false false false true env t in +let compute_implicits_names env sigma t = + let _, impls = compute_implicits_gen false false false false true env sigma t in List.map fst impls (* Extra information about implicit arguments *) @@ -398,24 +396,25 @@ let set_manual_implicits env flags enriching autoimps l = in merge 1 l autoimps -let compute_semi_auto_implicits env f manual t = +let compute_semi_auto_implicits env sigma f manual t = match manual with | [] -> if not f.auto then [DefaultImpArgs, []] - else let _,l = compute_implicits_flags env f false t in + else let _,l = compute_implicits_flags env sigma f false t in [DefaultImpArgs, prepare_implicits f l] | _ -> - let _,autoimpls = compute_auto_implicits env f f.auto t in + let _,autoimpls = compute_auto_implicits env sigma f f.auto t in [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] (*s Constants. *) let compute_constant_implicits flags manual cst = let env = Global.env () in + let sigma = Evd.from_env env in let cb = Environ.lookup_constant cst env in - let ty = cb.const_type in - let impls = compute_semi_auto_implicits env flags manual ty in - impls + let ty = of_constr cb.const_type in + let impls = compute_semi_auto_implicits env sigma flags manual ty in + impls (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -424,7 +423,8 @@ let compute_constant_implicits flags manual cst = let compute_mib_implicits flags manual kn = let env = Global.env () in - let mib = lookup_mind kn env in + let sigma = Evd.from_env env in + let mib = Environ.lookup_mind kn env in let ar = Array.to_list (Array.mapi (* No need to lift, arities contain no de Bruijn *) @@ -433,14 +433,14 @@ let compute_mib_implicits flags manual kn = let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in - let env_ar = push_rel_context ar env in + let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in let ar, _ = Global.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env flags manual ar), + ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) - mip.mind_nf_lc) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c)) + (Array.map of_constr mip.mind_nf_lc)) in Array.mapi imps_one_inductive mib.mind_packets @@ -453,7 +453,8 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env)) + let sigma = Evd.from_env env in + compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) @@ -524,7 +525,7 @@ let impls_of_context ctx = | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) | _ -> None in - List.rev_map map (List.filter (fst %> is_local_assum) ctx) + List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -649,8 +650,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation list -let compute_implicits_with_manual env typ enriching l = - let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in +let compute_implicits_with_manual env sigma typ enriching l = + let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in set_manual_implicits env !implicit_args enriching autoimpls l let check_inclusion l = @@ -674,9 +675,10 @@ let projection_implicits env p impls = let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in - let t, _ = Global.type_of_global_in_context (Global.env ()) ref in + let sigma = Evd.from_env env in + let t, _ = Global.type_of_global_in_context env ref in let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env flags enriching t in + let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in let l' = match l with | [] -> assert false | [l] -> diff --git a/interp/impargs.mli b/interp/impargs.mli index 40fa4cb26..dcfe527b0 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Constr +open EConstr open Globnames open Environ @@ -90,10 +90,10 @@ type manual_explicitation = Constrexpr.explicitation * type manual_implicits = manual_explicitation list -val compute_implicits_with_manual : env -> types -> bool -> +val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool -> manual_implicits -> implicit_status list -val compute_implicits_names : env -> types -> Name.t list +val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list (** {6 Computation of implicits (done using the global environment). } *) diff --git a/interp/modintern.ml b/interp/modintern.ml index e631b3ea4..128152cc2 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,13 +61,16 @@ let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ((_,fqid),c) -> - let c, ectx = interp_constr env (Evd.from_env env) c in + let sigma = Evd.from_env env in + let c, ectx = interp_constr env sigma c in if Flags.is_universe_polymorphism () then let ctx = UState.context ectx in let inst, ctx = Univ.abstract_universes ctx in - let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty else + let c = EConstr.to_constr sigma c in WithDef (fqid,(c, None)), UState.context_set ectx let loc_of_module l = l.CAst.loc diff --git a/interp/notation.ml b/interp/notation.ml index ea7ef21b1..bf39c726a 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -668,8 +668,8 @@ type scope_class = cl_typ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord -let compute_scope_class t = - let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in cl module ScopeClassOrd = @@ -698,22 +698,22 @@ let find_scope_class_opt = function (**********************************************************************) (* Special scopes associated to arguments of a global reference *) -let rec compute_arguments_classes t = - match Constr.kind (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with +let rec compute_arguments_classes sigma t = + match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with | Prod (_,t,u) -> - let cl = try Some (compute_scope_class t) with Not_found -> None in - cl :: compute_arguments_classes u + let cl = try Some (compute_scope_class sigma t) with Not_found -> None in + cl :: compute_arguments_classes sigma u | _ -> [] -let compute_arguments_scope_full t = - let cls = compute_arguments_classes t in +let compute_arguments_scope_full sigma t = + let cls = compute_arguments_classes sigma t in let scs = List.map find_scope_class_opt cls in scs, cls -let compute_arguments_scope t = fst (compute_arguments_scope_full t) +let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) -let compute_type_scope t = - find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) +let compute_type_scope sigma t = + find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) let current_type_scope_name () = find_scope_class_opt (Some CL_SORT) @@ -779,20 +779,24 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let classify_arguments_scope (req,_,_,_,_ as obj) = if req == ArgsScopeNoDischarge then Dispose else Substitute obj -let rebuild_arguments_scope (req,r,n,l,_) = +let rebuild_arguments_scope sigma (req,r,n,l,_) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in - (req,r,List.length scs,scs,cls) + let env = Global.env () in (*FIXME?*) + let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let scs,cls = compute_arguments_scope_full sigma typ in + (req,r,List.length scs,scs,cls) | ArgsScopeManual -> - (* Add to the manually given scopes the one found automatically - for the extra parameters of the section. Discard the classes - of the manually given scopes to avoid further re-computations. *) - let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in - let l1 = List.firstn n l' in - let cls1 = List.firstn n cls in - (req,r,0,l1@l,cls1) + (* Add to the manually given scopes the one found automatically + for the extra parameters of the section. Discard the classes + of the manually given scopes to avoid further re-computations. *) + let env = Global.env () in (*FIXME?*) + let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let l',cls = compute_arguments_scope_full sigma typ in + let l1 = List.firstn n l' in + let cls1 = List.firstn n cls in + (req,r,0,l1@l,cls1) type arguments_scope_obj = arguments_scope_discharge_request * global_reference * @@ -807,7 +811,8 @@ let inArgumentsScope : arguments_scope_obj -> obj = subst_function = subst_arguments_scope; classify_function = classify_arguments_scope; discharge_function = discharge_arguments_scope; - rebuild_function = rebuild_arguments_scope } + (* XXX: Should we pass the sigma here or not, see @herbelin's comment in 6511 *) + rebuild_function = rebuild_arguments_scope Evd.empty } let is_local local ref = local || isVarRef ref && Lib.is_in_section ref @@ -819,7 +824,7 @@ let declare_arguments_scope local r scl = (* We empty the list of argument classes to disable further scope re-computations and keep these manually given scopes. *) declare_arguments_scope_gen req r 0 (scl,[]) - + let find_arguments_scope r = try let (scl,cls,stamp) = Refmap.find r !arguments_scope in @@ -832,12 +837,12 @@ let find_arguments_scope r = scl' with Not_found -> [] -let declare_ref_arguments_scope ref = - let t, _ = Global.type_of_global_in_context (Global.env ()) ref in - let (scs,cls as o) = compute_arguments_scope_full t in +let declare_ref_arguments_scope sigma ref = + let env = Global.env () in (* FIXME? *) + let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in + let (scs,cls as o) = compute_arguments_scope_full sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o - (********************************) (* Encoding notations as string *) diff --git a/interp/notation.mli b/interp/notation.mli index a4c79d6d3..79b56bd41 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -163,10 +163,10 @@ val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit -val declare_ref_arguments_scope : global_reference -> unit +val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit -val compute_arguments_scope : Constr.types -> scope_name option list -val compute_type_scope : Constr.types -> scope_name option +val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list +val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option -- cgit v1.2.3