diff options
Diffstat (limited to 'kernel')
51 files changed, 921 insertions, 553 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune new file mode 100644 index 0000000000..3a714a8a59 --- /dev/null +++ b/kernel/byterun/dune @@ -0,0 +1,10 @@ +(library + (name byterun) + (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") + (public_name coq.vm) + (c_names coq_fix_code coq_memory coq_values coq_interp)) + +(rule + (targets coq_jumptbl.h) + (deps (:h-file coq_instruct.h)) + (action (run ./make_jumptbl.sh %{h-file} %{targets}))) diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh new file mode 100755 index 0000000000..eacd4daac8 --- /dev/null +++ b/kernel/byterun/make_jumptbl.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2} diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index ac4c6c52c6..fd9394025a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -31,7 +31,6 @@ open Environ open Esubst let stats = ref false -let share = ref true (* Profiling *) let beta = ref 0 @@ -266,6 +265,7 @@ type 'a infos_cache = { i_env : env; i_sigma : existential -> constr option; i_rels : (Constr.rel_declaration * lazy_val) Range.t; + i_share : bool; } and 'a infos = { @@ -313,12 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let evar_value cache ev = cache.i_sigma ev -let create mk_cl flgs env evars = +let create ~repr ~share flgs env evars = let cache = - { i_repr = mk_cl; + { i_repr = repr; i_env = env; i_sigma = evars; i_rels = env.env_rel_context.env_rel_map; + i_share = share; } in { i_flags = flgs; i_cache = cache } @@ -384,8 +385,8 @@ let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update v1 no t = - if !share then +let update ~share v1 no t = + if share then (v1.norm <- no; v1.term <- t; v1) @@ -498,14 +499,16 @@ let compact_stack head stk = (* Be sure to create a new cell otherwise sharing would be lost by the update operation *) let h' = lft_fconstr depth head in - let _ = update m h'.norm h'.term in + (** The stack contains [Zupdate] marks only if in sharing mode *) + let _ = update ~share:true m h'.norm h'.term in strip_rec depth s | stk -> zshift depth stk in strip_rec 0 stk (* Put an update mark in the stack, only if needed *) -let zupdate m s = - if !share && begin match m.norm with Red -> true | _ -> false end +let zupdate info m s = + let share = info.i_cache.i_share in + if share && begin match m.norm with Red -> true | _ -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -698,7 +701,8 @@ let rec zip m stk = | Zshift(n)::s -> zip (lift_fconstr n m) s | Zupdate(rf)::s -> - zip (update rf m.norm m.term) s + (** The stack contains [Zupdate] marks only if in sharing mode *) + zip (update ~share:true rf m.norm m.term) s let fapp_stack (m,stk) = zip m stk @@ -718,7 +722,8 @@ let strip_update_shift_app_red head stk = strip_rec (Zapp args :: rstk) {norm=h.norm;term=FApp(h,args)} depth s | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) depth s + (** The stack contains [Zupdate] marks only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) depth s | stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk @@ -743,7 +748,8 @@ let get_nth_arg head n stk = List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) n s + (** The stack contains [Zupdate] mark only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) n s | s -> (None, List.rev rstk @ s) in strip_rec [] head n stk @@ -752,7 +758,8 @@ let get_nth_arg head n stk = let rec get_args n tys f e stk = match stk with Zupdate r :: s -> - let _hd = update r Cstr (FLambda(n,tys,f,e)) in + (** The stack contains [Zupdate] mark only if in sharing mode *) + let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in get_args n tys f e s | Zshift k :: s -> get_args n tys f (subs_shft (k,e)) s @@ -889,10 +896,10 @@ let unfold_projection info p = let rec knh info m stk = match m.term with | FLIFT(k,a) -> knh info a (zshift k stk) - | FCLOS(t,e) -> knht info e t (zupdate m stk) + | FCLOS(t,e) -> knht info e t (zupdate info m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) + | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') @@ -901,7 +908,7 @@ let rec knh info m stk = | FProj (p,c) -> (match unfold_projection info p with | None -> (m, stk) - | Some s -> knh info c (s :: zupdate m stk)) + | Some s -> knh info c (s :: zupdate info m stk)) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| @@ -1019,10 +1026,11 @@ let rec zip_term zfun m stk = 2- tries to rebuild the term. If a closure still has to be computed, calls itself recursively. *) let rec kl info tab m = + let share = info.i_cache.i_share in if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info tab m [] in - let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) + let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info tab) (norm_head info tab nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1078,14 +1086,15 @@ let whd_stack infos tab m stk = match m.norm with knh infos m stk | Red | Cstr -> let k = kni infos tab m stk in - let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) + let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = - create (fun _ _ c -> inject c) flgs env evars + let share = (Environ.typing_flags env).Declarations.share_reduction in + create ~share ~repr:(fun _ _ c -> inject c) flgs env evars let create_tab () = KeyTable.create 17 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1e3e7b48ac..6121b3a1ec 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -15,7 +15,6 @@ open Esubst (** Flags for profiling reductions. *) val stats : bool ref -val share : bool ref val with_stats: 'a Lazy.t -> 'a @@ -106,8 +105,13 @@ type 'a infos = { i_cache : 'a infos_cache } val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env -> - (existential -> constr option) -> 'a infos +val create: + repr:('a infos -> 'a infos_tab -> constr -> 'a) -> + share:bool -> + reds -> + env -> + (existential -> constr option) -> + 'a infos val create_tab : unit -> 'a infos_tab val evar_value : 'a infos_cache -> existential -> constr option diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 9a1224aab2..ed3bd866a4 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -15,78 +15,7 @@ (* This file defines the type of bytecode instructions *) open Names -open Constr - -type tag = int - -let accu_tag = 0 - -let type_atom_tag = 2 -let max_atom_tag = 2 -let proj_tag = 3 -let fix_app_tag = 4 -let switch_tag = 5 -let cofix_tag = 6 -let cofix_evaluated_tag = 7 - -(* It would be great if OCaml exported this value, - So fixme if this happens in a new version of OCaml *) -let last_variant_tag = 245 - -type structured_constant = - | Const_sort of Sorts.t - | Const_ind of inductive - | Const_b0 of tag - | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.Level.t - -type reloc_table = (tag * int) array - -type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} - -let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 -| Const_sort _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 -| Const_ind _, _ -> false -| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 -| Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 -| Const_univ_level _ , _ -> false - -let rec hash_structured_constant c = - let open Hashset.Combine in - match c with - | Const_sort s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_b0 t -> combinesmall 3 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 4 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l) - -let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in - let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && - CArray.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall - -let hash_annot_switch asw = - let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 +open Vmvalues module Label = struct @@ -232,21 +161,6 @@ type comp_env = { open Pp open Util -let pp_sort s = - let open Sorts in - match s with - | Prop -> str "Prop" - | Set -> str "Set" - | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" - -let rec pp_struct_const = function - | Const_sort s -> pp_sort s - | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i - | Const_b0 i -> int i - | Const_bn (i,t) -> - int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) - | Const_univ_level l -> Univ.Level.pr l - let pp_lbl lbl = str "L" ++ int lbl let pp_fv_elem = function diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f17a1e657e..9c04c166a2 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -11,41 +11,7 @@ (* $Id$ *) open Names -open Constr - -type tag = int - -val accu_tag : tag - -val type_atom_tag : tag -val max_atom_tag : tag -val proj_tag : tag -val fix_app_tag : tag -val switch_tag : tag -val cofix_tag : tag -val cofix_evaluated_tag : tag - -val last_variant_tag : tag - -type structured_constant = - | Const_sort of Sorts.t - | Const_ind of inductive - | Const_b0 of tag - | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.Level.t - -val pp_struct_const : structured_constant -> Pp.t - -type reloc_table = (tag * int) array - -type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} - -val eq_structured_constant : structured_constant -> structured_constant -> bool -val hash_structured_constant : structured_constant -> int - -val eq_annot_switch : annot_switch -> annot_switch -> bool -val hash_annot_switch : annot_switch -> int +open Vmvalues module Label : sig diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index e336ea922d..5362f9a814 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -14,6 +14,7 @@ open Util open Names +open Vmvalues open Cbytecodes open Cemitcodes open Cinstr @@ -395,17 +396,17 @@ let init_fun_code () = fun_code := [] (* If [tag] hits the OCaml limitation for non constant constructors, we switch to another representation for the remaining constructors: -[last_variant_tag|tag - last_variant_tag|args] +[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args] -We subtract last_variant_tag for efficiency of match interpretation. +We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation. *) let nest_block tag arity cont = - Kconst (Const_b0 (tag - last_variant_tag)) :: - Kmakeblock(arity+1, last_variant_tag) :: cont + Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) :: + Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont let code_makeblock ~stack_size ~arity ~tag cont = - if tag < last_variant_tag then + if tag < Obj.last_non_constant_constructor_tag then Kmakeblock(arity, tag) :: cont else begin set_max_stack_size (stack_size + 1); @@ -490,7 +491,9 @@ let rec compile_lam env cenv lam sz cont = match lam with | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant cenv v sz cont + | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont + + | Lval v -> compile_structured_constant cenv (Const_val v) sz cont | Lproj (p,arg) -> compile_lam env cenv arg sz (Kproj p :: cont) @@ -634,9 +637,9 @@ let rec compile_lam env cenv lam sz cont = let lbl_consts = Array.make oib.mind_nb_constant Label.no in let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) let nconst = Array.length branches.constant_branches in - let nblock = min nallblock (last_variant_tag + 1) in + let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in let lbl_blocks = Array.make nblock Label.no in - let neblock = max 0 (nallblock - last_variant_tag) in + let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in let lbl_eblocks = Array.make neblock Label.no in let branch1, cont = make_branch cont in (* Compilation of the return type *) @@ -662,7 +665,7 @@ let rec compile_lam env cenv lam sz cont = let lbl_b, code_b = label_code ( Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in - lbl_blocks.(last_variant_tag) <- lbl_b; + lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b; c := code_b end; @@ -684,7 +687,7 @@ let rec compile_lam env cenv lam sz cont = compile_lam env (push_param arity sz_b cenv) body (sz_b+arity) (add_pop arity (branch::!c)) in let code_b = - if tag < last_variant_tag then begin + if tag < Obj.last_non_constant_constructor_tag then begin set_max_stack_size (sz_b + arity); Kpushfields arity :: code_b end @@ -694,8 +697,8 @@ let rec compile_lam env cenv lam sz cont = end in let lbl_b, code_b = label_code code_b in - if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b - else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; + if tag < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b; c := code_b done; diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ca24f9b689..50f5607e31 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -14,6 +14,7 @@ open Names open Constr +open Vmvalues open Cbytecodes open Copcodes open Mod_subst @@ -357,10 +358,9 @@ let rec emit env insns remaining = match insns with type to_patch = emitcodes * patches * fv (* Substitution *) -let rec subst_strcst s sc = +let subst_strcst s sc = match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc - | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_reloc s ri = diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 9009926bdb..39ddf4a047 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,4 +1,5 @@ open Names +open Vmvalues open Cbytecodes type reloc_info = diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 171ca38830..dca1757b7d 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names open Constr +open Vmvalues open Cbytecodes (** This file defines the lambda code for the bytecode compiler. It has been @@ -33,10 +34,11 @@ and lambda = | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array - | Lval of structured_constant + | Lval of structured_values | Lsort of Sorts.t | Lind of pinductive | Lproj of Projection.Repr.t * lambda + | Lint of int | Luint of uint (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7c00e40fb0..31dede6f5d 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -4,6 +4,7 @@ open Esubst open Term open Constr open Declarations +open Vmvalues open Cbytecodes open Cinstr open Environ @@ -115,6 +116,8 @@ let rec pp_lam lam = hov 1 (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg ++ str ")") + | Lint i -> + Pp.(str "(int:" ++ int i ++ str ")") | Luint _ -> str "(uint)" @@ -150,7 +153,7 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') @@ -269,7 +272,7 @@ let lam_subst_args subst args = let can_subst lam = match lam with | Lrel _ | Lvar _ | Lconst _ - | Lval _ | Lsort _ | Lind _ | Llam _ -> true + | Lval _ | Lsort _ | Lind _ -> true | _ -> false let rec simplify subst lam = @@ -349,7 +352,7 @@ let rec occurrence k kind lam = if n = k then if kind then false else raise Not_found else kind - | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> @@ -419,7 +422,7 @@ let rec remove_let subst lam = exception TooLargeInductive of Pp.t let max_nb_const = 0x1000000 -let max_nb_block = 0x1000000 + last_variant_tag - 1 +let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_tag - 1 let str_max_constructors = Format.sprintf @@ -436,23 +439,22 @@ let check_compilable ib = let is_value lc = match lc with - | Lval _ -> true + | Lval _ | Lint _ -> true | _ -> false let get_value lc = match lc with | Lval v -> v + | Lint i -> val_of_int i | _ -> raise Not_found -let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n) - let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) (* Translation of constructors *) let expand_constructor tag nparams arity = let ids = Array.make (nparams + arity) Anonymous in - if arity = 0 then mkLlam ids (mkConst_b0 tag) + if arity = 0 then mkLlam ids (Lint tag) else let args = make_args arity 1 in Llam(ids, Lmakeblock (tag, args)) @@ -463,15 +465,15 @@ let makeblock tag nparams arity args = mkLapp (expand_constructor tag nparams arity) args else (* The constructor is fully applied *) - if arity = 0 then mkConst_b0 tag + if arity = 0 then Lint tag else if Array.for_all is_value args then - if tag < last_variant_tag then - Lval(Cbytecodes.Const_bn(tag, Array.map get_value args)) + if tag < Obj.last_non_constant_constructor_tag then + Lval(val_of_block tag (Array.map get_value args)) else let args = Array.map get_value args in - let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in - Lval(Cbytecodes.Const_bn(last_variant_tag, args)) + let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in + Lval(val_of_block Obj.last_non_constant_constructor_tag args) else Lmakeblock(tag, args) @@ -659,11 +661,11 @@ let rec lambda_of_constr env c = (* translation of the argument *) let la = lambda_of_constr env a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = try Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge - entry la + gr la with Not_found -> la in (* translation of the type *) @@ -721,7 +723,7 @@ and lambda_of_app env f args = (try (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge - (mkConstU (kn,u)) in + (GlobRef.ConstRef kn) in let args = lambda_of_args env 0 args in f args with Not_found -> @@ -734,6 +736,7 @@ and lambda_of_app env f args = | Construct (c,_) -> let tag, nparams, arity = Renv.get_construct_info env c in let nargs = Array.length args in + let gr = GlobRef.ConstructRef c in if Int.equal (nparams + arity) nargs then (* fully applied *) (* spiwack: *) (* 1/ tries to compile the constructor in an optimal way, @@ -748,7 +751,7 @@ and lambda_of_app env f args = try Retroknowledge.get_vm_constant_static_info env.global_env.retroknowledge - f args + gr args with NotClosed -> (* 2/ if the arguments are not all closed (this is expectingly (and it is currently the case) the only @@ -769,7 +772,7 @@ and lambda_of_app env f args = let args = lambda_of_args env nparams rargs in Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f args + gr args with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) @@ -782,7 +785,7 @@ and lambda_of_app env f args = (try (Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f) args + gr) args with Not_found -> if nparams <= nargs then (* got all parameters *) makeblock tag 0 arity args @@ -834,10 +837,11 @@ let dynamic_int31_compilation fc args = if not fc then raise Not_found else Luint (UintDigits args) +let d0 = Lint 0 +let d1 = Lint 1 + (* We are relying here on the tags of digits constructors *) let digits_from_uint i = - let d0 = mkConst_b0 0 in - let d1 = mkConst_b0 1 in let digits = Array.make 31 d0 in for k = 0 to 30 do if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then diff --git a/kernel/constr.ml b/kernel/constr.ml index 9bf743152f..c73fe7fbde 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -503,7 +503,79 @@ let fold_constr_with_binders g f n acc c = not recursive and the order with which subterms are processed is not specified *) -let map f c = match kind c with +let rec map_under_context f n d = + if n = 0 then f d else + match kind d with + | LetIn (na,b,t,c) -> + let b' = f b in + let t' = f t in + let c' = map_under_context f (n-1) c in + if b' == b && t' == t && c' == c then d + else mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f t in + let b' = map_under_context f (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches f ci bl = + let nl = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context f) nl bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate f ci p = + map_under_context f (List.length ci.ci_pp_info.ind_tags) p + +let rec map_under_context_with_binders g f l n d = + if n = 0 then f l d else + match kind d with + | LetIn (na,b,t,c) -> + let b' = f l b in + let t' = f l t in + let c' = map_under_context_with_binders g f (g l) (n-1) c in + if b' == b && t' == t && c' == c then d + else mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f l t in + let b' = map_under_context_with_binders g f (g l) (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches_with_binders g f l ci bl = + let tags = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate_with_binders g f l ci p = + map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p + +let rec map_under_context_with_full_binders g f l n d = + if n = 0 then f l d else + match kind d with + | LetIn (na,b,t,c) -> + let b' = f l b in + let t' = f l t in + let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in + if b' == b && t' == t && c' == c then d + else mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f l t in + let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches_with_full_binders g f l ci bl = + let tags = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate_with_full_binders g f l ci p = + map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p + +let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c | Cast (b,k,t) -> @@ -540,6 +612,12 @@ let map f c = match kind c with let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') + | Case (ci,p,b,bl) when userview -> + let b' = f b in + let p' = map_return_predicate f ci p in + let bl' = map_branches f ci bl in + if b'==b && p'==p && bl'==bl then c + else mkCase (ci, p', b', bl') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in @@ -557,6 +635,9 @@ let map f c = match kind c with if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) +let map_user_view = map_gen true +let map = map_gen false + (* Like {!map} but with an accumulator. *) let fold_map f accu c = match kind c with diff --git a/kernel/constr.mli b/kernel/constr.mli index 70acf19328..ea38dabd5c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -285,8 +285,8 @@ val destMeta : constr -> metavariable (** Destructs a variable *) val destVar : constr -> Id.t -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) +(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether + [isprop] recognizes both [Prop] and [Set]. *) val destSort : constr -> Sorts.t (** Destructs a casted term *) @@ -381,6 +381,85 @@ type rel_context = rel_declaration list type named_context = named_declaration list type compacted_context = compacted_declaration list +(** {6 Functionals working on expressions canonically abstracted over + a local context (possibly with let-ins)} *) + +(** [map_under_context f l c] maps [f] on the immediate subterms of a + term abstracted over a context of length [n] (local definitions + are counted) *) + +val map_under_context : (constr -> constr) -> int -> constr -> constr + +(** [map_branches f br] maps [f] on the immediate subterms of an array + of "match" branches [br] in canonical eta-let-expanded form; it is + not recursive and the order with which subterms are processed is + not specified; it preserves sharing; the immediate subterms are the + types and possibly terms occurring in the context of each branch as + well as the body of each branch *) + +val map_branches : (constr -> constr) -> case_info -> constr array -> constr array + +(** [map_return_predicate f p] maps [f] on the immediate subterms of a + return predicate of a "match" in canonical eta-let-expanded form; + it is not recursive and the order with which subterms are processed + is not specified; it preserves sharing; the immediate subterms are + the types and possibly terms occurring in the context of each + branch as well as the body of the predicate *) + +val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr + +(** [map_under_context_with_binders g f n l c] maps [f] on the + immediate subterms of a term abstracted over a context of length + [n] (local definitions are counted); it preserves sharing; it + carries an extra data [n] (typically a lift index) which is + processed by [g] (which typically add 1 to [n]) at each binder + traversal *) + +val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr + +(** [map_branches_with_binders f br] maps [f] on the immediate + subterms of an array of "match" branches [br] in canonical + eta-let-expanded form; it carries an extra data [n] (typically a + lift index) which is processed by [g] (which typically adds 1 to + [n]) at each binder traversal; it is not recursive and the order + with which subterms are processed is not specified; it preserves + sharing; the immediate subterms are the types and possibly terms + occurring in the context of the branch as well as the body of the + branch *) + +val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array + +(** [map_return_predicate_with_binders f p] maps [f] on the immediate + subterms of a return predicate of a "match" in canonical + eta-let-expanded form; it carries an extra data [n] (typically a + lift index) which is processed by [g] (which typically adds 1 to + [n]) at each binder traversal; it is not recursive and the order + with which subterms are processed is not specified; it preserves + sharing; the immediate subterms are the types and possibly terms + occurring in the context of each branch as well as the body of the + predicate *) + +val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr + +(** [map_under_context_with_full_binders g f n l c] is similar to + [map_under_context_with_binders] except that [g] takes also a full + binder as argument and that only the number of binders (and not + their signature) is required *) + +val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr + +(** [map_branches_with_full_binders g f l br] is equivalent to + [map_branches_with_binders] but using + [map_under_context_with_full_binders] *) + +val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array + +(** [map_return_predicate_with_full_binders g f l p] is equivalent to + [map_return_predicate_with_binders] but using + [map_under_context_with_full_binders] *) + +val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr + (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] @@ -395,6 +474,13 @@ val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a val map : (constr -> constr) -> constr -> constr +(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it + differs from [map f c] in that the typing context and body of the + return predicate and of the branches of a [match] are considered as + immediate subterm of a [match] *) + +val map_user_view : (constr -> constr) -> constr -> constr + (** Like {!map}, but also has an additional accumulator. *) val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c06358054e..657478a106 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -24,6 +24,7 @@ open Declarations open Univ module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration (*s Cooking the constants. *) @@ -140,11 +141,31 @@ let expmod_constr cache modlist c = if is_empty_modlist modlist then c else substrec c -let abstract_constant_type = - List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) +(** Transforms a named context into a rel context. Also returns the list of + variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to + abstract a term that lived in that context. *) +let abstract_context hyps = + let fold decl (ctx, subst) = + let id, decl = match decl with + | NamedDecl.LocalDef (id, b, t) -> + let b = Vars.subst_vars subst b in + let t = Vars.subst_vars subst t in + id, RelDecl.LocalDef (Name id, b, t) + | NamedDecl.LocalAssum (id, t) -> + let t = Vars.subst_vars subst t in + id, RelDecl.LocalAssum (Name id, t) + in + (decl :: ctx, id :: subst) + in + Context.Named.fold_outside fold hyps ~init:([], []) + +let abstract_constant_type t (hyps, subst) = + let t = Vars.subst_vars subst t in + List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps -let abstract_constant_body = - List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) +let abstract_constant_body c (hyps, subst) = + let c = Vars.subst_vars subst c in + it_mkLambda_or_LetIn c hyps type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool @@ -173,6 +194,7 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let cache = RefTable.create 13 in let expmod = expmod_constr_subst cache modlist subst in let hyps = Context.Named.map expmod vars in + let hyps = abstract_context hyps in abstract_constant_body (expmod c) hyps let lift_univs cb subst auctx0 = @@ -207,12 +229,13 @@ let cook_constant ~hcons { from = cb; info } = let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst abs_ctx in let expmod = expmod_constr_subst cache modlist usubst in - let hyps = Context.Named.map expmod abstract in + let hyps0 = Context.Named.map expmod abstract in + let hyps = abstract_context hyps0 in let map c = let c = abstract_constant_body (expmod c) hyps in if hcons then Constr.hcons c else c in - let body = on_body modlist (hyps, usubst, abs_ctx) + let body = on_body modlist (hyps0, usubst, abs_ctx) map cb.const_body in @@ -220,7 +243,7 @@ let cook_constant ~hcons { from = cb; info } = Context.Named.fold_outside (fun decl hyps -> List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) - hyps ~init:cb.const_hyps in + hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0811eb72fd..61fcb4832a 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -65,6 +65,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } (* some contraints are in constant_constraints, some other may be in @@ -163,7 +164,7 @@ type one_inductive_body = { mind_nb_args : int; (** number of no constant constructor *) - mind_reloc_tbl : Cbytecodes.reloc_table; + mind_reloc_tbl : Vmvalues.reloc_table; } type abstract_inductive_universes = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index bbe4bc0dcb..51ec3defb3 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -21,6 +21,7 @@ let safe_flags oracle = { check_guarded = true; check_universes = true; conv_oracle = oracle; + share_reduction = true; } (** {6 Arities } *) @@ -305,13 +306,6 @@ let hcons_mind mib = mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } -(** {6 Stm machinery } *) - -let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" - | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" - (** Hashconsing of modules *) let hcons_functorize hty he hself f = match f with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index f91e69807f..35490ceef9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -11,7 +11,6 @@ open Declarations open Mod_subst open Univ -open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool val is_opaque : constant_body -> bool -(** Side effects *) - -val string_of_side_effect : side_effect -> string - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/dune b/kernel/dune new file mode 100644 index 0000000000..011af9c28c --- /dev/null +++ b/kernel/dune @@ -0,0 +1,15 @@ +(library + (name kernel) + (synopsis "The Coq Kernel") + (public_name coq.kernel) + (wrapped false) + (modules_without_implementation cinstr nativeinstr) + (libraries clib config lib byterun)) + +(rule + (targets copcodes.ml) + (deps (:h-file byterun/coq_instruct.h) make-opcodes) + (action (run ./make_opcodes.sh %{h-file} %{targets}))) + +(documentation + (package coq)) diff --git a/kernel/entries.ml b/kernel/entries.ml index 40873bea76..94248ad26b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -120,11 +120,14 @@ type seff_env = Same as the constant_body's but not in an ephemeron *) | `Opaque of Constr.t * Univ.ContextSet.t ] -type side_eff = - | SEsubproof of Constant.t * Declarations.constant_body * seff_env - | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string - -type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; - eff : side_eff; +(** Not used by the kernel. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type side_eff = { + seff_constant : Constant.t; + seff_body : Declarations.constant_body; + seff_env : seff_env; + seff_role : side_effect_role; } diff --git a/kernel/environ.ml b/kernel/environ.ml index e7efa5e2c9..62c14f6f07 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -693,12 +693,12 @@ let register_one env field entry = { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry } (* [register env field entry] may register several fields when needed *) -let register env field entry = +let register env field gr = match field with - | KInt31 (grp, Int31Type) -> - let i31c = match kind entry with - | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> 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 + | KInt31 Int31Type -> + let i31c = match gr with + | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1) + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") + in + register_one (register_one env (KInt31 Int31Constructor) i31c) field gr + | field -> register_one env field gr diff --git a/kernel/environ.mli b/kernel/environ.mli index f45b7be821..1343b9029b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -325,7 +325,7 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a val registered : env -> field -> bool -val register : env -> field -> Retroknowledge.entry -> env +val register : env -> field -> GlobRef.t -> env (** Native compiler *) val no_link_info : link_info diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index d7eb865e0a..f79e5270a2 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -280,7 +280,7 @@ let typecheck_inductive env mie = List.fold_left (fun (env_ar,l) ind -> (* Arities (without params) are typed-checked here *) - let expltype = ind.mind_entry_template in + let template = ind.mind_entry_template in let arity = if isArity ind.mind_entry_arity then let (ctx,s) = dest_arity env_params ind.mind_entry_arity in @@ -316,7 +316,7 @@ let typecheck_inductive env mie = let env_ar' = push_rel (LocalAssum (Name id, full_arity)) env_ar in (* (add_constraints cst2 env_ar) in *) - (env_ar', (id,full_arity,sign @ paramsctxt,expltype,deflev,inflev)::l)) + (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l)) (env',[]) mie.mind_entry_inds in @@ -343,7 +343,7 @@ let typecheck_inductive env mie = (* Compute/check the sorts of the inductive types *) let inds = - Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev) -> + Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev) -> let infu = (** Inferred level, with parameters and constructors. *) match inf_level with @@ -369,31 +369,34 @@ let typecheck_inductive env mie = RegularArity (not is_natural,full_arity,defu) in let template_polymorphic () = - let sign, s = + let _, s = try dest_arity env full_arity with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) - in - match s with - | Type u when expltype (* Explicitly polymorphic *) -> - (* The polymorphic level is a function of the level of the *) - (* conclusions of the parameters *) - (* We enforce [u >= lev] in case [lev] has a strict upper *) - (* constraints over [u] *) - let b = type_in_type env || UGraph.check_leq (universes env') infu u in - if not b then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev ++ Pp.str ".") - else - TemplateArity (param_ccls paramsctxt, infu) - | _ (* Not an explicit occurrence of Type *) -> - full_polymorphic () + in + let u = Sorts.univ_of_sort s in + (* The polymorphic level is a function of the level of the *) + (* conclusions of the parameters *) + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + let b = type_in_type env || UGraph.check_leq (universes env') infu u in + if not b then + anomaly ~label:"check_inductive" + (Pp.str"Incorrect universe " ++ + Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " + ++ Universe.pr clev ++ Pp.str ".") + else + TemplateArity (param_ccls paramsctxt, infu) in let arity = match mie.mind_entry_universes with - | Monomorphic_ind_entry _ -> template_polymorphic () - | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic () + | Monomorphic_ind_entry _ -> + if template then template_polymorphic () + else full_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> + if template + then anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") + else full_polymorphic () in (id,cn,lc,(sign,arity))) inds diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4d13a5fcb8..1d2f22b006 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -932,7 +932,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 07a02f6ef5..a18c5d1e20 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -10,13 +10,13 @@ Constr Vars Term Mod_subst +Vmvalues Cbytecodes Copcodes Cemitcodes Opaqueproof Declarations Entries -Vmvalues Nativevalues CPrimitives Declareops diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh new file mode 100755 index 0000000000..bb8aba2f07 --- /dev/null +++ b/kernel/make_opcodes.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +script_dir="$(dirname "$0")" +tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | awk -f "$script_dir"/make-opcodes > "${2}" diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index b35b9dda31..f1d08ef6dd 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -53,18 +53,25 @@ type delta_resolver = Deltamap.t let empty_delta_resolver = Deltamap.empty -module Umap = struct - type 'a t = 'a MPmap.t * 'a MBImap.t - let empty = MPmap.empty, MBImap.empty - let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 - let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) - let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) - let find_mp mp map = MPmap.find mp (fst map) - let find_mbi mbi map = MBImap.find mbi (snd map) - let iter_mbi f map = MBImap.iter f (snd map) - let fold fmp fmbi (m1,m2) i = - MPmap.fold fmp m1 (MBImap.fold fmbi m2 i) - let join map1 map2 = fold add_mp add_mbi map1 map2 +module Umap : + sig + type 'a t + val empty : 'a t + val is_empty : 'a t -> bool + val add_mbi : MBId.t -> 'a -> 'a t -> 'a t + val add_mp : ModPath.t -> 'a -> 'a t -> 'a t + val find : ModPath.t -> 'a t -> 'a + val join : 'a t -> 'a t -> 'a t + val fold : (ModPath.t -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + end = struct + type 'a t = 'a MPmap.t + let empty = MPmap.empty + let is_empty m = MPmap.is_empty m + let add_mbi mbi x m = MPmap.add (MPbound mbi) x m + let add_mp mp x m = MPmap.add mp x m + let find = MPmap.find + let fold = MPmap.fold + let join map1 map2 = fold add_mp map1 map2 end type substitution = (ModPath.t * delta_resolver) Umap.t @@ -93,8 +100,7 @@ let debug_string_of_delta resolve = let list_contents sub = let one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in - let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in - Umap.fold mp_one_pair mbi_one_pair sub [] + Umap.fold mp_one_pair sub [] let debug_string_of_subst sub = let l = List.map (fun (s1,(s2,s3)) -> s1^"|->"^s2^"["^s3^"]") @@ -222,15 +228,10 @@ let search_delta_inline resolve kn1 kn2 = let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPfile sid -> Umap.find_mp mp sub - | MPbound bid -> - begin - try Umap.find_mbi bid sub - with Not_found -> Umap.find_mp mp sub - end + | MPfile _ | MPbound _ -> Umap.find mp sub | MPdot (mp1,l) as mp2 -> begin - try Umap.find_mp mp2 sub + try Umap.find mp2 sub with Not_found -> let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve @@ -525,9 +526,7 @@ let substition_prefixed_by k mp subst = Umap.add_mp new_key (mp_to,reso) sub else sub in - let mbi_prefixmp mbi _ sub = sub - in - Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst + Umap.fold mp_prefixmp subst empty_subst let join subst1 subst2 = let apply_subst mpk add (mp,resolve) res = @@ -547,24 +546,9 @@ let join subst1 subst2 = Umap.join prefixed_subst (add (mp',resolve'') res) in let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in - let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in - let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in + let subst = Umap.fold mp_apply_subst subst1 empty_subst in Umap.join subst2 subst -let rec occur_in_path mbi = function - | MPbound bid' -> MBId.equal mbi bid' - | MPdot (mp1,_) -> occur_in_path mbi mp1 - | _ -> false - -let occur_mbid mbi sub = - let check_one mbi' (mp,_) = - if MBId.equal mbi mbi' || occur_in_path mbi mp then raise Exit - in - try - Umap.iter_mbi check_one sub; - false - with Exit -> true - type 'a substituted = { mutable subst_value : 'a; mutable subst_subst : substitution list; diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 2e5211c770..8416094063 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -165,11 +165,6 @@ val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t names appearing in [c] *) val subst_mps : substitution -> constr -> constr -(** [occur_*id id sub] returns true iff [id] occurs in [sub] - on either side *) - -val occur_mbid : MBId.t -> substitution -> bool - (** [repr_substituted r] dumps the representation of a substituted: - [None, a] when r is a value - [Some s, a] when r is a delayed substitution [s] applied to [a] *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 98a9973117..9435f46c6b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge = let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> Environ.register env f e | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" diff --git a/kernel/names.ml b/kernel/names.ml index e1d70e8111..933cefe993 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -935,7 +935,7 @@ end type projection = Projection.t -module GlobRef = struct +module GlobRefInternal = struct type t = | VarRef of variable (** A reference to the section-context. *) @@ -951,11 +951,84 @@ module GlobRef = struct | VarRef v1, VarRef v2 -> Id.equal v1 v2 | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false + let global_eq_gen eq_cst eq_ind eq_cons x y = + x == y || + match x, y with + | ConstRef cx, ConstRef cy -> eq_cst cx cy + | IndRef indx, IndRef indy -> eq_ind indx indy + | ConstructRef consx, ConstructRef consy -> eq_cons consx consy + | VarRef v1, VarRef v2 -> Id.equal v1 v2 + | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false + + let global_ord_gen ord_cst ord_ind ord_cons x y = + if x == y then 0 + else match x, y with + | VarRef v1, VarRef v2 -> Id.compare v1 v2 + | VarRef _, _ -> -1 + | _, VarRef _ -> 1 + | ConstRef cx, ConstRef cy -> ord_cst cx cy + | ConstRef _, _ -> -1 + | _, ConstRef _ -> 1 + | IndRef indx, IndRef indy -> ord_ind indx indy + | IndRef _, _ -> -1 + | _ , IndRef _ -> 1 + | ConstructRef consx, ConstructRef consy -> ord_cons consx consy + + let global_hash_gen hash_cst hash_ind hash_cons gr = + let open Hashset.Combine in + match gr with + | ConstRef c -> combinesmall 1 (hash_cst c) + | IndRef i -> combinesmall 2 (hash_ind i) + | ConstructRef c -> combinesmall 3 (hash_cons c) + | VarRef id -> combinesmall 4 (Id.hash id) + +end + +module GlobRef = struct + + type t = GlobRefInternal.t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + + let equal = GlobRefInternal.equal + + (* By default, [global_reference] are ordered on their canonical part *) + + module Ordered = struct + open Constant.CanOrd + type t = GlobRefInternal.t + let compare gr1 gr2 = + GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr + end + + module Ordered_env = struct + open Constant.UserOrd + type t = GlobRefInternal.t + let compare gr1 gr2 = + GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2 + let equal gr1 gr2 = + GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr + end + + module Map = HMap.Make(Ordered) + module Set = Map.Set + + (* Alternative sets and maps indexed by the user part of the kernel names *) + + module Map_env = HMap.Make(Ordered_env) + module Set_env = Map_env.Set + end type global_reference = GlobRef.t [@@ocaml.deprecated "Alias for [GlobRef.t]"] + type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t diff --git a/kernel/names.mli b/kernel/names.mli index 1cdf5c2402..2ea8108734 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -645,6 +645,28 @@ module GlobRef : sig val equal : t -> t -> bool + module Ordered : sig + type nonrec t = t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + + module Ordered_env : sig + type nonrec t = t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + + module Set_env : CSig.SetS with type elt = t + module Map_env : Map.ExtS + with type key = t and module Set := Set_env + + module Set : CSig.SetS with type elt = t + module Map : Map.ExtS + with type key = t and module Set := Set + end type global_reference = GlobRef.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index cc35a70cbf..eed25a4ca4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -632,6 +632,14 @@ let mkMLapp f args = | MLapp(f,args') -> MLapp(f,Array.append args' args) | _ -> MLapp(f,args) +let mkForceCofix prefix ind arg = + let name = fresh_lname Anonymous in + MLlet (name, arg, + MLif ( + MLisaccu (prefix, ind, MLlocal name), + MLapp (MLprimitive Force_cofix, [|MLlocal name|]), + MLlocal name)) + let empty_params = [||] let decompose_MLlam c = @@ -1067,12 +1075,11 @@ let ml_of_instance instance u = let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) - | Levar(evk,ty,args) -> - let tyn = fresh_lname Anonymous in + | Levar(evk, args) -> let i = push_symbol (SymbEvar evk) in + (** Arguments are *not* reversed in evar instances in native compilation *) let args = MLarray(Array.map (ml_of_lam env l) args) in - MLlet(tyn, ml_of_lam env l ty, - MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|]) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in @@ -1144,7 +1151,7 @@ let ml_of_instance instance u = let arg = ml_of_lam env l a in let force = if annot.asw_finite then arg - else MLapp(MLprimitive Force_cofix, [|arg|]) in + else mkForceCofix annot.asw_prefix annot.asw_ind arg in mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) @@ -1749,7 +1756,7 @@ let pp_mllam fmt l = | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i | Mk_var id -> - Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) + Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" @@ -2000,7 +2007,7 @@ let compile_mind mb mind stack = let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in let gn = Gproj ("", ind, proj_arg) in Glet (gn, mkMLlam [|c_uid|] code) :: acc in diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 931b8bbc86..c75dde843e 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu = match a1, a2 with | Ameta (m1,_), Ameta (m2,_) -> if Int.equal m1 m2 then cu else raise NotConvertible - | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + | Aevar (ev1, args1), Aevar (ev2, args2) -> if Evar.equal ev1 ev2 then Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu else raise NotConvertible diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 5075bd3d14..2d8e2ba2f0 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -25,7 +25,7 @@ and lambda = | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) - | Levar of Evar.t * lambda (* type *) * lambda array (* arguments *) + | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index cec0ee57d5..ab40c643f9 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -23,7 +23,6 @@ exception NotClosed type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } (*s Constructors *) @@ -88,7 +87,7 @@ let get_const_prefix env c = let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam + | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -139,6 +138,9 @@ let rec map_lam_with_binders g f n lam = | Luint u -> let u' = map_uint g f n u in if u == u' then lam else Luint u' + | Levar (evk, args) -> + let args' = Array.Smart.map (f n) args in + if args == args' then lam else Levar (evk, args') and map_uint g f n u = match u with @@ -371,14 +373,14 @@ let is_lazy env prefix t = | App (f,args) -> begin match kind f with | Construct (c,_) -> - let entry = mkInd (fst c) in - (try - let _ = - Retroknowledge.get_native_before_match_info env.retroknowledge - entry prefix c Llazy; - in + let gr = GlobRef.IndRef (fst c) in + (try + let _ = + Retroknowledge.get_native_before_match_info env.retroknowledge + gr prefix c Llazy; + in false - with Not_found -> true) + with Not_found -> true) | _ -> true end | LetIn _ | Case _ | Proj _ -> true @@ -386,13 +388,10 @@ let is_lazy env prefix t = let evar_value sigma ev = sigma.evars_val ev -let evar_type sigma ev = sigma.evars_typ ev - let meta_type sigma mv = sigma.evars_metas mv let empty_evars = { evars_val = (fun _ -> None); - evars_typ = (fun _ -> assert false); evars_metas = (fun _ -> assert false) } let empty_ids = [||] @@ -420,9 +419,8 @@ let rec lambda_of_constr cache env sigma c = | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> - let ty = evar_type sigma ev in let args = Array.map (lambda_of_constr cache env sigma) args in - Levar(evk, lambda_of_constr cache env sigma ty, args) + Levar(evk, args) | Some t -> lambda_of_constr cache env sigma t) | Cast (c, _, _) -> lambda_of_constr cache env sigma c @@ -484,12 +482,12 @@ let rec lambda_of_constr cache env sigma c = in (* translation of the argument *) let la = lambda_of_constr cache env sigma a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = - try - Retroknowledge.get_native_before_match_info (env).retroknowledge - entry prefix (ind,1) la - with Not_found -> la + try + Retroknowledge.get_native_before_match_info (env).retroknowledge + gr prefix (ind,1) la + with Not_found -> la in (* translation of the type *) let lt = lambda_of_constr cache env sigma t in @@ -538,7 +536,7 @@ and lambda_of_app cache env sigma f args = let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (env).retroknowledge (mkConst kn) prefix in + (env).retroknowledge (GlobRef.ConstRef kn) prefix in let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> @@ -563,17 +561,18 @@ and lambda_of_app cache env sigma f args = let expected = nparams + arity in let nargs = Array.length args in let prefix = get_mind_prefix env (fst (fst c)) in + let gr = GlobRef.ConstructRef c in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info (env).retroknowledge - f args + gr args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> let args = lambda_of_args cache env sigma nparams args in makeblock env c u tag args @@ -581,7 +580,7 @@ and lambda_of_app cache env sigma f args = let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index efe1700cd7..7b20258929 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -15,7 +15,6 @@ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } val empty_evars : evars diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 91f6add1c3..93e74af845 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -63,7 +63,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t * t array + | Aevar of Evar.t * t array | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 @@ -135,8 +135,8 @@ let mk_prod_accu s dom codom = let mk_meta_accu mv ty = mk_accu (Ameta (mv,ty)) -let mk_evar_accu ev ty args = - mk_accu (Aevar (ev,ty,args)) +let mk_evar_accu ev args = + mk_accu (Aevar (ev, args)) let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) @@ -154,10 +154,6 @@ let args_of_accu (k:accumulator) = let acc = (get_accu k).acc_arg in (Obj.magic (Array.of_list acc) : t array) -let is_accu x = - let o = Obj.repr x in - Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag - let mk_fix_accu rec_pos pos types bodies = mk_accu (Afix(types,bodies,rec_pos, pos)) @@ -172,19 +168,17 @@ let upd_cofix (cofix :t) (cofix_fun : t) = | _ -> assert false let force_cofix (cofix : t) = - if is_accu cofix then - let accu = (Obj.magic cofix : accumulator) in - let atom = atom_of_accu accu in - match atom with - | Acofix(typ,norm,pos,f) -> - let args = args_of_accu accu in - let f = Array.fold_right (fun arg f -> f arg) args f in - let v = f (Obj.magic ()) in - set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); - v - | Acofixe(_,_,_,v) -> v - | _ -> cofix - else cofix + let accu = (Obj.magic cofix : accumulator) in + let atom = atom_of_accu accu in + match atom with + | Acofix(typ,norm,pos,f) -> + let args = args_of_accu accu in + let f = Array.fold_right (fun arg f -> f arg) args f in + let v = f (Obj.magic ()) in + set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); + v + | Acofixe(_,_,_,v) -> v + | _ -> cofix let mk_const tag = Obj.magic tag diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 6bbf15160c..10689941e8 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -53,7 +53,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t (* type *) * t array (* arguments *) + | Aevar of Evar.t * t array (* arguments *) | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -70,7 +70,7 @@ val mk_prod_accu : Name.t -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t -val mk_evar_accu : Evar.t -> t -> t array -> t +val mk_evar_accu : Evar.t -> t array -> t val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 34f62defb8..e51c25c06b 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -19,12 +19,9 @@ open Names open Constr (* The retroknowledge defines a bijective correspondance between some - [entry]-s (which are, in fact, merely terms) and [field]-s which + [entry]-s (which are, in fact, merely names) and [field]-s which are roles assigned to these entries. *) -(* aliased type for clarity purpose*) -type entry = Constr.t - type int31_field = | Int31Bits | Int31Type @@ -53,8 +50,37 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field - + | KInt31 of int31_field + +let int31_field_of_string = + function + | "bits" -> Int31Bits + | "type" -> Int31Type + | "twice" -> Int31Twice + | "twice_plus_one" -> Int31TwicePlusOne + | "phi" -> Int31Phi + | "phi_inv" -> Int31PhiInv + | "plus" -> Int31Plus + | "plusc" -> Int31PlusC + | "pluscarryc" -> Int31PlusCarryC + | "minus" -> Int31Minus + | "minusc" -> Int31MinusC + | "minuscarryc" -> Int31MinusCarryC + | "times" -> Int31Times + | "timesc" -> Int31TimesC + | "div21" -> Int31Div21 + | "div" -> Int31Div + | "diveucl" -> Int31Diveucl + | "addmuldiv" -> Int31AddMulDiv + | "compare" -> Int31Compare + | "head0" -> Int31Head0 + | "tail0" -> Int31Tail0 + | "lor" -> Int31Lor + | "land" -> Int31Land + | "lxor" -> Int31Lxor + | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s) + +let int31_path = DirPath.make [ Id.of_string "int31" ] (* record representing all the flags of the internal state of the kernel *) type flags = {fastcomputation : bool} @@ -68,19 +94,13 @@ type flags = {fastcomputation : bool} module Proactive = Map.Make (struct type t = field let compare = Pervasives.compare end) -type proactive = entry Proactive.t +type proactive = GlobRef.t Proactive.t (* The [reactive] knowledge contains the mapping [entry->field]. Fields are later to be interpreted as a [reactive_info]. *) -module EntryOrd = -struct - type t = entry - let compare = Constr.compare -end - -module Reactive = Map.Make (EntryOrd) +module Reactive = GlobRef.Map type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : @@ -127,7 +147,7 @@ and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive} (* As per now, there is only the possibility of registering things the possibility of unregistering or changing the flag is under study *) type action = - | RKRegister of field*entry + | RKRegister of field * GlobRef.t (*initialisation*) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 02d961d893..0a2ef5300e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -13,9 +13,6 @@ open Constr type retroknowledge -(** aliased type for clarity purpose*) -type entry = Constr.t - (** the following types correspond to the different "things" the kernel can learn about.*) type int31_field = @@ -46,14 +43,18 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field + | KInt31 of int31_field + +val int31_field_of_string : string -> int31_field + +val int31_path : DirPath.t (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries As per now, there is only the possibility of registering things the possibility of unregistering or changing the flag is under study *) type action = - | RKRegister of field*entry + | RKRegister of field * GlobRef.t (** initial value for retroknowledge *) @@ -64,7 +65,7 @@ val initial_retroknowledge : retroknowledge and the continuation cont of the bytecode compilation returns the compilation of id in cont if it has a specific treatment or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> entry -> +val get_vm_compiling_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (*Given an identifier id (usually Construct _) and its argument array, returns a function that tries an ad-hoc optimisated @@ -73,7 +74,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> raises Not_found if id should be compiled as usual, and expectingly CBytecodes.NotClosed if the term is not a closed constructor pattern (a constant for the compiler) *) -val get_vm_constant_static_info : retroknowledge -> entry -> +val get_vm_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Cinstr.lambda (*Given an identifier id (usually Construct _ ) @@ -81,45 +82,45 @@ val get_vm_constant_static_info : retroknowledge -> entry -> of id+args+cont when id has a specific treatment (in the case of 31-bit integers, that would be the dynamic compilation into integers) or raises Not_found if id should be compiled as usual *) -val get_vm_constant_dynamic_info : retroknowledge -> entry -> +val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (** Given a type identifier, this function is used before compiling a match over this type. In the case of 31-bit integers for instance, it is used to add the instruction sequence which would perform a dynamic decompilation in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda +val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda -> Cinstr.lambda (** Given a type identifier, this function is used by pretyping/vnorm.ml to recover the elements of that type from their compiled form if it's non standard (it is used (and can be used) only when the compiled form is not a block *) -val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr +val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr -val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> +val get_native_compiling_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_constant_static_info : retroknowledge -> entry -> +val get_native_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Nativeinstr.lambda -val get_native_constant_dynamic_info : retroknowledge -> entry -> +val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_before_match_info : retroknowledge -> entry -> +val get_native_before_match_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda -> Nativeinstr.lambda (** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) -val add_field : retroknowledge -> field -> entry -> retroknowledge +val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge val mem : retroknowledge -> field -> bool (* val remove : retroknowledge -> field -> retroknowledge *) -val find : retroknowledge -> field -> entry +val find : retroknowledge -> field -> GlobRef.t (** Dispatching type for the above [get_*] functions. *) @@ -161,4 +162,4 @@ val empty_reactive_info : reactive_info (** Hook to be set after the compiler are installed to dispatch fields into the above [get_*] functions. *) -val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t +val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t 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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index aca77ccd13..08b97b718e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -type private_constant type private_constants -type private_constant_role = - | Subproof - | Schema of inductive * string - val side_effects_of_private_constants : - private_constants -> Entries.side_effect list + private_constants -> Entries.side_eff list (** Return the list of individual side-effects in the order of their creation. *) val empty_private_constants : private_constants -val add_private : private_constant -> private_constants -> private_constants -(** Add a constant to a list of private constants. The former must be more - recent than all constants appearing in the latter, i.e. one should not - create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constants +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -105,7 +96,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role val export_private_constants : in_section:bool -> private_constants Entries.definition_entry -> @@ -224,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a [@@ocaml.deprecated "Use the projection of Environ.env"] val register : - field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 + field -> GlobRef.t -> safe_transformer0 val register_inline : Constant.t -> safe_transformer0 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1f7ee145a2..43351737e5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -27,16 +27,10 @@ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) -let equal_eff e1 e2 = - let open Entries in - match e1, e2 with - | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> - Names.Constant.equal c1 c2 - | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> - CList.for_all2eq - (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) - cl1 cl2 - | _ -> false +type side_effect = { + from_env : Declarations.structure_body CEphemeron.key; + eff : side_eff list; +} module SideEffects : sig @@ -48,17 +42,11 @@ sig end = struct -let compare_seff e1 e2 = match e1, e2 with -| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2 -| SEscheme (cl1, _), SEscheme (cl2, _) -> - let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in - CList.compare cmp cl1 cl2 -| SEsubproof _, SEscheme _ -> -1 -| SEscheme _, SEsubproof _ -> 1 - module SeffOrd = struct type t = side_effect -let compare e1 e2 = compare_seff e1.eff e2.eff +let compare e1 e2 = + let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in + List.compare cmp e1.eff e2.eff end module SeffSet = Set.Make(SeffOrd) @@ -83,10 +71,14 @@ type _ trust = | SideEffects : structure_body -> side_effects trust let uniq_seff_rev = SideEffects.repr -let uniq_seff l = List.rev (SideEffects.repr l) +let uniq_seff l = + let ans = List.rev (SideEffects.repr l) in + List.map_append (fun { eff } -> eff) ans let empty_seff = SideEffects.empty -let add_seff = SideEffects.add +let add_seff mb eff effs = + let from_env = CEphemeron.create mb in + SideEffects.add { eff; from_env } effs let concat_seff = SideEffects.concat let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff @@ -94,11 +86,8 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff let inline_side_effects env body ctx side_eff = (** First step: remove the constants that are still in the environment *) let filter { eff = se; from_env = mb } = - let cbl = match se with - | SEsubproof (c, cb, b) -> [c, cb, b] - | SEscheme (cl,_) -> - List.map (fun (_, c, cb, b) -> c, cb, b) cl - in + let map e = (e.seff_constant, e.seff_body, e.seff_env) in + let cbl = List.map map se in let not_exists (c,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -468,58 +457,50 @@ let constant_entry_of_side_effect cb u = const_entry_inline_code = cb.const_inline_code } ;; -let turn_direct (kn,cb,u,r as orig) = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b,c) -> - let pt = Future.from_val (b,c) in - kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r - | _ -> orig -;; - -type side_effect_role = - | Subproof - | Schema of inductive * string +let turn_direct orig = + let cb = orig.seff_body in + if Declareops.is_opaque cb then + let p = match orig.seff_env with + | `Opaque (b, c) -> (b, c) + | _ -> assert false + in + let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in + let cb = { cb with const_body } in + { orig with seff_body = cb } + else orig type exported_side_effect = Constant.t * constant_body * side_effect_role +let export_eff eff = + (eff.seff_constant, eff.seff_body, eff.seff_role) + let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in - let not_exists (c,_,_,_) = - try ignore(Environ.lookup_constant c env); false + let not_exists e = + try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = match se with - | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] - | SEscheme (cl,k) -> - List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in - let cbl = List.filter not_exists cbl in - if cbl = [] then acc, sl + let cbl = List.filter not_exists se in + if List.is_empty cbl then acc, sl else cbl :: acc, (mb,List.length cbl) :: sl in let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in - let push_seff env = function - | kn, cb, `Nothing, _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const ctx -> - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end - | kn, cb, `Opaque(_, ctx), _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const cstctx -> - let env = Environ.push_context_set ~strict:true cstctx env in - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end + let push_seff env eff = + let { seff_constant = kn; seff_body = cb } = eff in + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Polymorphic_const _ -> env + | Monomorphic_const ctx -> + let ctx = match eff.seff_env with + | `Nothing -> ctx + | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx + in + Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = match seff with @@ -527,18 +508,22 @@ let export_side_effects mb env c = | cbs :: rest -> if Int.equal sl 0 then let env, cbs = - List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + List.fold_left (fun (env,cbs) eff -> + let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) + let eff = { eff with + seff_body = cb; + seff_env = `Nothing; + } in + (push_seff env eff, export_eff eff :: cbs)) (env,[]) cbs in translate_seff 0 rest (cbs @ acc) env else let cbs_len = List.length cbs in let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in - let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, r) cbs in + let ecbs = List.map export_eff cbs in translate_seff (sl - cbs_len) rest (ecbs @ acc) env in translate_seff trusted seff [] env diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 6a0ff072f5..b05e05e4dc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -38,24 +38,18 @@ val inline_entry_side_effects : yet type checked proof. *) val empty_seff : side_effects -val add_seff : side_effect -> side_effects -> side_effects +val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects val concat_seff : side_effects -> side_effects -> side_effects (** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in [e1] must be more recent than those of [e2]. *) -val uniq_seff : side_effects -> side_effect list +val uniq_seff : side_effects -> side_eff list (** Return the list of individual side-effects in the order of their creation. *) -val equal_eff : side_effect -> side_effect -> bool - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type side_effect_role = - | Subproof - | Schema of inductive * string - type exported_side_effect = Constant.t * constant_body * side_effect_role diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 1c323e3ea2..60293fe864 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -62,6 +62,7 @@ type ('constr, 'types) ptype_error = | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t + | UndeclaredUniverse of Univ.Level.t type type_error = (constr, types) ptype_error @@ -125,3 +126,6 @@ let error_elim_explain kp ki = let error_unsatisfied_constraints env c = raise (TypeError (env, UnsatisfiedConstraints c)) + +let error_undeclared_universe env l = + raise (TypeError (env, UndeclaredUniverse l)) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 20bf300ac3..3fd40a7f42 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -12,7 +12,7 @@ open Names open Constr open Environ -(** Type errors. {% \label{%}typeerrors{% }%} *) +(** Type errors. {% \label{typeerrors} %} *) (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) @@ -63,6 +63,7 @@ type ('constr, 'types) ptype_error = | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t + | UndeclaredUniverse of Univ.Level.t type type_error = (constr, types) ptype_error @@ -108,3 +109,5 @@ val error_ill_typed_rec_body : val error_elim_explain : Sorts.family -> Sorts.family -> arity_error val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a + +val error_undeclared_universe : env -> Univ.Level.t -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7f36f3813f..25c1cbff3a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -431,7 +431,28 @@ and execute_recdef env (names,lar,vdef) i = and execute_array env = Array.map (execute env) (* Derived functions *) + +let universe_levels_of_constr env c = + let rec aux s c = + match kind c with + | Const (c, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Sorts.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c + +let check_wellformed_universes env c = + let univs = universe_levels_of_constr env c in + try UGraph.check_declared_universes (universes env) univs + with UGraph.UndeclaredLevel u -> + error_undeclared_universe env u + let infer env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in make_judge constr t @@ -449,11 +470,13 @@ let type_judgment env {uj_val=c; uj_type=t} = {utj_val = c; utj_type = s } let infer_type env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in let s = check_type env constr t in {utj_val = constr; utj_type = s} let infer_v env cv = + let () = Array.iter (check_wellformed_universes env) cv in let jv = execute_array env cv in make_judgev cv jv @@ -461,9 +484,11 @@ let infer_v env cv = let infer_local_decl env id = function | Entries.LocalDefEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalDef (Name id, c, t) | Entries.LocalAssumEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalAssum (Name id, check_assumption env c t) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index bc624ba56d..95d71965df 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -529,6 +529,11 @@ let add_universe vlev strict g = let add_universe_unconstrained vlev g = fst (add_universe_gen vlev g) +exception UndeclaredLevel of Univ.Level.t +let check_declared_universes g us = + let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in + Univ.LSet.iter check us + exception Found_explanation of explanation let get_explanation strict u v g = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8c2d877b0b..752bf76270 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -55,6 +55,12 @@ val add_universe : Level.t -> bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t +(** Check that the universe levels are declared. Otherwise + @raise UndeclaredLevel l for the first undeclared level found. *) +exception UndeclaredLevel of Univ.Level.t + +val check_declared_universes : t -> Univ.LSet.t -> unit + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t diff --git a/kernel/vm.ml b/kernel/vm.ml index d7eedc226c..9917e94a35 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Cbytecodes open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index d6d9312938..8edd49f77f 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -9,8 +9,8 @@ (************************************************************************) open Names open Sorts -open Cbytecodes open Univ +open Constr (*******************************************) (* Initalization of the abstract machine ***) @@ -25,11 +25,124 @@ let _ = init_vm () (* Abstract data types and utility functions **********) (******************************************************) +(* The representation of values relies on this assertion *) +let _ = assert (Int.equal Obj.first_non_constant_constructor_tag 0) + (* Values of the abstract machine *) type values +type structured_values = values let val_of_obj v = ((Obj.obj v):values) let crazy_val = (val_of_obj (Obj.repr 0)) +type tag = int + +let accu_tag = 0 + +let type_atom_tag = 2 +let max_atom_tag = 2 +let proj_tag = 3 +let fix_app_tag = 4 +let switch_tag = 5 +let cofix_tag = 6 +let cofix_evaluated_tag = 7 + +(** Structured constants are constants whose construction is done once. Their +occurrences share the same value modulo kernel name substitutions (for functor +application). Structured values have the additional property that no +substitution will need to be performed, so their runtime value can directly be +shared without reallocating a more structured representation. *) +type structured_constant = + | Const_sort of Sorts.t + | Const_ind of inductive + | Const_b0 of tag + | Const_univ_level of Univ.Level.t + | Const_val of structured_values + +type reloc_table = (tag * int) array + +type annot_switch = + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + +let rec eq_structured_values v1 v2 = + v1 == v2 || + let o1 = Obj.repr v1 in + let o2 = Obj.repr v2 in + if Obj.is_int o1 && Obj.is_int o2 then o1 == o2 + else + let t1 = Obj.tag o1 in + let t2 = Obj.tag o2 in + if Int.equal t1 t2 && + Int.equal (Obj.size o1) (Obj.size o2) + then begin + assert (t1 <= Obj.last_non_constant_constructor_tag && + t2 <= Obj.last_non_constant_constructor_tag); + let i = ref 0 in + while (!i < Obj.size o1 && eq_structured_values + (Obj.magic (Obj.field o1 !i) : structured_values) + (Obj.magic (Obj.field o2 !i) : structured_values)) do + incr i + done; + !i >= Obj.size o1 + end + else false + +let hash_structured_values (v : structured_values) = + (* We may want a better hash function here *) + Hashtbl.hash v + +let eq_structured_constant c1 c2 = match c1, c2 with +| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 +| Const_sort _, _ -> false +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind _, _ -> false +| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 +| Const_univ_level _ , _ -> false +| Const_val v1, Const_val v2 -> eq_structured_values v1 v2 +| Const_val v1, _ -> false + +let hash_structured_constant c = + let open Hashset.Combine in + match c with + | Const_sort s -> combinesmall 1 (Sorts.hash s) + | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_b0 t -> combinesmall 3 (Int.hash t) + | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) + | Const_val v -> combinesmall 5 (hash_structured_values v) + +let eq_annot_switch asw1 asw2 = + let eq_ci ci1 ci2 = + eq_ind ci1.ci_ind ci2.ci_ind && + Int.equal ci1.ci_npar ci2.ci_npar && + CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls + in + let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in + eq_ci asw1.ci asw2.ci && + CArray.equal eq_rlc asw1.rtbl asw2.rtbl && + (asw1.tailcall : bool) == asw2.tailcall + +let hash_annot_switch asw = + let open Hashset.Combine in + let h1 = Constr.case_info_hash asw.ci in + let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h3 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 h3 + +let pp_sort s = + let open Sorts in + match s with + | Prop -> Pp.str "Prop" + | Set -> Pp.str "Set" + | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}") + +let pp_struct_const = function + | Const_sort s -> pp_sort s + | Const_ind (mind, i) -> Pp.(MutInd.print mind ++ str"#" ++ int i) + | Const_b0 i -> Pp.int i + | Const_univ_level l -> Univ.Level.pr l + | Const_val _ -> Pp.str "(value)" + (* Abstract data *) type vprod type vfun @@ -293,19 +406,21 @@ let obj_of_atom : atom -> Obj.t = res (* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = +let obj_of_str_const str = match str with | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_val v -> Obj.repr v + +let val_of_block tag (args : structured_values array) = + let nargs = Array.length args in + let r = Obj.new_block tag nargs in + for i = 0 to nargs - 1 do + Obj.set_field r i (Obj.repr args.(i)) + done; + (Obj.magic r : structured_values) let val_of_obj o = ((Obj.obj o) : values) @@ -313,6 +428,8 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str) let val_of_atom a = val_of_obj (obj_of_atom a) +let val_of_int i = (Obj.magic i : values) + let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in Obj.set_field r 0 (Obj.repr kn); @@ -514,10 +631,10 @@ let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 + if tag < Obj.last_non_constant_constructor_tag then Obj.new_block tag arity, 0 else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + let b = Obj.new_block Obj.last_non_constant_constructor_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-Obj.last_non_constant_constructor_tag)); b,1 in for i = ofs to ofs + arity - 1 do Obj.set_field b i (Obj.repr (val_of_rel (k+i))) diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6eedcf1d37..ae1d416ed5 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,11 +9,12 @@ (************************************************************************) open Names -open Cbytecodes +open Constr (** Values *) type values +type structured_values type vm_env type vm_global type vprod @@ -25,6 +26,38 @@ type arguments type vstack = values array type to_update +type tag = int + +val accu_tag : tag + +val type_atom_tag : tag +val max_atom_tag : tag +val proj_tag : tag +val fix_app_tag : tag +val switch_tag : tag +val cofix_tag : tag +val cofix_evaluated_tag : tag + +type structured_constant = + | Const_sort of Sorts.t + | Const_ind of inductive + | Const_b0 of tag + | Const_univ_level of Univ.Level.t + | Const_val of structured_values + +val pp_struct_const : structured_constant -> Pp.t + +type reloc_table = (tag * int) array + +type annot_switch = + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + val fun_val : vfun -> values val fix_val : vfix -> values val cofix_upd_val : to_update -> values @@ -110,6 +143,8 @@ val val_of_constant : Constant.t -> values val val_of_evar : Evar.t -> values val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values +val val_of_int : int -> structured_values +val val_of_block : tag -> structured_values array -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" @@ -158,4 +193,4 @@ val bfield : vblock -> int -> values (** Switch *) val check_switch : vswitch -> vswitch -> bool -val branch_arg : int -> Cbytecodes.tag * int -> values +val branch_arg : int -> tag * int -> values |