diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 202 |
1 files changed, 93 insertions, 109 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 16ddfac6..89ba6f65 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Author: Jean-Christophe Filliâtre as part of the rebuilding of Coq @@ -23,7 +25,7 @@ open CErrors open Util open Names -open Term +open Constr open Vars open Declarations open Pre_env @@ -37,8 +39,10 @@ type env = Pre_env.env let pre_env env = env let env_of_pre_env env = env -let oracle env = env.env_conv_oracle -let set_oracle env o = { env with env_conv_oracle = o } +let oracle env = env.env_typing_flags.conv_oracle +let set_oracle env o = + let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in + { env with env_typing_flags } let empty_named_context_val = empty_named_context_val @@ -58,18 +62,17 @@ let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context -let rel_context env = env.env_rel_context +let rel_context env = env.env_rel_context.env_rel_ctx let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context.env_named_ctx with + match env.env_rel_context.env_rel_ctx, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false (* Rel context *) -let lookup_rel n env = - Context.Rel.lookup n env.env_rel_context +let lookup_rel = lookup_rel let evaluable_rel n env = is_local_def (lookup_rel n env) @@ -86,13 +89,12 @@ let push_rec_types (lna,typarray,_) env = let fold_rel_context f env ~init = let rec fold_right env = - match env.env_rel_context with - | [] -> init - | rd::rc -> + match match_rel_context_val env.env_rel_context with + | None -> init + | Some (rd, _, rc) -> let env = { env with env_rel_context = rc; - env_rel_val = List.tl env.env_rel_val; env_nb_rel = env.env_nb_rel - 1 } in f env rd (fold_right env) in fold_right env @@ -101,6 +103,8 @@ let fold_rel_context f env ~init = let named_context_of_val c = c.env_named_ctx +let ids_of_named_context_val c = Id.Map.domain c.env_named_map + (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) @@ -120,7 +124,7 @@ let lookup_named = lookup_named let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = - c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -140,16 +144,21 @@ let evaluable_named id env = let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_rel_context = Context.Rel.empty; - env_rel_val = []; + env_rel_context = empty_rel_context_val; env_nb_rel = 0 } let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = + let rec skip n ctx = + if Int.equal n 0 then ctx + else match match_rel_context_val ctx with + | None -> invalid_arg "List.skipn" + | Some (_, _, ctx) -> skip (pred n) ctx + in let ctxt = env.env_rel_context in { env with - env_rel_context = List.skipn n ctxt; + env_rel_context = skip n ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = @@ -185,8 +194,7 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun g v -> UGraph.add_universe v strict g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g @@ -196,6 +204,7 @@ let push_context ?(strict=false) ctx env = let add_universes_set strict ctx g = let g = Univ.LSet.fold + (* Be lenient, module typing reintroduces universes and constraints due to includes *) (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g @@ -228,59 +237,39 @@ let add_constant kn cb env = add_constant_key kn cb no_link_info env let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) - -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (subst_instance_constr u cb.const_type, csts) let constant_context env kn = let cb = lookup_constant kn env in - if cb.const_polymorphic then cb.const_universes - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx -type const_evaluation_result = NoBody | Opaque | IsProj +type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -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 csts = constraints_of cb u in - (subst_instance_constr u (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 + if Declareops.constant_is_polymorphic cb then let cst = constraints_of cb u in let b' = match cb.const_body with | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_instance_constr u) cb.const_type, cst + b', subst_instance_constr u cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -295,8 +284,8 @@ let constant_value_and_type env (kn, u) = (* 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 - map_regular_arity (subst_instance_constr u) cb.const_type + if Declareops.constant_is_polymorphic cb then + subst_instance_constr u cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -321,7 +310,7 @@ let evaluable_constant kn env = | Undef _ -> false let polymorphic_constant cst env = - (lookup_constant cst env).const_polymorphic + Declareops.constant_is_polymorphic (lookup_constant cst env) let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false @@ -330,19 +319,10 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -let template_polymorphic_constant cst env = - match (lookup_constant cst env).const_type with - | TemplateArity _ -> true - | RegularArity _ -> false - -let template_polymorphic_pconstant (cst,u) env = - if not (Univ.Instance.is_empty u) then false - else template_polymorphic_constant cst env - let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection") + | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") let is_projection cst env = match (lookup_constant cst env).const_proj with @@ -353,7 +333,7 @@ let is_projection cst env = let lookup_mind = lookup_mind let polymorphic_ind (mind,i) env = - (lookup_mind mind env).mind_polymorphic + Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false @@ -397,7 +377,7 @@ let lookup_constructor_variables (ind,_) env = (* Returns the list of global variables in a term *) let vars_of_global env constr = - match kind_of_term constr with + match kind constr with Var id -> Id.Set.singleton id | Const (kn, _) -> lookup_constant_variables kn env | Ind (ind, _) -> lookup_inductive_variables ind env @@ -408,12 +388,12 @@ let vars_of_global env constr = let global_vars_set env constr = let rec filtrec acc c = let acc = - match kind_of_term c with + match kind c with | Var _ | Const _ | Ind _ | Construct _ -> Id.Set.union (vars_of_global env c) acc | _ -> acc in - fold_constr filtrec acc c + Constr.fold filtrec acc c in filtrec Id.Set.empty constr @@ -469,9 +449,11 @@ let lookup_modtype mp env = (*s Judgments. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = { uj_val = v; @@ -480,13 +462,15 @@ let make_judge v tj = let j_val j = j.uj_val let j_type j = j.uj_type -type unsafe_type_judgment = { - utj_val : constr; - utj_type : sorts } +type 'types punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } + +type unsafe_type_judgment = types punsafe_type_judgment (*s Compilation of global declaration *) -let compile_constant_body = Cbytegen.compile_constant_body false +let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false exception Hyp_not_found @@ -540,9 +524,9 @@ let register_one env field entry = let register env field entry = match field with | KInt31 (grp, Int31Type) -> - let i31c = match kind_of_term entry with + let i31c = match kind entry with | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry @@ -578,7 +562,7 @@ let dispatch = it to the name of the coq definition in the reactive retroknowledge) *) let int31_op n op prim kn = { empty_reactive_info with - vm_compiling = Some (Cbytegen.op_compilation n op kn); + vm_compiling = Some (Clambda.compile_prim n op kn); native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); } in @@ -586,9 +570,9 @@ let dispatch = fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = - match kind_of_term value with + match kind value with | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in let int31_unop_from_const op prim = int31_op_from_const 1 op prim in @@ -600,67 +584,67 @@ fun rk value field -> match field with | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field") + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = - match kind_of_term int31bit with + match kind int31bit with | Ind (i31bit_type,_) -> i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type") + (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = - match kind_of_term value with + match kind value with | Ind (i31t,_) -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type") + (Pp.str "should be an inductive type.") in { empty_reactive_info with vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Cbytegen.int31_escape_before_match; + vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } | KInt31 (_, Int31Constructor) -> { empty_reactive_info with - vm_constant_static = Some Cbytegen.compile_structured_int31; - vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation; + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; native_constant_static = Some Nativelambda.compile_static_int31; native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - Primitives.Int31add + CPrimitives.Int31add | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - Primitives.Int31addc + CPrimitives.Int31addc | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - Primitives.Int31addcarryc + CPrimitives.Int31addcarryc | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - Primitives.Int31sub + CPrimitives.Int31sub | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - Primitives.Int31subc + CPrimitives.Int31subc | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - Primitives.Int31mul + CPrimitives.Int31mul | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - Primitives.Int31mulc + CPrimitives.Int31mulc | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - Primitives.Int31div21 + CPrimitives.Int31div21 | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - Primitives.Int31diveucl + CPrimitives.Int31diveucl | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - Primitives.Int31addmuldiv + CPrimitives.Int31addmuldiv | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - Primitives.Int31compare + CPrimitives.Int31compare | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - Primitives.Int31head0 + CPrimitives.Int31head0 | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - Primitives.Int31tail0 + CPrimitives.Int31tail0 | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - Primitives.Int31lor + CPrimitives.Int31lor | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - Primitives.Int31land + CPrimitives.Int31land | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - Primitives.Int31lxor + CPrimitives.Int31lxor | _ -> empty_reactive_info let _ = Hook.set Retroknowledge.dispatch_hook dispatch |