diff options
Diffstat (limited to 'kernel')
64 files changed, 1219 insertions, 867 deletions
diff --git a/kernel/.merlin.in b/kernel/.merlin.in new file mode 100644 index 0000000000..912ff61496 --- /dev/null +++ b/kernel/.merlin.in @@ -0,0 +1,8 @@ +FLG -rectypes -thread -safe-string -w +a-4-44-50 + +S ../clib +B ../clib +S ../config +B ../config +S ../lib +B ../lib 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..003b49535f 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 = { @@ -281,7 +281,7 @@ let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache} as infos) tab ref = +let ref_value_cache ({i_cache = cache;_} as infos) tab ref = try Some (KeyTable.find tab ref) with Not_found -> @@ -289,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let body = match ref with | RelKey n -> - let open Context.Rel.Declaration in + let open! Context.Rel.Declaration in let i = n - 1 in let (d, _) = try Range.get cache.i_rels i @@ -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 @@ -548,45 +551,7 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v -(* Translate the head constructor of t from constr to fconstr. This - function is parameterized by the function to apply on the direct - subterms. - Could be used insted of mk_clos. *) -let mk_clos_deep clos_fun env t = - match kind t with - | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> - mk_clos env t - | Cast (a,k,b) -> - { norm = Red; - term = FCast (clos_fun env a, k, clos_fun env b)} - | App (f,v) -> - { norm = Red; - term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } - | Proj (p,c) -> - { norm = Red; - term = FProj (p, clos_fun env c) } - | Case (ci,p,c,v) -> - { norm = Red; - term = FCaseT (ci, p, clos_fun env c, v, env) } - | Fix fx -> - { norm = Cstr; term = FFix (fx, env) } - | CoFix cfx -> - { norm = Cstr; term = FCoFix(cfx,env) } - | Lambda _ -> - { norm = Cstr; term = mk_lambda env t } - | Prod (n,t,c) -> - { norm = Whnf; - term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } - | LetIn (n,b,t,c) -> - { norm = Red; - term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar ev -> - { norm = Red; term = FEvar(ev,env) } - -(* A better mk_clos? *) -let mk_clos2 = mk_clos_deep mk_clos - -(* The inverse of mk_clos_deep: move back to constr *) +(* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) @@ -698,7 +663,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 +684,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 +710,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 +720,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 @@ -830,7 +799,7 @@ let eta_expand_ind_stack env ind m s (f, s') = arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in + let (depth, args, _s) = strip_update_shift_app m s in (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> @@ -889,10 +858,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 +870,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 _| @@ -915,13 +884,18 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix _ -> knh info (mk_clos2 e t) stk + | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p,c) -> knh info (mk_clos2 e t) stk - | (Lambda _|Prod _|Construct _|CoFix _|Ind _| - LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> - (mk_clos2 e t, stk) + | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) + | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk + | LetIn (n,b,t,c) -> + { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk (************************************************************************) @@ -945,7 +919,7 @@ let rec knr info tab m stk = (match ref_value_cache info tab (RelKey k) with Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) -> + | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then @@ -1011,7 +985,7 @@ let rec zip_term zfun m stk = zip_term zfun h s | Zshift(n)::s -> zip_term zfun (lift n m) s - | Zupdate(rf)::s -> + | Zupdate(_rf)::s -> zip_term zfun m s (* Computes the strong normal form of a term. @@ -1019,10 +993,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 @@ -1030,7 +1005,7 @@ let rec kl info tab m = and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with - | FLambda(n,tys,f,e) -> + | FLambda(_n,tys,f,e) -> let (e',rvtys) = List.fold_left (fun (e,ctxt) (na,ty) -> (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) @@ -1078,14 +1053,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..c63795b295 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 @@ -197,8 +126,8 @@ let compare e1 e2 = match e1, e2 with | FVrel r1, FVrel r2 -> Int.compare r1 r2 | FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 -| FVuniv_var i1, FVevar _ -> -1 +| FVuniv_var _i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _i1, FVevar _ -> -1 | FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 | FVevar e1, FVevar e2 -> Evar.compare e1 e2 @@ -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..73620ae578 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,24 +396,24 @@ 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); Kpush :: nest_block tag arity cont end -let compile_structured_constant cenv sc sz cont = +let compile_structured_constant _cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont @@ -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) @@ -531,7 +534,7 @@ let rec compile_lam env cenv lam sz cont = comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - | Llet (id,def,body) -> + | Llet (_id,def,body) -> compile_lam env cenv def sz (Kpush :: compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) @@ -558,7 +561,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end - | Lfix ((rec_args, init), (decl, types, bodies)) -> + | Lfix ((rec_args, init), (_decl, types, bodies)) -> let ndef = Array.length types in let rfv = ref empty_fv in let lbl_types = Array.make ndef Label.no in @@ -591,7 +594,7 @@ let rec compile_lam env cenv lam sz cont = (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - | Lcofix(init, (decl,types,bodies)) -> + | Lcofix(init, (_decl,types,bodies)) -> let ndef = Array.length types in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in @@ -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..c21ce22421 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 @@ -106,7 +107,7 @@ let rec pp_lam lam = | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim((kn,_u),ar,op,args) -> + | Lprim((kn,_u),_ar,_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ @@ -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') @@ -212,7 +215,7 @@ let rec map_lam_with_binders g f n lam = let u' = map_uint g f n u in if u == u' then lam else Luint u' -and map_uint g f n u = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(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) @@ -530,7 +532,7 @@ struct size = 0; } - let extend v = + let extend (v : 'a t) = if v.size = Array.length v.elems then let new_size = min (2*v.size) Sys.max_array_length in if new_size <= v.size then raise (Invalid_argument "Vect.extend"); @@ -543,12 +545,12 @@ struct v.elems.(v.size) <- a; v.size <- v.size + 1 - let popn v n = + let popn (v : 'a t) n = v.size <- max 0 (v.size - n) let pop v = popn v 1 - let get_last v n = + let get_last (v : 'a t) n = if v.size <= n then raise (Invalid_argument "Vect.get:index out of bounds"); v.elems.(v.size - n - 1) @@ -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 *) @@ -713,7 +715,7 @@ let rec lambda_of_constr env c = and lambda_of_app env f args = match Constr.kind f with - | Const (kn,u as c) -> + | Const (kn,_u as c) -> let kn = get_alias env.global_env kn in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function @@ -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..c97969c0e0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -237,6 +237,17 @@ let mkVar id = Var id let kind c = c +let rec kind_nocast_gen kind c = + match kind c with + | Cast (c, _, _) -> kind_nocast_gen kind c + | App (h, outer) as k -> + (match kind_nocast_gen kind h with + | App (h, inner) -> App (h, Array.append inner outer) + | _ -> k) + | k -> k + +let kind_nocast c = kind_nocast_gen kind c + (* The other way around. We treat specifically smart constructors *) let of_kind = function | App (f, a) -> mkApp (f, a) @@ -360,17 +371,17 @@ let destConst c = match kind c with (* Destructs an existential variable *) let destEvar c = match kind c with - | Evar (kn, a as r) -> r + | Evar (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a (co)inductive type named kn *) let destInd c = match kind c with - | Ind (kn, a as r) -> r + | Ind (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a constructor *) let destConstruct c = match kind c with - | Construct (kn, a as r) -> r + | Construct (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) @@ -421,12 +432,12 @@ let fold f acc c = match kind c with | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c + | Proj (_p,c) -> f acc c | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> + | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> + | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl (* [iter f c] iters [f] on the immediate subterms of [c]; it is @@ -441,7 +452,7 @@ let iter f c = match kind c with | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c + | Proj (_p,c) -> f c | Evar (_,l) -> Array.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -463,7 +474,7 @@ let iter_with_binders g f n c = match kind c with | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> Array.Fun1.iter f n l | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl - | Proj (p,c) -> f n c + | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl @@ -483,19 +494,19 @@ let fold_constr_with_binders g f n acc c = | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g n) (f n acc t) c - | Lambda (na,t,c) -> f (g n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | Prod (_na,t,c) -> f (g n) (f n acc t) c + | Lambda (_na,t,c) -> f (g n) (f n acc t) c + | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c + | Proj (_p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -503,7 +514,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 +623,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 +646,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 @@ -674,10 +766,10 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose @@ -691,19 +783,16 @@ type constr_compare_fn = int -> constr -> constr -> bool calls to {!Array.equal_norefl}). *) let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = - match kind1 t1, kind2 t2 with + match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with + | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1, _, _), _ -> leq nargs c1 t2 - | _, Cast (c2, _, _) -> leq nargs t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 - | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && @@ -882,11 +971,11 @@ let constr_ord_int f t1 t2 = | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | App _, _ -> -1 | _, App _ -> 1 - | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -1145,9 +1234,9 @@ let rec hash t = combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) - | Fix (ln ,(_, tl, bl)) -> + | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) - | CoFix(ln, (_, tl, bl)) -> + | CoFix(_ln, (_, tl, bl)) -> combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n diff --git a/kernel/constr.mli b/kernel/constr.mli index 70acf19328..2efdae007c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -241,6 +241,11 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr +val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) + +val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + (** {6 Simple case analysis} *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -285,8 +290,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 +386,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 +479,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 @@ -432,50 +523,50 @@ val iter_with_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : constr_compare_fn -> constr_compare_fn +val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe instances, [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen : instance_compare_fn -> +val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn val compare_head_gen_leq_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -484,11 +575,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : instance_compare_fn -> +val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn -> + constr constr_compare_fn (** {6 Hashconsing} *) diff --git a/kernel/context.ml b/kernel/context.ml index 4a7204b75c..3d98381fbb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,8 +142,8 @@ struct (** Reduce all terms in a given declaration to a single value. *) let fold_constr f decl acc = match decl with - | LocalAssum (n,ty) -> f ty acc - | LocalDef (n,v,ty) -> f ty (f v acc) + | LocalAssum (_n,ty) -> f ty acc + | LocalDef (_n,v,ty) -> f ty (f v acc) let to_tuple = function | LocalAssum (na, ty) -> na, None, ty @@ -151,7 +151,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (na, v, ty) -> LocalAssum (na, ty) + | LocalDef (na, _v, ty) -> LocalAssum (na, ty) end @@ -356,7 +356,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (id, v, ty) -> LocalAssum (id, ty) + | LocalDef (id, _v, ty) -> LocalAssum (id, ty) let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 7ef63c1860..c74f2ab318 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -42,7 +42,7 @@ let empty = { cst_trstate = Cpred.full; } -let get_strategy { var_opacity; cst_opacity } f = function +let get_strategy { var_opacity; cst_opacity; _ } f = function | VarKey id -> (try Id.Map.find id var_opacity with Not_found -> default) @@ -51,7 +51,7 @@ let get_strategy { var_opacity; cst_opacity } f = function with Not_found -> default) | RelKey _ -> Expand -let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = +let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l = match k with | VarKey id -> let var_opacity = @@ -75,13 +75,13 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = { oracle with cst_opacity; cst_trstate; } | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") -let fold_strategy f { var_opacity; cst_opacity; } accu = +let fold_strategy f { var_opacity; cst_opacity; _ } accu = let fvar id lvl accu = f (VarKey id) lvl accu in let fcst cst lvl accu = f (ConstKey cst) lvl accu in let accu = Id.Map.fold fvar var_opacity accu in Cmap.fold fcst cst_opacity accu -let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) +let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c06358054e..b361e36bbf 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. *) @@ -90,7 +91,7 @@ let update_case_info cache ci modlist = try let ind, n = match share cache (IndRef ci.ci_ind) modlist with - | (IndRef f,(u,l)) -> (f, Array.length l) + | (IndRef f,(_u,l)) -> (f, Array.length l) | _ -> assert false in { ci with ci_ind = ind; ci_npar = ci.ci_npar + n } with Not_found -> @@ -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/csymtable.ml b/kernel/csymtable.ml index bb9231d000..8bef6aec42 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -173,7 +173,7 @@ and slot_for_fv env fv = | Some (v, _) -> v end | FVevar evk -> val_of_evar evk - | FVuniv_var idu -> + | FVuniv_var _idu -> assert false and eval_to_patch env (buff,pl,fv) = @@ -192,5 +192,5 @@ and val_of_constr env c = | Some v -> eval_to_patch env (to_memory v) | None -> assert false -let set_transparent_const kn = () (* !?! *) -let set_opaque_const kn = () (* !?! *) +let set_transparent_const _kn = () (* !?! *) +let set_opaque_const _kn = () (* !?! *) 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..d995786d97 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 } *) @@ -180,7 +181,7 @@ let subst_regular_ind_arity sub s = if uar' == s.mind_user_arity then s else { mind_user_arity = uar'; mind_sort = s.mind_sort } -let subst_template_ind_arity sub s = s +let subst_template_ind_arity _sub s = s (* FIXME records *) let subst_ind_arity = @@ -239,14 +240,14 @@ let inductive_polymorphic_context mib = let inductive_is_polymorphic mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> true - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> true + | Cumulative_ind _cumi -> true let inductive_is_cumulative mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> false - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> false + | Cumulative_ind _cumi -> true let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with @@ -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..a503238907 --- /dev/null +++ b/kernel/dune @@ -0,0 +1,20 @@ +(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)) + +; In dev profile, we check the kernel against a more strict set of +; warnings. +(env + (dev (flags :standard -w +a-4-44-50))) 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..dffcd70282 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -296,12 +296,12 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) -open Context.Named.Declaration - let named_type id env = + let open Context.Named.Declaration in get_type (lookup_named id env) let named_body id env = + let open Context.Named.Declaration in get_value (lookup_named id env) let evaluable_named id env = @@ -333,7 +333,7 @@ let fold_named_context f env ~init = let rec fold_right env = match match_named_context_val env.env_named_context with | None -> init - | Some (d, v, rem) -> + | Some (d, _v, rem) -> let env = reset_with_named_context rem env in f env d (fold_right env) @@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun g v -> UGraph.add_universe v strict g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g @@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env = let add_universes_set strict ctx g = let g = Univ.LSet.fold + (* Be lenient, module typing reintroduces universes and constraints due to includes *) (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g @@ -415,7 +415,7 @@ let constant_type env (kn,u) = let cb = lookup_constant kn env in match cb.const_universes with | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty - | Polymorphic_const ctx -> + | Polymorphic_const _ctx -> let csts = constraints_of cb u in (subst_instance_constr u cb.const_type, csts) @@ -508,14 +508,14 @@ let get_projections env ind = Declareops.inductive_make_projections ind mib (* Mutual Inductives *) -let polymorphic_ind (mind,i) env = +let polymorphic_ind (mind,_i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false else polymorphic_ind ind env -let type_in_type_ind (mind,i) env = +let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes let template_polymorphic_ind (mind,i) env = @@ -527,7 +527,7 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn (mind, _ as mind_key) env = +let add_mind_key kn (_mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = { env.env_globals with @@ -543,7 +543,7 @@ let lookup_constant_variables c env = let cmap = lookup_constant c env in Context.Named.to_vars cmap.const_hyps -let lookup_inductive_variables (kn,i) env = +let lookup_inductive_variables (kn,_i) env = let mis = lookup_mind kn env in Context.Named.to_vars mis.mind_hyps @@ -579,6 +579,7 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = + let open! Context.Named.Declaration in Context.Named.fold_inside (fun need decl -> if Id.Set.mem (get_id decl) need then @@ -594,6 +595,7 @@ let really_needed env needed = (named_context env) let keep_hyps env needed = + let open Context.Named.Declaration in let really_needed = really_needed env needed in Context.Named.fold_outside (fun d nsign -> @@ -647,6 +649,7 @@ type unsafe_type_judgment = types punsafe_type_judgment exception Hyp_not_found let apply_to_hyp ctxt id f = + let open Context.Named.Declaration in let rec aux rtail ctxt = match match_named_context_val ctxt with | Some (d, v, ctxt) -> @@ -663,6 +666,7 @@ let remove_hyps ids check_context check_value ctxt = let rec remove_hyps ctxt = match match_named_context_val ctxt with | None -> empty_named_context_val, false | Some (d, v, rctxt) -> + let open Context.Named.Declaration in let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) else if not seen then ctxt, false @@ -693,12 +697,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..b976469ff7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds = let instance_other = Instance.of_array new_levels in let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env_ar in - let env = Environ.push_context uctx_other env in + let env = Environ.push_context uctx_other env_ar in let subtyp_constraints = CumulativityInfo.leq_constraints cumi (UContext.instance uctx) instance_other @@ -243,7 +242,7 @@ let check_subtyping cumi paramsctxt env_ar inds = in let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) - Array.iter (fun (id,cn,lc,(sign,arity)) -> + Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; @@ -280,7 +279,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 +315,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 +342,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 +368,34 @@ let typecheck_inductive env mie = RegularArity (not is_natural,full_arity,defu) in let template_polymorphic () = - let sign, s = + let _sign, 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 @@ -426,7 +428,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum let explain_ind_err id ntyp env nparamsctxt c err = - let (lparams,c') = mind_extract_params nparamsctxt c in + let (_lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt)))) @@ -594,7 +596,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) - | err -> + | _err -> (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) @@ -611,7 +613,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( defined types, not one of the types of the mutually inductive block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) - and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = + and check_positive_nested (env,n,ntypes,_ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnrecpar = mib.mind_nparams_rec in let auxnnonrecpar = mib.mind_nparams - auxnrecpar in @@ -662,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( the type [c]) is checked to be the right (properly applied) inductive type. *) and check_constructors ienv check_head nmr c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = + let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -811,7 +813,7 @@ let compute_projections (kn, i as ind) mib = in let projections decl (i, j, labs, pbs, letsubst) = match decl with - | LocalDef (na,c,t) -> + | LocalDef (_na,c,_t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in @@ -839,7 +841,7 @@ let compute_projections (kn, i as ind) mib = (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, labs, pbs, letsubst) = + let (_, _, labs, pbs, _letsubst) = List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev labs), diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4d13a5fcb8..9bbcf07f7e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -154,10 +154,10 @@ let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) - | d::sign, None::exp, args -> + | _d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in make subst (sign, exp, args) - | d::sign, Some u::exp, a::args -> + | _d::sign, Some u::exp, a::args -> (* We recover the level of the argument, but we don't change the *) (* level in the corresponding type in the arity; this level in the *) (* arity is a global level which, at typing time, will be enforce *) @@ -165,7 +165,7 @@ let make_subst env = (* a useless extra constraint *) let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | LocalAssum (na,t) :: sign, Some u::exp, [] -> + | LocalAssum (_na,_t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -173,7 +173,7 @@ let make_subst env = (* update its image [x] by [sup x u] in order not to forget the *) (* dependency in [u] that remains to be fullfilled. *) make (remember_subst u subst) (sign, exp, []) - | sign, [], _ -> + | _sign, [], _ -> (* Uniform parameters are exhausted *) subst | [], _, _ -> @@ -199,7 +199,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -215,12 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = let type_of_inductive env pind = type_of_inductive_gen env pind [||] -let constrained_type_of_inductive env ((mib,mip),u as pind) = +let constrained_type_of_inductive env ((mib,_mip),u as pind) = let ty = type_of_inductive env pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = +let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = let ty = type_of_inductive_gen env pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -249,7 +249,7 @@ let type_of_constructor (cstr, u) (mib,mip) = if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = +let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let ty = type_of_constructor cstru ind in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -279,7 +279,7 @@ let inductive_sort_family mip = let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (ind,u) (mib,mip) params = +let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s @@ -563,7 +563,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_all env s) in + let i,_l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -635,10 +635,10 @@ let get_recargs_approx env tree ind args = build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end - | err -> + | _err -> mk_norec - and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = + and build_recargs_nested (env,_ra_env as ienv) tree (((mind,i),u), largs) = (* If the inferred tree already disallows recursion, no need to go further *) if eq_wf_paths tree mk_norec then tree else @@ -676,7 +676,7 @@ let get_recargs_approx env tree ind args = (Rtree.mk_rec irecargs).(i) and build_recargs_constructors ienv trees c = - let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = + let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -685,7 +685,7 @@ let get_recargs_approx env tree ind args = let recarg = build_recargs ienv (List.hd trees) b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d - | hd -> + | _hd -> List.rev lrec in recargs_constr_rec ienv trees [] c @@ -794,7 +794,7 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> + | Subterm (_s, wf) -> (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) @@ -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 @@ -964,7 +964,7 @@ let check_one_fix renv recpos trees def = else check_rec_call renv' [] body) bodies - | Const (kn,u as cu) -> + | Const (kn,_u as cu) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> @@ -983,7 +983,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b - | CoFix (i,(_,typarray,bodies as recdef)) -> + | CoFix (_i,(_,typarray,bodies as recdef)) -> List.iter (check_rec_call renv []) l; Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in @@ -992,13 +992,13 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Proj (p, c) -> + | Proj (_p, c) -> List.iter (check_rec_call renv []) l; check_rec_call renv [] c | Var id -> begin - let open Context.Named.Declaration in + let open! Context.Named.Declaration in match lookup_named id renv.env with | LocalAssum _ -> List.iter (check_rec_call renv []) l @@ -1129,10 +1129,10 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct ((_,i as cstr_kn),u) -> + | Construct ((_,i as cstr_kn),_u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in - let (mib,mip) = lookup_mind_specif env mI in + let (mib,_mip) = lookup_mind_specif env mI in let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> @@ -1157,7 +1157,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - | CoFix (j,(_,varit,vdefs as recdef)) -> + | CoFix (_j,(_,varit,vdefs as recdef)) -> if List.for_all (noccur_with_meta n nbfix) args then if Array.for_all (noccur_with_meta n nbfix) varit then @@ -1203,7 +1203,7 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = +let check_cofix env (_bodynum,(names,types,bodies as recdef)) = let flags = Environ.typing_flags env in if flags.check_guarded then let nbfix = Array.length bodies in 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..bff3092655 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 @@ -318,12 +319,12 @@ let subst_con sub cst = let subst_con_kn sub con = subst_con sub (con,Univ.Instance.empty) -let subst_pcon sub (con,u as pcon) = - try let con', can = subst_con0 sub pcon in +let subst_pcon sub (_con,u as pcon) = + try let con', _can = subst_con0 sub pcon in con',u with No_subst -> pcon -let subst_pcon_term sub (con,u as pcon) = +let subst_pcon_term sub (_con,u as pcon) = try let con', can = subst_con0 sub pcon in (con',u), can with No_subst -> pcon, mkConstU pcon @@ -440,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn = let rec mp_in_mp mp mp1 = match mp1 with | _ when ModPath.equal mp1 mp -> true - | MPdot (mp2,l) -> mp_in_mp mp mp2 + | MPdot (mp2,_l) -> mp_in_mp mp mp2 | _ -> false let subset_prefixed_by mp resolver = @@ -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..424d329e09 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -138,7 +138,7 @@ let rec functor_smart_map fty f0 funct = match funct with let a' = f0 a in if a==a' then funct else NoFunctor a' let rec functor_iter fty f0 = function - |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e + |MoreFunctor (_mbid,ty,e) -> fty ty; functor_iter fty f0 e |NoFunctor a -> f0 a (** {6 Misc operations } *) @@ -171,7 +171,7 @@ let implem_iter fs fa impl = match impl with (** {6 Substitutions of modular structures } *) -let id_delta x y = x +let id_delta x _y = x let subst_with_body sub = function |WithMod(id,mp) as orig -> @@ -200,7 +200,7 @@ let rec subst_structure sub do_delta sign = and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> - let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in let mp' = subst_mp sub mp in let sub = if ModPath.equal mp mp' then sub @@ -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" @@ -371,7 +371,7 @@ and strengthen_sig mp_from struc mp_to reso = match struc with let item' = l,SFBmodule mb' in let reso',rest' = strengthen_sig mp_from rest mp_to reso in add_delta_resolver reso' mb.mod_delta, item':: rest' - |(l,SFBmodtype mty as item) :: rest -> + |(_l,SFBmodtype _mty as item) :: rest -> let reso',rest' = strengthen_sig mp_from rest mp_to reso in reso',item::rest' @@ -628,7 +628,7 @@ let join_structure except otab s = let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type - and join_field (l,body) = match body with + and join_field (_l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () |SFBmodule m -> diff --git a/kernel/names.ml b/kernel/names.ml index e1d70e8111..6d33f233e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -207,7 +207,7 @@ struct let repr mbid = mbid - let to_string (i, s, p) = + let to_string (_i, s, p) = DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = @@ -328,7 +328,7 @@ module ModPath = struct let rec dp = function | MPfile sl -> sl | MPbound (_,_,dp) -> dp - | MPdot (mp,l) -> dp mp + | MPdot (mp,_l) -> dp mp module Self_Hashcons = struct type t = module_path @@ -420,7 +420,7 @@ module KerName = struct let hash kn = let h = kn.refhash in if h < 0 then - let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in + let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in (* Ensure positivity on all platforms. *) let h = h land 0x3FFFFFFF in @@ -623,8 +623,8 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let inductive_of_constructor (ind, i) = ind -let index_of_constructor (ind, i) = i +let inductive_of_constructor (ind, _i) = ind +let index_of_constructor (_ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = @@ -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..74b075f4a5 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 = @@ -999,7 +1007,7 @@ let compile_prim decl cond paux = *) let rec opt_prim_aux paux = match paux with - | PAprim(prefix, kn, op, args) -> + | PAprim(_prefix, _kn, op, args) -> let args = Array.map opt_prim_aux args in app_prim (Coq_primitive(op,None)) args (* @@ -1063,16 +1071,15 @@ let ml_of_instance instance u = match t with | Lrel(id ,i) -> get_rel env id i | Lvar id -> get_var env id - | Lmeta(mv,ty) -> + | Lmeta(mv,_ty) -> 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) @@ -1177,7 +1184,7 @@ let ml_of_instance instance u = let lf,env_n = push_rels (empty_env env.env_univ ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in - let mk_let envi (id,def) t = MLlet (id,def,t) in + let mk_let _envi (id,def) t = MLlet (id,def,t) in let mk_lam_or_let (params,lets,env) (id,def) = let ln,env' = push_rel env id in match def with @@ -1210,7 +1217,7 @@ let ml_of_instance instance u = (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in (* Compilation of fix *) let fv_args = fv_args env fvn fvr in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in let mk_norm = MLapp(MLglobal norm, fv_args) in let mkrec i lname = @@ -1265,9 +1272,9 @@ let ml_of_instance instance u = let mk_norm = MLapp(MLglobal norm, fv_args) in let lnorm = fresh_lname Anonymous in let ltype = fresh_lname Anonymous in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in - let upd i lname cont = + let upd i _lname cont = let paramsi = t_params.(i) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in let uniti = fresh_lname Anonymous in @@ -1298,7 +1305,7 @@ let ml_of_instance instance u = (lname, paramsi, body) in MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) - | Lmakeblock (prefix,(cn,u),_,args) -> + | Lmakeblock (prefix,(cn,_u),_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) | Lconstruct (prefix, (cn,u)) -> @@ -1554,7 +1561,7 @@ let rec list_of_mp acc = function let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,dp,l) = KerName.repr kn in + let (mp,_dp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l @@ -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" @@ -1980,7 +1987,7 @@ let compile_mind mb mind stack = (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in - let add_proj proj_arg acc pb = + let add_proj proj_arg acc _pb = let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -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 @@ -2046,9 +2053,9 @@ let compile_mind_deps env prefix ~interactive let compile_deps env sigma prefix ~interactive init t = let rec aux env lvl init t = match kind t with - | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind + | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in + let c,_u = get_alias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref @@ -2067,11 +2074,11 @@ let compile_deps env sigma prefix ~interactive init t = let comp_stack = code@comp_stack in let const_updates = Cmap_env.add c (nameref, name) const_updates in comp_stack, (mind_updates, const_updates) - | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind + | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in aux env lvl init c - | Case (ci, p, c, ac) -> + | Case (ci, _p, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in fold_constr_with_binders succ (aux env) lvl init t diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 931b8bbc86..054b6a2d17 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -25,9 +25,9 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in conv_val env CONV (lvl+1) (f1 v) (f2 v) cu - | Vfun f1, _ -> + | Vfun _f1, _ -> conv_val env CONV lvl v1 (fun x -> v2 x) cu - | _, Vfun f2 -> + | _, Vfun _f2 -> conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> conv_accu env pb lvl k1 k2 cu @@ -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 @@ -110,7 +110,7 @@ and conv_atom env pb lvl a1 a2 cu = else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu - | Aprod(_,d1,c1), Aprod(_,d2,c2) -> + | Aprod(_,d1,_c1), Aprod(_,d2,_c2) -> let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu 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..70cb8691c6 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,8 +138,11 @@ 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 = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(prefix,c,args) -> @@ -201,7 +203,7 @@ let can_subst lam = let can_merge_if bt bf = match bt, bf with - | Llam(idst,_), Llam(idsf,_) -> true + | Llam(_idst,_), Llam(_idsf,_) -> true | _ -> false let merge_if t bt bf = @@ -368,17 +370,17 @@ module Cache = let is_lazy env prefix t = match kind t with - | App (f,args) -> + | 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 @@ -433,7 +431,7 @@ let rec lambda_of_constr cache env sigma c = | Sort s -> Lsort s - | Ind (ind,u as pind) -> + | Ind (ind,_u as pind) -> let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) @@ -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 @@ -531,14 +529,14 @@ let rec lambda_of_constr cache env sigma c = and lambda_of_app cache env sigma f args = match kind f with - | Const (kn,u as c) -> + | Const (_kn,_u as c) -> let kn,u = get_alias env c in let cb = lookup_constant kn env in (try 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/nativelib.ml b/kernel/nativelib.ml index f784509b6f..b4126dd68c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -40,7 +40,7 @@ let include_dirs () = [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) -let load_obj = ref (fun x -> () : string -> unit) +let load_obj = ref (fun _x -> () : string -> unit) let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) @@ -113,7 +113,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true - | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> warn_native_compiler_failed (Inl res); false in res, link_filename @@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds = (try if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix - with Dynlink.Error e as exn -> + with Dynlink.Error _ as exn -> let exn = CErrors.push exn in if fatal then iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index edce9367fc..8ac3538fc5 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -29,7 +29,7 @@ and translate_field prefix mp env acc (l,x) = | SFBconst cb -> let con = Constant.make3 mp DirPath.empty l in (if !Flags.debug then - let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in + let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); compile_constant_field env prefix con acc cb | SFBmind mb -> 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/opaqueproof.ml b/kernel/opaqueproof.ml index f8b71e4564..303cb06c55 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -87,21 +87,21 @@ let discharge_direct_opaque ~cook_constr ci = function | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp } = function +let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> ignore(Future.join cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in ignore(Future.join fp) -let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function +let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some (Future.uuid cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some (Future.uuid (snd (Int.Map.find i prfs))) else None -let force_proof { opaque_val = prfs; opaque_dir = odp } = function +let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> fst(Future.force cu) | Indirect (l,dp,i) -> @@ -112,7 +112,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints { opaque_val = prfs; opaque_dir = odp } = function +let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp @@ -121,14 +121,14 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | None -> Univ.ContextSet.empty | Some u -> Future.force u -let get_constraints { opaque_val = prfs; opaque_dir = odp } = function +let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof { opaque_val = prfs; opaque_dir = odp } = function +let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = @@ -144,7 +144,7 @@ let a_constr = Future.from_val (mkRel 1) let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : cooking_info list = [] -let dump { opaque_val = otab; opaque_len = n } = +let dump { opaque_val = otab; opaque_len = n; _ } = let opaque_table = Array.make n a_constr in let univ_table = Array.make n a_univ in let disch_table = Array.make n a_discharge in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c701b53fe4..2abb4b485c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -53,9 +53,9 @@ let compare_stack_shape stk1 stk2 = | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2 | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 - | (Zproj p1::s1, Zproj p2::s2) -> + | (Zproj _p1::s1, Zproj _p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> + | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -261,7 +261,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u s | Declarations.Polymorphic_ind _ -> cmp_instances u1 u2 s - | Declarations.Cumulative_ind cumi -> + | Declarations.Cumulative_ind _cumi -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s @@ -296,7 +296,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = (match (z1,z2) with | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,l1),Zlproj (c2,l2)) -> + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> if not (Projection.Repr.equal c1 c2) then raise NotConvertible else cu1 @@ -498,7 +498,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with - | FConstruct ((ind2,j2),u2) -> + | FConstruct ((ind2,_j2),_u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -515,7 +515,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with - | FConstruct ((ind1,j1),u1) -> + | FConstruct ((ind1,_j1),_u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -554,14 +554,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Eta expansion of records *) - | (FConstruct ((ind1,j1),u1), _) -> + | (FConstruct ((ind1,_j1),_u1), _) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) - | (_, FConstruct ((ind2,j2),u2)) -> + | (_, FConstruct ((ind2,_j2),_u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -659,14 +659,14 @@ let check_sort_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible | Set, Prop -> raise NotConvertible | Set, Type u -> check_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> check_pb u Univ.type0_univ | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances ~flex u u' univs = +let check_convert_instances ~flex:_ u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible @@ -707,7 +707,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 @@ -781,7 +781,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -let default_conv cv_pb ?(l2r=false) env t1 t2 = +let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL @@ -912,7 +912,7 @@ let is_arity env c = with NotArity -> false let eta_expand env t ty = - let ctxt, codom = dest_prod env ty in + let ctxt, _codom = dest_prod env ty in let ctxt',t = dest_lam env t in let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in let eta_args = List.rev_map mkRel (List.interval 1 d) in 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..b036aa6a67 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 @@ -284,7 +273,6 @@ let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst let push_context_set poly ctx = add_constraints (Now (poly,ctx)) -let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx)) let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false @@ -489,7 +477,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 +891,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 +976,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 +1018,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..6e0febaa3f 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 -> @@ -137,9 +128,6 @@ val add_modtype : val push_context_set : bool -> Univ.ContextSet.t -> safe_transformer0 -val push_context : - bool -> Univ.UContext.t -> safe_transformer0 - val add_constraints : Univ.Constraint.t -> safe_transformer0 @@ -224,7 +212,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/subtyping.ml b/kernel/subtyping.ml index 74042f9e04..bfe68671a2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -138,7 +138,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 + cst (inductive_is_polymorphic mib1) (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in let check_packet cst p1 p2 = @@ -162,10 +162,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst in let mind = MutInd.make1 kn1 in - let check_cons_types i cst p1 p2 = + let check_cons_types _i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - (inductive_is_polymorphic mib1) infer_conv env t1 t2) + (inductive_is_polymorphic mib1) (infer_conv ?l2r:None ?evars:None ?ts:None) env t1 t2) cst p2.mind_consnames (arities_of_specif (mind, inst) (mib1, p1)) @@ -229,7 +229,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = let err = NotConvertibleTypeField (env, t1, t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in match info1 with | Constant cb1 -> @@ -268,14 +268,14 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = Anyway [check_conv] will handle that afterwards. *) let c1 = Mod_subst.force_constr lc1 in let c2 = Mod_subst.force_constr lc2 in - check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2)) - | IndType ((kn,i),mind1) -> + check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2)) + | IndType ((_kn,_i),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ "name.") - | IndConstr (((kn,i),j),mind1) -> + | IndConstr (((_kn,_i),_j),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 4851a9c0d0..795cdeb040 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -54,13 +54,13 @@ let mkProd_wo_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkProd (na, t, c) - | LocalDef (na,b,t) -> subst1 b c + | LocalDef (_na,b,_t) -> subst1 b c let mkNamedProd_wo_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c - | LocalDef (id,b,t) -> subst1 b (subst_var id c) + | LocalDef (id,b,_t) -> subst1 b (subst_var id c) (* non-dependent product t1 -> t2 *) let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) @@ -81,7 +81,7 @@ let mkNamedLambda_or_LetIn decl c = (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = let rec prodrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) | _ -> assert false in @@ -93,7 +93,7 @@ let compose_prod l b = prodn (List.length l) l b (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *) let lamn n env b = let rec lamrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) | _ -> assert false in @@ -276,7 +276,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") + | _ -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -297,7 +297,7 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") + | _c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -313,7 +313,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") + | _ -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1f7ee145a2..47247ff25e 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 @@ -114,12 +103,7 @@ let inline_side_effects env body ctx side_eff = if List.is_empty side_eff then (body, ctx, sigs) else (** Second step: compute the lifts and substitutions to apply *) - let cname c = - let name = Constant.to_string c in - let map c = if c == '.' || c == '#' then '_' else c in - let name = String.map map name in - Name (Id.of_string name) - in + let cname c = Name (Label.to_id (Constant.label c)) in let fold (subst, var, ctx, args) (c, cb, b) = let (b, opaque) = match cb.const_body, b with | Def b, _ -> (Mod_subst.force_constr b, false) @@ -133,7 +117,7 @@ let inline_side_effects env body ctx side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const auctx -> + | Polymorphic_const _auctx -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) @@ -261,12 +245,14 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_universes = Monomorphic_const_entry univs } as c) -> + const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in @@ -297,8 +283,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let (body, ctx), side_eff = Future.join body in let body, ctx, _ = match trust with | Pure -> body, ctx, [] @@ -357,7 +343,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration kn env result = +let build_constant_declaration _kn env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -468,58 +454,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 { 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 +505,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 @@ -556,7 +538,7 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons r) -let translate_local_def env id centry = +let translate_local_def env _id centry = let open Cooking in let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { 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..7456ecea56 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -118,14 +118,14 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant env (kn,u as cst) = +let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let type_of_constant_in env (kn,u as cst) = +let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in constant_type_in env cst @@ -142,7 +142,7 @@ let type_of_constant_in env (kn,u as cst) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let type_of_abstraction env name var ty = +let type_of_abstraction _env name var ty = mkProd (name, var, ty) (* Type of an application. *) @@ -204,7 +204,7 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let type_of_product env name s1 s2 = +let type_of_product env _name s1 s2 = let s = sort_of_product env s1 s2 in mkSort s @@ -247,7 +247,7 @@ let check_cast env c ct k expected_type = dynamic constraints of the form u<=v are enforced *) let type_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in + let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args @@ -264,7 +264,7 @@ let type_of_inductive env (ind,u as indu) = (* Constructors. *) -let type_of_constructor env (c,u as cu) = +let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in @@ -285,7 +285,7 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let type_of_case env ci p pt c ct lf lft = +let type_of_case env ci p pt c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in @@ -399,7 +399,7 @@ let rec execute env cstr = let lft = execute_array env lf in type_of_case env ci p pt c ct lf lft - | Fix ((vn,i as vni),recdef) -> + | Fix ((_vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in check_fix env fix; fix_ty @@ -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) @@ -505,7 +530,7 @@ let judge_of_product env x varj outj = make_judge (mkProd (x, varj.utj_val, outj.utj_val)) (mkSort (sort_of_product env varj.utj_type outj.utj_type)) -let judge_of_letin env name defj typj j = +let judge_of_letin _env name defj typj j = make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) (subst1 defj.uj_val j.uj_type) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index bc624ba56d..9ff51fca55 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -194,7 +194,7 @@ let check_universes_invariants g = UMap.iter (fun l u -> match u with | Canonical u -> - UMap.iter (fun v strict -> + UMap.iter (fun v _strict -> incr n_edges; let v = repr g v in assert (topo_compare u v = -1); @@ -435,7 +435,7 @@ let reorder g u v = | n0::q0 -> (* Computing new root. *) let root, rank_rest = - List.fold_left (fun ((best, rank_rest) as acc) n -> + List.fold_left (fun ((best, _rank_rest) as acc) n -> if n.rank >= best.rank then n, best.rank else acc) (n0, min_int) q0 in @@ -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 = @@ -804,7 +809,7 @@ let normalize_universes g = in UMap.fold (fun _ u g -> match u with - | Equiv u -> g + | Equiv _u -> g | Canonical u -> let _, u, g = get_ltle g u in let _, _, g = get_gtge g u in @@ -816,7 +821,7 @@ let constraints_of_universes g = let uf = UF.create () in let constraints_of u v acc = match v with - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc @@ -938,7 +943,7 @@ let check_eq_instances g t1 t2 = (** Pretty-printing *) let pr_arc prl = function - | _, Canonical {univ=u; ltle} -> + | _, Canonical {univ=u; ltle; _} -> if UMap.is_empty ltle then mt () else prl u ++ str " " ++ @@ -958,7 +963,7 @@ let pr_universes prl g = let dump_universes output g = let dump_arc u = function - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in 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/univ.ml b/kernel/univ.ml index 311477daca..61ad1d0a82 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -86,7 +86,7 @@ struct | Level (n,d) as x -> let d' = Names.DirPath.hcons d in if d' == d then x else Level (n,d') - | Var n as x -> x + | Var _n as x -> x open Hashset.Combine @@ -160,13 +160,6 @@ module Level = struct let compare u v = if u == v then 0 - else - let c = Int.compare (hash u) (hash v) in - if c == 0 then RawLevel.compare (data u) (data v) - else c - - let natural_compare u v = - if u == v then 0 else RawLevel.compare (data u) (data v) let to_string x = @@ -206,13 +199,13 @@ module LMap = struct include M let union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some _, _ -> l | _, _ -> r) l r let subst_union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some (Some _), _ -> l | Some None, None -> l @@ -365,14 +358,14 @@ struct else f v ++ str"+" ++ int n let is_level = function - | (v, 0) -> true + | (_v, 0) -> true | _ -> false let level = function | (v,0) -> Some v | _ -> None - let get_level (v,n) = v + let get_level (v,_n) = v let map f (v, n as x) = let v' = f v in @@ -582,7 +575,7 @@ struct prl u2 ++ fnl () ) c (str "") let universes_of c = - fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty + fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end let universes_of_constraints = Constraint.universes_of @@ -907,7 +900,7 @@ let subst_instance_constraints s csts = type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t -let out_punivs (x, y) = x +let out_punivs (x, _y) = x let in_punivs x = (x, Instance.empty) let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' @@ -932,8 +925,8 @@ struct let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) - let instance (univs, cst) = univs - let constraints (univs, cst) = cst + let instance (univs, _cst) = univs + let constraints (_univs, cst) = cst let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' @@ -952,7 +945,9 @@ struct include UContext let repr (inst, cst) = - (Array.mapi (fun i l -> Level.var i) inst, cst) + (Array.mapi (fun i _l -> Level.var i) inst, cst) + + let pr f ?variance ctx = pr f ?variance (repr ctx) let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); @@ -988,8 +983,8 @@ struct let hcons (univs, variance) = (* should variance be hconsed? *) (UContext.hcons univs, variance) - let univ_context (univs, subtypcst) = univs - let variance (univs, variance) = variance + let univ_context (univs, _subtypcst) = univs + let variance (_univs, variance) = variance (** This function takes a universe context representing constraints of an inductive and produces a CumulativityInfo.t with the @@ -1054,7 +1049,7 @@ struct (univs, cst) let sort_levels a = - Array.sort Level.natural_compare a; a + Array.sort Level.compare a; a let to_context (ctx, cst) = (Instance.of_array (sort_levels (Array.of_list (LSet.elements ctx))), cst) @@ -1066,8 +1061,8 @@ struct if is_empty ctx then mt() else h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) - let constraints (univs, cst) = cst - let levels (univs, cst) = univs + let constraints (_univs, cst) = cst + let levels (univs, _cst) = univs let size (univs,_) = LSet.cardinal univs end @@ -1155,7 +1150,7 @@ let make_inverse_instance_subst i = LMap.empty arr let make_abstract_instance (ctx, _) = - Array.mapi (fun i l -> Level.var i) ctx + Array.mapi (fun i _l -> Level.var i) ctx let abstract_universes ctx = let instance = UContext.instance ctx in diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f588a6302..9d5d79124b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -66,7 +66,7 @@ let isMeta c = match Constr.kind c with let noccur_with_meta n m term = let rec occur_rec n c = match Constr.kind c with | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur - | Constr.App(f,cl) -> + | Constr.App(f,_cl) -> (match Constr.kind f with | Constr.Cast (c,_,_) when isMeta c -> () | Constr.Meta _ -> () @@ -188,7 +188,7 @@ let adjust_rel_to_rel_context sign n = let open RelDecl in match sign with | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) - | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | LocalDef (_,_c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) | [] -> (0,n) in snd (aux sign) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index d19bea5199..5965853e1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -11,7 +11,7 @@ open Csymtable let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2) - | Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2) + | Zfix(_f1,args1), Zfix(_f2,args2) -> Int.equal (nargs args1) (nargs args2) | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false @@ -84,7 +84,7 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ((mi,i) as ind1) , Aind ind2 -> + | Aind ((mi,_i) as ind1) , Aind ind2 -> if eq_ind ind1 ind2 && compare_stack stk1 stk2 then if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in diff --git a/kernel/vm.ml b/kernel/vm.ml index d7eedc226c..eaf64ba4af 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" @@ -188,5 +187,5 @@ let apply_whd k whd = interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v - | Vuniv_level lvl -> assert false + | Vuniv_level _lvl -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index d6d9312938..217ef4b8e5 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 @@ -132,7 +245,7 @@ type id_key = | RelKey of Int.t | EvarKey of Evar.t -let eq_id_key k1 k2 = match k1, k2 with +let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 @@ -191,9 +304,9 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" + | Vconstr_const _i -> str "Vconstr_const" + | Vconstr_block _b -> str "Vconstr_block" + | Vatom_stk (_a,_stk) -> str "Vatom_stk" | _ -> assert false in CErrors.anomaly @@ -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); @@ -327,7 +444,7 @@ struct type t = id_key let equal = eq_id_key open Hashset.Combine - let hash = function + let hash : t -> tag = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) @@ -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))) @@ -541,7 +658,7 @@ and pr_whd w = | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" + | Vconstr_block _b -> str "Vconstr_block" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = @@ -551,6 +668,6 @@ and pr_stack stk = and pr_zipper z = Pp.(match z with | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" + | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch _s -> str "Zswitch(...)" | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") 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 |