diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 10 | ||||
| -rw-r--r-- | interp/notation.ml | 38 | ||||
| -rw-r--r-- | interp/notation.mli | 6 |
3 files changed, 28 insertions, 26 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f82783f47d..a1aac60b35 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty let compute_internalization_data env sigma id ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - (ty, impl, compute_arguments_scope sigma typ, var_uid id) + (ty, impl, compute_arguments_scope env sigma typ, var_uid id) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 @@ -2358,9 +2358,9 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty -let scope_of_type_kind sigma = function +let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope sigma typ + | OfType typ -> compute_type_scope env sigma typ | WithoutTypeConstraint | UnknownIfTermOrType -> None let allowed_binder_kind_of_type_kind = function @@ -2377,7 +2377,7 @@ let empty_ltac_sign = { 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 sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; @@ -2462,7 +2462,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = - let tmp_scope = scope_of_type_kind sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env diff --git a/interp/notation.ml b/interp/notation.ml index 7761606f11..2703930705 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1448,8 +1448,8 @@ type scope_class = cl_typ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in +let compute_scope_class env sigma t = + let (cl,_,_) = find_class_type env sigma t in cl module ScopeClassOrd = @@ -1478,22 +1478,23 @@ let find_scope_class_opt = function (**********************************************************************) (* Special scopes associated to arguments of a global reference *) -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 sigma t) with Not_found -> None in - cl :: compute_arguments_classes sigma u +let rec compute_arguments_classes env sigma t = + match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with + | Prod (na, t, u) -> + let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in + let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in + cl :: compute_arguments_classes env sigma u | _ -> [] -let compute_arguments_scope_full sigma t = - let cls = compute_arguments_classes sigma t in +let compute_arguments_scope_full env sigma t = + let cls = compute_arguments_classes env sigma t in let scs = List.map find_scope_class_opt cls in scs, cls -let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) +let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t) -let compute_type_scope sigma t = - find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) +let compute_type_scope env sigma t = + find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None) let current_type_scope_name () = find_scope_class_opt (Some CL_SORT) @@ -1531,15 +1532,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_scope_class subst cs = - try Some (subst_cl_typ subst cs) with Not_found -> None +let subst_scope_class env subst cs = + try Some (subst_cl_typ env subst cs) with Not_found -> None let subst_arguments_scope (subst,(req,r,n,scl,cls)) = let r' = fst (subst_global subst r) in let subst_cl ocl = match ocl with | None -> ocl | Some cl -> - match subst_scope_class subst cl with + let env = Global.env () in + match subst_scope_class env subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in let cls' = List.Smart.map subst_cl cls in @@ -1565,7 +1567,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = | ArgsScopeAuto -> let env = Global.env () in (*FIXME?*) let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in - let scs,cls = compute_arguments_scope_full sigma typ in + let scs,cls = compute_arguments_scope_full env sigma typ in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically @@ -1573,7 +1575,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = of the manually given scopes to avoid further re-computations. *) let env = Global.env () in (*FIXME?*) let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in - let l',cls = compute_arguments_scope_full sigma typ in + let l',cls = compute_arguments_scope_full env sigma typ in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in (req,r,0,l1@l,cls1) @@ -1620,7 +1622,7 @@ let find_arguments_scope r = let declare_ref_arguments_scope sigma ref = let env = Global.env () in (* FIXME? *) let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in - let (scs,cls as o) = compute_arguments_scope_full sigma typ in + let (scs,cls as o) = compute_arguments_scope_full env sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o (********************************) diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..b427aa9bb3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -264,13 +264,13 @@ type scope_class val scope_class_compare : scope_class -> scope_class -> int val subst_scope_class : - Mod_subst.substitution -> scope_class -> scope_class option + Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit -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 +val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list +val compute_type_scope : Environ.env -> 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 |