diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 127 |
1 files changed, 58 insertions, 69 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f87ec9e023..9d302c69fb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -210,13 +210,8 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -type private_constant = Entries.side_effect type private_constants = Term_typing.side_effects -type private_constant_role = Term_typing.side_effect_role = - | Subproof - | Schema of inductive * string - let empty_private_constants = Term_typing.empty_seff let add_private = Term_typing.add_seff let concat_private = Term_typing.concat_seff @@ -225,44 +220,38 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects let side_effects_of_private_constants = Term_typing.uniq_seff +let make_eff env cst r = + let open Entries in + let cbo = Environ.lookup_constant cst env.env in + { + seff_constant = cst; + seff_body = cbo; + seff_env = get_opaque_body env.env cbo; + seff_role = r; + } + let private_con_of_con env c = - let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + let open Entries in + let eff = [make_eff env c Subproof] in + add_private env.revstruct eff empty_private_constants let private_con_of_scheme ~kind env cl = - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) } + let open Entries in + let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in + add_private env.revstruct eff empty_private_constants let universes_of_private eff = - let open Declarations in - List.fold_left - (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc - in - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - acc l - | Entries.SEsubproof (c, cb, e) -> - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - [] (Term_typing.uniq_seff eff) + let open Entries in + let fold acc eff = + let acc = match eff.seff_env with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match eff.seff_body.const_universes with + | Monomorphic_const ctx -> ctx :: acc + | Polymorphic_const _ -> acc + in + List.fold_left fold [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -489,7 +478,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -903,8 +892,8 @@ let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) [@@@ocaml.warning "+3"] -let register field value by_clause senv = - (* todo : value closed, by_clause safe, by_clause of the proper type*) +let register field value senv = + (* todo : value closed *) (* spiwack : updates the safe_env with the information that the register action has to be performed (again) when the environment is imported *) { senv with @@ -988,39 +977,39 @@ 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 (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *) + native_compiling = Some (Nativelambda.compile_prim prim kn); } in fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = - match Constr.kind value with - | Constr.Const kn -> int31_op n op prim kn + match value with + | GlobRef.ConstRef kn -> int31_op n op prim kn | _ -> 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 match field with - | KInt31 (grp, Int31Type) -> + | KInt31 Int31Type -> let int31bit = (* invariant : the type of bits is registered, otherwise the function would raise Not_found. The invariant is enforced in safe_typing.ml *) match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits) | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = - match Constr.kind int31bit with - | Constr.Ind (i31bit_type,_) -> i31bit_type + match int31bit with + | GlobRef.IndRef i31bit_type -> i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = - match Constr.kind value with - | Constr.Ind (i31t,_) -> + match value with + | GlobRef.IndRef i31t -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") @@ -1030,46 +1019,46 @@ fun rk value field -> vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } - | KInt31 (_, Int31Constructor) -> + | KInt31 Int31Constructor -> { empty_reactive_info with 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 + | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31 CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31 CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31 CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31 CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + | KInt31 Int31MinusCarryC -> int31_binop_from_const Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31 CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31 CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31 CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31 CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31 CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31 CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31 CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31 CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31 CPrimitives.Int31lxor | _ -> empty_reactive_info |