diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 174 |
1 files changed, 138 insertions, 36 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d306599ad8..323d6fcea6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -26,7 +26,6 @@ open Names open Term open Context open Vars -open Univ open Declarations open Pre_env @@ -46,6 +45,12 @@ let empty_named_context_val = empty_named_context_val let empty_env = empty_env let engagement env = env.env_stratification.env_engagement + +let is_impredicative_set env = + match engagement env with + | Some ImpredicativeSet -> true + | _ -> false + let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context let named_context_val env = env.env_named_context,env.env_named_vals @@ -160,6 +165,30 @@ let fold_named_context f env ~init = let fold_named_context_reverse f ~init env = Context.fold_named_context_reverse f ~init:init (named_context env) + +(* Universe constraints *) + +let add_constraints c env = + if Univ.Constraint.is_empty c then + env + else + let s = env.env_stratification in + { env with env_stratification = + { s with env_universes = Univ.merge_constraints c s.env_universes } } + +let check_constraints c env = + Univ.check_constraints c env.env_stratification.env_universes + +let set_engagement c env = (* Unsafe *) + { env with env_stratification = + { env.env_stratification with env_engagement = Some c } } + +let push_constraints_to_env (_,univs) env = + add_constraints univs env + +let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env +let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env + (* Global constants *) let lookup_constant = lookup_constant @@ -177,30 +206,113 @@ let add_constant_key kn cb linkinfo env = let add_constant kn cb env = add_constant_key kn cb (no_link_info ()) env +let universes_of cb = + Future.force cb.const_universes + +let universes_and_subst_of cb u = + let univs = universes_of cb in + let subst = Univ.make_universe_subst u univs in + subst, Univ.instantiate_univ_context subst univs + (* constant_type gives the type of a constant *) -let constant_type env kn = +let constant_type env (kn,u) = let cb = lookup_constant kn env in - cb.const_type + if cb.const_polymorphic then + let subst, csts = universes_and_subst_of cb u in + (subst_univs_constr subst cb.const_type, csts) + else cb.const_type, Univ.Constraint.empty -type const_evaluation_result = NoBody | Opaque +let constant_type_in_ctx env kn = + let cb = lookup_constant kn env in + cb.const_type, Future.force cb.const_universes + +let constant_context env kn = + let cb = lookup_constant kn env in + if cb.const_polymorphic then Future.force cb.const_universes + else Univ.UContext.empty + +type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result -let constant_value env kn = +let constant_value env (kn,u) = + let cb = lookup_constant kn env in + if cb.const_proj = None then + match cb.const_body with + | Def l_body -> + if cb.const_polymorphic then + let subst, csts = universes_and_subst_of cb u in + (subst_univs_constr subst (Mod_subst.force_constr l_body), csts) + else Mod_subst.force_constr l_body, Univ.Constraint.empty + | OpaqueDef _ -> raise (NotEvaluableConst Opaque) + | Undef _ -> raise (NotEvaluableConst NoBody) + else raise (NotEvaluableConst IsProj) + +let constant_opt_value env cst = + try Some (constant_value env cst) + with NotEvaluableConst _ -> None + +let constant_value_and_type env (kn, u) = + let cb = lookup_constant kn env in + if cb.const_polymorphic then + let subst, cst = universes_and_subst_of cb u in + let b' = match cb.const_body with + | Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body)) + | OpaqueDef _ -> None + | Undef _ -> None + in b', subst_univs_constr subst cb.const_type, cst + else + let b' = match cb.const_body with + | Def l_body -> Some (Mod_subst.force_constr l_body) + | OpaqueDef _ -> None + | Undef _ -> None + in b', cb.const_type, Univ.Constraint.empty + +(* These functions should be called under the invariant that [env] + already contains the constraints corresponding to the constant + application. *) + +(* constant_type gives the type of a constant *) +let constant_type_in env (kn,u) = + let cb = lookup_constant kn env in + if cb.const_polymorphic then + let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in + subst_univs_constr subst cb.const_type + else cb.const_type + +let constant_value_in env (kn,u) = let cb = lookup_constant kn env in match cb.const_body with - | Def l_body -> Mod_subst.force_constr l_body + | Def l_body -> + let b = Mod_subst.force_constr l_body in + if cb.const_polymorphic then + let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in + subst_univs_constr subst b + else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) -let constant_opt_value env cst = - try Some (constant_value env cst) +let constant_opt_value_in env cst = + try Some (constant_value_in env cst) with NotEvaluableConst _ -> None (* A global const is evaluable if it is defined and not opaque *) -let evaluable_constant cst env = - try let _ = constant_value env cst in true - with NotEvaluableConst _ -> false +let evaluable_constant kn env = + let cb = lookup_constant kn env in + match cb.const_body with + | Def _ -> true + | OpaqueDef _ -> false + | Undef _ -> false + +let lookup_projection cst env = + match (lookup_constant cst env).const_proj with + | Some pb -> pb + | None -> anomaly (Pp.str "lookup_projection: constant is not a projection") + +let is_projection cst env = + match (lookup_constant cst env).const_proj with + | Some _ -> true + | None -> false (* Mutual Inductives *) let lookup_mind = lookup_mind @@ -215,21 +327,10 @@ let add_mind_key kn mind_key env = let add_mind kn mib env = let li = no_link_info () in add_mind_key kn (mib, li) env -(* Universe constraints *) - -let add_constraints c env = - if is_empty_constraint c then - env - else - let s = env.env_stratification in - { env with env_stratification = - { s with env_universes = merge_constraints c s.env_universes } } +(* Lookup of section variables *) -let set_engagement c env = (* Unsafe *) - { env with env_stratification = - { env.env_stratification with env_engagement = Some c } } +let constant_body_hyps cb = cb.const_hyps -(* Lookup of section variables *) let lookup_constant_variables c env = let cmap = lookup_constant c env in Context.vars_of_named_context cmap.const_hyps @@ -246,9 +347,10 @@ let lookup_constructor_variables (ind,_) env = let vars_of_global env constr = match kind_of_term constr with Var id -> Id.Set.singleton id - | Const kn -> lookup_constant_variables kn env - | Ind ind -> lookup_inductive_variables ind env - | Construct cstr -> lookup_constructor_variables cstr env + | Const (kn, _) -> lookup_constant_variables kn env + | Ind (ind, _) -> lookup_inductive_variables ind env + | Construct (cstr, _) -> lookup_constructor_variables cstr env + (** FIXME: is Proj missing? *) | _ -> raise Not_found let global_vars_set env constr = @@ -423,7 +525,7 @@ let unregister env field = is abstract, and that the only function which add elements to the retroknowledge is Environ.register which enforces this shape *) (match kind_of_term (retroknowledge find env field) with - | Ind i31t -> let i31c = mkConstruct (i31t, 1) in + | Ind i31t -> let i31c = mkConstructUi (i31t, 1) in {env with retroknowledge = remove (retroknowledge clear_info env i31c) field} | _ -> assert false) @@ -487,7 +589,7 @@ let register = let add_int31_before_match rk grp v = let rk = add_vm_before_match_info rk v Cbytegen.int31_escape_before_match in match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with - | Ind i31bit_type -> + | Ind (i31bit_type,_) -> add_native_before_match_info rk v (Nativelambda.before_match_int31 i31bit_type) | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type") @@ -498,13 +600,13 @@ fun env field value -> operators to the reactive retroknowledge. *) let add_int31_binop_from_const op prim = match kind_of_term value with - | Const kn -> retroknowledge add_int31_op env value 2 + | Const (kn,_) -> retroknowledge add_int31_op env value 2 op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in let add_int31_unop_from_const op prim = match kind_of_term value with - | Const kn -> retroknowledge add_int31_op env value 1 + | Const (kn,_) -> retroknowledge add_int31_op env value 1 op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in @@ -516,9 +618,9 @@ fun env field value -> match field with | KInt31 (grp, Int31Type) -> (match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with - | Ind i31bit_type -> + | Ind (i31bit_type,_) -> (match kind_of_term value with - | Ind i31t -> + | Ind (i31t,_) -> Retroknowledge.add_vm_decompile_constant_info rk value (constr_of_int31 i31t i31bit_type) | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")) @@ -530,7 +632,7 @@ fun env field value -> match field with | KInt31 (grp, Int31Type) -> let i31c = match kind_of_term value with - | Ind i31t -> mkConstruct (i31t, 1) + | Ind i31t -> mkConstructUi (i31t, 1) | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") in add_int31_decompilation_from_type @@ -554,7 +656,7 @@ fun env field value -> Primitives.Int31mulc | KInt31 (_, Int31Div21) -> (* this is a ternary operation *) (match kind_of_term value with - | Const kn -> + | Const (kn,u) -> retroknowledge add_int31_op env value 3 Cbytecodes.Kdiv21int31 Primitives.Int31div21 kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) @@ -562,7 +664,7 @@ fun env field value -> Primitives.Int31div | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *) (match kind_of_term value with - | Const kn -> + | Const (kn,u) -> retroknowledge add_int31_op env value 3 Cbytecodes.Kaddmuldivint31 Primitives.Int31addmuldiv kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) |