diff options
Diffstat (limited to 'kernel')
59 files changed, 1910 insertions, 470 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 306643f758..814cdfe1d8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -75,6 +75,8 @@ void init_arity () { arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= + arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]= + arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]= arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 7588c1ce07..9921208e04 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -22,6 +22,7 @@ #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> +#include <caml/callback.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -111,7 +112,8 @@ if (sp - num_args < coq_stack_threshold) { \ /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } - +#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } +#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } /* Register optimization. Some compilers underestimate the use of the local variables representing @@ -1771,6 +1773,71 @@ value coq_interprete Next; } + + Instruct(ISINT_CAML_CALL2) { + value arg; + print_instr("ISINT_CAML_CALL2"); + if (Is_uint63(accu)) { + pc++; + print_int(*pc); + arg = sp[0]; + Setup_for_caml_call; + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; + } + + Instruct(ISARRAY_CAML_CALL1) { + print_instr("ISARRAY_CAML_CALL1"); + if (Is_coq_array(accu)) { + pc++; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback(Field(coq_global_data, *pc),accu); + Restore_after_caml_call; + pc++; + } + else pc += *pc; + Next; + } + + Instruct(ISARRAY_INT_CAML_CALL2) { + value arg; + print_instr("ISARRAY_INT_CAML_CALL2"); + if (Is_coq_array(accu) && Is_uint63(sp[0])) { + pc++; + arg = sp[0]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; + } + + Instruct(ISARRAY_INT_CAML_CALL3) { + value arg1; + value arg2; + print_instr("ISARRAY_INT_CAML_CALL3"); + if (Is_coq_array(accu) && Is_uint63(sp[0])) { + pc++; + arg1 = sp[0]; + arg2 = sp[1]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2); + Restore_after_caml_call; + sp += 2; + pc++; + } else pc += *pc; + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index b027673ac7..86ae6295fd 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -33,6 +33,9 @@ #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) +/* coq array */ +#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) + /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index de02882370..a23ef8fdca 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -343,16 +343,20 @@ and fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t | FFloat of Float64.t + | FArray of Univ.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED +and finvert = Univ.Instance.t * fconstr array + let fterm_of v = v.term let set_norm v = v.mark <- Mark.set_norm v.mark let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false @@ -375,16 +379,30 @@ type infos_cache = { i_env : env; i_sigma : existential -> constr option; i_share : bool; + i_univs : UGraph.t; } type clos_infos = { i_flags : reds; + i_relevances : Sorts.relevance Range.t; i_cache : infos_cache } type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env +let info_univs info = info.i_cache.i_univs + +let push_relevance infos r = + { infos with i_relevances = Range.cons r.Context.binder_relevance infos.i_relevances } + +let push_relevances infos nas = + { infos with i_relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) + infos.i_relevances nas } + +let set_info_relevances info r = { info with i_relevances = r } + +let info_relevances info = info.i_relevances (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) @@ -438,8 +456,8 @@ let rec lft_fconstr n ft = {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ - | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)} + | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FCaseInvert _ | FProd _ + | FLetIn _ | FEvar _ | FCLOS _ | FArray _ -> {mark=ft.mark; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -501,11 +519,13 @@ let mk_clos e t = | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } | Int i -> {mark = mark Cstr Unknown; term = FInt i} | Float f -> {mark = mark Cstr Unknown; term = FFloat f} - | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _|Array _) -> {mark = mark Red Unknown; term = FCLOS(t,e)} let inject c = mk_clos (subs_id 0) c +(************************************************************************) + (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) let mk_clos_vect env v = match v with @@ -541,7 +561,7 @@ let ref_value_cache ({ i_cache = cache; _ }) tab ref = in Def (inject body) with - | NotEvaluableConst (IsPrimitive op) (* Const *) -> Primitive op + | NotEvaluableConst (IsPrimitive (_u,op)) (* Const *) -> Primitive op | Not_found (* List.assoc *) | NotEvaluableConst _ (* Const *) -> Undef None @@ -558,14 +578,10 @@ let rec to_constr lfts v = | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op - | FCaseT (ci,p,c,ve,env) -> - if is_subs_id env && is_lift_id lfts then - mkCase (ci, p, to_constr lfts c, ve) - else - let subs = comp_subs lfts env in - mkCase (ci, subst_constr subs p, - to_constr lfts c, - Array.map (fun b -> subst_constr subs b) ve) + | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env + | FCaseInvert (ci,p,(univs,args),c,ve,env) -> + let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in + to_constr_case lfts ci p iv c ve env | FFix ((op,(lna,tys,bds)) as fx, e) -> if is_subs_id e && is_lift_id lfts then mkFix fx @@ -613,7 +629,7 @@ let rec to_constr lfts v = subst_constr subs f) | FEvar ((ev,args),env) -> let subs = comp_subs lfts env in - mkEvar(ev,List.map (fun a -> subst_constr subs a) args) + mkEvar(ev, List.map (fun a -> subst_constr subs a) args) | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FInt i -> @@ -621,6 +637,11 @@ let rec to_constr lfts v = | FFloat f -> Constr.mkFloat f + | FArray (u,t,ty) -> + let ty = to_constr lfts ty in + let init i = to_constr lfts (Parray.get t (Uint63.of_int i)) in + mkArray(u,Array.init (Parray.length_int t) init, to_constr lfts (Parray.default t),ty) + | FCLOS (t,env) -> if is_subs_id env && is_lift_id lfts then t else @@ -628,6 +649,15 @@ let rec to_constr lfts v = subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and to_constr_case lfts ci p iv c ve env = + if is_subs_id env && is_lift_id lfts then + mkCase (ci, p, iv, to_constr lfts c, ve) + else + let subs = comp_subs lfts env in + mkCase (ci, subst_constr subs p, iv, + to_constr lfts c, + Array.map (fun b -> subst_constr subs b) ve) + and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with | Rel i -> begin match expand_rel i subst with @@ -909,54 +939,6 @@ let unfold_projection info p = Some (Zproj (Projection.repr p)) else None -(*********************************************************************) -(* A machine that inspects the head of a term until it finds an - atom or a subterm that may produce a redex (abstraction, - constructor, cofix, letin, constant), or a neutral term (product, - inductive) *) -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 info m stk) - | FLOCKED -> assert false - | 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') - | (None, stk') -> (m,stk')) - | FProj (p,c) -> - (match unfold_projection info p with - | None -> (m, stk) - | Some s -> knh info c (s :: zupdate info m stk)) - -(* cases where knh stops *) - | (FFlex _|FLetIn _|FConstruct _|FEvar _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) -> - (m, stk) - -(* The same for pure terms *) -and knht info e t stk = - match kind t with - | App(a,b) -> - 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 fx -> knh info { mark = mark Cstr Unknown; 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 { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk - | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk) - | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk - | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk - | Prod (n, t, c) -> - { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk - | LetIn (n,b,t,c) -> - { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk - | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk - -let inject c = mk_clos (subs_id 0) c - (************************************************************************) (* Reduction of Native operators *) @@ -967,6 +949,7 @@ module FNativeEntries = type elem = fconstr type args = fconstr array type evd = unit + type uinstance = Univ.Instance.t let get = Array.get @@ -980,6 +963,11 @@ module FNativeEntries = | FFloat f -> f | _ -> raise Primred.NativeDestKO + let get_parray () e = + match [@ocaml.warning "-4"] e.term with + | FArray (_u,t,_ty) -> t + | _ -> raise Not_found + let dummy = {mark = mark Norm KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty @@ -1108,6 +1096,17 @@ module FNativeEntries = frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } | None -> defined_refl := false + let defined_array = ref false + + let farray = ref dummy + + let init_array retro = + match retro.Retroknowledge.retro_array with + | Some c -> + defined_array := true; + farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + | None -> defined_array := false + let init env = current_retro := env.retroknowledge; init_int !current_retro; @@ -1118,7 +1117,8 @@ module FNativeEntries = init_cmp !current_retro; init_f_cmp !current_retro; init_f_class !current_retro; - init_refl !current_retro + init_refl !current_retro; + init_array !current_retro let check_env env = if not (!current_retro == env.retroknowledge) then init env @@ -1155,6 +1155,10 @@ module FNativeEntries = check_env env; assert (!defined_f_class) + let check_array env = + check_env env; + assert (!defined_array) + let mkInt env i = check_int env; { mark = mark Cstr KnownR; term = FInt i } @@ -1244,12 +1248,76 @@ module FNativeEntries = let mkNaN env = check_f_class env; !fNaN + + let mkArray env u t ty = + check_array env; + { mark = mark Whnf KnownR; term = FArray (u,t,ty)} + end module FredNative = RedNative(FNativeEntries) +(*********************************************************************) +(* A machine that inspects the head of a term until it finds an + atom or a subterm that may produce a redex (abstraction, + constructor, cofix, letin, constant), or a neutral term (product, + inductive) *) +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 info m stk) + | FLOCKED -> assert false + | 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') + | (None, stk') -> (m,stk')) + | FProj (p,c) -> + (match unfold_projection info p with + | None -> (m, stk) + | Some s -> knh info c (s :: zupdate info m stk)) + +(* cases where knh stops *) + | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _| + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _|FArray _) -> + (m, stk) + +(* The same for pure terms *) +and knht info e t stk = + match kind t with + | App(a,b) -> + knht info e a (append_stack (mk_clos_vect e b) stk) + | Case(ci,p,NoInvert,t,br) -> + knht info e t (ZcaseT(ci, p, br, e)::stk) + | Case(ci,p,CaseInvert{univs;args},t,br) -> + let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in + { mark = mark Red Unknown; term }, stk + | Fix fx -> knh info { mark = mark Cstr Unknown; 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 { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk) + | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk + | LetIn (n,b,t,c) -> + { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk + | Array(u,t,def,ty) -> + let len = Array.length t in + let ty = mk_clos e ty in + let t = Parray.init (Uint63.of_int len) (fun i -> mk_clos e t.(i)) (mk_clos e def) in + let term = FArray (u,t,ty) in + knh info { mark = mark Cstr Unknown; term } stk + (************************************************************************) +let conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) ref + = ref (fun _ _ _ _ -> (assert false : bool)) +let set_conv f = conv := f + (* Computes a weak head normal form from the result of knh. *) let rec knr info tab m stk = match m.term with @@ -1257,7 +1325,7 @@ let rec knr info tab m stk = (match get_args n tys f e stk with Inl e', s -> knit info tab e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) -> + | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with | Def v -> kni info tab v stk | Primitive op when check_native_args op stk -> @@ -1306,15 +1374,16 @@ let rec knr info tab m stk = (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FInt _ | FFloat _ -> + | FInt _ | FFloat _ | FArray _ -> (match [@ocaml.warning "-4"] strip_update_shift_app m stk with - | (_, _, Zprimitive(op,c,rargs,nargs)::s) -> + | (_, _, Zprimitive(op,(_,u as c),rargs,nargs)::s) -> let (rargs, nargs) = skip_native_args (m::rargs) nargs in begin match nargs with | [] -> let args = Array.of_list (List.rev rargs) in - begin match FredNative.red_prim (info_env info) () op args with - | Some m -> kni info tab m s + begin match FredNative.red_prim (info_env info) () op u args with + | Some m -> + kni info tab m s | None -> let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in @@ -1325,8 +1394,13 @@ let rec knr info tab m stk = kni info tab a (Zprimitive(op,c,rargs,nargs)::s) end | (_, _, s) -> (m, s)) + | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH -> + begin match case_inversion info tab ci iv v with + | Some c -> knit info tab env c stk + | None -> (m, stk) + end | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ - | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ + | FFix _ | FCoFix _ | FCaseT _ | FCaseInvert _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -1338,6 +1412,28 @@ and knit info tab e t stk = let (ht,s) = knht info e t stk in knr info tab ht s +and case_inversion info tab ci (univs,args) v = + let open Declarations in + if Array.is_empty args then Some v.(0) + else + let env = info_env info in + let ind = ci.ci_ind in + let params, indices = Array.chop ci.ci_npar args in + let psubst = subs_cons (params, subs_id 0) in + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + (* indtyping enforces 1 ctor with no letins in the context *) + let _, expect = mip.mind_nf_lc.(0) in + let _ind, expect_args = destApp expect in + let check_index i index = + let expected = expect_args.(ci.ci_npar + i) in + let expected = Vars.subst_instance_constr univs expected in + let expected = mk_clos psubst expected in + !conv {info with i_flags=all} tab expected index + in + if Array.for_all_i check_index 0 indices + then Some v.(0) else None + let kh info tab v stk = fapp_stack(kni info tab v stk) (************************************************************************) @@ -1348,7 +1444,7 @@ let rec zip_term zfun m stk = | Zapp args :: s -> zip_term zfun (mkApp(m, Array.map zfun args)) s | ZcaseT(ci,p,br,e)::s -> - let t = mkCase(ci, zfun (mk_clos e p), m, + let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m, Array.map (fun b -> zfun (mk_clos e b)) br) in zip_term zfun t s | Zproj p::s -> @@ -1388,31 +1484,35 @@ and norm_head info tab m = | FLambda(_n,tys,f,e) -> let (e',info,rvtys) = List.fold_left (fun (e,info,ctxt) (na,ty) -> + let info = push_relevance info na in (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt)) (e,info,[]) tys in let bd = kl info tab (mk_clos e' f) in List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in - mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) + mkLetIn(na, kl info tab a, kl info tab b, kl (push_relevance info na) tab c) | FProd(na,dom,rng,e) -> - mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng)) + mkProd(na, kl info tab dom, kl (push_relevance info na) tab (mk_clos (subs_lift e) rng)) | FCoFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) + let infobd = push_relevances info na in + mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds)) | FFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) + let infobd = push_relevances info na in + mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds)) | FEvar((i,args),env) -> mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args) | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ - | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ + | FFloat _ | FArray _ -> term_of_fconstr m (* Initialization and then normalization *) @@ -1434,14 +1534,16 @@ let whd_stack infos tab m stk = match Mark.red_state m.mark with let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k -let create_clos_infos ?(evars=fun _ -> None) flgs env = +let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env = + let univs = Option.default (universes env) univs in let share = (Environ.typing_flags env).Declarations.share_reduction in let cache = { i_env = env; i_sigma = evars; i_share = share; + i_univs = univs; } in - { i_flags = flgs; i_cache = cache } + { i_flags = flgs; i_relevances = Range.empty; i_cache = cache } let create_tab () = KeyTable.create 17 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 79092813bc..ada0fc9780 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -95,10 +95,11 @@ module KeyTable : Hashtbl.S with type key = table_key (** [fconstr] is the type of frozen constr *) type fconstr - (** [fconstr] can be accessed by using the function [fterm_of] and by matching on type [fterm] *) +type finvert + type fterm = | FRel of int | FAtom of constr (** Metas and Sorts *) @@ -110,12 +111,14 @@ type fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t | FFloat of Float64.t + | FArray of Univ.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -173,15 +176,22 @@ val set_relevance : Sorts.relevance -> fconstr -> unit type clos_infos type clos_tab val create_clos_infos : - ?evars:(existential->constr option) -> reds -> env -> clos_infos + ?univs:UGraph.t -> ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle val create_tab : unit -> clos_tab val info_env : clos_infos -> env val info_flags: clos_infos -> reds +val info_univs : clos_infos -> UGraph.t val unfold_projection : clos_infos -> Projection.t -> stack_member option +val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos +val push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos +val set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos + +val info_relevances : clos_infos -> Sorts.relevance Range.t + val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) @@ -214,6 +224,9 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def +(** Hook for Reduction *) +val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit + (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index c4036e9677..314cb54d1d 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Univ + type t = | Int63head0 | Int63tail0 @@ -51,6 +53,13 @@ type t = | Float64ldshiftexp | Float64next_up | Float64next_down + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength let parse = function | "int63_head0" -> Int63head0 @@ -95,6 +104,13 @@ let parse = function | "float64_ldshiftexp" -> Float64ldshiftexp | "float64_next_up" -> Float64next_up | "float64_next_down" -> Float64next_down + | "array_make" -> Arraymake + | "array_get" -> Arrayget + | "array_default" -> Arraydefault + | "array_set" -> Arrayset + | "array_length" -> Arraylength + | "array_copy" -> Arraycopy + | "array_reroot" -> Arrayreroot | _ -> raise Not_found let equal (p1 : t) (p2 : t) = @@ -143,6 +159,13 @@ let hash = function | Float64eq -> 40 | Float64lt -> 41 | Float64le -> 42 + | Arraymake -> 43 + | Arrayget -> 44 + | Arraydefault -> 45 + | Arrayset -> 46 + | Arraycopy -> 47 + | Arrayreroot -> 48 + | Arraylength -> 49 (* Should match names in nativevalues.ml *) let to_string = function @@ -188,28 +211,66 @@ let to_string = function | Float64ldshiftexp -> "ldshiftexp" | Float64next_up -> "next_up" | Float64next_down -> "next_down" + | Arraymake -> "arraymake" + | Arrayget -> "arrayget" + | Arraydefault -> "arraydefault" + | Arrayset -> "arrayset" + | Arraycopy -> "arraycopy" + | Arrayreroot -> "arrayreroot" + | Arraylength -> "arraylength" + +type const = + | Arraymaxlength -type prim_type = - | PT_int63 - | PT_float64 +let const_to_string = function + | Arraymaxlength -> "arraymaxlength" + +let const_of_string = function + | "array_max_length" -> Arraymaxlength + | _ -> raise Not_found -type 'a prim_ind = +let const_univs = function + | Arraymaxlength -> AUContext.empty + +type 'a prim_type = + | PT_int63 : unit prim_type + | PT_float64 : unit prim_type + | PT_array : (Instance.t * ind_or_type) prim_type + +and 'a prim_ind = | PIT_bool : unit prim_ind - | PIT_carry : prim_type prim_ind - | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_carry : ind_or_type prim_ind + | PIT_pair : (ind_or_type * ind_or_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind | PIT_f_class : unit prim_ind -type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex - -type ind_or_type = +and ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type - | PITT_type : prim_type -> ind_or_type + | PITT_type : 'a prim_type * 'a -> ind_or_type + | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *) + +let one_univ = + AUContext.make Names.[|Name (Id.of_string "u")|] Constraint.empty + +let typ_univs (type a) (t : a prim_type) = match t with + | PT_int63 -> AUContext.empty + | PT_float64 -> AUContext.empty + | PT_array -> one_univ + +type prim_type_ex = PTE : 'a prim_type -> prim_type_ex + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex let types = - let int_ty = PITT_type PT_int63 in - let float_ty = PITT_type PT_float64 in + let int_ty = PITT_type (PT_int63, ()) in + let float_ty = PITT_type (PT_float64, ()) in + let array_ty = + PITT_type + (PT_array, + (Instance.of_array [|Level.var 0|], + PITT_param 1)) + in function | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul @@ -217,25 +278,144 @@ let types = | Int63lsr | Int63lsl | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> - [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)] + [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] | Int63mulc | Int63diveucl -> - [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] | Int63div21 -> - [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] | Float64opp | Float64abs | Float64sqrt | Float64next_up | Float64next_down -> [float_ty; float_ty] | Float64ofInt63 -> [int_ty; float_ty] | Float64normfr_mantissa -> [float_ty; int_ty] - | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))] + | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))] | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())] | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())] | Float64add | Float64sub | Float64mul | Float64div -> [float_ty; float_ty; float_ty] | Float64ldshiftexp -> [float_ty; int_ty; float_ty] + | Arraymake -> [int_ty; PITT_param 1; array_ty] + | Arrayget -> [array_ty; int_ty; PITT_param 1] + | Arraydefault -> [array_ty; PITT_param 1] + | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] + | Arraycopy -> [array_ty; array_ty] + | Arrayreroot -> [array_ty; array_ty] + | Arraylength -> [array_ty; int_ty] + +let one_param = + (* currently if there's a parameter it's always this *) + let a_annot = Context.nameR (Names.Id.of_string "A") in + let ty = Constr.mkType (Universe.make (Level.var 0)) in + Context.Rel.Declaration.[LocalAssum (a_annot, ty)] + +let params = function + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down -> [] + + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> one_param + +let nparams x = List.length (params x) + +let univs = function + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down -> AUContext.empty + + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> one_univ type arg_kind = | Kparam (* not needed for the evaluation of the primitive when it reduces *) @@ -247,17 +427,21 @@ type args_red = arg_kind list (* Invariant only argument of type int63, float or an inductive can have kind Kwhnf *) -let arity t = List.length (types t) - 1 +let arity t = let sign = types t in nparams t + List.length sign - 1 let kind t = - let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in - aux (arity t) + let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in + let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in + params (nparams t) @ List.map args (CList.drop_last (types t)) + +let types t = params t, types t (** Special Entries for Register **) type op_or_type = | OT_op of t - | OT_type of prim_type + | OT_type : 'a prim_type -> op_or_type + | OT_const of const let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_bool -> "bool" @@ -267,24 +451,40 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_f_cmp -> "f_cmp" | PIT_f_class -> "f_class" -let prim_type_to_string = function +let prim_type_to_string (type a) (ty : a prim_type) = match ty with | PT_int63 -> "int63_type" | PT_float64 -> "float64_type" + | PT_array -> "array_type" let op_or_type_to_string = function | OT_op op -> to_string op | OT_type t -> prim_type_to_string t + | OT_const c -> const_to_string c let prim_type_of_string = function - | "int63_type" -> PT_int63 - | "float64_type" -> PT_float64 + | "int63_type" -> PTE PT_int63 + | "float64_type" -> PTE PT_float64 + | "array_type" -> PTE PT_array | _ -> raise Not_found let op_or_type_of_string s = - try OT_type (prim_type_of_string s) - with Not_found -> OT_op (parse s) + match prim_type_of_string s with + | PTE ty -> OT_type ty + | exception Not_found -> + begin try OT_op (parse s) + with Not_found -> OT_const (const_of_string s) + end let parse_op_or_type ?loc s = try op_or_type_of_string s with Not_found -> CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist.")) + +let op_or_type_univs = function + | OT_op t -> univs t + | OT_type t -> typ_univs t + | OT_const c -> const_univs c + +let body_of_prim_const = function + | Arraymaxlength -> + Constr.mkInt (Parray.max_length) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index a5db51111f..5e5fad9f04 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -51,6 +51,13 @@ type t = | Float64ldshiftexp | Float64next_up | Float64next_down + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength (** Can raise [Not_found]. Beware that this is not exactly the reverse of [to_string] below. *) @@ -58,8 +65,11 @@ val parse : string -> t val equal : t -> t -> bool +type const = + | Arraymaxlength + type arg_kind = - | Kparam (* not needed for the elavuation of the primitive*) + | Kparam (* not needed for the evaluation of the primitive*) | Kwhnf (* need to be reduced in whnf before reducing the primitive *) | Karg (* no need to be reduced in whnf *) @@ -70,32 +80,49 @@ val hash : t -> int val to_string : t -> string val arity : t -> int +(** Including parameters *) + +val nparams : t -> int val kind : t -> args_red +(** Includes parameters *) (** Special Entries for Register **) -type prim_type = - | PT_int63 - | PT_float64 - -(** Can raise [Not_found] *) -val prim_type_of_string : string -> prim_type -val prim_type_to_string : prim_type -> string +type 'a prim_type = + | PT_int63 : unit prim_type + | PT_float64 : unit prim_type + | PT_array : (Univ.Instance.t * ind_or_type) prim_type -type 'a prim_ind = +and 'a prim_ind = | PIT_bool : unit prim_ind - | PIT_carry : prim_type prim_ind - | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_carry : ind_or_type prim_ind + | PIT_pair : (ind_or_type * ind_or_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind | PIT_f_class : unit prim_ind +and ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : 'a prim_type * 'a -> ind_or_type + | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *) + +val typ_univs : 'a prim_type -> Univ.AUContext.t + +type prim_type_ex = PTE : 'a prim_type -> prim_type_ex + type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex +(** Can raise [Not_found] *) +val prim_type_of_string : string -> prim_type_ex +val prim_type_to_string : 'a prim_type -> string + type op_or_type = | OT_op of t - | OT_type of prim_type + | OT_type : 'a prim_type -> op_or_type + | OT_const of const + +val op_or_type_univs : op_or_type -> Univ.AUContext.t val prim_ind_to_string : 'a prim_ind -> string @@ -105,8 +132,12 @@ val op_or_type_to_string : op_or_type -> string val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type -type ind_or_type = - | PITT_ind : 'a prim_ind * 'a -> ind_or_type - | PITT_type : prim_type -> ind_or_type +val univs : t -> Univ.AUContext.t + +val types : t -> Constr.rel_context * ind_or_type list +(** Parameters * Reduction relevant arguments and output type + + XXX we could reify universes in ind_or_type (currently polymorphic types + like array are assumed to use universe 0). *) -val types : t -> ind_or_type list +val body_of_prim_const : const -> Constr.t diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 25ec250367..74405a0105 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -61,6 +61,7 @@ type instruction = | Kensurestackcapacity of int | Kbranch of Label.t (* jump to label *) | Kprim of CPrimitives.t * pconstant option + | Kcamlprim of CPrimitives.t * Label.t | Kareint of int and bytecodes = instruction list @@ -147,6 +148,10 @@ let rec pp_instr i = | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ (match id with Some (id,_u) -> Constant.print id | None -> str "") + | Kcamlprim (op, lbl) -> + str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ + pp_lbl lbl + | Kareint n -> str "areint " ++ int n and pp_bytecodes c = diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f1d441ca76..b703058fb7 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -60,7 +60,7 @@ type instruction = | Kbranch of Label.t (** jump to label, is it needed ? *) | Kprim of CPrimitives.t * pconstant option - + | Kcamlprim of CPrimitives.t * Label.t | Kareint of int and bytecodes = instruction list diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 59ae8c0745..7bff377238 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -516,6 +516,18 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> kn) +(* Some primitives are not implemented natively by the VM, but calling OCaml + code instead *) +let is_caml_prim = let open CPrimitives in function + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> true + | _ -> false + (* sz is the size of the local stack *) let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; @@ -775,6 +787,27 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont + | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + let arity = CPrimitives.arity op in + let nparams = CPrimitives.nparams op in + let nargs = arity - nparams in + assert (arity = Array.length args && arity <= 4); + let (jump, cont) = make_branch cont in + let lbl_default = Label.create () in + let default = + let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = + if Univ.Instance.is_empty u then cont + else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) + in + Klabel lbl_default :: + Kpush :: + if Int.equal nparams 0 then cont + else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) + in + fun_code := [Ksequence(default, !fun_code)]; + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + | Lprim (kn, op, args) -> comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d855dbf2bb..6b4daabf0c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -30,6 +30,7 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t | Reloc_proj_name of Projection.Repr.t + | Reloc_caml_prim of CPrimitives.t let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 @@ -40,6 +41,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_getglobal _, _ -> false | Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 | Reloc_proj_name _, _ -> false +| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 +| Reloc_caml_prim _, _ -> false let hash_reloc_info r = let open Hashset.Combine in @@ -48,6 +51,7 @@ let hash_reloc_info r = | Reloc_const c -> combinesmall 2 (hash_structured_constant c) | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) + | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) module RelocTable = Hashtbl.Make(struct type t = reloc_info @@ -199,6 +203,10 @@ let slot_for_proj_name env p = enter env (Reloc_proj_name p); out_int env 0 +let slot_for_caml_prim env op = + enter env (Reloc_caml_prim op); + out_int env 0 + (* Emission of one instruction *) let nocheck_prim_op = function @@ -252,6 +260,11 @@ let check_prim_op = function | Float64ldshiftexp -> opCHECKLDSHIFTEXP | Float64next_up -> opCHECKNEXTUPFLOAT | Float64next_down -> opCHECKNEXTDOWNFLOAT + | Arraymake -> opISINT_CAML_CALL2 + | Arrayget -> opISARRAY_INT_CAML_CALL2 + | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> + opISARRAY_CAML_CALL1 let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -349,6 +362,11 @@ let emit_instr env = function out env (check_prim_op op); slot_for_getglobal env q + | Kcamlprim (op,lbl) -> + out env (check_prim_op op); + out_label env lbl; + slot_for_caml_prim env op + | Kareint 1 -> out env opISINT | Kareint 2 -> out env opAREINT2; @@ -415,6 +433,7 @@ let subst_reloc s ri = | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) + | Reloc_caml_prim _ -> ri let subst_patches subst p = let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 209d741ba8..c4262f3380 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -16,6 +16,7 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t | Reloc_proj_name of Projection.Repr.t + | Reloc_caml_prim of CPrimitives.t type patches type emitcodes diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 65de52c0f6..6690a379ce 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -542,6 +542,14 @@ let makeblock tag nparams arity args = Lval(val_of_block Obj.last_non_constant_constructor_tag args) else Lmakeblock(tag, args) +let makearray args def = + try + let p = Array.map get_value args in + Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def)) + with Not_found -> + let ar = Lmakeblock(0, args) in (* build the ocaml array *) + let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *) + Lmakeblock(0,[|kind|]) (* the reference *) (* Compiling constants *) @@ -568,8 +576,13 @@ let expand_prim kn op arity = let lambda_of_prim kn op args = let arity = CPrimitives.arity op in - if Array.length args >= arity then prim kn op args - else mkLapp (expand_prim kn op arity) args + match Int.compare (Array.length args) arity with + | 0 -> prim kn op args + | x when x > 0 -> + let prim_args = Array.sub args 0 arity in + let extra_args = Array.sub args arity (Array.length args - arity) in + mkLapp(prim kn op prim_args) extra_args + | _ -> mkLapp (expand_prim kn op arity) args (*i Global environment *) @@ -710,7 +723,7 @@ let rec lambda_of_constr env c = | Construct _ -> lambda_of_app env c empty_args - | Case(ci,t,a,branches) -> + | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env.global_env in let oib = mib.mind_packets.(snd ind) in @@ -768,6 +781,9 @@ let rec lambda_of_constr env c = | Int i -> Luint i | Float f -> Lfloat f + | Array(_u, t,def,_ty) -> + let def = lambda_of_constr env def in + makearray (lambda_of_args env 0 t) def and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/constr.ml b/kernel/constr.ml index 703e3616a0..1837a39764 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -83,6 +83,10 @@ type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses +type ('constr, 'univs) case_invert = + | NoInvert + | CaseInvert of { univs : 'univs; args : 'constr array } + (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) type ('constr, 'types, 'sort, 'univs) kind_of_term = @@ -99,12 +103,13 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array + | Case of case_info * 'constr * ('constr, 'univs) case_invert * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr | Int of Uint63.t | Float of Float64.t + | Array of 'univs * 'constr array * 'constr * 'types (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term @@ -189,7 +194,7 @@ let mkConstructU c = Construct c let mkConstructUi ((ind,u),i) = Construct ((ind,i),u) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) +let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac) (* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] @@ -242,6 +247,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with (* Constructs a primitive integer *) let mkInt i = Int i +(* Constructs an array *) +let mkArray (u,t,def,ty) = Array (u,t,def,ty) + (* Constructs a primitive float number *) let mkFloat f = Float f @@ -417,7 +425,7 @@ let destConstruct c = match kind c with (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) let destCase c = match kind c with - | Case (ci,p,c,v) -> (ci,p,c,v) + | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v) | _ -> raise DestKO let destProj c = match kind c with @@ -461,6 +469,11 @@ let decompose_appvect c = starting from [acc] and proceeding from left to right according to the usual representation of the constructions; it is not recursive *) +let fold_invert f acc = function + | NoInvert -> acc + | CaseInvert {univs=_;args} -> + Array.fold_left f acc args + let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> acc @@ -471,16 +484,23 @@ let fold f acc c = match kind c with | App (c,l) -> Array.fold_left f (f acc c) l | Proj (_p,c) -> f acc c | Evar (_,l) -> List.fold_left f acc l - | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl + | Array(_u,t,def,ty) -> + f (f (Array.fold_left f acc t) def) ty (* [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) +let iter_invert f = function + | NoInvert -> () + | CaseInvert {univs=_; args;} -> + Array.iter f args + let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> () @@ -491,9 +511,10 @@ let iter f c = match kind c with | App (c,l) -> f c; Array.iter f l | Proj (_p,c) -> f c | Evar (_,l) -> List.iter f l - | Case (_,p,c,bl) -> f p; f c; Array.iter f bl + | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl + | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty (* [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -510,7 +531,7 @@ let iter_with_binders g f n c = match kind c with | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> List.iter (fun c -> f n c) l - | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl + | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; @@ -518,6 +539,8 @@ let iter_with_binders g f n c = match kind c with | CoFix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl + | Array(_u,t,def,ty) -> + Array.iter (f n) t; f n def; f n ty (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -537,7 +560,7 @@ let fold_constr_with_binders g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_p,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl | Fix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in @@ -546,6 +569,8 @@ let fold_constr_with_binders g f n acc c = let n' = iterate g (Array.length tl) n 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 + | Array(_u,t,def,ty) -> + f n (f n (Array.fold_left (f n) acc t) def) ty (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -623,6 +648,13 @@ let map_branches_with_full_binders g f l ci 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_invert f = function + | NoInvert -> NoInvert + | CaseInvert {univs;args;} as orig -> + let args' = Array.Smart.map f args in + if args == args' then orig + else CaseInvert {univs;args=args';} + let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> c @@ -660,18 +692,20 @@ let map_gen userview f c = match kind c with let l' = List.Smart.map f l in if l'==l then c else mkEvar (e, l') - | Case (ci,p,b,bl) when userview -> + | Case (ci,p,iv,b,bl) when userview -> let b' = f b in + let iv' = map_invert f iv 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) -> + if b'==b && iv'==iv && p'==p && bl'==bl then c + else mkCase (ci, p', iv', b', bl') + | Case (ci,p,iv,b,bl) -> let b' = f b in + let iv' = map_invert f iv in let p' = f p in let bl' = Array.Smart.map f bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') + if b'==b && iv'==iv && p'==p && bl'==bl then c + else mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let tl' = Array.Smart.map f tl in let bl' = Array.Smart.map f bl in @@ -682,12 +716,25 @@ let map_gen userview f c = match kind c with let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.Smart.map f t in + let def' = f def in + let ty' = f ty in + if def'==def && t==t' && ty==ty' then c + else mkArray(u,t',def',ty') let map_user_view = map_gen true let map = map_gen false (* Like {!map} but with an accumulator. *) +let fold_map_invert f acc = function + | NoInvert -> acc, NoInvert + | CaseInvert {univs;args;} as orig -> + let acc, args' = Array.fold_left_map f acc args in + if args==args' then acc, orig + else acc, CaseInvert {univs;args=args';} + let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> accu, c @@ -726,12 +773,13 @@ let fold_map f accu c = match kind c with let accu, l' = List.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') - | Case (ci,p,b,bl) -> + | Case (ci,p,iv,b,bl) -> let accu, b' = f accu b in + let accu, iv' = fold_map_invert f accu iv in let accu, p' = f accu p in let accu, bl' = Array.Smart.fold_left_map f accu bl in - if b'==b && p'==p && bl'==bl then accu, c - else accu, mkCase (ci, p', b', bl') + if b'==b && iv'==iv && p'==p && bl'==bl then accu, c + else accu, mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let accu, tl' = Array.Smart.fold_left_map f accu tl in let accu, bl' = Array.Smart.fold_left_map f accu bl in @@ -742,6 +790,12 @@ let fold_map f accu c = match kind c with let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let accu, t' = Array.Smart.fold_left_map f accu t in + let accu, def' = f accu def in + let accu, ty' = f accu ty in + if def'==def && t==t' && ty==ty' then accu, c + else accu, mkArray(u,t',def',ty') (* [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -786,12 +840,13 @@ let map_with_binders g f l c0 = match kind c0 with let al' = List.Smart.map (fun c -> f l c) al in if al' == al then c0 else mkEvar (e, al') - | Case (ci, p, c, bl) -> + | Case (ci, p, iv, c, bl) -> let p' = f l p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = Array.Fun1.Smart.map f l bl in - if p' == p && c' == c && bl' == bl then c0 - else mkCase (ci, p', c', bl') + if p' == p && iv' == iv && c' == c && bl' == bl then c0 + else mkCase (ci, p', iv', c', bl') | Fix (ln, (lna, tl, bl)) -> let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in @@ -803,6 +858,12 @@ let map_with_binders g f l c0 = match kind c0 with let l' = iterate g (Array.length tl) l in let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.Fun1.Smart.map f l t in + let def' = f l def in + let ty' = f l ty in + if def'==def && t==t' && ty==ty' then c0 + else mkArray(u,t',def',ty') (*********************) (* Lifting *) @@ -836,7 +897,7 @@ let fold_with_full_binders g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl | Fix (_,(lna,tl,bl)) -> let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in @@ -845,9 +906,10 @@ let fold_with_full_binders g f n acc c = let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) 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 + | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty -type 'univs instance_compare_fn = GlobRef.t -> int -> +type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool @@ -863,6 +925,14 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) +let eq_invert eq leq_universes iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> true + | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false + | CaseInvert {univs;args}, CaseInvert iv2 -> + leq_universes univs iv2.univs + && Array.equal eq args iv2.args + let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) @@ -884,20 +954,24 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2 + Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2 - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 + eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 + | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> + eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 + | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) -> + leq_universes None u1 u2 && + Array.equal_norefl (eq 0) t1 t2 && + eq 0 def1 def2 && eq 0 ty1 ty2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ - | CoFix _ | Int _ | Float _), _ -> false + | CoFix _ | Int _ | Float _| Array _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -923,7 +997,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = let compare_head_gen eq_universes eq_sorts eq t1 t2 = compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 -let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal +let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal (*******************************) (* alpha conversion functions *) @@ -932,14 +1006,14 @@ let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal (* alpha conversion : ignore print names and casts *) let rec eq_constr nargs m n = - (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n + (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr nargs m n let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -948,7 +1022,7 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || @@ -965,7 +1039,7 @@ let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -985,7 +1059,7 @@ let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in + let eq_universes _ l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -1015,7 +1089,16 @@ let leq_constr_univs_infer univs m n = res, !cstrs let rec eq_constr_nounivs m n = - (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n + (m == n) || compare_head_gen (fun _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n + +let compare_invert f iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> 0 + | NoInvert, CaseInvert _ -> -1 + | CaseInvert _, NoInvert -> 1 + | CaseInvert iv1, CaseInvert iv2 -> + (* univs ignored deliberately *) + Array.compare f iv1.args iv2.args let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= @@ -1060,8 +1143,12 @@ let constr_ord_int f t1 t2 = | Ind _, _ -> -1 | _, Ind _ -> 1 | 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 + | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> + let c = f p1 p2 in + if Int.equal c 0 then let c = compare_invert f iv1 iv2 in + if Int.equal c 0 then let c = f c1 c2 in + if Int.equal c 0 then Array.compare f bl1 bl2 + else c else c else c | Case _, _ -> -1 | _, Case _ -> 1 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) @@ -1076,6 +1163,9 @@ let constr_ord_int f t1 t2 = | Int i1, Int i2 -> Uint63.compare i1 i2 | Int _, _ -> -1 | _, Int _ -> 1 | Float f1, Float f2 -> Float64.total_compare f1 f2 + | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) -> + (((Array.compare f) =? f) ==? f) t1 t2 def1 def2 ty1 ty2 + | Array _, _ -> -1 | _, Array _ -> 1 let rec compare m n= constr_ord_int compare m n @@ -1129,6 +1219,14 @@ let array_eqeq t1 t2 = (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) in aux 0) +let invert_eqeq iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> true + | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false + | CaseInvert iv1, CaseInvert iv2 -> + iv1.univs == iv2.univs + && iv1.args == iv2.args + let hasheq t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> n1 == n2 @@ -1146,8 +1244,8 @@ let hasheq t1 t2 = | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 - | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> - ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 + | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) -> + ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 @@ -1161,9 +1259,11 @@ let hasheq t1 t2 = && array_eqeq bl1 bl2 | Int i1, Int i2 -> i1 == i2 | Float f1, Float f2 -> Float64.equal f1 f2 + | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) -> + u1 == u2 && def1 == def2 && ty1 == ty2 && array_eqeq t1 t2 | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ - | Fix _ | CoFix _ | Int _ | Float _), _ -> false + | Fix _ | CoFix _ | Int _ | Float _ | Array _), _ -> false (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) @@ -1236,12 +1336,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let u', hu = sh_instance u in (Construct (sh_construct c, u'), combinesmall 11 (combine (constructor_syntactic_hash c) hu)) - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> let p, hp = sh_rec p + and iv, hiv = sh_invert iv and c, hc = sh_rec c in let bl,hbl = hash_term_array bl in - let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) + let hbl = combine4 hc hp hiv hbl in + (Case (sh_ci ci, p, iv, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in @@ -1270,6 +1371,20 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let (h,l) = Uint63.to_int2 i in (t, combinesmall 18 (combine h l)) | Float f -> (t, combinesmall 19 (Float64.hash f)) + | Array (u,t,def,ty) -> + let u, hu = sh_instance u in + let t, ht = hash_term_array t in + let def, hdef = sh_rec def in + let ty, hty = sh_rec ty in + let h = combine4 hu ht hdef hty in + (Array(u,t,def,ty), combinesmall 20 h) + + and sh_invert = function + | NoInvert -> NoInvert, 0 + | CaseInvert {univs;args;} -> + let univs, hu = sh_instance univs in + let args, ha = hash_term_array args in + CaseInvert {univs;args;}, combinesmall 1 (combine hu ha) and sh_rec t = let (y, h) = hash_term t in @@ -1332,8 +1447,8 @@ let rec hash t = combinesmall 10 (combine (ind_hash ind) (Instance.hash u)) | Construct (c,u) -> combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) - | Case (_ , p, c, bl) -> - combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) + | Case (_ , p, iv, c, bl) -> + combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) | CoFix(_ln, (_, tl, bl)) -> @@ -1344,6 +1459,13 @@ let rec hash t = combinesmall 17 (combine (Projection.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) + | Array(u,t,def,ty) -> + combinesmall 20 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty)) + +and hash_invert = function + | NoInvert -> 0 + | CaseInvert {univs;args;} -> + combinesmall 1 (combine (Instance.hash univs) (hash_term_array args)) and hash_term_array t = Array.fold_left (fun acc t -> combine acc (hash t)) 0 t @@ -1476,9 +1598,9 @@ let rec debug_print c = | Construct (((sp,i),j),u) -> str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")" - | Case (_ci,p,c,bl) -> v 0 + | Case (_ci,p,iv,c,bl) -> v 0 (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++ - debug_print c ++ str"of") ++ cut() ++ + debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++ prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++ cut() ++ str"end") | Fix f -> debug_print_fix debug_print f @@ -1492,3 +1614,12 @@ let rec debug_print c = str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" | Float i -> str"Float("++str (Float64.to_string i) ++ str")" + | Array(u,t,def,ty) -> str"Array(" ++ prlist_with_sep pr_comma debug_print (Array.to_list t) ++ str" | " + ++ debug_print def ++ str " : " ++ debug_print ty + ++ str")@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str"}" + +and debug_invert = let open Pp in function + | NoInvert -> mt() + | CaseInvert {univs;args;} -> + spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++ + str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} " diff --git a/kernel/constr.mli b/kernel/constr.mli index 00051d7551..62f2555a7e 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -49,6 +49,14 @@ type case_info = ci_pp_info : case_printing (* not interpreted by the kernel *) } +type ('constr, 'univs) case_invert = + | NoInvert + (** Normal reduction: match when the scrutinee is a constructor. *) + + | CaseInvert of { univs : 'univs; args : 'constr array; } + (** Reduce when the indices match those of the unique constructor. + (SProp to non SProp only) *) + (** {6 The type of constructions } *) type t @@ -76,6 +84,9 @@ val mkVar : Id.t -> constr (** Constructs a machine integer *) val mkInt : Uint63.t -> constr +(** Constructs an array *) +val mkArray : Univ.Instance.t * constr array * constr * types -> constr + (** Constructs a machine float number *) val mkFloat : Float64.t -> constr @@ -148,7 +159,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) -val mkCase : case_info * constr * constr * constr array -> constr +val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr (** If [recindxs = [|i1,...in|]] [funnames = [|f1,.....fn|]] @@ -232,12 +243,13 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) - | Case of case_info * 'constr * 'constr * 'constr array + | Case of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr | Int of Uint63.t | Float of Float64.t + | Array of 'univs * 'constr array * 'constr * 'types (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -339,7 +351,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args return P in t1], or [if c then t1 else t2]) @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * constr * constr array +val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array (** Destructs a projection *) val destProj : constr -> Projection.t * constr @@ -497,12 +509,16 @@ val fold_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b +val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) val map : (constr -> constr) -> constr -> constr +val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert + (** [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 @@ -514,6 +530,9 @@ val map_user_view : (constr -> constr) -> constr -> constr val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr +val fold_map_invert : ('a -> 'b -> 'a * 'b) -> + 'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert + (** [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at @@ -529,6 +548,8 @@ val map_with_binders : val iter : (constr -> unit) -> constr -> unit +val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit + (** [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at @@ -558,7 +579,7 @@ 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 'univs instance_compare_fn = GlobRef.t -> int -> +type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to @@ -605,6 +626,9 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> constr constr_compare_fn -> constr constr_compare_fn +val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool) + -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool + (** {6 Hashconsing} *) val hash : constr -> int diff --git a/kernel/cooking.ml b/kernel/cooking.ml index a17aff9b09..fdcf44c943 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -75,23 +75,30 @@ let share_univs cache r u l = let (u', args) = share cache r l in mkApp (instantiate_my_gr r (Instance.append u' u), args) -let update_case_info cache ci modlist = - try - let (_u,l) = share cache (IndRef ci.ci_ind) modlist in - { ci with ci_npar = ci.ci_npar + Array.length l } - with Not_found -> - ci +let update_case cache ci iv modlist = + match share cache (IndRef ci.ci_ind) modlist with + | exception Not_found -> ci, iv + | u, l -> + let iv = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs; args;} -> + let univs = Instance.append u univs in + let args = Array.append l args in + CaseInvert {univs; args;} + in + { ci with ci_npar = ci.ci_npar + Array.length l }, iv let is_empty_modlist (cm, mm) = Cmap.is_empty cm && Mindmap.is_empty mm let expmod_constr cache modlist c = let share_univs = share_univs cache in - let update_case_info = update_case_info cache in + let update_case = update_case cache in let rec substrec c = match kind c with - | Case (ci,p,t,br) -> - Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br)) + | Case (ci,p,iv,t,br) -> + let ci,iv = update_case ci iv modlist in + Constr.map substrec (mkCase (ci,p,iv,t,br)) | Ind (ind,u) -> (try diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index f41585e93a..185fb9f5a4 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -63,6 +63,15 @@ let set_global v = global_data.glob_len <- global_data.glob_len + 1; n +(* Initialization of OCaml primitives *) +let parray_make = set_global Vmvalues.parray_make +let parray_get = set_global Vmvalues.parray_get +let parray_get_default = set_global Vmvalues.parray_get_default +let parray_set = set_global Vmvalues.parray_set +let parray_copy = set_global Vmvalues.parray_copy +let parray_reroot = set_global Vmvalues.parray_reroot +let parray_length = set_global Vmvalues.parray_length + (* table pour les structured_constant et les annotations des switchs *) module SConstTable = Hashtbl.Make (struct @@ -119,6 +128,17 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n +let slot_for_caml_prim = + let open CPrimitives in function + | Arraymake -> parray_make + | Arrayget -> parray_get + | Arraydefault -> parray_get_default + | Arrayset -> parray_set + | Arraycopy -> parray_copy + | Arrayreroot -> parray_reroot + | Arraylength -> parray_length + | _ -> assert false + let slot_for_proj_name key = try ProjNameTable.find proj_name_tbl key with Not_found -> @@ -182,6 +202,7 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_const sc -> slot_for_str_cst sc | Reloc_getglobal kn -> slot_for_getglobal env kn | Reloc_proj_name p -> slot_for_proj_name p + | Reloc_caml_prim op -> slot_for_caml_prim op in let tc = patch buff pl slots in let vm_env = diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 2f6a870c8a..7609c1a64d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -55,7 +55,7 @@ type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) | OpaqueDef of 'opaque (** or an opaque global definition *) - | Primitive of CPrimitives.t (** or a primitive operation *) + | Primitive of CPrimitives.t (** or a primitive operation *) type universes = | Monomorphic of Univ.ContextSet.t @@ -94,6 +94,10 @@ type typing_flags = { cumulative_sprop : bool; (** SProp <= Type *) + + allow_uip: bool; + (** Allow definitional UIP (breaks termination) *) + } (* some contraints are in constant_constraints, some other may be in @@ -112,11 +116,14 @@ type 'opaque constant_body = { } (** {6 Representation of mutual inductive types in the kernel } *) +type nested_type = +| NestedInd of inductive +| NestedPrimitive of Constant.t type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive +| Norec +| Mrec of inductive +| Nested of nested_type type wf_paths = recarg Rtree.t diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0ab99cab35..326bf0d6ad 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -27,6 +27,7 @@ let safe_flags oracle = { enable_native_compiler = true; indices_matter = true; cumulative_sprop = false; + allow_uip = false; } (** {6 Arities } *) @@ -155,21 +156,47 @@ let hcons_const_body cb = } (** {6 Inductive types } *) +let eq_nested_type t1 t2 = match t1, t2 with +| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2 +| NestedInd _, _ -> false +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive _, _ -> false let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true +| Norec, _ -> false | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false +| Mrec _, _ -> false +| Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2 +| Nested _, _ -> false + +let pp_recarg = let open Pp in function + | Declarations.Norec -> str "Norec" + | Declarations.Mrec (mind,i) -> + str "Mrec[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]" + | Declarations.(Nested (NestedInd (mind,i))) -> + str "Nested[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]" + | Declarations.(Nested (NestedPrimitive c)) -> + str "Nested[" ++ Names.Constant.print c ++ str "]" + +let pp_wf_paths x = Rtree.pp_tree pp_recarg x + +let subst_nested_type sub ty = match ty with +| NestedInd (kn,i) -> + let kn' = subst_mind sub kn in + if kn==kn' then ty else NestedInd (kn',i) +| NestedPrimitive c -> + let c',_ = subst_con sub c in + if c==c' then ty else NestedPrimitive c' let subst_recarg sub r = match r with | Norec -> r | Mrec (kn,i) -> let kn' = subst_mind sub kn in if kn==kn' then r else Mrec (kn',i) - | Imbr (kn,i) -> - let kn' = subst_mind sub kn in - if kn==kn' then r else Imbr (kn',i) + | Nested ty -> + let ty' = subst_nested_type sub ty in + if ty==ty' then r else Nested ty' let mk_norec = Rtree.mk_node Norec [||] diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 01e4429e7e..4ab8d45e60 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -46,6 +46,9 @@ val is_opaque : 'a constant_body -> bool val eq_recarg : recarg -> recarg -> bool +val pp_recarg : recarg -> Pp.t +val pp_wf_paths : wf_paths -> Pp.t + val subst_recarg : substitution -> recarg -> recarg val mk_norec : wf_paths diff --git a/kernel/entries.ml b/kernel/entries.ml index e0b678621a..ae64112e33 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -91,8 +91,7 @@ type parameter_entry = Id.Set.t option * types in_universes_entry * inline type primitive_entry = { - prim_entry_type : types option; - prim_entry_univs : Univ.ContextSet.t; (* always monomorphic *) + prim_entry_type : types in_universes_entry option; prim_entry_content : CPrimitives.op_or_type; } diff --git a/kernel/environ.ml b/kernel/environ.ml index 182ed55d0e..e75ccbb252 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -449,6 +449,7 @@ let same_flags { enable_VM; enable_native_compiler; cumulative_sprop; + allow_uip; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,7 +459,8 @@ let same_flags { share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && enable_native_compiler == alt.enable_native_compiler && - cumulative_sprop == alt.cumulative_sprop + cumulative_sprop == alt.cumulative_sprop && + allow_uip == alt.allow_uip [@warning "+9"] let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b) @@ -501,7 +503,7 @@ let constant_type env (kn,u) = type const_evaluation_result = | NoBody | Opaque - | IsPrimitive of CPrimitives.t + | IsPrimitive of Univ.Instance.t * CPrimitives.t exception NotEvaluableConst of const_evaluation_result @@ -533,7 +535,7 @@ let constant_value_in env (kn,u) = subst_instance_constr u b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) - | Primitive p -> raise (NotEvaluableConst (IsPrimitive p)) + | Primitive p -> raise (NotEvaluableConst (IsPrimitive (u,p))) let constant_opt_value_in env cst = try Some (constant_value_in env cst) diff --git a/kernel/environ.mli b/kernel/environ.mli index f489b13a3b..5cb56a2a29 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -225,7 +225,7 @@ val type_in_type_constant : Constant.t -> env -> bool type const_evaluation_result = | NoBody | Opaque - | IsPrimitive of CPrimitives.t + | IsPrimitive of Univ.Instance.t * CPrimitives.t exception NotEvaluableConst of const_evaluation_result val constant_type : env -> Constant.t puniverses -> types constrained diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 0a9f137c45..67a672c349 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -157,6 +157,10 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; + "ISINT_CAML_CALL2"; + "ISARRAY_CAML_CALL1"; + "ISARRAY_INT_CAML_CALL2"; + "ISARRAY_INT_CAML_CALL3"; "STOP" |] diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index e9687991c0..179353d3f0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -134,11 +134,18 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = (* Empty type: all OK *) | 0 -> univ_info - (* SProp primitive records are OK, if we squash and become fakerecord also OK *) - | 1 when isrecord -> univ_info - - (* Unit and identity types must squash if SProp *) - | 1 -> check_univ_leq env_ar_par Univ.Universe.type0m univ_info + | 1 -> + (* SProp primitive records are OK, if we squash and become fakerecord also OK *) + if isrecord then univ_info + (* 1 constructor with no arguments also OK in SProp (to make + things easier on ourselves when reducing we forbid letins) *) + else if (Environ.typing_flags env_ar_par).allow_uip + && fst (splayed_lc.(0)) = [] + && List.for_all Context.Rel.Declaration.is_local_assum params + then univ_info + (* 1 constructor with arguments must squash if SProp + (we could allow arguments in SProp but the reduction rule is a pain) *) + else check_univ_leq env_ar_par Univ.Universe.type0m univ_info (* More than 1 constructor: must squash if Prop/SProp *) | _ -> check_univ_leq env_ar_par Univ.Universe.type0 univ_info diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9da6c7842e..a27ff41a1c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -165,7 +165,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in push_rel decl env in let ra_env' = - (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: + (Nested (NestedInd mi),(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in (* New index of the inductive types *) let newidx = n + auxntyp in @@ -241,6 +241,9 @@ 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) + | Const (c,_) when is_primitive_positive_container env c -> + if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) + else check_positive_nested_primitive ienv nmr (c, largs) | _err -> (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives @@ -298,7 +301,16 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr in - (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) + (nmr',(Rtree.mk_rec [|mk_paths (Nested (NestedInd mi)) irecargs|]).(0)) + + and check_positive_nested_primitive (env,n,ntypes,ra_env) nmr (c, largs) = + (* We model the primitive type c X1 ... Xn as if it had one constructor + C : X1 -> ... -> Xn -> c X1 ... Xn + The subterm relation is defined for each primitive in `inductive.ml`. *) + let ra_env = List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + let ienv = (env,n,ntypes,ra_env) in + let nmr',recargs = List.fold_left_map (check_pos ienv) nmr largs in + (nmr', (Rtree.mk_rec [| mk_paths (Nested (NestedPrimitive c)) [| recargs |] |]).(0)) (** [check_constructors ienv check_head nmr c] checks the positivity condition in the type [c] of a constructor (i.e. that recursive diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8423813639..d751d9875a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -464,11 +464,16 @@ let eq_wf_paths = Rtree.equal Declareops.eq_recarg let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 +| Norec, _ -> None | Mrec i1, Mrec i2 -| Imbr i1, Imbr i2 -| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None -| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None -| _ -> None +| Nested (NestedInd i1), Nested (NestedInd i2) +| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None +| Mrec _, _ -> None +| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Nested (NestedInd _), _ -> None +| Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) -> + if Names.Constant.equal c1 c2 then Some r1 else None +| Nested (NestedPrimitive _), _ -> None let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec @@ -551,8 +556,8 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | (Mrec i | Imbr i) -> eq_ind ind i - | Norec -> false + | Mrec i | Nested (NestedInd i) -> eq_ind ind i + | Norec | Nested (NestedPrimitive _) -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} [branches_specif renv c_spec ci] returns an array of x_s specs knowing @@ -603,7 +608,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in - let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in + let rc = Array.mapi (fun j t -> (Nested (NestedInd (mind,j)),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in (env, lra_ind @ ra_env) @@ -637,6 +642,11 @@ let abstract_mind_lc ntyps npars lc = in Array.map (substl make_abs) lc +let is_primitive_positive_container env c = + match env.retroknowledge.Retroknowledge.retro_array with + | Some c' when Constant.equal c c' -> true + | _ -> false + (* [get_recargs_approx env tree ind args] builds an approximation of the recargs tree for ind, knowing args. The argument tree is used to know when candidate nested types should be traversed, pruning the tree otherwise. This code is very @@ -657,8 +667,14 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> - build_recargs_nested ienv tree (ind_kn, largs) + | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' -> + build_recargs_nested ienv tree (ind_kn, largs) + | _ -> mk_norec + end + | Const (c,_) when is_primitive_positive_container env c -> + begin match dest_recarg tree with + | Nested (NestedPrimitive c') when Constant.equal c c' -> + build_recargs_nested_primitive ienv tree (c, largs) | _ -> mk_norec end | _err -> @@ -696,11 +712,21 @@ let get_recargs_approx env tree ind args = build_recargs_constructors ienv' trees.(j).(k) c') auxlcvect in - mk_paths (Imbr (mind,j)) paths + mk_paths (Nested (NestedInd (mind,j))) paths in let irecargs = Array.mapi mk_irecargs mib.mind_packets in (Rtree.mk_rec irecargs).(i) + and build_recargs_nested_primitive (env, ra_env) tree (c, largs) = + if eq_wf_paths tree mk_norec then tree + else + let ntypes = 1 in (* Primitive types are modelled by non-mutual inductive types *) + let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in + let ienv = (env, ra_env) in + let paths = List.map2 (build_recargs ienv) (dest_subterms tree).(0) largs in + let recargs = [| mk_paths (Nested (NestedPrimitive c)) [| paths |] |] in + (Rtree.mk_rec recargs).(0) + and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in @@ -756,7 +782,7 @@ let rec subterm_specif renv stack t = let f,l = decompose_app (whd_all renv.env t) in match kind f with | Rel k -> subterm_var k renv - | Case (ci,p,c,lbr) -> + | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *) let stack' = push_stack_closures renv l stack in let cases_spec = branches_specif renv (lazy_subterm_specif renv [] c) ci @@ -829,8 +855,17 @@ let rec subterm_specif renv stack t = | Dead_code -> Dead_code | Not_subterm -> Not_subterm) - | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm + | Const c -> + begin try + let _ = Environ.constant_value_in renv.env c in Not_subterm + with + | NotEvaluableConst (IsPrimitive (_u,op)) when List.length l >= CPrimitives.arity op -> + primitive_specif renv op l + | NotEvaluableConst _ -> Not_subterm + end + + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Ind _ + | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Not_subterm (* Other terms are not subterms *) @@ -846,6 +881,24 @@ and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t +and primitive_specif renv op args = + let open CPrimitives in + match op with + | Arrayget | Arraydefault -> + (* t.[i] and default t can be seend as strict subterms of t, with a + potentially nested rectree. *) + let arg = List.nth args 1 in (* the result is a strict subterm of the second argument *) + let subt = subterm_specif renv [] arg in + begin match subt with + | Subterm (_s, wf) -> + let wf_args = (dest_subterms wf).(0) in + spec_of_tree (List.nth wf_args 0) (* first and only parameter of `array` *) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm + end + | _ -> Not_subterm + + (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm x tree = match Lazy.force x with @@ -954,7 +1007,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(lift p c,l)) end - | Case (ci,p,c_0,lrest) -> + | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *) begin try List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg info for the arguments of each branch *) @@ -976,7 +1029,7 @@ let check_one_fix renv recpos trees def = (* the call to whd_betaiotazeta will reduce the apparent iota redex away *) check_rec_call renv [] - (Term.applist (mkCase (ci,p,c_0,lrest), l)) + (Term.applist (mkCase (ci,p,iv,c_0,lrest), l)) | _ -> Exninfo.iraise exn end @@ -1086,6 +1139,12 @@ let check_one_fix renv recpos trees def = | Sort _ | Int _ | Float _ -> assert (List.is_empty l) + | Array (_u, t,def,ty) -> + assert (List.is_empty l); + Array.iter (check_rec_call renv []) t; + check_rec_call renv [] def; + check_rec_call renv [] ty + (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () @@ -1254,7 +1313,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) - | Case (_,p,tm,vrest) -> + | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *) begin let tree = match restrict_spec env (Subterm (Strict, tree)) p with | Dead_code -> assert false @@ -1278,7 +1337,7 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ | Int _ | Float _ -> + | Ind _ | Fix _ | Proj _ | Int _ | Float _ | Array _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9f865f8f01..78658dc4de 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -105,6 +105,13 @@ val check_case_info : env -> pinductive -> Sorts.relevance -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) +(** [is_primitive_positive_container env c] tells if the constant [c] is + registered as a primitive type that can be seen as a container where the + occurrences of its parameters are positive, in which case the positivity and + guard conditions are extended to allow inductive types to nest their subterms + in these containers. *) +val is_primitive_positive_container : env -> Constant.t -> bool + (** When [chk] is false, the guard condition is not actually checked. *) val check_fix : env -> fixpoint -> unit diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 662ad550b8..8191a5b0f3 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -138,6 +138,18 @@ let rec infer_fterm cv_pb infos variances hd stk = let le = Esubst.subs_liftn n e in let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in infer_stack infos variances stk + | FArray (u,elemsdef,ty) -> + let variances = infer_generic_instance_eq variances u in + let variances = infer_fterm CONV infos variances ty [] in + let elems, def = Parray.to_array elemsdef in + let variances = infer_fterm CONV infos variances def [] in + let variances = infer_vect infos variances elems in + infer_stack infos variances stk + + | FCaseInvert (_,p,_,_,br,e) -> + let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in + let variances = infer p variances in + Array.fold_right infer br variances (* Removed by whnf *) | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index cc9da3a2ce..41388d9f17 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,8 +1,8 @@ Names TransparentState Uint63 +Parray Float64 -CPrimitives Univ UGraph Esubst @@ -12,6 +12,7 @@ Context Constr Vars Term +CPrimitives Mod_subst Vmvalues Cbytecodes diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 317141e324..2aeb1ea202 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -364,20 +364,21 @@ let rec map_kn f f' c = | Construct (((kn,i),j),u) -> let kn' = f kn in if kn'==kn then c else mkConstructU (((kn',i),j),u) - | Case (ci,p,ct,l) -> + | Case (ci,p,iv,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in let kn' = f kn in if kn'==kn then ci.ci_ind else kn',i in let p' = func p in + let iv' = map_invert func iv in let ct' = func ct in let l' = Array.Smart.map func l in - if (ci.ci_ind==ci_ind && p'==p + if (ci.ci_ind==ci_ind && p'==p && iv'==iv && l'==l && ct'==ct)then c else mkCase ({ci with ci_ind = ci_ind}, - p',ct', l') + p',iv',ct', l') | Cast (ct,k,t) -> let ct' = func ct in let t'= func t in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index f30ddce4d7..ae070e6f8e 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -259,6 +259,7 @@ type primitive = | Mk_proj | Is_int | Is_float + | Is_parray | Cast_accu | Upd_cofix | Force_cofix @@ -285,7 +286,8 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * pconstant) option + | MLparray_of_array + | Coq_primitive of CPrimitives.t * bool (* check for accu *) let eq_primitive p1 p2 = match p1, p2 with @@ -346,15 +348,15 @@ let primitive_hash = function | MLsub -> 31 | MLmul -> 32 | MLmagic -> 33 - | Coq_primitive (prim, None) -> combinesmall 34 (CPrimitives.hash prim) - | Coq_primitive (prim, Some (prefix,(kn,_))) -> - combinesmall 35 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) - | Mk_proj -> 36 - | MLarrayget -> 37 - | Mk_empty_instance -> 38 - | Mk_float -> 39 - | Is_float -> 40 + | Coq_primitive (prim, b) -> combinesmall 34 (combine (CPrimitives.hash prim) (Hashtbl.hash b)) + | Mk_proj -> 35 + | MLarrayget -> 36 + | Mk_empty_instance -> 37 + | Mk_float -> 38 + | Is_float -> 39 + | Is_parray -> 41 | MLnot -> 41 + | MLparray_of_array -> 42 type mllambda = | MLlocal of lname @@ -971,11 +973,14 @@ type prim_aux = let add_check cond targs args = let aux cond t a = - match a with - | PAml(MLint _) -> cond - | PAml ml -> + match t, a with + | CPrimitives.(PITT_type (PT_int63, _)), PAml(MLapp(MLprimitive Mk_uint, _)) -> cond + | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp(MLprimitive MLparray_of_array, _)) -> cond + | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp (MLglobal (Ginternal "get_value"),_)) -> cond + | CPrimitives.(PITT_type (prim_ty, _)), PAml ml -> (* FIXME: use explicit equality function *) - if List.mem (t, ml) cond then cond else (t, ml)::cond + let c = (CPrimitives.PTE prim_ty, ml) in + if List.mem c cond then cond else c::cond | _ -> cond in Array.fold_left2 aux cond targs args @@ -985,13 +990,15 @@ let extract_prim ml_of l = let cond = ref [] in let type_args p = let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in - Array.of_list (aux (CPrimitives.types p)) in + let params, sign = CPrimitives.types p in + List.length params, Array.of_list (aux sign) in let rec aux l = match l with | Lprim(prefix,kn,p,args) -> - let targs = type_args p in + let nparams, targs = type_args p in let args = Array.map aux args in - cond := add_check !cond targs args; + let checked_args = Array.init (Array.length args - nparams) (fun i -> args.(i+nparams)) in + cond := add_check !cond targs checked_args; PAprim(prefix,kn,p,args) | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l) | _ -> @@ -1006,31 +1013,48 @@ let cast_to_int v = | MLint _ -> v | _ -> MLapp(MLprimitive Val_to_int, [|v|]) -let compile_prim decl cond paux = +let ml_of_instance instance u = + let ml_of_level l = + match Univ.Level.var_index l with + | Some i -> + let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in + mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] + | None -> let i = push_symbol (SymbLevel l) in get_level_code i + in + let u = Univ.Instance.to_array u in + if Array.is_empty u then [||] + else let u = Array.map ml_of_level u in + [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] + +let compile_prim env decl cond paux = let rec opt_prim_aux paux = match paux with | PAprim(_prefix, _kn, op, args) -> - let args = Array.map opt_prim_aux args in - app_prim (Coq_primitive(op,None)) args + let n = CPrimitives.nparams op in + let args = Array.map opt_prim_aux (Array.sub args n (Array.length args - n)) in + app_prim (Coq_primitive(op, false)) args | PAml ml -> ml and naive_prim_aux paux = match paux with - | PAprim(prefix, kn, op, args) -> - app_prim (Coq_primitive(op, Some (prefix,kn))) (Array.map naive_prim_aux args) + | PAprim(prefix, (kn,u), op, args) -> + let uarg = ml_of_instance env.env_univ u in + let prim_const = mkMLapp (MLglobal (Gconstant(prefix,kn))) uarg in + let prim = mkMLapp (MLprimitive(Coq_primitive(op, true))) [|prim_const|] in + mkMLapp prim (Array.map naive_prim_aux args) | PAml ml -> ml in let compile_cond cond paux = match cond with | [] -> opt_prim_aux paux - | [CPrimitives.(PITT_type PT_int63), c1] -> + | [CPrimitives.(PTE PT_int63), c1] -> MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) | _ -> - let ci, cf = + let ci, co = let is_int = - function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in + function CPrimitives.(PTE PT_int63), _ -> true | _ -> false in List.partition is_int cond in let condi = let cond = @@ -1038,21 +1062,25 @@ let compile_prim decl cond paux = (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|]) (MLint 0) ci in app_prim MLmagic [|cond|] in - let condf = match cf with + let condo = match co with | [] -> MLint 0 - | [_, c1] -> app_prim Is_float [|c1|] - | (_, c1) :: condf -> + | (CPrimitives.PTE ty, c1) :: condo -> + let check = match ty with + | CPrimitives.PT_float64 -> Is_float + | CPrimitives.PT_array -> Is_parray + | CPrimitives.PT_int63 -> assert false + in List.fold_left - (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|]) - (app_prim Is_float [|c1|]) condf in - match ci, cf with + (fun ml (_, c) -> app_prim MLand [| ml; app_prim check [|c|]|]) + (app_prim check [|c1|]) condo in + match ci, co with | [], [] -> opt_prim_aux paux | _ :: _, [] -> MLif(condi, naive_prim_aux paux, opt_prim_aux paux) | [], _ :: _ -> - MLif(condf, opt_prim_aux paux, naive_prim_aux paux) + MLif(condo, opt_prim_aux paux, naive_prim_aux paux) | _ :: _, _ :: _ -> - let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in + let cond = app_prim MLand [|condo; app_prim MLnot [|condi|]|] in MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in let add_decl decl body = @@ -1065,19 +1093,6 @@ let compile_prim decl cond paux = else add_decl decl (compile_cond cond paux) -let ml_of_instance instance u = - let ml_of_level l = - match Univ.Level.var_index l with - | Some i -> - let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in - mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] - | None -> let i = push_symbol (SymbLevel l) in get_level_code i - in - let u = Univ.Instance.to_array u in - if Array.is_empty u then [||] - else let u = Array.map ml_of_level u in - [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] - let rec ml_of_lam env l t = match t with | Lrel(id ,i) -> get_rel env id i @@ -1118,7 +1133,7 @@ let ml_of_instance instance u = | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in - compile_prim decl cond paux + compile_prim env decl cond paux | Lcase (annot,p,a,bs) -> (* let predicate_uid fv_pred = compilation of p let rec case_uid fv a_uid = @@ -1333,6 +1348,9 @@ let ml_of_instance instance u = MLconstruct(prefix,cn,tag,args) | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|]) + | Lparray (t,def) -> + let def = ml_of_lam env l def in + MLapp(MLprimitive MLparray_of_array, [| MLarray (Array.map (ml_of_lam env l) t); def |]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> @@ -1777,6 +1795,7 @@ let pp_mllam fmt l = | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" | Is_float -> Format.fprintf fmt "is_float" + | Is_parray -> Format.fprintf fmt "is_parray" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" | Force_cofix -> Format.fprintf fmt "force_cofix" @@ -1803,11 +1822,10 @@ let pp_mllam fmt l = | MLmagic -> Format.fprintf fmt "Obj.magic" | MLarrayget -> Format.fprintf fmt "Array.get" | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" - | Coq_primitive (op,None) -> + | MLparray_of_array -> Format.fprintf fmt "parray_of_array" + | Coq_primitive (op, false) -> Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) - | Coq_primitive (op, Some (prefix,(c,_))) -> - Format.fprintf fmt "%s %a" (CPrimitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix,c))) + | Coq_primitive (op, true) -> Format.fprintf fmt "%s" (CPrimitives.to_string op) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -2088,7 +2106,7 @@ let compile_deps env sigma prefix ~interactive init t = | 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, _iv, _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 31a716a786..01e9550ec5 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -38,6 +38,10 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfloat64 f1, Vfloat64 f2 -> if Float64.(equal (of_float f1) (of_float f2)) then cu else raise NotConvertible + | Varray t1, Varray t2 -> + let len = Parray.length_int t1 in + if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible; + Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV lvl v1 v2 cu) cu t1 t2 | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -51,7 +55,7 @@ let rec conv_val env pb lvl v1 v2 cu = aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu - | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible + | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Varray _ | Vblock _), _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 02ee501f5f..b00b96018f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -40,6 +40,7 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) + | Lparray of lambda array * lambda | Lmakeblock of prefix * inductive * int * lambda array (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) @@ -187,6 +188,10 @@ let map_lam_with_binders g f n lam = | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') + | Lparray (p,def) -> + let p' = Array.Smart.map (f n) p in + let def' = f n def in + if def' == def && p == p' then lam else Lparray (p', def') (*s Lift and substitution *) @@ -377,6 +382,12 @@ let makeblock env ind tag nparams arity args = let prefix = get_mind_prefix env (fst ind) in Lmakeblock(prefix, ind, tag, args) +let makearray args def = + try + let p = Array.map get_value args in + Lval (Nativevalues.parray_of_array p (get_value def)) + with Not_found -> Lparray (args, def) + (* Translation of constants *) let rec get_alias env (kn, u as p) = @@ -400,8 +411,13 @@ let expand_prim env kn op arity = let lambda_of_prim env kn op args = let arity = CPrimitives.arity op in - if Array.length args >= arity then prim env kn op args - else mkLapp (expand_prim env kn op arity) args + match Int.compare (Array.length args) arity with + | 0 -> prim env kn op args + | x when x > 0 -> + let prim_args = Array.sub args 0 arity in + let extra_args = Array.sub args arity (Array.length args - arity) in + mkLapp(prim env kn op prim_args) extra_args + | _ -> mkLapp (expand_prim env kn op arity) args (*i Global environment *) @@ -521,7 +537,7 @@ let rec lambda_of_constr cache env sigma c = let prefix = get_mind_prefix env (fst ind) in mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|] - | Case(ci,t,a,branches) -> + | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) let (mind,i as ind) = ci.ci_ind in let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in @@ -589,6 +605,10 @@ let rec lambda_of_constr cache env sigma c = | Float f -> Lfloat f + | Array (_u, t, def, _ty) -> + let def = lambda_of_constr cache env sigma def in + makearray (lambda_of_args cache env sigma 0 t) def + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index e339286329..619d362f35 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -34,6 +34,7 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) + | Lparray of lambda array * lambda | Lmakeblock of prefix * inductive * int * lambda array (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index a5fcfae1fc..9e17f97a56 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -244,6 +244,7 @@ type kind_of_value = | Vconst of int | Vint64 of int64 | Vfloat64 of float + | Varray of t Parray.t | Vblock of block let kind_of_value (v:t) = @@ -253,7 +254,8 @@ let kind_of_value (v:t) = else let tag = Obj.tag o in if Int.equal tag accumulate_tag then - Vaccu (Obj.magic v) + if Int.equal (Obj.size o) 1 then Varray (Obj.magic v) + else Vaccu (Obj.magic v) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) @@ -686,6 +688,84 @@ let next_down accu x = if is_float x then no_check_next_down x else accu x +let is_parray t = + let t = Obj.magic t in + Obj.is_block t && Obj.size t = 1 + +let to_parray t = Obj.magic t +let of_parray t = Obj.magic t + +let no_check_arraymake n def = + of_parray (Parray.make (to_uint n) def) + +let arraymake accu vA n def = + if is_int n then + no_check_arraymake n def + else accu vA n def + +let no_check_arrayget t n = + Parray.get (to_parray t) (to_uint n) +[@@ocaml.inline always] + +let arrayget accu vA t n = + if is_parray t && is_int n then + no_check_arrayget t n + else accu vA t n + +let no_check_arraydefault t = + Parray.default (to_parray t) +[@@ocaml.inline always] + +let arraydefault accu vA t = + if is_parray t then + no_check_arraydefault t + else accu vA t + +let no_check_arrayset t n v = + of_parray (Parray.set (to_parray t) (to_uint n) v) +[@@ocaml.inline always] + +let arrayset accu vA t n v = + if is_parray t && is_int n then + no_check_arrayset t n v + else accu vA t n v + +let no_check_arraycopy t = + of_parray (Parray.copy (to_parray t)) +[@@ocaml.inline always] + +let arraycopy accu vA t = + if is_parray t then + no_check_arraycopy t + else accu vA t + +let no_check_arrayreroot t = + of_parray (Parray.reroot (to_parray t)) +[@@ocaml.inline always] + +let arrayreroot accu vA t = + if is_parray t then + no_check_arrayreroot t + else accu vA t + +let no_check_arraylength t = + mk_uint (Parray.length (to_parray t)) +[@@ocaml.inline always] + +let arraylength accu vA t = + if is_parray t then + no_check_arraylength t + else accu vA t + +let parray_of_array t def = + (Obj.magic (Parray.unsafe_of_array t def) : t) + +let arrayinit n (f:t->t) def = + of_parray (Parray.init (to_uint n) (Obj.magic f) def) + +let arraymap f t = + of_parray (Parray.map f (to_parray t)) + let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i) let bohcnv = Array.init 256 (fun i -> i - (if 0x30 <= i then 0x30 else 0) - diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 78a9b2ea13..08c5bd7126 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -134,6 +134,7 @@ type kind_of_value = | Vconst of int | Vint64 of int64 | Vfloat64 of float + | Varray of t Parray.t | Vblock of block val kind_of_value : t -> kind_of_value @@ -332,3 +333,39 @@ val no_check_next_up : t -> t val no_check_next_down : t -> t [@@ocaml.inline always] + +(** Support for arrays *) + +val parray_of_array : t array -> t -> t +val is_parray : t -> bool + +val arraymake : t -> t -> t -> t -> t (* accu A n def *) +val arrayget : t -> t -> t -> t -> t (* accu A t n *) +val arraydefault : t -> t -> t (* accu A t *) +val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *) +val arraycopy : t -> t -> t -> t (* accu A t *) +val arrayreroot : t -> t -> t -> t (* accu A t *) +val arraylength : t -> t -> t -> t (* accu A t *) +val arrayinit : t -> t -> t -> t (* accu A n f def *) +val arraymap : t -> t -> t (* accu A B f t *) + +val no_check_arraymake : t -> t -> t +[@@ocaml.inline always] + +val no_check_arrayget : t -> t -> t -> t +[@@ocaml.inline always] + +val no_check_arraydefault : t -> t +[@@ocaml.inline always] + +val no_check_arrayset : t -> t -> t -> t +[@@ocaml.inline always] + +val no_check_arraycopy : t -> t +[@@ocaml.inline always] + +val no_check_arrayreroot : t -> t +[@@ocaml.inline always] + +val no_check_arraylength : t -> t +[@@ocaml.inline always] diff --git a/kernel/parray.ml b/kernel/parray.ml new file mode 100644 index 0000000000..ea314c1883 --- /dev/null +++ b/kernel/parray.ml @@ -0,0 +1,124 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let max_array_length32 = 4194303 + +let max_length = Uint63.of_int max_array_length32 + +let length_to_int i = snd (Uint63.to_int2 i) + +let trunc_size n = + if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int max_array_length32) then + length_to_int n + else max_array_length32 + +type 'a t = ('a kind) ref +and 'a kind = + | Array of 'a array * 'a + | Updated of int * 'a * 'a t + +let unsafe_of_array t def = ref (Array (t,def)) +let of_array t def = unsafe_of_array (Array.copy t) def + +let rec length_int p = + match !p with + | Array (t,_) -> Array.length t + | Updated (_, _, p) -> length_int p + +let length p = Uint63.of_int @@ length_int p + +let rec get p n = + match !p with + | Array (t,def) -> + let l = Array.length t in + if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then + Array.unsafe_get t (length_to_int n) + else def + | Updated (k,e,p) -> + if Uint63.equal n (Uint63.of_int k) then e + else get p n + +let set p n e = + let kind = !p in + match kind with + | Array (t,_) -> + let l = Uint63.of_int @@ Array.length t in + if Uint63.le Uint63.zero n && Uint63.lt n l then + let res = ref kind in + let n = length_to_int n in + p := Updated (n, Array.unsafe_get t n, res); + Array.unsafe_set t n e; + res + else p + | Updated _ -> + if Uint63.le Uint63.zero n && Uint63.lt n (length p) then + ref (Updated((length_to_int n), e, p)) + else p + +let rec default p = + match !p with + | Array (_,def) -> def + | Updated (_,_,p) -> default p + +let make n def = + ref (Array (Array.make (trunc_size n) def, def)) + +let init n f def = + let n = trunc_size n in + let t = Array.init n f in + ref (Array (t, def)) + +let rec to_array p = + match !p with + | Array (t,def) -> Array.copy t, def + | Updated (n,e,p) -> + let (t,_) as r = to_array p in + Array.unsafe_set t n e; r + +let copy p = + let (t,def) = to_array p in + ref (Array (t,def)) + +let rec rerootk t k = + match !t with + | Array _ -> k () + | Updated (i, v, t') -> + let k' () = + begin match !t' with + | Array (a,_def) as n -> + let v' = a.(i) in + Array.unsafe_set a i v; + t := n; + t' := Updated (i, v', t) + | Updated _ -> assert false + end; k() in + rerootk t' k' + +let reroot t = rerootk t (fun () -> t) + +let map f p = + let p = reroot p in + match !p with + | Array (t,def) -> ref (Array (Array.map f t, f def)) + | Updated _ -> assert false + +let fold_left f x p = + let p = reroot p in + match !p with + | Array (t,def) -> f (Array.fold_left f x t) def + | Updated _ -> assert false + +let fold_left2 f a p1 p2 = + let p1 = reroot p1 in + let p2 = reroot p2 in + match !p1, !p2 with + | Array (t1, def1), Array (t2, def2) -> + f (CArray.fold_left2 f a t1 t2) def1 def2 + | _ -> assert false diff --git a/kernel/parray.mli b/kernel/parray.mli new file mode 100644 index 0000000000..0276278bd0 --- /dev/null +++ b/kernel/parray.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val max_length : Uint63.t + +type 'a t +val length : 'a t -> Uint63.t +val length_int : 'a t -> int +val get : 'a t -> Uint63.t -> 'a +val set : 'a t -> Uint63.t -> 'a -> 'a t +val default : 'a t -> 'a +val make : Uint63.t -> 'a -> 'a t +val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t +val copy : 'a t -> 'a t +val reroot : 'a t -> 'a t + +val map : ('a -> 'b) -> 'a t -> 'b t + +val to_array : 'a t -> 'a array * 'a (* default *) + +val of_array : 'a array -> 'a (* default *) -> 'a t + +val unsafe_of_array : 'a array -> 'a -> 'a t +(* [unsafe_of_array] injects a mutable array into a persistent one, but does + not perform a copy. This means that if the persistent array is mutated, the + original one will be too. *) + +val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a +val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a diff --git a/kernel/primred.ml b/kernel/primred.ml index c475828cb3..10a8da8813 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -21,6 +21,13 @@ let add_retroknowledge env action = | None -> { retro with retro_float64 = Some c } | Some c' -> assert (Constant.equal c c'); retro in set_retroknowledge env retro + | Register_type(PT_array,c) -> + let retro = env.retroknowledge in + let retro = + match retro.retro_array with + | None -> { retro with retro_array = Some c } + | Some c' -> assert (Constant.equal c c'); retro in + set_retroknowledge env retro | Register_ind(pit,ind) -> let retro = env.retroknowledge in let retro = @@ -120,10 +127,12 @@ module type RedNativeEntries = type elem type args type evd (* will be unit in kernel, evar_map outside *) + type uinstance val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t val get_float : evd -> elem -> Float64.t + val get_parray : evd -> elem -> elem Parray.t val mkInt : env -> Uint63.t -> elem val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem @@ -146,6 +155,7 @@ module type RedNativeEntries = val mkPInf : env -> elem val mkNInf : env -> elem val mkNaN : env -> elem + val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem end module type RedNative = @@ -153,17 +163,20 @@ module type RedNative = type elem type args type evd - val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + type uinstance + val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option end module RedNative (E:RedNativeEntries) : RedNative with type elem = E.elem with type args = E.args - with type evd = E.evd = + with type evd = E.evd + with type uinstance = E.uinstance = struct type elem = E.elem type args = E.args type evd = E.evd + type uinstance = E.uinstance let get_int evd args i = E.get_int evd (E.get args i) @@ -180,7 +193,9 @@ struct let get_float2 evd args = get_float evd args 0, get_float evd args 1 - let red_prim_aux env evd op args = + let get_parray evd args i = E.get_parray evd (E.get args i) + + let red_prim_aux env evd op u args = let open CPrimitives in match op with | Int63head0 -> @@ -315,11 +330,43 @@ struct let f = get_float1 evd args in E.mkFloat env (Float64.next_up f) | Float64next_down -> let f = get_float1 evd args in E.mkFloat env (Float64.next_down f) + | Arraymake -> + let ty = E.get args 0 in + let i = get_int evd args 1 in + let d = E.get args 2 in + E.mkArray env u (Parray.make i d) ty + | Arrayget -> + let t = get_parray evd args 1 in + let i = get_int evd args 2 in + Parray.get t i + | Arraydefault -> + let t = get_parray evd args 1 in + Parray.default t + | Arrayset -> + let ty = E.get args 0 in + let t = get_parray evd args 1 in + let i = get_int evd args 2 in + let a = E.get args 3 in + let t' = Parray.set t i a in + E.mkArray env u t' ty + | Arraycopy -> + let ty = E.get args 0 in + let t = get_parray evd args 1 in + let t' = Parray.copy t in + E.mkArray env u t' ty + | Arrayreroot -> + let ar = E.get args 1 in + let t = E.get_parray evd ar in + let _ = Parray.reroot t in + ar + | Arraylength -> + let t = get_parray evd args 1 in + E.mkInt env (Parray.length t) - let red_prim env evd p args = + let red_prim env evd p u args = try let r = - red_prim_aux env evd p args + red_prim_aux env evd p u args in Some r with NativeDestKO -> None diff --git a/kernel/primred.mli b/kernel/primred.mli index bbe564d8e7..1bfaffaa44 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -24,10 +24,12 @@ module type RedNativeEntries = type elem type args type evd (* will be unit in kernel, evar_map outside *) + type uinstance val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t val get_float : evd -> elem -> Float64.t + val get_parray : evd -> elem -> elem Parray.t val mkInt : env -> Uint63.t -> elem val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem @@ -50,6 +52,7 @@ module type RedNativeEntries = val mkPInf : env -> elem val mkNInf : env -> elem val mkNaN : env -> elem + val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem end module type RedNative = @@ -57,7 +60,8 @@ module type RedNative = type elem type args type evd - val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + type uinstance + val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option end module RedNative : @@ -65,3 +69,4 @@ module RedNative : RedNative with type elem = E.elem with type args = E.args with type evd = E.evd + with type uinstance = E.uinstance diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4ff90dd70d..0754e9d4cc 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -138,10 +138,10 @@ let nf_betaiota env t = let whd_betaiotazeta env x = match kind x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> x + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> x | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ | Array _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) @@ -152,10 +152,10 @@ let whd_betaiotazeta env x = let whd_all env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> t + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ | Array _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos all env) (create_tab ()) (inject t) @@ -166,10 +166,10 @@ let whd_all env t = let whd_allnolet env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _) -> t + Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _|Array _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ | Array _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) @@ -209,12 +209,16 @@ type conv_pb = let is_cumul = function CUMUL -> true | CONV -> false -type 'a universe_compare = - { (* Might raise NotConvertible *) - compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; - compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.Variance.t array -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } +type 'a universe_compare = { + (* used in reduction *) + compare_graph : 'a -> UGraph.t; + + (* Might raise NotConvertible *) + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; +} type 'a universe_state = 'a * 'a universe_compare @@ -302,7 +306,6 @@ let unfold_ref_with_args infos tab fl v = type conv_tab = { cnv_inf : clos_infos; - relevances : Sorts.relevance Range.t; lft_tab : clos_tab; rgt_tab : clos_tab; } @@ -313,13 +316,13 @@ type conv_tab = { passed to each respective side of the conversion function below. *) let push_relevance infos r = - { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances } + { infos with cnv_inf = CClosure.push_relevance infos.cnv_inf r } let push_relevances infos nas = - { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas } + { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas } let rec skip_pattern infos relevances n c1 c2 = - if Int.equal n 0 then {infos with relevances}, c1, c2 + if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2 else match kind c1, kind c2 with | Lambda (x, _, c1), Lambda (_, _, c2) -> skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 @@ -327,11 +330,11 @@ let rec skip_pattern infos relevances n c1 c2 = let skip_pattern infos n c1 c2 = if Int.equal n 0 then infos, c1, c2 - else skip_pattern infos infos.relevances n c1 c2 + else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2 let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in - try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = @@ -633,13 +636,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible + | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> + (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible); + let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in + let ccnv = ccnv CONV l2r infos el1 el2 in + let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in + Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv) + br1 br2 cuniv + + | FArray (u1,t1,ty1), FArray (u2,t2,ty2) -> + let len = Parray.length_int t1 in + if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible; + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in + let cuniv = Parray.fold_left2 (fun u v1 v2 -> ccnv CONV l2r infos el1 el2 v1 v2 u) cuniv t1 t2 in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false - | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ - | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible + | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ | FCaseInvert _ + | FProd _ | FEvar _ | FInt _ | FFloat _ | FArray _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in @@ -711,10 +732,10 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in - let infos = create_clos_infos ~evars reds env in + let graph = (snd univs).compare_graph (fst univs) in + let infos = create_clos_infos ~univs:graph ~evars reds env in let infos = { cnv_inf = infos; - relevances = Range.empty; lft_tab = create_tab (); rgt_tab = create_tab (); } in @@ -759,10 +780,25 @@ let check_inductive_instances cv_pb variance u1 u2 univs = else raise NotConvertible let checked_universes = - { compare_sorts = checked_sort_cmp_universes; + { compare_graph = (fun x -> x); + compare_sorts = checked_sort_cmp_universes; compare_instances = check_convert_instances; compare_cumul_instances = check_inductive_instances; } +let () = + let conv infos tab a b = + try + let univs = info_univs infos in + let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; } in + let univs', _ = ccnv CONV false infos el_id el_id a b + (univs, checked_universes) + in + assert (univs==univs'); + true + with NotConvertible -> false + in + CClosure.set_conv conv + let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv else @@ -807,7 +843,8 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') = (univs, Univ.Constraint.union csts csts') let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = - { compare_sorts = infer_cmp_universes; + { compare_graph = (fun (x,_) -> x); + compare_sorts = infer_cmp_universes; compare_instances = infer_convert_instances; compare_cumul_instances = infer_inductive_instances; } diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ff5934c66c..4ae3838691 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,12 +36,15 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL -type 'a universe_compare = - { (* Might raise NotConvertible *) - compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; - compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.Variance.t array -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } +type 'a universe_compare = { + compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *) + + (* Might raise NotConvertible *) + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; +} type 'a universe_state = 'a * 'a universe_compare diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml index 3f3e722245..f12b8cba37 100644 --- a/kernel/relevanceops.ml +++ b/kernel/relevanceops.ml @@ -54,14 +54,14 @@ let rec relevance_of_fterm env extra lft f = | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1) | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c | FFlex key -> relevance_of_flex env key - | FInt _ | FFloat _ -> Sorts.Relevant + | FInt _ | FFloat _ | FArray _ -> Sorts.Relevant | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) | FConstruct (c,_) -> relevance_of_constructor env c | FApp (f, _) -> relevance_of_fterm env extra lft f | FProj (p, _) -> relevance_of_projection env p | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance - | FCaseT (ci, _, _, _, _) -> ci.ci_relevance + | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance | FLambda (len, tys, bdy, e) -> let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in let lft = Esubst.el_liftn len lft in @@ -97,11 +97,12 @@ and relevance_of_term_extra env extra lft subs c = | App (c, _) -> relevance_of_term_extra env extra lft subs c | Const (c,_) -> relevance_of_constant env c | Construct (c,_) -> relevance_of_constructor env c - | Case (ci, _, _, _) -> ci.ci_relevance + | Case (ci, _, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> relevance_of_projection env p | Int _ | Float _ -> Sorts.Relevant + | Array _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 4e642ca11d..f7c4b62d1f 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -19,6 +19,7 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; retro_float64 : Constant.t option; + retro_array : Constant.t option; retro_bool : (constructor * constructor) option; (* true, false *) retro_carry : (constructor * constructor) option; (* C0, C1 *) retro_pair : constructor option; @@ -40,6 +41,7 @@ type retroknowledge = { let empty = { retro_int63 = None; retro_float64 = None; + retro_array = None; retro_bool = None; retro_carry = None; retro_pair = None; @@ -51,4 +53,4 @@ let empty = { type action = | Register_ind : 'a CPrimitives.prim_ind * inductive -> action - | Register_type : CPrimitives.prim_type * Constant.t -> action + | Register_type : 'a CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index bf8ec8badb..fd412cdd0a 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -13,6 +13,7 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; retro_float64 : Constant.t option; + retro_array : Constant.t option; retro_bool : (constructor * constructor) option; (* true, false *) retro_carry : (constructor * constructor) option; (* C0, C1 *) retro_pair : constructor option; @@ -35,4 +36,4 @@ val empty : retroknowledge type action = | Register_ind : 'a CPrimitives.prim_ind * inductive -> action - | Register_type : CPrimitives.prim_type * Constant.t -> action + | Register_type : 'a CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 93337fca5d..8b85072d6d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1023,6 +1023,8 @@ let start_module l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = STRUCT ([],senv); required = senv.required } @@ -1034,6 +1036,8 @@ let start_modtype l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = SIG ([], senv); required = senv.required } diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c8c2301171..04e7a81697 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -21,13 +21,14 @@ open Constr open Declarations open Environ open Entries +open Univ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) type 'a effect_handler = - env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) + env -> Constr.t -> 'a -> (Constr.t * ContextSet.t * int) let skip_trusted_seff sl b e = let rec aux sl b e acc = @@ -62,55 +63,91 @@ let feedback_completion_typecheck = type typing_context = | MonoTyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * Stateid.t option -| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option +| PolyTyCtx of Environ.env * unsafe_type_judgment * universe_level_subst * AUContext.t * Id.Set.t * Stateid.t option -let infer_declaration env (dcl : constant_entry) = - match dcl with - | ParameterEntry (ctx,(t,uctx),nl) -> - let env = match uctx with - | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env +let check_primitive_type env op_t u t = + let inft = Typeops.type_of_prim_or_type env u op_t in + try Reduction.default_conv ~l2r:false Reduction.CONV env inft t + with Reduction.NotConvertible -> + Type_errors.error_incorrect_primitive env (make_judge op_t inft) t + +let merge_unames = + Array.map2 (fun base user -> match user with Anonymous -> base | Name _ -> user) + +let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = + let open CPrimitives in + let auctx = CPrimitives.op_or_type_univs p in + let univs, typ = + match utyp with + | None -> + let u = UContext.instance (AUContext.repr auctx) in + let typ = Typeops.type_of_prim_or_type env u p in + let univs = if AUContext.is_empty auctx then Monomorphic ContextSet.empty + else Polymorphic auctx in - let j = Typeops.infer env t in - let usubst, univs = Declareops.abstract_universes uctx in - let r = Typeops.assumption_of_judgment env j in - let t = Vars.subst_univs_level_constr usubst j.uj_val in - { - Cooking.cook_body = Undef nl; - cook_type = t; - cook_universes = univs; - cook_relevance = r; - cook_inline = false; - cook_context = ctx; - } + univs, typ - (** Primitives cannot be universe polymorphic *) - | PrimitiveEntry ({ prim_entry_type = otyp; - prim_entry_univs = uctxt; - prim_entry_content = op_t; - }) -> - let env = push_context_set ~strict:true uctxt env in - let ty = match otyp with - | Some typ -> + | Some (typ,Monomorphic_entry uctx) -> + assert (AUContext.is_empty auctx); + let env = push_context_set ~strict:true uctx env in + let u = Instance.empty in + let typ = let typ = Typeops.infer_type env typ in - Typeops.check_primitive_type env op_t typ.utj_val; + check_primitive_type env p u typ.utj_val; typ.utj_val - | None -> - match op_t with - | CPrimitives.OT_op op -> Typeops.type_of_prim env op - | CPrimitives.OT_type _ -> mkSet in - let cd = - match op_t with - | CPrimitives.OT_op op -> Declarations.Primitive op - | CPrimitives.OT_type _ -> Undef None in - { Cooking.cook_body = cd; - cook_type = ty; - cook_universes = Monomorphic uctxt; - cook_inline = false; - cook_context = None; - cook_relevance = Sorts.Relevant; - } + Monomorphic uctx, typ + + | Some (typ,Polymorphic_entry (unames,uctx)) -> + assert (not (AUContext.is_empty auctx)); + (* push_context will check that the universes aren't repeated in the instance + so comparing the sizes works *) + assert (AUContext.size auctx = UContext.size uctx); + (* No polymorphic primitive uses constraints currently *) + assert (Constraint.is_empty (UContext.constraints uctx)); + let env = push_context ~strict:false uctx env in + (* Now we know that uctx matches the auctx *) + let typ = (Typeops.infer_type env typ).utj_val in + let () = check_primitive_type env p (UContext.instance uctx) typ in + let unames = merge_unames (AUContext.names auctx) unames in + let u, auctx = abstract_universes unames uctx in + let typ = Vars.subst_univs_level_constr (make_instance_subst u) typ in + Polymorphic auctx, typ + in + let body = match p with + | OT_op op -> Declarations.Primitive op + | OT_type _ -> Undef None + | OT_const c -> Def (Mod_subst.from_val (CPrimitives.body_of_prim_const c)) + in + { Cooking.cook_body = body; + cook_type = typ; + cook_universes = univs; + cook_inline = false; + cook_context = None; + cook_relevance = Sorts.Relevant; + } + +let infer_declaration env (dcl : constant_entry) = + match dcl with + | ParameterEntry (ctx,(t,uctx),nl) -> + let env = match uctx with + | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env + in + let j = Typeops.infer env t in + let usubst, univs = Declareops.abstract_universes uctx in + let r = Typeops.assumption_of_judgment env j in + let t = Vars.subst_univs_level_constr usubst j.uj_val in + { + Cooking.cook_body = Undef nl; + cook_type = t; + cook_universes = univs; + cook_relevance = r; + cook_inline = false; + cook_context = ctx; + } + + | PrimitiveEntry entry -> infer_primitive env entry | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in @@ -118,13 +155,13 @@ let infer_declaration env (dcl : constant_entry) = let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic ctx + env, empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in - let sbst, auctx = Univ.abstract_universes nas uctx in - let sbst = Univ.make_instance_subst sbst in + let sbst, auctx = abstract_universes nas uctx in + let sbst = make_instance_subst sbst in env, sbst, Polymorphic auctx in let j = Typeops.infer env body in @@ -171,8 +208,8 @@ let infer_opaque env = function let { opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in - let sbst, auctx = Univ.abstract_universes nas uctx in - let usubst = Univ.make_instance_subst sbst in + let sbst, auctx = abstract_universes nas uctx in + let usubst = make_instance_subst sbst in let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in let def = OpaqueDef () in let typ = Vars.subst_univs_level_constr usubst tj.utj_val in @@ -260,7 +297,7 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out | MonoTyCtx (env, tyj, declared, feedback_id) -> let ((body, uctx), side_eff) = body in let (body, uctx', valid_signatures) = handle env body side_eff in - let uctx = Univ.ContextSet.union uctx uctx' in + let uctx = ContextSet.union uctx uctx' in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = Typeops.infer env body in @@ -273,17 +310,17 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out | PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) -> let ((body, ctx), side_eff) = body in let body, ctx', _ = handle env body side_eff in - let ctx = Univ.ContextSet.union ctx ctx' in + let ctx = ContextSet.union ctx ctx' in (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_subgraph ctx env in - let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let private_univs = on_snd (subst_univs_level_constraints usubst) ctx in let j = Typeops.infer env body in let _ = Typeops.judge_of_cast env j DEFAULTcast tj in let () = check_section_variables env declared tj.utj_val body in let def = Vars.subst_univs_level_constr usubst j.uj_val in let () = feedback_completion_typecheck feedback_id in - def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + def, Opaqueproof.PrivatePolymorphic (AUContext.size auctx, private_univs) (*s Global and local constant declaration. *) @@ -325,13 +362,13 @@ let translate_local_def env _id centry = const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; + const_entry_universes = Monomorphic_entry ContextSet.empty; const_entry_inline_code = false; } in let decl = infer_declaration env (DefinitionEntry centry) in let typ = decl.cook_type in let () = match decl.cook_universes with - | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Monomorphic ctx -> assert (ContextSet.is_empty ctx) | Polymorphic _ -> assert false in let c = match decl.cook_body with diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 42fc6b2e45..ae5c4b6880 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -68,6 +68,7 @@ type ('constr, 'types) ptype_error = | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance + | BadInvert type type_error = (constr, types) ptype_error @@ -159,6 +160,9 @@ let error_disallowed_sprop env = let error_bad_relevance env = raise (TypeError (env, BadRelevance)) +let error_bad_invert env = + raise (TypeError (env, BadInvert)) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -202,3 +206,4 @@ let map_ptype_error f = function | UndeclaredUniverse l -> UndeclaredUniverse l | DisallowedSProp -> DisallowedSProp | BadRelevance -> BadRelevance +| BadInvert -> BadInvert diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index a58d9aa50d..b1f7eb8a34 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error = | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance + | BadInvert type type_error = (constr, types) ptype_error @@ -143,5 +144,7 @@ val error_disallowed_sprop : env -> 'a val error_bad_relevance : env -> 'a +val error_bad_invert : env -> 'a + val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 19d76bfee6..f86c12e1f1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -213,9 +213,20 @@ let type_of_apply env func funt argsv argstv = apply_rec 0 (inject funt) (* Type of primitive constructs *) -let type_of_prim_type _env = function - | CPrimitives.PT_int63 -> Constr.mkSet - | CPrimitives.PT_float64 -> Constr.mkSet +let type_of_prim_type _env u (type a) (prim : a CPrimitives.prim_type) = match prim with + | CPrimitives.PT_int63 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_float64 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_array -> + begin match Univ.Instance.to_array u with + | [|u|] -> + let ty = Constr.mkType (Univ.Universe.make u) in + Constr.mkProd(Context.anonR, ty , ty) + | _ -> anomaly Pp.(str"universe instance for array type should have length 1") + end let type_of_int env = match env.retroknowledge.Retroknowledge.retro_int63 with @@ -228,71 +239,11 @@ let type_of_float env = | None -> raise (Invalid_argument "Typeops.type_of_float: float64 not_defined") -let type_of_prim env t = - let int_ty () = type_of_int env in - let float_ty () = type_of_float env in - let bool_ty () = - match env.retroknowledge.Retroknowledge.retro_bool with - | Some ((ind,_),_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") - in - let compare_ty () = - match env.retroknowledge.Retroknowledge.retro_cmp with - | Some ((ind,_),_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") - in - let f_compare_ty () = - match env.retroknowledge.Retroknowledge.retro_f_cmp with - | Some ((ind,_),_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") - in - let f_class_ty () = - match env.retroknowledge.Retroknowledge.retro_f_class with - | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") - in - let pair_ty fst_ty snd_ty = - match env.retroknowledge.Retroknowledge.retro_pair with - | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) - | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") - in - let carry_ty int_ty = - match env.retroknowledge.Retroknowledge.retro_carry with - | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) - | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") - in - let open CPrimitives in - let tr_prim_type = function - | PT_int63 -> int_ty () - | PT_float64 -> float_ty () in - let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with - | PIT_bool, () -> bool_ty () - | PIT_carry, t -> carry_ty (tr_prim_type t) - | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2) - | PIT_cmp, () -> compare_ty () - | PIT_f_cmp, () -> f_compare_ty () - | PIT_f_class, () -> f_class_ty () in - let tr_type = function - | PITT_ind (i, a) -> tr_ind i a - | PITT_type t -> tr_prim_type t in - let rec nary_op = function - | [] -> assert false - | [ret_ty] -> tr_type ret_ty - | arg_ty :: r -> - let arg_ty = tr_type arg_ty in - Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in - nary_op (types t) - -let type_of_prim_or_type env = let open CPrimitives in - function - | OT_type t -> type_of_prim_type env t - | OT_op op -> type_of_prim env op - -let judge_of_int env i = - make_judge (Constr.mkInt i) (type_of_int env) - -let judge_of_float env f = - make_judge (Constr.mkFloat f) (type_of_float env) +let type_of_array env u = + assert (Univ.Instance.length u = 1); + match env.retroknowledge.Retroknowledge.retro_array with + | Some c -> mkConstU (c,u) + | None -> CErrors.user_err Pp.(str"The type array must be registered before this construction can be typechecked.") (* Type of product *) @@ -354,6 +305,18 @@ let check_cast env c ct k expected_type = with NotConvertible -> error_actual_type env (make_judge c ct) expected_type +let judge_of_int env i = + make_judge (Constr.mkInt i) (type_of_int env) + +let judge_of_float env f = + make_judge (Constr.mkFloat f) (type_of_float env) + +let judge_of_array env u tj defj = + let def = defj.uj_val in + let ty = defj.uj_type in + Array.iter (fun j -> check_cast env j.uj_val j.uj_type DEFAULTcast ty) tj; + make_judge (mkArray(u, Array.map j_val tj, def, ty)) (mkApp (type_of_array env u, [|ty|])) + (* Inductive types. *) (* The type is parametric over the uniform parameters whose conclusion @@ -407,7 +370,20 @@ 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 should_invert_case env ci = + ci.ci_relevance == Sorts.Relevant && + let mib,mip = lookup_mind_specif env ci.ci_ind in + mip.mind_relevance == Sorts.Irrelevant && + (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks + but we don't do special reduction in such cases + + XXX Someday consider more carefully what happens with letin params and arguments + (currently they're squashed, see indtyping) + *) + Array.length mip.mind_nf_lc = 1 && + List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt + +let type_of_case env ci p pt iv 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 @@ -418,6 +394,14 @@ let type_of_case env ci p pt c ct _lf lft = else (warn_bad_relevance_ci (); {ci with ci_relevance=rp}) in let () = check_case_info env pind rp ci in + let () = + let is_inversion = match iv with + | NoInvert -> false + | CaseInvert _ -> true (* contents already checked *) + in + if not (is_inversion = should_invert_case env ci) + then error_bad_invert env + in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in @@ -564,13 +548,22 @@ let rec execute env cstr = | Construct c -> cstr, type_of_constructor env c - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> let c', ct = execute env c in + let iv' = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs;args} -> + let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in + let (ct', _) : constr * Sorts.t = execute_is_type env ct' in + let () = conv_leq false env ct ct' in + let _, args' = decompose_appvect ct' in + if args == args' then iv else CaseInvert {univs;args=args'} + in let p', pt = execute env p in let lf', lft = execute_array env lf in - let ci', t = type_of_case env ci p' pt c' ct lf' lft in - let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr - else mkCase(ci',p',c',lf') + let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in + let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr + else mkCase(ci',p',iv',c',lf') in cstr, t @@ -591,6 +584,23 @@ let rec execute env cstr = (* Primitive types *) | Int _ -> cstr, type_of_int env | Float _ -> cstr, type_of_float env + | Array(u,t,def,ty) -> + (* ty : Type@{u} and all of t,def : ty *) + let ulev = match Univ.Instance.to_array u with + | [|u|] -> u + | _ -> assert false + in + let ty',tyty = execute env ty in + check_cast env ty' tyty DEFAULTcast (mkType (Universe.make ulev)); + let def', def_ty = execute env def in + check_cast env def' def_ty DEFAULTcast ty'; + let ta = type_of_array env u in + let t' = Array.Smart.map (fun x -> + let x', xt = execute env x in + check_cast env x' xt DEFAULTcast ty'; + x') t in + let cstr = if def'==def && t'==t && ty'==ty then cstr else mkArray(u, t',def',ty') in + cstr, mkApp(ta, [|ty'|]) (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -710,14 +720,84 @@ let judge_of_inductive env indu = let judge_of_constructor env cu = make_judge (mkConstructU cu) (type_of_constructor env cu) -let judge_of_case env ci pj cj lfj = +let judge_of_case env ci pj iv cj lfj = let lf, lft = dest_judgev lfj in - let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t + let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t (* Building type of primitive operators and type *) -let check_primitive_type env op_t t = - let inft = type_of_prim_or_type env op_t in - try default_conv ~l2r:false CUMUL env inft t - with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t +let type_of_prim_const env _u c = + let int_ty () = type_of_int env in + match c with + | CPrimitives.Arraymaxlength -> + int_ty () + +let type_of_prim env u t = + let int_ty () = type_of_int env in + let float_ty () = type_of_float env in + let array_ty u a = mkApp(type_of_array env u, [|a|]) in + let bool_ty () = + match env.retroknowledge.Retroknowledge.retro_bool with + | Some ((ind,_),_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") + in + let compare_ty () = + match env.retroknowledge.Retroknowledge.retro_cmp with + | Some ((ind,_),_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") + in + let f_compare_ty () = + match env.retroknowledge.Retroknowledge.retro_f_cmp with + | Some ((ind,_),_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") + in + let f_class_ty () = + match env.retroknowledge.Retroknowledge.retro_f_class with + | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") + in + let pair_ty fst_ty snd_ty = + match env.retroknowledge.Retroknowledge.retro_pair with + | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) + | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") + in + let carry_ty int_ty = + match env.retroknowledge.Retroknowledge.retro_carry with + | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) + | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") + in + let open CPrimitives in + let tr_prim_type (tr_type : ind_or_type -> constr) (type a) (ty : a prim_type) (t : a) = match ty with + | PT_int63 -> int_ty t + | PT_float64 -> float_ty t + | PT_array -> array_ty (fst t) (tr_type (snd t)) + in + let tr_ind (tr_type : ind_or_type -> constr) (type t) (i : t prim_ind) (a : t) = match i, a with + | PIT_bool, () -> bool_ty () + | PIT_carry, t -> carry_ty (tr_type t) + | PIT_pair, (t1, t2) -> pair_ty (tr_type t1) (tr_type t2) + | PIT_cmp, () -> compare_ty () + | PIT_f_cmp, () -> f_compare_ty () + | PIT_f_class, () -> f_class_ty () + in + let rec tr_type n = function + | PITT_ind (i, a) -> tr_ind (tr_type n) i a + | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t + | PITT_param i -> Constr.mkRel (n+i) + in + let rec nary_op n = function + | [] -> assert false + | [ret_ty] -> tr_type n ret_ty + | arg_ty :: r -> + Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r) + in + let params, sign = types t in + assert (AUContext.size (univs t) = Instance.length u); + Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params) + +let type_of_prim_or_type env u = let open CPrimitives in + function + | OT_type t -> type_of_prim_type env u t + | OT_op op -> type_of_prim env u op + | OT_const c -> type_of_prim_const env u c diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e61d5c399e..87a5666fcc 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment + -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment + -> unsafe_judgment array + -> unsafe_judgment (** {6 Type of global references. } *) @@ -113,8 +114,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> GlobRef.t -> Constr.named_context -> unit -val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit - (** Types for primitives *) val type_of_int : env -> types @@ -123,8 +122,16 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment val type_of_float : env -> types val judge_of_float : env -> Float64.t -> unsafe_judgment -val type_of_prim_type : env -> CPrimitives.prim_type -> types -val type_of_prim : env -> CPrimitives.t -> types +val type_of_array : env -> Univ.Instance.t -> types +val judge_of_array : env -> Univ.Instance.t -> unsafe_judgment array -> unsafe_judgment -> unsafe_judgment + +val type_of_prim_type : env -> Univ.Instance.t -> 'a CPrimitives.prim_type -> types +val type_of_prim : env -> Univ.Instance.t -> CPrimitives.t -> types +val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) + +val should_invert_case : env -> case_info -> bool +(** We have case inversion exactly when going from irrelevant nonempty + (ie 1 constructor) inductive to relevant type. *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 0aca4b41ad..6d8aa02dff 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -985,6 +985,8 @@ module AUContext = struct type t = Names.Name.t array constrained + let make names csts : t = names, csts + let repr (inst, cst) = (Array.init (Array.length inst) (fun i -> Level.var i), cst) diff --git a/kernel/univ.mli b/kernel/univ.mli index 7651e34b12..7286fc84cb 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -353,6 +353,10 @@ module AUContext : sig type t + val make : Names.Name.t array -> Constraint.t -> t + (** Build an abstract context. Constraints may be between universe + variables. *) + val repr : t -> UContext.t (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of the context and [cstr] the abstracted Constraint.t. *) diff --git a/kernel/vars.ml b/kernel/vars.ml index a4465c293b..f7e28b0cfe 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -252,6 +252,22 @@ let subst_univs_level_constr subst c = let u' = Univ.subst_univs_level_universe subst u in if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) + + | Case (ci,p,CaseInvert {univs;args},c,br) -> + if Univ.Instance.is_empty univs then Constr.map aux t + else + let univs' = f univs in + if univs' == univs then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) + + | Array (u,elems,def,ty) -> + let u' = f u in + let elems' = CArray.Smart.map aux elems in + let def' = aux def in + let ty' = aux ty in + if u == u' && elems == elems' && def == def' && ty == ty' then t + else (changed := true; mkArray (u',elems',def',ty')) + | _ -> Constr.map aux t in let c' = aux c in @@ -288,6 +304,20 @@ let subst_instance_constr subst c = let u' = Univ.subst_instance_universe subst u in if u' == u then t else (mkSort (Sorts.sort_of_univ u')) + + | Case (ci,p,CaseInvert {univs;args},c,br) -> + let univs' = f univs in + if univs' == univs then Constr.map aux t + else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) + + | Array (u,elems,def,ty) -> + let u' = f u in + let elems' = CArray.Smart.map aux elems in + let def' = aux def in + let ty' = aux ty in + if u == u' && elems == elems' && def == def' && ty == ty' then t + else mkArray (u',elems',def',ty') + | _ -> Constr.map aux t in aux c @@ -309,11 +339,14 @@ let universes_of_constr c = let rec aux s c = match kind c with | Const (_c, u) -> - LSet.fold LSet.add (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> - LSet.fold LSet.add (Instance.levels u) s + 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 + | Array (u,_,_,_) -> + let s = LSet.fold LSet.add (Instance.levels u) s in + Constr.fold aux s c | _ -> Constr.fold aux s c in aux LSet.empty c diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3563407f7e..f78f0d4d1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -76,6 +76,11 @@ and conv_whd env pb k whd1 whd2 cu = | Vfloat64 f1, Vfloat64 f2 -> if Float64.(equal (of_float f1) (of_float f2)) then cu else raise NotConvertible + | Varray t1, Varray t2 -> + if t1 == t2 then cu else + let n = Parray.length_int t1 in + if not (Int.equal n (Parray.length_int t2)) then raise NotConvertible; + Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV k v1 v2 cu) cu t1 t2 | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> @@ -83,7 +88,7 @@ and conv_whd env pb k whd1 whd2 cu = conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ - | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + | Vfloat64 _, _ | Varray _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible and conv_atom env pb k a1 stk1 a2 stk2 cu = diff --git a/kernel/vm.ml b/kernel/vm.ml index f2d033f89b..d8c66bebd2 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -169,7 +169,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ -> + | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ | Varray _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index f4ce953d4a..ec429d5f9e 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -292,6 +292,7 @@ type whd = | Vconstr_block of vblock | Vint64 of int64 | Vfloat64 of float + | Varray of values Parray.t | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -324,6 +325,7 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vconstr_block _b -> str "Vconstr_block" | Vint64 _ -> str "Vint64" | Vfloat64 _ -> str "Vfloat64" + | Varray _ -> str "Varray" | Vatom_stk (_a,_stk) -> str "Vatom_stk" | Vuniv_level _ -> assert false in @@ -403,7 +405,9 @@ let whd_val : values -> whd = else let tag = Obj.tag o in if tag = accu_tag then - if is_accumulate (fun_code o) then whd_accu o [] + if Int.equal (Obj.size o) 1 then + Varray(Obj.obj o) + else if is_accumulate (fun_code o) then whd_accu o [] else Vprod(Obj.obj o) else if tag = Obj.closure_tag || tag = Obj.infix_tag then @@ -456,7 +460,9 @@ let val_of_atom a = val_of_obj (obj_of_atom a) let val_of_int i = (Obj.magic i : values) -let val_of_uint i = (Obj.magic i : values) +let val_of_uint i = (Obj.magic i : structured_values) + +let val_of_parray p = (Obj.magic p : structured_values) let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in @@ -689,6 +695,7 @@ and pr_whd w = | Vconstr_block _b -> str "Vconstr_block" | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")" + | Varray _ -> str "Varray" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = @@ -701,3 +708,13 @@ and pr_zipper z = | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch _s -> str "Zswitch(...)" | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") + +(** Primitives implemented in OCaml *) + +let parray_make = Obj.magic Parray.make +let parray_get = Obj.magic Parray.get +let parray_get_default = Obj.magic Parray.default +let parray_set = Obj.magic Parray.set +let parray_copy = Obj.magic Parray.copy +let parray_reroot = Obj.magic Parray.reroot +let parray_length = Obj.magic Parray.length diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index cd85440fed..f4070a02a3 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -129,6 +129,7 @@ type whd = | Vconstr_block of vblock | Vint64 of int64 | Vfloat64 of float + | Varray of values Parray.t | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -150,6 +151,7 @@ val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values val val_of_uint : Uint63.t -> structured_values +val val_of_parray : structured_values Parray.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" @@ -199,3 +201,12 @@ val bfield : vblock -> int -> values val check_switch : vswitch -> vswitch -> bool val branch_arg : int -> tag * int -> values + +(** Primitives implemented in OCaml, seen as values (to be used as globals) *) +val parray_make : values +val parray_get : values +val parray_get_default : values +val parray_set : values +val parray_copy : values +val parray_reroot : values +val parray_length : values |