From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/environ.ml | 376 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 215 insertions(+), 161 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 89ba6f65..778c9a24 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -28,26 +28,208 @@ open Names open Constr open Vars open Declarations -open Pre_env open Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* The type of environments. *) -type named_context_val = Pre_env.named_context_val +(* The key attached to each constant is used by the VM to retrieve previous *) +(* evaluations of the constant. It is essentially an index in the symbols table *) +(* used by the VM. *) +type key = int CEphemeron.key option ref + +(** Linking information for the native compiler. *) + +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t; +} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type val_kind = + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key + | VKnone + +type lazy_val = val_kind ref + +let force_lazy_val vk = match !vk with +| VKnone -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None + +let dummy_lazy_val () = ref VKnone +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) + +type named_context_val = { + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; +} + +type rel_context_val = { + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; +} + +type env = { + env_globals : globals; + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} + +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} + +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + +let empty_env = { + env_globals = { + env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_modules = MPmap.empty; + env_modtypes = MPmap.empty}; + env_named_context = empty_named_context_val; + env_rel_context = empty_rel_context_val; + env_nb_rel = 0; + env_stratification = { + env_universes = UGraph.initial_universes; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } + + +(* Rel context *) + +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + +let push_rel d env = + { env with + env_rel_context = push_rel_context_val d env.env_rel_context; + env_nb_rel = env.env_nb_rel + 1 } + +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let lookup_rel_val n env = + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} + +let env_of_rel n env = + { env with + env_rel_context = rel_skipn n env.env_rel_context; + env_nb_rel = env.env_nb_rel - n + } + +(* Named context *) + +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } + +let push_named d env = + {env with env_named_context = push_named_context_val d env.env_named_context} -type env = Pre_env.env +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_val id env = + snd(Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_ctxt id ctxt = + fst (Id.Map.find id ctxt.env_named_map) + +let fold_constants f env acc = + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + +(* Global constants *) + +let lookup_constant_key kn env = + Cmap_env.find kn env.env_globals.env_constants + +let lookup_constant kn env = + fst (Cmap_env.find kn env.env_globals.env_constants) + +(* Mutual Inductives *) +let lookup_mind kn env = + fst (Mindmap_env.find kn env.env_globals.env_inductives) + +let lookup_mind_key kn env = + Mindmap_env.find kn env.env_globals.env_inductives -let pre_env env = env -let env_of_pre_env env = env 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 - -let empty_env = empty_env - let engagement env = env.env_stratification.env_engagement let typing_flags env = env.env_typing_flags @@ -72,15 +254,11 @@ let empty_context env = | _ -> false (* Rel context *) -let lookup_rel = lookup_rel - let evaluable_rel n env = is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel -let push_rel = push_rel - let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = @@ -105,24 +283,14 @@ 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 *) -let map_named_val = map_named_val - let empty_named_context = Context.Named.empty -let push_named = push_named let push_named_context = List.fold_right push_named -let push_named_context_val = push_named_context_val let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -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 Constr.equal (named_context_of_val c1) (named_context_of_val c2) @@ -181,7 +349,10 @@ let map_universes f env = let s = env.env_stratification in { env with env_stratification = { s with env_universes = f s.env_universes } } - + +let set_universes env u = + { env with env_stratification = { env.env_stratification with env_universes = u } } + let add_constraints c env = if Univ.Constraint.is_empty c then env else map_universes (UGraph.merge_constraints c) env @@ -221,8 +392,6 @@ let set_typing_flags c env = (* Unsafe *) (* Global constants *) -let lookup_constant = lookup_constant - let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = @@ -319,19 +488,26 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -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.") - -let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false +let lookup_projection p env = + let mind,i = Projection.inductive p in + let mib = lookup_mind mind env in + (if not (Int.equal mib.mind_nparams (Projection.npars p)) + then anomaly ~label:"lookup_projection" Pp.(str "Bad number of parameters on projection.")); + match mib.mind_record with + | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection") + | PrimRecord infos -> + let _,_,typs = infos.(i) in + typs.(Projection.arg p) + +let get_projection env ind ~proj_arg = + let mib = lookup_mind (fst ind) env in + Declareops.inductive_make_projection ind mib ~proj_arg + +let get_projections env ind = + let mib = lookup_mind (fst ind) env in + Declareops.inductive_make_projections ind mib (* Mutual Inductives *) -let lookup_mind = lookup_mind - let polymorphic_ind (mind,i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) @@ -351,11 +527,11 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -468,10 +644,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(*s Compilation of global declaration *) - -let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false - exception Hyp_not_found let apply_to_hyp ctxt id f = @@ -530,121 +702,3 @@ let register env field entry = in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry - -(* the Environ.register function syncrhonizes the proactive and reactive - retroknowledge. *) -let dispatch = - - (* subfunction used for static decompilation of int31 (after a vm_compute, - see pretyping/vnorm.ml for more information) *) - let constr_of_int31 = - let nth_digit_plus_one i n = (* calculates the nth (starting with 0) - digit of i and adds 1 to it - (nth_digit_plus_one 1 3 = 2) *) - if Int.equal (i land (1 lsl n)) 0 then - 1 - else - 2 - in - fun ind -> fun digit_ind -> fun tag -> - let array_of_int i = - Array.init 31 (fun n -> mkConstruct - (digit_ind, nth_digit_plus_one i (30-n))) - in - (* We check that no bit above 31 is set to one. This assertion used to - fail in the VM, and led to conversion tests failing at Qed. *) - assert (Int.equal (tag lsr 31) 0); - mkApp(mkConstruct(ind, 1), array_of_int tag) - in - - (* subfunction which dispatches the compiling information of an - int31 operation which has a specific vm instruction (associates - 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)); - } - in - -fun rk value field -> - (* subfunction which shortens the (very common) dispatch of operations *) - let int31_op_from_const n op prim = - match kind value with - | Const 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) -> - 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)) - | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") - in - let i31bit_type = - match kind int31bit with - | Ind (i31bit_type,_) -> i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type.") - in - let int31_decompilation = - match kind value with - | Ind (i31t,_) -> - constr_of_int31 i31t i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type.") - in - { empty_reactive_info with - vm_decompile_const = Some int31_decompilation; - 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 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 - CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - CPrimitives.Int31lxor - | _ -> empty_reactive_info - -let _ = Hook.set Retroknowledge.dispatch_hook dispatch -- cgit v1.2.3