diff options
Diffstat (limited to 'kernel')
63 files changed, 1107 insertions, 2054 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8ac1ecc79..a944dbb06 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1032,7 +1032,7 @@ value coq_interprete CHECK_STACK(nargs+1); sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; // Last argument is the pointer to the suspension + *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 435cf0a79..1d5142a5c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; + i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; } and 'a infos = { @@ -314,12 +314,11 @@ let evar_value cache ev = cache.i_sigma ev let create mk_cl flgs env evars = - let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + i_rels = env.env_rel_context.env_rel_map; } in { i_flags = flgs; i_cache = cache } @@ -588,78 +587,95 @@ let mk_clos_deep clos_fun env t = let mk_clos2 = mk_clos_deep mk_clos (* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = +let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x | FAtom c -> exliftn lfts c | FCast (a,k,b) -> - mkCast (constr_fun lfts a, k, constr_fun lfts b) + mkCast (to_constr lfts a, k, to_constr lfts b) | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op | FCaseT (ci,p,c,ve,env) -> - mkCase (ci, constr_fun lfts (mk_clos env p), - constr_fun lfts c, - Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) - | FFix ((op,(lna,tys,bds)),e) -> + 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) + | FFix ((op,(lna,tys,bds)) as fx, e) -> + if is_subs_id e && is_lift_id lfts then + mkFix fx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn n lfts in - mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) - | FCoFix ((op,(lna,tys,bds)),e) -> + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkFix (op, (lna, tys, bds)) + | FCoFix ((op,(lna,tys,bds)) as cfx, e) -> + if is_subs_id e && is_lift_id lfts then + mkCoFix cfx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkCoFix (op, (lna, tys, bds)) | FApp (f,ve) -> - mkApp (constr_fun lfts f, - Array.Fun1.map constr_fun lfts ve) + mkApp (to_constr lfts f, + Array.Fun1.map to_constr lfts ve) | FProj (p,c) -> - mkProj (p,constr_fun lfts c) + mkProj (p,to_constr lfts c) - | FLambda _ -> - let (na,ty,bd) = destFLambda mk_clos2 v in - mkLambda (na, constr_fun lfts ty, - constr_fun (el_lift lfts) bd) + | FLambda (len, tys, f, e) -> + if is_subs_id e && is_lift_id lfts then + Term.compose_lam (List.rev tys) f + else + let subs = comp_subs lfts e in + let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in + let f = subst_constr (subs_liftn len subs) f in + Term.compose_lam (List.rev tys) f | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) + mkProd (n, to_constr lfts t, + to_constr (el_lift lfts) c) | FLetIn (n,b,t,f,e) -> - let fc = mk_clos2 (subs_lift e) f in - mkLetIn (n, constr_fun lfts b, - constr_fun lfts t, - constr_fun (el_lift lfts) fc) + let subs = comp_subs (el_lift lfts) (subs_lift e) in + mkLetIn (n, to_constr lfts b, + to_constr lfts t, + subst_constr subs f) | FEvar ((ev,args),env) -> - mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) - | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + let subs = comp_subs lfts env in + mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) + | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FCLOS (t,env) -> - let fr = mk_clos2 env t in - let unfv = update v fr.norm fr.term in - to_constr constr_fun lfts unfv + if is_subs_id env && is_lift_id lfts then t + else + let subs = comp_subs lfts env in + subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and subst_constr subst c = match Constr.kind c with +| Rel i -> + begin match expand_rel i subst with + | Inl (k, lazy v) -> Vars.lift k v + | Inr (m, _) -> mkRel m + end +| _ -> + Constr.map_with_binders Esubst.subs_lift subst_constr subst c + +and comp_subs el s = + Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s + (* This function defines the correspondance between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) -let term_of_fconstr = - let rec term_of_fconstr_lift lfts v = - match v.term with - | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> - Term.compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx - | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift el_id - - +let term_of_fconstr c = to_constr el_id c (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a @@ -804,10 +820,12 @@ let drop_parameters depth n argstk = constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = + let open Declarations in let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (_,projs,pbs)) when + | PrimRecord infos when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = infos.(snd ind) in (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in @@ -818,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') = let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) term = FProj (Projection.make p true, right) }) projs in argss, [Zapp hstack] - | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) + | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with @@ -1052,7 +1070,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 63daa4a7c..f8f98f0ab 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -244,6 +244,6 @@ val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr -val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr +val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 5ed9b6c67..521f540d2 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -36,7 +36,6 @@ let last_variant_tag = 245 type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive - | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t @@ -51,8 +50,6 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false -| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 -| Const_proj _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_b0 _, _ -> false | Const_bn (t1, a1), Const_bn (t2, a2) -> @@ -66,13 +63,12 @@ let rec hash_structured_constant c = match c with | Const_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_proj p -> combinesmall 3 (Constant.hash p) - | Const_b0 t -> combinesmall 4 (Int.hash t) + | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in let h = Array.fold_left fold 0 a in - combinesmall 5 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + combinesmall 4 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -246,7 +242,6 @@ let pp_sort s = let rec pp_struct_const = function | Const_sort s -> pp_sort s | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i - | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) @@ -309,7 +304,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblb)) | Kpushfields n -> str "pushfields " ++ int n | Kfield n -> str "field " ++ int n - | Ksetfield n -> str "set field" ++ int n + | Ksetfield n -> str "setfield " ++ int n | Kstop -> str "stop" diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 03b6bc619..238edc0af 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -30,7 +30,6 @@ val last_variant_tag : tag type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive - | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index a771945dd..7a27a3d20 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -20,7 +20,7 @@ open Cinstr open Clambda open Constr open Declarations -open Pre_env +open Environ (* Compilation of variables + computing free variables *) @@ -77,6 +77,7 @@ open Pre_env (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) (* If such a block is matched against, we have to force evaluation, *) (* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) (* Once evaluation is completed [ai'] is updated with the result: *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) @@ -398,55 +399,55 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant reloc sc sz cont = +let compile_structured_constant cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont (* compiling application *) -let comp_args comp_expr reloc args sz cont = +let comp_args comp_expr cenv args sz cont = let nargs_m_1 = Array.length args - 1 in - let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in + let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in for i = 1 to nargs_m_1 do - c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) + c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) done; !c -let comp_app comp_fun comp_arg reloc f args sz cont = +let comp_app comp_fun comp_arg cenv f args sz cont = let nargs = Array.length args in - if Int.equal nargs 0 then comp_fun reloc f sz cont + if Int.equal nargs 0 then comp_fun cenv f sz cont else match is_tailcall cont with | Some k -> - comp_args comp_arg reloc args sz + comp_args comp_arg cenv args sz (Kpush :: - comp_fun reloc f (sz + nargs) + comp_fun cenv f (sz + nargs) (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) | None -> if nargs < 4 then - comp_args comp_arg reloc args sz - (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont))) + comp_args comp_arg cenv args sz + (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: - (comp_args comp_arg reloc args (sz + 3) - (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1)))) + (comp_args comp_arg cenv args (sz + 3) + (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) (* Compiling free variables *) -let compile_fv_elem reloc fv sz cont = +let compile_fv_elem cenv fv sz cont = match fv with - | FVrel i -> pos_rel i reloc sz :: cont - | FVnamed id -> pos_named id reloc :: cont - | FVuniv_var i -> pos_universe_var i reloc sz :: cont - | FVevar evk -> pos_evar evk reloc :: cont + | FVrel i -> pos_rel i cenv sz :: cont + | FVnamed id -> pos_named id cenv :: cont + | FVuniv_var i -> pos_universe_var i cenv sz :: cont + | FVevar evk -> pos_evar evk cenv :: cont -let rec compile_fv reloc l sz cont = +let rec compile_fv cenv l sz cont = match l with | [] -> cont - | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont | fvn :: tl -> - compile_fv_elem reloc fvn sz - (Kpush :: compile_fv reloc tl (sz + 1) cont) + compile_fv_elem cenv fvn sz + (Kpush :: compile_fv cenv tl (sz + 1) cont) (* Compiling constants *) @@ -471,58 +472,58 @@ let make_areconst n else_lbl cont = Kareconst (n, else_lbl)::cont (* sz is the size of the local stack *) -let rec compile_lam env reloc lam sz cont = +let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; match lam with - | Lrel(_, i) -> pos_rel i reloc sz :: cont + | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant reloc v sz cont + | Lval v -> compile_structured_constant cenv v sz cont | Lproj (n,kn,arg) -> - compile_lam env reloc arg sz (Kproj (n,kn) :: cont) + compile_lam env cenv arg sz (Kproj (n,kn) :: cont) - | Lvar id -> pos_named id reloc :: cont + | Lvar id -> pos_named id cenv :: cont | Levar (evk, args) -> if Array.is_empty args then - compile_fv_elem reloc (FVevar evk) sz cont + compile_fv_elem cenv (FVevar evk) sz cont else - comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont - | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont | Lind (ind,u) -> if Univ.Instance.is_empty u then - compile_structured_constant reloc (Const_ind ind) sz cont - else comp_app compile_structured_constant compile_universe reloc + compile_structured_constant cenv (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sort s) sz cont + compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes "compacted", i.e. as [u arg0 ... argn] where we will substitute (after evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) let u,s = Univ.compact_univ u in - let compile_get_univ reloc idx sz cont = + let compile_get_univ cenv idx sz cont = set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont + compile_fv_elem cenv (FVuniv_var idx) sz cont in if List.is_empty s then - compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont + compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont else - comp_app compile_structured_constant compile_get_univ reloc + comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont | Llet (id,def,body) -> - compile_lam env reloc def sz + compile_lam env cenv def sz (Kpush :: - compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont)) + compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) | Lprod (dom,codom) -> let cont1 = - Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in - compile_lam env reloc codom sz cont1 + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + compile_lam env cenv codom sz cont1 | Llam (ids,body) -> let arity = Array.length ids in @@ -533,12 +534,12 @@ let rec compile_lam env reloc lam sz cont = in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in - compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) | Lapp (f, args) -> begin match f with - | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont - | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end | Lfix ((rec_args, init), (decl, types, bodies)) -> @@ -570,7 +571,7 @@ let rec compile_lam env reloc lam sz cont = fun_code := [Ksequence(fcode,!fun_code)] done; let fv = !rfv in - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) @@ -606,7 +607,7 @@ let rec compile_lam env reloc lam sz cont = done; let fv = !rfv in set_max_stack_size (sz + fv.size + ndef + 2); - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -624,7 +625,7 @@ let rec compile_lam env reloc lam sz cont = let branch1, cont = make_branch cont in (* Compilation of the return type *) let fcode = - ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop] + ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] in let lbl_typ,fcode = label_code fcode in fun_code := [Ksequence(fcode,!fun_code)]; @@ -652,7 +653,7 @@ let rec compile_lam env reloc lam sz cont = (* Compilation of constant branches *) for i = nconst - 1 downto 0 do let aux = - compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c) + compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c) in let lbl_b,code_b = label_code aux in lbl_consts.(i) <- lbl_b; @@ -664,7 +665,7 @@ let rec compile_lam env reloc lam sz cont = let (ids, body) = branches.nonconstant_branches.(i) in let arity = Array.length ids in let code_b = - compile_lam env (push_param arity sz_b reloc) + compile_lam env (push_param arity sz_b cenv) body (sz_b+arity) (add_pop arity (branch::!c)) in let code_b = if tag < last_variant_tag then begin @@ -702,25 +703,25 @@ let rec compile_lam env reloc lam sz cont = | Kbranch lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - compile_lam env reloc a sz code_sw + compile_lam env cenv a sz code_sw | Lmakeblock (tag,args) -> let arity = Array.length args in let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in - comp_args (compile_lam env) reloc args sz cont + comp_args (compile_lam env) cenv args sz cont | Lprim (kn, ar, op, args) -> - op_compilation env ar op kn reloc args sz cont + op_compilation env ar op kn cenv args sz cont | Luint v -> (match v with - | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont + | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont | UintDigits ds -> let nargs = Array.length ds in if Int.equal nargs 31 then let (escape,labeled_cont) = make_branch cont in let else_lbl = Label.create() in - comp_args (compile_lam env) reloc ds sz + comp_args (compile_lam env) cenv ds sz ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) else let code_construct cont = (* spiwack: variant of the global code_construct @@ -736,40 +737,40 @@ let rec compile_lam env reloc lam sz cont = Kclosure(lbl,0) :: cont in comp_app (fun _ _ _ cont -> code_construct cont) - (compile_lam env) reloc () ds sz cont + (compile_lam env) cenv () ds sz cont | UintDecomp t -> let escape_lbl, labeled_cont = label_code cont in - compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) + compile_lam env cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) -and compile_get_global reloc (kn,u) sz cont = +and compile_get_global cenv (kn,u) sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then Kgetglobal kn :: cont else comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_universe reloc () (Univ.Instance.to_array u) sz cont + compile_universe cenv () (Univ.Instance.to_array u) sz cont -and compile_universe reloc uni sz cont = +and compile_universe cenv uni sz cont = set_max_stack_size sz; match Univ.Level.var_index uni with - | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont - | Some idx -> pos_universe_var idx reloc sz :: cont + | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont + | Some idx -> pos_universe_var idx cenv sz :: cont -and compile_constant env reloc kn u args sz cont = +and compile_constant env cenv kn u args sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then (* normal compilation *) comp_app (fun _ _ sz cont -> - compile_get_global reloc (kn,u) sz cont) - (compile_lam env) reloc () args sz cont + compile_get_global cenv (kn,u) sz cont) + (compile_lam env) cenv () args sz cont else - let compile_arg reloc constr_or_uni sz cont = + let compile_arg cenv constr_or_uni sz cont = match constr_or_uni with - | ArgLambda t -> compile_lam env reloc t sz cont - | ArgUniv uni -> compile_universe reloc uni sz cont + | ArgLambda t -> compile_lam env cenv t sz cont + | ArgUniv uni -> compile_universe cenv uni sz cont in let u = Univ.Instance.to_array u in let lu = Array.length u in @@ -778,7 +779,7 @@ and compile_constant env reloc kn u args sz cont = (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu)) in comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_arg reloc () all sz cont + compile_arg cenv () all sz cont (*template for n-ary operation, invariant: n>=1, the operations does the following : @@ -787,34 +788,34 @@ and compile_constant env reloc kn u args sz cont = 3/ if at least one is not, branches to the normal behavior: Kgetglobal (get_alias !global_env kn) *) and op_compilation env n op = - let code_construct reloc kn sz cont = + let code_construct cenv kn sz cont = let f_cont = let else_lbl = Label.create () in Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: op:: Kreturn 0:: Klabel else_lbl:: (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - compile_get_global reloc kn sz ( + compile_get_global cenv kn sz ( Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) in let lbl = Label.create () in fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun kn reloc args sz cont -> + fun kn cenv args sz cont -> let nargs = Array.length args in if Int.equal nargs n then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in assert (n < 4); - comp_args (compile_lam env) reloc args sz + comp_args (compile_lam env) cenv args sz (Kisconst else_lbl::(make_areconst (n-1) else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: (* works as comp_app with nargs < 4 and non-tailcall cont*) - compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont)))) + compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont)))) else - comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) - (compile_lam env) reloc () args sz cont + comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont) + (compile_lam env) cenv () args sz cont let is_univ_copy max u = @@ -845,11 +846,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c = Label.reset_label_counter (); let cont = [Kstop] in try - let reloc, init_code = + let cenv, init_code = if Int.equal universes 0 then let lam = lambda_of_constr ~optimize:true env c in - let reloc = empty_comp_env () in - reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont + let cenv = empty_comp_env () in + cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. @@ -857,7 +858,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = let lam = lambda_of_constr ~optimize:true env c in let params, body = decompose_Llam lam in let arity = Array.length params in - let reloc = empty_comp_env () in + let cenv = empty_comp_env () in let full_arity = arity + universes in let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in @@ -868,12 +869,12 @@ let compile ~fail_on_error ?universes:(universes=0) env c = fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in let init_code = - ensure_stack_capacity (compile_fv reloc fv.fv_rev 0) + ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) (Kclosure(lbl_fun,fv.size) :: cont) in - reloc, init_code + cenv, init_code in - let fv = List.rev (!(reloc.in_env).fv_rev) in + let fv = List.rev (!(cenv.in_env).fv_rev) in (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) @@ -921,13 +922,13 @@ let op2_compilation op = fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun normal fc _ reloc args sz cont -> + fun normal fc _ cenv args sz cont -> if not fc then raise Not_found else let nargs = Array.length args in if nargs=2 then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in - comp_args compile_constr reloc args sz + comp_args compile_constr cenv args sz (Kisconst else_lbl::(make_areconst 1 else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: @@ -939,5 +940,5 @@ let op2_compilation op = code_construct normal cont else comp_app (fun _ _ _ cont -> code_construct normal cont) - compile_constr reloc () args sz cont *) + compile_constr cenv () args sz cont *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 1c4cdcbeb..57d3e6fc2 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -12,7 +12,7 @@ open Cbytecodes open Cemitcodes open Constr open Declarations -open Pre_env +open Environ (** Should only be used for monomorphic terms *) val compile : fail_on_error:bool -> diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index cea09c510..2426255e4 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,7 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Term +open Constr open Cbytecodes open Copcodes open Mod_subst @@ -27,6 +27,7 @@ type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t + | Reloc_proj_name of Constant.t let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 @@ -35,6 +36,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_const _, _ -> false | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 | Reloc_getglobal _, _ -> false +| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2 +| Reloc_proj_name _, _ -> false let hash_reloc_info r = let open Hashset.Combine in @@ -42,6 +45,7 @@ let hash_reloc_info r = | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) | Reloc_const c -> combinesmall 2 (hash_structured_constant c) | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) + | Reloc_proj_name p -> combinesmall 4 (Constant.hash p) module RelocTable = Hashtbl.Make(struct type t = reloc_info @@ -187,6 +191,9 @@ let slot_for_getglobal env p = enter env (Reloc_getglobal p); out_int env 0 +let slot_for_proj_name env p = + enter env (Reloc_proj_name p); + out_int env 0 (* Emission of one instruction *) @@ -277,7 +284,7 @@ let emit_instr env = function if n <= 1 then out env (opSETFIELD0+n) else (out env opSETFIELD;out_int env n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p) + | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) | Kbranch lbl -> out env opBRANCH; out_label env lbl @@ -353,7 +360,6 @@ type to_patch = emitcodes * patches * fv let rec subst_strcst s sc = match sc with | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc - | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) @@ -365,6 +371,7 @@ let subst_reloc s ri = Reloc_annot {a with ci = ci} | 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_constant s p) 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 03920dc1a..696721c37 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -5,6 +5,7 @@ type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Constant.t + | Reloc_proj_name of Constant.t type patches type emitcodes diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 4a3c03d85..f42c46175 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -31,7 +31,7 @@ and lambda = | Lprim of pconstant * int (* arity *) * instruction * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array | Lval of structured_constant | Lsort of Sorts.t @@ -39,6 +39,10 @@ and lambda = | Lproj of int * Constant.t * lambda | Luint of uint +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = { constant_branches : lambda array; nonconstant_branches : (Name.t array * lambda) array } diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 0727eaeac..b722e4200 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -6,7 +6,7 @@ open Constr open Declarations open Cbytecodes open Cinstr -open Pre_env +open Environ open Pp let pr_con sp = str(Names.Label.to_string (Constant.label sp)) @@ -700,6 +700,7 @@ let rec lambda_of_constr env c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env 0 rec_bodies in @@ -707,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 6cf46163e..8ff10b454 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -1,13 +1,14 @@ open Names open Cinstr +open Environ exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t array * lambda -val get_alias : Pre_env.env -> Constant.t -> Constant.t +val get_alias : env -> Constant.t -> Constant.t val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda diff --git a/kernel/constr.ml b/kernel/constr.ml index 8f83d6baa..418229330 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array -type rec_declaration = Name.t array * constr array * constr array -type fixpoint = (int array * int) * rec_declaration - (* The array of [int]'s tells for each component of the array of - mutual fixpoints the number of lambdas to skip before finding the - recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) - (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is - the recursive argument); - The second component [int] tells which component of the block is - returned *) -type cofixpoint = int * rec_declaration - (* The component [int] tells which component of the block of - cofixpoint is returned *) type types = constr +type rec_declaration = (constr, types) prec_declaration +type fixpoint = (constr, types) pfixpoint +type cofixpoint = (constr, types) pcofixpoint + (*********************) (* Term constructors *) (*********************) @@ -479,6 +471,34 @@ let iter_with_binders g f n c = match kind c with Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl +(* [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 + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g n) (f n acc t) c + | Lambda (na,t,c) -> f (g n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let 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 + (* [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 *) diff --git a/kernel/constr.mli b/kernel/constr.mli index b35ea6653..bf7b5e87b 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) -type rec_declaration = Name.t array * types array * constr array -type fixpoint = (int array * int) * rec_declaration +type ('constr, 'types) prec_declaration = + Name.t array * 'types array * 'constr array +type ('constr, 'types) pfixpoint = + (int array * int) * ('constr, 'types) prec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) + +type ('constr, 'types) pcofixpoint = + int * ('constr, 'types) prec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) + +type rec_declaration = (constr, types) prec_declaration + +type fixpoint = (constr, types) pfixpoint val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] @@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr ... with fn = bn.] *) -type cofixpoint = int * rec_declaration +type cofixpoint = (constr, types) pcofixpoint val mkCoFix : cofixpoint -> constr @@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = Evar.t * 'constr array -type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) @@ -402,6 +414,15 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> 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 + each binder traversal; it is not recursive and the order with which + subterms are processed is not specified *) + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + type constr_compare_fn = int -> constr -> constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e95..c7a84f617 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,16 +126,15 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in - let make c = Projection.make c (Projection.unfolded p) in - match kind p' with - | Const (p',_) -> mkProj (make p', substrec c') - | App (f, args) -> - (match kind f with - | Const (p', _) -> mkProj (make p', substrec c') - | _ -> assert false) - | _ -> assert false + (try + (** No need to expand parameters or universes for projections *) + let map cst = + let _ = Cmap.find cst (fst modlist) in + pop_con cst + in + let p = Projection.map map p in + let c' = substrec c' in + mkProj (p, c') with Not_found -> Constr.map substrec c) | _ -> Constr.map substrec c @@ -156,7 +155,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +225,9 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae566..76c79335f 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 4f3cbf289..bbe093782 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -20,7 +20,7 @@ open Vmvalues open Cemitcodes open Cbytecodes open Declarations -open Pre_env +open Environ open Cbytegen module NamedDecl = Context.Named.Declaration @@ -77,11 +77,19 @@ module AnnotTable = Hashtbl.Make (struct let hash = hash_annot_switch end) +module ProjNameTable = Hashtbl.Make (struct + type t = Constant.t + let equal = Constant.equal + let hash = Constant.hash +end) + let str_cst_tbl : int SConstTable.t = SConstTable.create 31 let annot_tbl : int AnnotTable.t = AnnotTable.create 31 (* (annot_switch * int) Hashtbl.t *) +let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31 + (*************************************************************) (*** Mise a jour des valeurs des variables et des constantes *) (*************************************************************) @@ -115,6 +123,13 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n +let slot_for_proj_name key = + try ProjNameTable.find proj_name_tbl key + with Not_found -> + let n = set_global (val_of_proj_name key) in + ProjNameTable.add proj_name_tbl key n; + n + let rec slot_for_getglobal env kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk @@ -142,23 +157,23 @@ and slot_for_fv env fv = | None -> v_of_id id, Id.Set.empty | Some c -> val_of_constr (env_of_id id env) c, - Environ.global_vars_set (Environ.env_of_pre_env env) c in + Environ.global_vars_set env c in build_lazy_val cache (v, d); v in let val_of_rel i = val_of_rel (nb_rel env - i) in let idfun _ x = x in match fv with | FVnamed id -> - let nv = Pre_env.lookup_named_val id env in + let nv = lookup_named_val id env in begin match force_lazy_val nv with | None -> - env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun + env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> - let rv = Pre_env.lookup_rel_val i env in + let rv = lookup_rel_val i env in begin match force_lazy_val rv with | None -> - env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVevar evk -> val_of_evar evk @@ -170,6 +185,7 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_annot a -> slot_for_annot a | 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 in let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index d32cfba36..72c96b0b9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,7 +12,7 @@ open Names open Constr -open Pre_env +open Environ val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a..58fb5d66b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -50,12 +50,10 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; - proj_arg : int; + proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) - proj_eta : constr * types; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility with VMs only, the match version *) } (* Global declarations (i.e. constants) can be either: *) @@ -87,7 +85,6 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for @@ -112,13 +109,22 @@ v} *) (** Record information: - If the record is not primitive, then None - Otherwise, we get: + If the type is not a record, then NotRecord + If the type is a non-primitive record, then FakeRecord + If it is a primitive record, for every type in the block, we get: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - - The checked projection bodies. *) + - The checked projection bodies. -type record_body = (Id.t * Constant.t array * projection_body array) option + The kernel does not exploit the difference between [NotRecord] and + [FakeRecord]. It is mostly used by extraction, and should be extruded from + the kernel at some point. +*) + +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : types; @@ -184,7 +190,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** The record information *) + mind_record : record_info; (** The record information *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 832d478b3..3e6c4858e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -84,9 +84,9 @@ let subst_const_def sub def = match def with | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) let subst_const_proj sub pb = - { pb with proj_ind = subst_mind sub pb.proj_ind; + { pb with proj_ind = subst_ind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; - proj_body = subst_const_type sub pb.proj_body } + } let subst_const_body sub cb = assert (List.is_empty cb.const_hyps); (* we're outside sections *) @@ -94,14 +94,12 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; @@ -210,14 +208,21 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (id, ps, pb as r) = - let ps' = Array.Smart.map (subst_constant sub) ps in - let pb' = Array.Smart.map (subst_const_proj sub) pb in - if ps' == ps && pb' == pb then r +let subst_mind_record sub r = match r with +| NotRecord -> NotRecord +| FakeRecord -> FakeRecord +| PrimRecord infos -> + let map (id, ps, pb as info) = + let ps' = Array.Smart.map (subst_constant sub) ps in + let pb' = Array.Smart.map (subst_const_proj sub) pb in + if ps' == ps && pb' == pb then info else (id, ps', pb') + in + let infos' = Array.Smart.map map infos in + if infos' == infos then r else PrimRecord infos' let subst_mind_body sub mib = - { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; + { mind_record = subst_mind_record sub mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7e..724ed9ec7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -49,9 +49,9 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : (Id.t option) option; - (** Some (Some id): primitive record with id the binder name of the record - in projections. + mind_entry_record : (Id.t array option) option; + (** Some (Some ids): primitive records with ids the binder name of each + record in their respective projections. Not used by the kernel. Some None: non-primitive record *) mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; @@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.Named.t option * types in_constant_universes_entry * inline -type projection_entry = { - proj_entry_ind : MutInd.t; - proj_entry_arg : int } - type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry - | ProjectionEntry of projection_entry (** {6 Modules } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 9d4063e43..0e34a7165 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -28,26 +28,206 @@ open Names open Constr open Vars open Declarations -open Pre_env open Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* The type of environments. *) -type named_context_val = Pre_env.named_context_val +(* The key attached to each constant is used by the VM to retrieve previous *) +(* evaluations of the constant. It is essentially an index in the symbols table *) +(* used by the VM. *) +type key = int CEphemeron.key option ref + +(** Linking information for the native compiler. *) + +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type val_kind = + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key + | VKnone + +type lazy_val = val_kind ref + +let force_lazy_val vk = match !vk with +| VKnone -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None + +let dummy_lazy_val () = ref VKnone +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) + +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} + +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} + +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + +let empty_env = { + env_globals = { + env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_modules = MPmap.empty; + env_modtypes = MPmap.empty}; + env_named_context = empty_named_context_val; + env_rel_context = empty_rel_context_val; + env_nb_rel = 0; + env_stratification = { + env_universes = UGraph.initial_universes; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } + + +(* Rel context *) + +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + +let push_rel d env = + { env with + env_rel_context = push_rel_context_val d env.env_rel_context; + env_nb_rel = env.env_nb_rel + 1 } + +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let lookup_rel_val n env = + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} + +let env_of_rel n env = + { env with + env_rel_context = rel_skipn n env.env_rel_context; + env_nb_rel = env.env_nb_rel - n + } + +(* Named context *) + +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } + +let push_named d env = + {env with env_named_context = push_named_context_val d env.env_named_context} + +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_val id env = + snd(Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_ctxt id ctxt = + fst (Id.Map.find id ctxt.env_named_map) + +(* Global constants *) -type env = Pre_env.env +let lookup_constant_key kn env = + Cmap_env.find kn env.env_globals.env_constants + +let lookup_constant kn env = + fst (Cmap_env.find kn env.env_globals.env_constants) + +(* Mutual Inductives *) +let lookup_mind kn env = + fst (Mindmap_env.find kn env.env_globals.env_inductives) + +let lookup_mind_key kn env = + Mindmap_env.find kn env.env_globals.env_inductives -let pre_env env = env -let env_of_pre_env env = env let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in { env with env_typing_flags } -let empty_named_context_val = empty_named_context_val - -let empty_env = empty_env - let engagement env = env.env_stratification.env_engagement let typing_flags env = env.env_typing_flags @@ -72,15 +252,11 @@ let empty_context env = | _ -> false (* Rel context *) -let lookup_rel = lookup_rel - let evaluable_rel n env = is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel -let push_rel = push_rel - let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = @@ -105,24 +281,14 @@ let named_context_of_val c = c.env_named_ctx let ids_of_named_context_val c = Id.Map.domain c.env_named_map -(* [map_named_val f ctxt] apply [f] to the body and the type of - each declarations. - *** /!\ *** [f t] should be convertible with t *) -let map_named_val = map_named_val - let empty_named_context = Context.Named.empty -let push_named = push_named let push_named_context = List.fold_right push_named -let push_named_context_val = push_named_context_val let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named = lookup_named -let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) - let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) @@ -181,7 +347,10 @@ let map_universes f env = let s = env.env_stratification in { env with env_stratification = { s with env_universes = f s.env_universes } } - + +let set_universes env u = + { env with env_stratification = { env.env_stratification with env_universes = u } } + let add_constraints c env = if Univ.Constraint.is_empty c then env else map_universes (UGraph.merge_constraints c) env @@ -221,8 +390,6 @@ let set_typing_flags c env = (* Unsafe *) (* Global constants *) -let lookup_constant = lookup_constant - let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = @@ -320,18 +487,12 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + Cmap_env.mem cst env.env_globals.env_projections (* Mutual Inductives *) -let lookup_mind = lookup_mind - let polymorphic_ind (mind,i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) @@ -351,11 +512,19 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | NotRecord | FakeRecord -> env.env_globals.env_projections + | PrimRecord projs -> + Array.fold_left (fun accu (id, kns, pbs) -> + Array.fold_left2 (fun accu kn pb -> + Cmap_env.add kn pb accu) accu kns pbs) + env.env_globals.env_projections projs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -468,10 +637,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(*s Compilation of global declaration *) - -let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false - exception Hyp_not_found let apply_to_hyp ctxt id f = @@ -530,121 +695,3 @@ let register env field entry = in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry - -(* the Environ.register function syncrhonizes the proactive and reactive - retroknowledge. *) -let dispatch = - - (* subfunction used for static decompilation of int31 (after a vm_compute, - see pretyping/vnorm.ml for more information) *) - let constr_of_int31 = - let nth_digit_plus_one i n = (* calculates the nth (starting with 0) - digit of i and adds 1 to it - (nth_digit_plus_one 1 3 = 2) *) - if Int.equal (i land (1 lsl n)) 0 then - 1 - else - 2 - in - fun ind -> fun digit_ind -> fun tag -> - let array_of_int i = - Array.init 31 (fun n -> mkConstruct - (digit_ind, nth_digit_plus_one i (30-n))) - in - (* We check that no bit above 31 is set to one. This assertion used to - fail in the VM, and led to conversion tests failing at Qed. *) - assert (Int.equal (tag lsr 31) 0); - mkApp(mkConstruct(ind, 1), array_of_int tag) - in - - (* subfunction which dispatches the compiling information of an - int31 operation which has a specific vm instruction (associates - it to the name of the coq definition in the reactive retroknowledge) *) - let int31_op n op prim kn = - { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); - } - in - -fun rk value field -> - (* subfunction which shortens the (very common) dispatch of operations *) - let int31_op_from_const n op prim = - match kind value with - | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") - in - let int31_binop_from_const op prim = int31_op_from_const 2 op prim in - let int31_unop_from_const op prim = int31_op_from_const 1 op prim in - match field with - | KInt31 (grp, Int31Type) -> - let int31bit = - (* invariant : the type of bits is registered, otherwise the function - would raise Not_found. The invariant is enforced in safe_typing.ml *) - match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) - | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") - in - let i31bit_type = - match kind int31bit with - | Ind (i31bit_type,_) -> i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type.") - in - let int31_decompilation = - match kind value with - | Ind (i31t,_) -> - constr_of_int31 i31t i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type.") - in - { empty_reactive_info with - vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Clambda.int31_escape_before_match; - native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); - } - | KInt31 (_, Int31Constructor) -> - { empty_reactive_info with - vm_constant_static = Some Clambda.compile_structured_int31; - vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; - native_constant_static = Some Nativelambda.compile_static_int31; - native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; - } - | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - CPrimitives.Int31lxor - | _ -> empty_reactive_info - -let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/environ.mli b/kernel/environ.mli index fdd84b25b..8928b32f1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -28,16 +28,61 @@ open Declarations - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) +type lazy_val + +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option +val dummy_lazy_val : unit -> lazy_val + +(** Linking information for the native compiler *) +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type key = int CEphemeron.key option ref + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t +} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = private { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = private { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} - - -type env -val pre_env : env -> Pre_env.env -val env_of_pre_env : Pre_env.env -> env val oracle : env -> Conv_oracle.oracle val set_oracle : env -> Conv_oracle.oracle -> env -type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env @@ -70,7 +115,9 @@ val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> Context.Rel.Declaration.t +val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool +val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) @@ -102,7 +149,8 @@ val push_named_context_val : raises [Not_found] if the Id.t is not found *) val lookup_named : variable -> env -> Context.Named.Declaration.t -val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named_val : variable -> env -> lazy_val +val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -112,6 +160,8 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a +val set_universes : env -> UGraph.t -> env + (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a @@ -129,8 +179,9 @@ val pop_rel_context : int -> env -> env {6 Add entries to global environment } *) val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> +val add_constant_key : Constant.t -> constant_body -> link_info -> env -> env +val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) @@ -172,7 +223,8 @@ val lookup_projection : Names.Projection.t -> env -> projection_body val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val lookup_mind_key : MutInd.t -> env -> mind_key +val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names @@ -251,10 +303,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(** {6 Compilation of global declaration } *) - -val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option - exception Hyp_not_found (** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and @@ -264,7 +312,7 @@ val apply_to_hyp : named_context_val -> variable -> (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val @@ -278,4 +326,4 @@ val registered : env -> field -> bool val register : env -> field -> Retroknowledge.entry -> env (** Native compiler *) -val no_link_info : Pre_env.link_info +val no_link_info : link_info diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 4b8edf63f..9fc3b11d7 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -134,6 +134,29 @@ let rec exp_rel lams k subs = let expand_rel k subs = exp_rel 0 k subs +let rec subs_map f = function +| ESID _ as s -> s +| CONS (x, s) -> CONS (Array.map f x, subs_map f s) +| SHIFT (n, s) -> SHIFT (n, subs_map f s) +| LIFT (n, s) -> LIFT (n, subs_map f s) + +let rec lift_subst mk_cl s1 s2 = match s1 with +| ELID -> subs_map (fun c -> mk_cl ELID c) s2 +| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2) +| ELLFT (k, s) -> + match s2 with + | CONS(x,s') -> + CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s') + | ESID n -> lift_subst mk_cl s (ESID (n + k)) + | SHIFT(k',s') -> + if k<k' + then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s'))) + else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s') + | LIFT(k',s') -> + if k<k' + then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s')) + else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s') + let rec comp mk_cl s1 s2 = match (s1, s2) with | _, ESID _ -> s1 diff --git a/kernel/esubst.mli b/kernel/esubst.mli index a674c425a..475b64f47 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift val el_lift : lift -> lift val reloc_rel : int -> lift -> int val is_lift_id : lift -> bool + +(** Lift applied to substitution: [lift_subst mk_clos el s] computes a + substitution equivalent to applying el then s. Argument + mk_clos is used when a closure has to be created, i.e. when + el is applied on an element of s. +*) +val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 439acd15b..e63f43849 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -797,65 +797,43 @@ exception UndefinableExpansion build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params - mind_consnrealdecls mind_consnrealargs paramslet ctx = +let compute_projections (kn, i as ind) mib = + let pkt = mib.mind_packets.(i) in + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx + | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) + in + let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in + let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) - let indty, paramsletsubst = - (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in - let ty = mkApp (mkIndU indu, inst) in + let paramsletsubst = (* [Ind inst] is typed in context [params-wo-let] *) - let inst' = rel_list 0 nparamargs in + let inst' = rel_list 0 mib.mind_nparams in (* {params-wo-let |- subst:params] *) let subst = subst_of_rel_context_instance paramslet inst' in (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst in - ty, subst - in - let ci = - let print_info = - { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in - { ci_ind = ind; - ci_npar = nparamargs; - ci_cstr_ndecls = mind_consnrealdecls; - ci_cstr_nargs = mind_consnrealargs; - ci_pp_info = print_info } - in - let len = List.length ctx in - let x = Name x in - let compat_body ccl i = - (* [ccl] is defined in context [params;x:indty] *) - (* [ccl'] is defined in context [params;x:indty;x:indty] *) - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 indty, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in - let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in - it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params + subst in - let projections decl (i, j, kns, pbs, subst, letsubst) = + let projections decl (i, j, kns, pbs, letsubst) = match decl with | LocalDef (na,c,t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] - to [params, x:I |- c(params,proj1 x,..,projj x)] *) - let c1 = substl subst c in - (* From [params, x:I |- subst:field1,..,fieldj] - to [params, x:I |- subst:field1,..,fieldj+1] where [subst] - is represented with instance of field1 last *) - let subst = c1 :: subst in - (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) let c2 = substl letsubst c in (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in - (i, j+1, kns, pbs, subst, letsubst) + (i, j+1, kns, pbs, letsubst) | LocalAssum (na,t) -> match na with | Name id -> @@ -868,21 +846,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let projty = substl letsubst t in (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) - let ty = substl subst t in - let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in - let compat = compat_body ty (j - 1) in - let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in - let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in - let body = { proj_ind = fst ind; proj_npars = nparamargs; - proj_arg = i; proj_type = projty; proj_eta = etab, etat; - proj_body = compat } in - (i + 1, j + 1, kn :: kns, body :: pbs, - fterm :: subst, fterm :: letsubst) + let body = { proj_ind = ind; proj_npars = mib.mind_nparams; + proj_arg = i; proj_type = projty; } in + (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, kns, pbs, subst, letsubst) = - List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst) + let (_, _, kns, pbs, letsubst) = + List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev kns), Array.of_list (List.rev pbs) @@ -969,33 +940,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in - let pkt = packets.(0) in - let isrecord = - match isrecord with - | Some (Some rid) when pkt.mind_kelim == all_sorts - && Array.length pkt.mind_consnames == 1 - && pkt.mind_consnrealargs.(0) > 0 -> - (** The elimination criterion ensures that all projections can be defined. *) - let u = - match aiu with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx - | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) - in - let indsp = ((kn, 0), u) in - let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in - (try - let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in - let kns, projs = - compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt - pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields - in Some (Some (rid, kns, projs)) - with UndefinableExpansion -> Some None) - | Some _ -> Some None - | None -> None - in - (* Build the mutual inductive *) - { mind_record = isrecord; + let mib = + (* Build the mutual inductive *) + { mind_record = NotRecord; mind_ntypes = ntypes; mind_finite = isfinite; mind_hyps = hyps; @@ -1007,6 +954,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_private = prv; mind_typing_flags = Environ.typing_flags env; } + in + let record_info = match isrecord with + | Some (Some rid) -> + let is_record pkt = + pkt.mind_kelim == all_sorts + && Array.length pkt.mind_consnames == 1 + && pkt.mind_consnrealargs.(0) > 0 + in + (** The elimination criterion ensures that all projections can be defined. *) + if Array.for_all is_record packets then + let map i id = + let kn, projs = compute_projections (kn, i) mib in + (id, kn, projs) + in + try PrimRecord (Array.mapi map rid) + with UndefinableExpansion -> FakeRecord + else FakeRecord + | Some None -> FakeRecord + | None -> NotRecord + in + { mib with mind_record = record_info } (************************************************************************) (************************************************************************) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a38172c2..7c36dac67 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,5 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_projections : pinductive -> Id.t -> Id.t -> - int -> Context.Rel.t -> int array -> int array -> - Context.Rel.t -> Context.Rel.t -> - (Constant.t array * projection_body array) +val compute_projections : inductive -> + mutual_inductive_body -> (Constant.t array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb..9130b8778 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -293,8 +293,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (Some _) -> true - | _ -> false + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5d270125a..50713b957 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -22,15 +22,17 @@ CPrimitives Declareops Retroknowledge Conv_oracle -Pre_env +Environ +CClosure +Reduction Clambda Nativelambda Cbytegen Nativecode Nativelib -Environ -CClosure -Reduction +Csymtable +Vm +Vconv Nativeconv Type_errors Modops @@ -43,6 +45,3 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Csymtable -Vm -Vconv diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 0027ebecf..a47af56ca 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -24,7 +24,7 @@ open Constr is the term into which we should inline. *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t (* NB: earlier constructor Prefix_equiv of ModPath.t @@ -158,7 +158,7 @@ let find_prefix resolve mp = (** Applying a resolver to a kernel name *) -exception Change_equiv_to_inline of (int * constr) +exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr)) let solve_delta_kn resolve kn = try @@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) = let knu = KerName.make mpu dir l in let knc = if mpu == mpc then knu else KerName.make mpc dir l in match search_delta_inline resolve knu knc with - | Some t -> + | Some (ctx, t) -> (* In case of inlining, discard the canonical part (cf #2608) *) - Constant.make1 knu, t + let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in + Constant.make1 knu, Vars.subst_instance_constr u t | None -> let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc @@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver = | Equiv kequ -> (try Equiv (subst_kn_delta subst kequ) with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c)) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index b14d39207..76a1d173b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -28,7 +28,7 @@ val add_kn_delta_resolver : KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 1baab7c98..d63dc057b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -120,7 +120,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = const_body = def; const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' cb.const_universes def) } + (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index 203817118..22f523a9a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + let ctx = Declareops.constant_polymorphic_context constant in + add_inline_delta_resolver kn (lev, Some (ctx, constr)) l with Not_found -> error_no_such_label_sub (Constant.label con) (ModPath.to_string (Constant.modpath con)) diff --git a/kernel/modops.mli b/kernel/modops.mli index cb41a5123..ac76d28cf 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -52,7 +52,7 @@ val add_module : module_body -> env -> env (** same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated. *) -val add_linked_module : module_body -> Pre_env.link_info -> env -> env +val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env diff --git a/kernel/names.ml b/kernel/names.ml index 58d311dd5..1d2a7c4ce 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ the module system, Aug 2002 *) (* Abstraction over the type of constant for module inlining by Claudio Sacerdoti, Nov 2004 *) -(* Miscellaneous features or improvements by Hugo Herbelin, +(* Miscellaneous features or improvements by Hugo Herbelin, Élie Soubiran, ... *) open Pp @@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath) module KerName = struct type t = { - canary : Canary.t; modpath : ModPath.t; dirpath : DirPath.t; knlabel : Label.t; @@ -372,16 +371,14 @@ module KerName = struct (** Lazily computed hash. If unset, it is set to negative values. *) } - let canary = Canary.obj - type kernel_name = t let make modpath dirpath knlabel = - { modpath; dirpath; knlabel; refhash = -1; canary; } + { modpath; dirpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.dirpath, kn.knlabel) let make2 modpath knlabel = - { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; } + { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; } let modpath kn = kn.modpath let label kn = kn.knlabel @@ -437,7 +434,7 @@ module KerName = struct * (string -> string) let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in - { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } + { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; } let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel @@ -760,55 +757,8 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (*******************************************************************) (** Compatibility layers *) -(** Backward compatibility for [Id] *) - -type identifier = Id.t - -let id_eq = Id.equal -let id_ord = Id.compare -let string_of_id = Id.to_string -let id_of_string = Id.of_string - -module Idset = Id.Set -module Idmap = Id.Map -module Idpred = Id.Pred - -(** Compatibility layer for [Name] *) - -let name_eq = Name.equal - -(** Compatibility layer for [DirPath] *) - -type dir_path = DirPath.t -let dir_path_ord = DirPath.compare -let dir_path_eq = DirPath.equal -let make_dirpath = DirPath.make -let repr_dirpath = DirPath.repr -let empty_dirpath = DirPath.empty -let is_empty_dirpath = DirPath.is_empty -let string_of_dirpath = DirPath.to_string -let initial_dir = DirPath.initial - -(** Compatibility layer for [MBId] *) - type mod_bound_id = MBId.t -let mod_bound_id_ord = MBId.compare -let mod_bound_id_eq = MBId.equal -let make_mbid = MBId.make -let repr_mbid = MBId.repr -let debug_string_of_mbid = MBId.debug_to_string -let string_of_mbid = MBId.to_string -let id_of_mbid = MBId.to_id - -(** Compatibility layer for [Label] *) - -type label = Id.t -let mk_label = Label.make -let string_of_label = Label.to_string -let pr_label = Label.print -let id_of_label = Label.to_id -let label_of_id = Label.of_id -let eq_label = Label.equal +let eq_constant_key = Constant.UserOrd.equal (** Compatibility layer for [ModPath] *) @@ -816,32 +766,13 @@ type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t -let check_bound_mp = ModPath.is_bound -let string_of_mp = ModPath.to_string -let mp_ord = ModPath.compare -let mp_eq = ModPath.equal -let initial_path = ModPath.initial - -(** Compatibility layer for [KerName] *) - -type kernel_name = KerName.t -let make_kn = KerName.make -let repr_kn = KerName.repr -let modpath = KerName.modpath -let label = KerName.label -let string_of_kn = KerName.to_string -let pr_kn = KerName.print -let kn_ord = KerName.compare (** Compatibility layer for [Constant] *) -type constant = Constant.t - +module Projection = +struct + type t = Constant.t * bool -module Projection = -struct - type t = constant * bool - let make c b = (c, b) let constant = fst @@ -906,6 +837,9 @@ module GlobRef = struct end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t @@ -916,39 +850,8 @@ let eq_egr e1 e2 = match e1, e2 with | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false -let constant_of_kn = Constant.make1 -let constant_of_kn_equiv = Constant.make -let make_con = Constant.make3 -let repr_con = Constant.repr3 -let canonical_con = Constant.canonical -let user_con = Constant.user -let con_label = Constant.label -let con_modpath = Constant.modpath -let eq_constant = Constant.equal -let eq_constant_key = Constant.UserOrd.equal -let con_ord = Constant.CanOrd.compare -let con_user_ord = Constant.UserOrd.compare -let string_of_con = Constant.to_string -let pr_con = Constant.print -let debug_string_of_con = Constant.debug_to_string -let debug_pr_con = Constant.debug_print -let con_with_label = Constant.change_label - -(** Compatibility layer for [MutInd] *) - -type mutual_inductive = MutInd.t -let mind_of_kn = MutInd.make1 -let mind_of_kn_equiv = MutInd.make -let make_mind = MutInd.make3 -let canonical_mind = MutInd.canonical -let user_mind = MutInd.user -let repr_mind = MutInd.repr3 -let mind_label = MutInd.label -let mind_modpath = MutInd.modpath -let eq_mind = MutInd.equal -let mind_ord = MutInd.CanOrd.compare -let mind_user_ord = MutInd.UserOrd.compare -let string_of_mind = MutInd.to_string -let pr_mind = MutInd.print -let debug_string_of_mind = MutInd.debug_to_string -let debug_pr_mind = MutInd.debug_print +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index 566fcd0f9..4eb5adb62 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -538,116 +538,8 @@ val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) -(** {5 Identifiers} *) - -type identifier = Id.t -[@@ocaml.deprecated "Alias for [Id.t]"] - -val string_of_id : Id.t -> string -[@@ocaml.deprecated "Same as [Id.to_string]."] - -val id_of_string : string -> Id.t -[@@ocaml.deprecated "Same as [Id.of_string]."] - -val id_ord : Id.t -> Id.t -> int -[@@ocaml.deprecated "Same as [Id.compare]."] - -val id_eq : Id.t -> Id.t -> bool -[@@ocaml.deprecated "Same as [Id.equal]."] - -module Idset : Set.S with type elt = Id.t and type t = Id.Set.t -[@@ocaml.deprecated "Same as [Id.Set]."] - -module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t -[@@ocaml.deprecated "Same as [Id.Pred]."] - -module Idmap : module type of Id.Map -[@@ocaml.deprecated "Same as [Id.Map]."] - -(** {5 Directory paths} *) - -type dir_path = DirPath.t -[@@ocaml.deprecated "Alias for [DirPath.t]."] - -val dir_path_ord : DirPath.t -> DirPath.t -> int -[@@ocaml.deprecated "Same as [DirPath.compare]."] - -val dir_path_eq : DirPath.t -> DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.equal]."] - -val make_dirpath : module_ident list -> DirPath.t -[@@ocaml.deprecated "Same as [DirPath.make]."] - -val repr_dirpath : DirPath.t -> module_ident list -[@@ocaml.deprecated "Same as [DirPath.repr]."] - -val empty_dirpath : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.empty]."] - -val is_empty_dirpath : DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.is_empty]."] - -val string_of_dirpath : DirPath.t -> string -[@@ocaml.deprecated "Same as [DirPath.to_string]."] - -val initial_dir : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.initial]."] - -(** {5 Labels} *) - -type label = Label.t -[@@ocaml.deprecated "Same as [Label.t]."] -(** Alias type *) - -val mk_label : string -> Label.t -[@@ocaml.deprecated "Same as [Label.make]."] - -val string_of_label : Label.t -> string -[@@ocaml.deprecated "Same as [Label.to_string]."] - -val pr_label : Label.t -> Pp.t -[@@ocaml.deprecated "Same as [Label.print]."] - -val label_of_id : Id.t -> Label.t -[@@ocaml.deprecated "Same as [Label.of_id]."] - -val id_of_label : Label.t -> Id.t -[@@ocaml.deprecated "Same as [Label.to_id]."] - -val eq_label : Label.t -> Label.t -> bool -[@@ocaml.deprecated "Same as [Label.equal]."] - -(** {5 Unique bound module names} *) - type mod_bound_id = MBId.t [@@ocaml.deprecated "Same as [MBId.t]."] - -val mod_bound_id_ord : MBId.t -> MBId.t -> int -[@@ocaml.deprecated "Same as [MBId.compare]."] - -val mod_bound_id_eq : MBId.t -> MBId.t -> bool -[@@ocaml.deprecated "Same as [MBId.equal]."] - -val make_mbid : DirPath.t -> Id.t -> MBId.t -[@@ocaml.deprecated "Same as [MBId.make]."] - -val repr_mbid : MBId.t -> int * Id.t * DirPath.t -[@@ocaml.deprecated "Same as [MBId.repr]."] - -val id_of_mbid : MBId.t -> Id.t -[@@ocaml.deprecated "Same as [MBId.to_id]."] - -val string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.to_string]."] - -val debug_string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] - -(** {5 Names} *) - -val name_eq : Name.t -> Name.t -> bool -[@@ocaml.deprecated "Same as [Name.equal]."] - (** {5 Module paths} *) type module_path = ModPath.t = @@ -656,52 +548,6 @@ type module_path = ModPath.t = | MPdot of ModPath.t * Label.t [@@ocaml.deprecated "Alias type"] -val mp_ord : ModPath.t -> ModPath.t -> int -[@@ocaml.deprecated "Same as [ModPath.compare]."] - -val mp_eq : ModPath.t -> ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.equal]."] - -val check_bound_mp : ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.is_bound]."] - -val string_of_mp : ModPath.t -> string -[@@ocaml.deprecated "Same as [ModPath.to_string]."] - -val initial_path : ModPath.t -[@@ocaml.deprecated "Same as [ModPath.initial]."] - -(** {5 Kernel names} *) - -type kernel_name = KerName.t -[@@ocaml.deprecated "Alias type"] - -val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t -[@@ocaml.deprecated "Same as [KerName.make]."] - -val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [KerName.repr]."] - -val modpath : KerName.t -> ModPath.t -[@@ocaml.deprecated "Same as [KerName.modpath]."] - -val label : KerName.t -> Label.t -[@@ocaml.deprecated "Same as [KerName.label]."] - -val string_of_kn : KerName.t -> string -[@@ocaml.deprecated "Same as [KerName.to_string]."] - -val pr_kn : KerName.t -> Pp.t -[@@ocaml.deprecated "Same as [KerName.print]."] - -val kn_ord : KerName.t -> KerName.t -> int -[@@ocaml.deprecated "Same as [KerName.compare]."] - -(** {5 Constant names} *) - -type constant = Constant.t -[@@ocaml.deprecated "Alias type"] - module Projection : sig type t @@ -749,6 +595,9 @@ module GlobRef : sig end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = @@ -757,100 +606,8 @@ type evaluable_global_reference = val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool -val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make]"] - -val constant_of_kn : KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make1]"] - -val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make3]"] - -val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [Constant.repr3]"] - -val user_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.user]"] - -val canonical_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.canonical]"] - -val con_modpath : Constant.t -> ModPath.t -[@@ocaml.deprecated "Same as [Constant.modpath]"] - -val con_label : Constant.t -> Label.t -[@@ocaml.deprecated "Same as [Constant.label]"] - -val eq_constant : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.equal]"] - -val con_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] - -val con_user_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] - -val con_with_label : Constant.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.change_label]"] - -val string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.to_string]"] - -val pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.print]"] - -val debug_pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.debug_print]"] - -val debug_string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] - -(** {5 Mutual Inductive names} *) - -type mutual_inductive = MutInd.t -[@@ocaml.deprecated "Alias type"] - -val mind_of_kn : KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make1]"] - -val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make]"] - -val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make3]"] - -val user_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.user]"] - -val canonical_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.canonical]"] - -val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [MutInd.repr3]"] - -val eq_mind : MutInd.t -> MutInd.t -> bool -[@@ocaml.deprecated "Same as [MutInd.equal]"] - -val mind_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] - -val mind_user_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] - -val mind_label : MutInd.t -> Label.t -[@@ocaml.deprecated "Same as [MutInd.label]"] - -val mind_modpath : MutInd.t -> ModPath.t -[@@ocaml.deprecated "Same as [MutInd.modpath]"] - -val string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.to_string]"] - -val pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.print]"] - -val debug_pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.debug_print]"] +(** Located identifiers and objects with syntax. *) -val debug_string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c82d982b4..6821fc980 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,7 +16,7 @@ open Util open Nativevalues open Nativeinstr open Nativelambda -open Pre_env +open Environ [@@@ocaml.warning "-32-37"] @@ -53,7 +53,7 @@ type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) | Gconstant of string * Constant.t (* prefix, constant name *) - | Gproj of string * Constant.t (* prefix, constant name *) + | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *) | Gcase of Label.t option * int | Gpred of Label.t option * int | Gfixtype of Label.t option * int @@ -108,7 +108,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 9 (String.hash s) | Grel i -> combinesmall 10 (Int.hash i) | Gnamed id -> combinesmall 11 (Id.hash id) -| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) +| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i)) let case_ctr = ref (-1) @@ -152,6 +152,7 @@ type symbol = | SymbMeta of metavariable | SymbEvar of Evar.t | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) let dummy_symb = SymbValue (dummy_value ()) @@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 = | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -179,6 +181,7 @@ let hash_symbol symb = | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) + | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -241,6 +244,11 @@ let get_level tbl i = | SymbLevel u -> u | _ -> anomaly (Pp.str "get_level failed.") +let get_proj tbl i = + match tbl.(i) with + | SymbProj p -> p + | _ -> anomaly (Pp.str "get_proj failed.") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -885,6 +893,10 @@ let get_level_code i = MLapp (MLglobal (Ginternal "get_level"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_proj_code i = + MLapp (MLglobal (Ginternal "get_proj"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -1070,7 +1082,7 @@ let ml_of_instance instance u = | Lconst (prefix, (c, u)) -> let args = ml_of_instance env.env_univ u in mkMLapp (MLglobal(Gconstant (prefix, c))) args - | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | 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 @@ -1544,8 +1556,8 @@ let string_of_gname g = Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) - | Gproj (prefix, c) -> - Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gproj (prefix, (mind, n), i) -> + Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i | Gcase (l,i) -> Format.sprintf "case_%s_%i" (string_of_label_def l) i | Gpred (l,i) -> @@ -1837,7 +1849,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in - let decl = Pre_env.lookup_rel n env in + let decl = lookup_rel n env in let n = List.length env.env_rel_context.env_rel_ctx - n in match decl with | LocalDef (_,t,_) -> @@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - match cb.const_proj with - | None -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,38 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> - let mind = pb.proj_ind in - let ind = (mind,0) in - let mib = lookup_mind mind env in - let oib = mib.mind_packets.(0) in - let tbl = oib.mind_reloc_tbl in - (* Building info *) - let prefix = get_mind_prefix env mind in - let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = [|0|]; - ci_cstr_ndecls = [||] (*FIXME*); - ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in - let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; - asw_reloc = tbl; asw_finite = true } in - let c_uid = fresh_lname Anonymous in - let cf_uid = fresh_lname Anonymous in - let _, arity = tbl.(0) in - let ci_uid = fresh_lname Anonymous in - let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) - in - let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in - let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("",con) in - let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in - let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal - arg|]))):: - [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -1961,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in + (** Generate data for every block *) let f i stack ob = - let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in - let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let ind = (mind, i) in + let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd ind) in + let name = Gind ("", ind) in let accu = let args = if Int.equal (Univ.AUContext.size u) 0 then @@ -1978,12 +1958,44 @@ let compile_mind prefix ~interactive mb mind stack = Array.init nparams (fun i -> {lname = param_name; luid = i}) in let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in - let c = (mind,i), (j+1) in + let c = ind, (j+1) in Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in - Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in + let add_proj j acc pb = + let () = assert (eq_ind ind pb.proj_ind) in + let tbl = ob.mind_reloc_tbl in + (* Building info *) + let ci = { ci_ind = ind; ci_npar = nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbProj (ind, j)) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let gn = Gproj ("", ind, pb.proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | NotRecord | FakeRecord -> [] + | PrimRecord info -> + let _, _, pbs = info.(i) in + Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2016,24 +2028,22 @@ let compile_mind_deps env prefix ~interactive (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let rec compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix ~interactive init t = + let rec aux env lvl init t = match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in - let cb,(nameref,_) = lookup_constant_key c env in - let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref - || (Cmap_env.mem c const_updates) - then init - else + let c,u = get_alias env c in + let cb,(nameref,_) = lookup_constant_key c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive nameref + || (Cmap_env.mem c const_updates) + then init + else let comp_stack, (mind_updates, const_updates) = - match cb.const_proj, cb.const_body with - | None, Def t -> - compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + match cb.const_body with + | Def t -> + aux env lvl init (Mod_subst.force_constr t) | _ -> init in let code, name = @@ -2044,13 +2054,32 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let term = mkApp (mkConst (Projection.constant p), [|c|]) in - compile_deps env sigma prefix ~interactive init term + let pb = lookup_projection p env in + let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in + aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - Constr.fold (compile_deps env sigma prefix ~interactive) init t - | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t + fold_constr_with_binders succ (aux env) lvl init t + | Var id -> + let open Context.Named.Declaration in + begin match lookup_named id env with + | LocalDef (_,t,_) -> + aux env lvl init t + | _ -> init + end + | Rel n when n > lvl -> + let open Context.Rel.Declaration in + let decl = lookup_rel n env in + let env = env_of_rel n env in + begin match decl with + | LocalDef (_,t,_) -> + aux env lvl init t + | LocalAssum _ -> init + end + | _ -> fold_constr_with_binders succ (aux env) lvl init t + in + aux env 0 init t let compile_constant_field env prefix con acc cb = let (gl, _) = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -10,7 +10,7 @@ open Names open Constr open Declarations -open Pre_env +open Environ open Nativelambda (** This file defines the mllambda code generation phase of the native @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c71f746be..e97dbd0d6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu = let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu - | Aproj(p1,ac1), Aproj(p2,ac2) -> - if not (Constant.equal p1 p2) then raise NotConvertible + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ @@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 cu let native_conv_gen pb sigma env univs t1 t2 = - let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in - let code, upds = mk_conv_code penv sigma prefix t1 t2 in + let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with | (true, fn) -> begin @@ -163,7 +162,7 @@ let warn_no_native_compiler = let native_conv cv_pb sigma env t1 t2 = if not Coq_config.native_compiler then begin warn_no_native_compiler (); - vm_conv cv_pb env t1 t2 + Vconv.vm_conv cv_pb env t1 t2 end else let univs = Environ.universes env in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5..eaad8ee0c 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -31,13 +31,13 @@ and lambda = | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 12cd5fe83..a809e1b18 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -12,7 +12,7 @@ open Names open Esubst open Constr open Declarations -open Pre_env +open Environ open Nativevalues open Nativeinstr @@ -296,15 +296,17 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true + | Luint (UintVal _) -> true | _ -> false - + let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> + | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag + | Luint (UintVal i) -> Nativevalues.mk_uint i | _ -> raise Not_found - + let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) @@ -517,8 +519,10 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - let kn = Projection.constant p in - mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] + let pb = lookup_projection p !global_env in + let ind = pb.proj_ind in + let prefix = get_mind_prefix !global_env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in @@ -570,6 +574,7 @@ let rec lambda_of_constr env sigma c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env sigma 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env sigma 0 rec_bodies in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 9a1e19b3c..26bfeb7e0 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,7 +9,7 @@ (************************************************************************) open Names open Constr -open Pre_env +open Environ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c69cf722b..8bff43632 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -10,7 +10,6 @@ open Names open Declarations -open Environ open Mod_subst open Modops open Nativecode @@ -32,7 +31,7 @@ and translate_field prefix mp env acc (l,x) = (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); - compile_constant_field (pre_env env) prefix con acc cb + compile_constant_field env prefix con acc cb | SFBmind mb -> (if !Flags.debug then let id = mb.mind_packets.(0).mind_typename in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485..da4413a0a 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 4a58a3c7d..649853f06 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -54,7 +54,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t (* type *) * t array (* arguments *) - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : Evar.t -> t -> t array -> t -val mk_proj_accu : Constant.t -> accumulator -> t +val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml deleted file mode 100644 index 8ebe48e20..000000000 --- a/kernel/pre_env.ml +++ /dev/null @@ -1,213 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -(* Created by Benjamin Grégoire out of environ.ml for better - modularity in the design of the bytecode virtual evaluation - machine, Dec 2005 *) -(* Bug fix by Jean-Marc Notin *) - -(* This file defines the type of kernel environments *) - -open Util -open Names -open Declarations - -module NamedDecl = Context.Named.Declaration - -(* The type of environments. *) - -(* The key attached to each constant is used by the VM to retrieve previous *) -(* evaluations of the constant. It is essentially an index in the symbols table *) -(* used by the VM. *) -type key = int CEphemeron.key option ref - -(** Linking information for the native compiler. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type val_kind = - | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key - | VKnone - -type lazy_val = val_kind ref - -let force_lazy_val vk = match !vk with -| VKnone -> None -| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None - -let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) - -type named_context_val = { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) - env_named_context : named_context_val; (* section variables *) - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -let empty_named_context_val = { - env_named_ctx = []; - env_named_map = Id.Map.empty; -} - -let empty_rel_context_val = { - env_rel_ctx = []; - env_rel_map = Range.empty; -} - -let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; - env_named_context = empty_named_context_val; - env_rel_context = empty_rel_context_val; - env_nb_rel = 0; - env_stratification = { - env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags Conv_oracle.empty; - retroknowledge = Retroknowledge.initial_retroknowledge; - indirect_pterms = Opaqueproof.empty_opaquetab } - - -(* Rel context *) - -let nb_rel env = env.env_nb_rel - -let push_rel_context_val d ctx = { - env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; - env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; -} - -let match_rel_context_val ctx = match ctx.env_rel_ctx with -| [] -> None -| decl :: rem -> - let (_, lval) = Range.hd ctx.env_rel_map in - let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in - Some (decl, lval, ctx) - -let push_rel d env = - { env with - env_rel_context = push_rel_context_val d env.env_rel_context; - env_nb_rel = env.env_nb_rel + 1 } - -let lookup_rel n env = - try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let lookup_rel_val n env = - try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let rel_skipn n ctx = { - env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; - env_rel_map = Range.skipn n ctx.env_rel_map; -} - -let env_of_rel n env = - { env with - env_rel_context = rel_skipn n env.env_rel_context; - env_nb_rel = env.env_nb_rel - n - } - -(* Named context *) - -let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) - { - env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; - } - -let push_named_context_val d ctxt = - push_named_context_val_val d (ref VKnone) ctxt - -let match_named_context_val c = match c.env_named_ctx with -| [] -> None -| decl :: ctx -> - let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in - let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in - let cval = { env_named_ctx = ctx; env_named_map = map } in - Some (decl, v, cval) - -let map_named_val f ctxt = - let open Context.Named.Declaration in - let fold accu d = - let d' = map_constr f d in - let accu = - if d == d' then accu - else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu - in - (accu, d') - in - let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in - if map == ctxt.env_named_map then ctxt - else { env_named_ctx = ctx; env_named_map = map } - -let push_named d env = - {env with env_named_context = push_named_context_val d env.env_named_context} - -let lookup_named id env = - fst (Id.Map.find id env.env_named_context.env_named_map) - -let lookup_named_val id env = - snd(Id.Map.find id env.env_named_context.env_named_map) - -(* Warning all the names should be different *) -let env_of_named id env = env - -(* Global constants *) - -let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants - -let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) - -(* Mutual Inductives *) -let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) - -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli deleted file mode 100644 index b05074814..000000000 --- a/kernel/pre_env.mli +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Names -open Constr -open Declarations - -(** The type of environments. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type key = int CEphemeron.key option ref - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type lazy_val - -val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option -val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit - -type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = private { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; - env_named_context : named_context_val; - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -val empty_named_context_val : named_context_val - -val empty_env : env - -(** Rel context *) - -val empty_rel_context_val : rel_context_val -val push_rel_context_val : - Context.Rel.Declaration.t -> rel_context_val -> rel_context_val -val match_rel_context_val : - rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option - -val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val lookup_rel : int -> env -> Context.Rel.Declaration.t -val lookup_rel_val : int -> env -> lazy_val -val env_of_rel : int -> env -> env - -(** Named context *) - -val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val -val push_named_context_val_val : - Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val -val match_named_context_val : - named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option -val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val - -val push_named : Context.Named.Declaration.t -> env -> env -val lookup_named : Id.t -> env -> Context.Named.Declaration.t -val lookup_named_val : Id.t -> env -> lazy_val -val env_of_named : Id.t -> env -> env - -(** Global constants *) - - -val lookup_constant_key : Constant.t -> env -> constant_key -val lookup_constant : Constant.t -> env -> constant_body - -(** Mutual Inductives *) -val lookup_mind_key : MutInd.t -> env -> mind_key -val lookup_mind : MutInd.t -> env -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 38106fbf6..f4af31386 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -648,25 +648,24 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if not (type_in_type env) then + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - if not (type_in_type env) then - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' = let infer_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if type_in_type env then univs + else + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) - else univs + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = @@ -789,24 +788,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb env -> - gen_conv cv_pb env ~evars:((fun _->None), universes env)) - -let warn_bytecode_compiler_failed = - let open Pp in - CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" - (fun () -> strbrk "Bytecode compiler failed, " ++ - strbrk "falling back to standard conversion") - -let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try - !vm_conv cv_pb env t1 t2 - with Not_found | Invalid_argument _ -> - warn_bytecode_compiler_failed (); - gen_conv cv_pb env t1 t2 - let default_conv cv_pb ?(l2r=false) env t1 t2 = gen_conv cv_pb env t1 t2 @@ -880,6 +861,17 @@ let dest_prod env = in decrec env Context.Rel.empty +let dest_lam env = + let rec decrec env m c = + let t = whd_all env c in + match kind t with + | Lambda (n,a,c0) -> + let d = LocalAssum (n,a) in + decrec (push_rel d env) (Context.Rel.add d m) c0 + | _ -> m,t + in + decrec env Context.Rel.empty + (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = @@ -925,3 +917,12 @@ let is_arity env c = let _ = dest_arity env c in true with NotArity -> false + +let eta_expand env t ty = + let ctxt, codom = dest_prod env ty in + let ctxt',t = dest_lam env t in + let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in + let eta_args = List.rev_map mkRel (List.interval 1 d) in + let t = Term.applistc (Vars.lift d t) eta_args in + let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in + Term.it_mkLambda_or_LetIn t ctxt' diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 14e4270b7..e53ab6aef 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -87,10 +87,6 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function -(** option for conversion *) -val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit -val vm_conv : conv_pb -> types kernel_conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function @@ -122,6 +118,7 @@ val betazeta_appvect : int -> constr -> constr array -> constr val dest_prod : env -> types -> Context.Rel.t * types val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam : env -> types -> Context.Rel.t * constr val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity @@ -129,4 +126,4 @@ exception NotArity val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool -val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit +val eta_expand : env -> constr -> types -> constr diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0334e7a9e..281c37b85 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -134,7 +134,7 @@ val get_native_before_match_info : retroknowledge -> entry -> Nativeinstr.lambda -> Nativeinstr.lambda -(** the following functions are solely used in Pre_env and Environ to implement +(** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) val add_field : retroknowledge -> field -> entry -> retroknowledge val mem : retroknowledge -> field -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index de2a890fb..12c82e20d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -59,6 +59,7 @@ etc. *) +open CErrors open Util open Names open Declarations @@ -914,16 +915,12 @@ let register field value by_clause senv = but it is meant to become a replacement for environ.register *) let register_inline kn senv = let open Environ in - let open Pre_env in if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); - let env = pre_env senv.env in + let env = senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in - let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in - let new_globals = { env.env_globals with env_constants = new_constants } in - let env = { env with env_globals = new_globals } in - { senv with env = env_of_pre_env env } + let env = add_constant kn cb env in { senv with env} let add_constraints c = add_constraints @@ -953,3 +950,125 @@ Would this be correct with respect to undo's and stuff ? let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } + +(** Register retroknowledge hooks *) + +open Retroknowledge + +(* the Environ.register function synchronizes the proactive and reactive + retroknowledge. *) +let dispatch = + + (* subfunction used for static decompilation of int31 (after a vm_compute, + see pretyping/vnorm.ml for more information) *) + let constr_of_int31 = + let nth_digit_plus_one i n = (* calculates the nth (starting with 0) + digit of i and adds 1 to it + (nth_digit_plus_one 1 3 = 2) *) + if Int.equal (i land (1 lsl n)) 0 then + 1 + else + 2 + in + fun ind -> fun digit_ind -> fun tag -> + let array_of_int i = + Array.init 31 (fun n -> Constr.mkConstruct + (digit_ind, nth_digit_plus_one i (30-n))) + in + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag) + in + + (* subfunction which dispatches the compiling information of an + int31 operation which has a specific vm instruction (associates + it to the name of the coq definition in the reactive retroknowledge) *) + let int31_op n op prim kn = + { empty_reactive_info with + vm_compiling = Some (Clambda.compile_prim n op kn); + native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + } + in + +fun rk value field -> + (* subfunction which shortens the (very common) dispatch of operations *) + let int31_op_from_const n op prim = + match Constr.kind value with + | Constr.Const kn -> int31_op n op prim kn + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") + in + let int31_binop_from_const op prim = int31_op_from_const 2 op prim in + let int31_unop_from_const op prim = int31_op_from_const 1 op prim in + match field with + | KInt31 (grp, Int31Type) -> + let int31bit = + (* invariant : the type of bits is registered, otherwise the function + would raise Not_found. The invariant is enforced in safe_typing.ml *) + match field with + | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | _ -> anomaly ~label:"Environ.register" + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") + in + let i31bit_type = + match Constr.kind int31bit with + | Constr.Ind (i31bit_type,_) -> i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "Int31Bits should be an inductive type.") + in + let int31_decompilation = + match Constr.kind value with + | Constr.Ind (i31t,_) -> + constr_of_int31 i31t i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "should be an inductive type.") + in + { empty_reactive_info with + vm_decompile_const = Some int31_decompilation; + vm_before_match = Some Clambda.int31_escape_before_match; + native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); + } + | KInt31 (_, Int31Constructor) -> + { empty_reactive_info with + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; + native_constant_static = Some Nativelambda.compile_static_int31; + native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; + } + | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 + CPrimitives.Int31add + | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + CPrimitives.Int31addc + | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + CPrimitives.Int31addcarryc + | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + CPrimitives.Int31sub + | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + CPrimitives.Int31subc + | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc + | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + CPrimitives.Int31mul + | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + CPrimitives.Int31mulc + | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + CPrimitives.Int31div21 + | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + CPrimitives.Int31diveucl + | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + CPrimitives.Int31addmuldiv + | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + CPrimitives.Int31compare + | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + CPrimitives.Int31head0 + | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + CPrimitives.Int31tail0 + | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + CPrimitives.Int31lor + | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + CPrimitives.Int31land + | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + CPrimitives.Int31lxor + | _ -> empty_reactive_info + +let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8cf588c3e..13701d489 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -226,8 +226,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 else error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x); - if mib1.mind_record <> None then begin + (** FIXME: this check looks nonsense *) + check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x); + if mib1.mind_record <> NotRecord then begin let rec names_prod_letin t = match kind t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) diff --git a/kernel/term.ml b/kernel/term.ml index e1affb1c0..b44e038e9 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -15,219 +15,17 @@ open Names open Vars open Constr -(**********************************************************************) -(** Redeclaration of types from module Constr *) -(**********************************************************************) - +(* Deprecated *) type contents = Sorts.contents = Pos | Null - -type sorts = Sorts.t = - | Prop of contents (** Prop and Set *) - | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.contents"] type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] -type constr = Constr.t -(** Alias types, for compatibility. *) - -type types = Constr.t -(** Same as [constr], for documentation purposes. *) - -type existential_key = Evar.t -type existential = Constr.existential - -type metavariable = Constr.metavariable - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : case_style } - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : case_printing - } - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -(********************************************************************) -(* Constructions as implemented *) -(********************************************************************) - -type rec_declaration = Constr.rec_declaration -type fixpoint = Constr.fixpoint -type cofixpoint = Constr.cofixpoint -type 'constr pexistential = 'constr Constr.pexistential -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type 'a puniverses = 'a Univ.puniverses - -(** Simply type aliases *) -type pconstant = Constant.t puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of 'constr pexistential - | Sort of 'sort - | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) pfixpoint - | CoFix of ('constr, 'types) pcofixpoint - | Proj of Projection.t * 'constr - -type values = Vmvalues.values - -(**********************************************************************) -(** Redeclaration of functions from module Constr *) -(**********************************************************************) - -let set_sort = Sorts.set -let prop_sort = Sorts.prop -let type1_sort = Sorts.type1 -let sorts_ord = Sorts.compare -let is_prop_sort = Sorts.is_prop -let family_of_sort = Sorts.family -let univ_of_sort = Sorts.univ_of_sort -let sort_of_univ = Sorts.sort_of_univ - -(** {6 Term constructors. } *) - -let mkRel = Constr.mkRel -let mkVar = Constr.mkVar -let mkMeta = Constr.mkMeta -let mkEvar = Constr.mkEvar -let mkSort = Constr.mkSort -let mkProp = Constr.mkProp -let mkSet = Constr.mkSet -let mkType = Constr.mkType -let mkCast = Constr.mkCast -let mkProd = Constr.mkProd -let mkLambda = Constr.mkLambda -let mkLetIn = Constr.mkLetIn -let mkApp = Constr.mkApp -let mkConst = Constr.mkConst -let mkProj = Constr.mkProj -let mkInd = Constr.mkInd -let mkConstruct = Constr.mkConstruct -let mkConstU = Constr.mkConstU -let mkIndU = Constr.mkIndU -let mkConstructU = Constr.mkConstructU -let mkConstructUi = Constr.mkConstructUi -let mkCase = Constr.mkCase -let mkFix = Constr.mkFix -let mkCoFix = Constr.mkCoFix - -(**********************************************************************) -(** Aliases of functions from module Constr *) -(**********************************************************************) - -let eq_constr = Constr.equal -let eq_constr_univs = Constr.eq_constr_univs -let leq_constr_univs = Constr.leq_constr_univs -let eq_constr_nounivs = Constr.eq_constr_nounivs - -let kind_of_term = Constr.kind -let compare = Constr.compare -let constr_ord = compare -let fold_constr = Constr.fold -let map_puniverses = Constr.map_puniverses -let map_constr = Constr.map -let map_constr_with_binders = Constr.map_with_binders -let iter_constr = Constr.iter -let iter_constr_with_binders = Constr.iter_with_binders -let compare_constr = Constr.compare_head -let hash_constr = Constr.hash -let hcons_sorts = Sorts.hcons -let hcons_constr = Constr.hcons -let hcons_types = Constr.hcons - -(**********************************************************************) -(** HERE BEGINS THE INTERESTING STUFF *) -(**********************************************************************) - -(**********************************************************************) -(* Non primitive term destructors *) -(**********************************************************************) - -exception DestKO = DestKO -(* Destructs a de Bruijn index *) -let destRel = destRel -let destMeta = destRel -let isMeta = isMeta -let destVar = destVar -let isSort = isSort -let destSort = destSort -let isprop = isprop -let is_Prop = is_Prop -let is_Set = is_Set -let is_Type = is_Type -let is_small = is_small -let iskind = iskind -let isEvar = isEvar -let isEvar_or_Meta = isEvar_or_Meta -let destCast = destCast -let isCast = isCast -let isRel = isRel -let isRelN = isRelN -let isVar = isVar -let isVarId = isVarId -let isInd = isInd -let destProd = destProd -let isProd = isProd -let destLambda = destLambda -let isLambda = isLambda -let destLetIn = destLetIn -let isLetIn = isLetIn -let destApp = destApp -let destApplication = destApp -let isApp = isApp -let destConst = destConst -let isConst = isConst -let destEvar = destEvar -let destInd = destInd -let destConstruct = destConstruct -let isConstruct = isConstruct -let destCase = destCase -let isCase = isCase -let isProj = isProj -let destProj = destProj -let destFix = destFix -let isFix = isFix -let destCoFix = destCoFix -let isCoFix = isCoFix - -(******************************************************************) -(* Flattening and unflattening of embedded applications and casts *) -(******************************************************************) - -let decompose_app c = - match kind_of_term c with - | App (f,cl) -> (f, Array.to_list cl) - | _ -> (c,[]) - -let decompose_appvect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) +type sorts = Sorts.t = + | Prop of Sorts.contents (** Prop and Set *) + | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.t"] (****************************************************************************) (* Functions for dealing with constr terms *) @@ -321,7 +119,7 @@ let rec to_lambda n prod = if Int.equal n 0 then prod else - match kind_of_term prod with + match kind prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c | _ -> user_err ~hdr:"to_lambda" (mt ()) @@ -330,7 +128,7 @@ let rec to_prod n lam = if Int.equal n 0 then lam else - match kind_of_term lam with + match kind lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c | _ -> user_err ~hdr:"to_prod" (mt ()) @@ -342,7 +140,7 @@ let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) let lambda_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough lambda's.") in @@ -355,7 +153,7 @@ let lambda_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -367,7 +165,7 @@ let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough prod's.") in @@ -381,7 +179,7 @@ let prod_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -397,7 +195,7 @@ let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) let decompose_prod = - let rec prodec_rec l c = match kind_of_term c with + let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c @@ -407,7 +205,7 @@ let decompose_prod = (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam = - let rec lamdec_rec l c = match kind_of_term c with + let rec lamdec_rec l c = match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c @@ -420,7 +218,7 @@ let decompose_prod_n n = if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> user_err (str "decompose_prod_n: not enough products") @@ -433,7 +231,7 @@ let decompose_lam_n n = if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> user_err (str "decompose_lam_n: not enough abstractions") @@ -445,7 +243,7 @@ let decompose_lam_n n = let decompose_prod_assum = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c @@ -458,7 +256,7 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c @@ -477,7 +275,7 @@ let decompose_prod_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c @@ -498,7 +296,7 @@ let decompose_lam_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c @@ -514,7 +312,7 @@ let decompose_lam_n_decls n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c @@ -541,12 +339,12 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * sorts +type arity = Context.Rel.t * Sorts.t let destArity = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c @@ -558,7 +356,7 @@ let destArity = let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign let rec isArity c = - match kind_of_term c with + match kind c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) | Cast (c,_,_) -> isArity c @@ -569,13 +367,13 @@ let rec isArity c = (* Experimental, used in Presburger contrib *) type ('constr, 'types) kind_of_type = - | SortType of sorts + | SortType of Sorts.t | CastType of 'types * 'types | ProdType of Name.t * 'types * 'types | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array -let kind_of_type t = match kind_of_term t with +let kind_of_type t = match kind t with | Sort s -> SortType s | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) diff --git a/kernel/term.mli b/kernel/term.mli index ee84dcb2b..f651d1a58 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -11,166 +11,6 @@ open Names open Constr -(** {5 Redeclaration of types from module Constr and Sorts} - - This reexports constructors of inductive types defined in module [Constr], - for compatibility purposes. Refer to this module for further info. - -*) - -exception DestKO -[@@ocaml.deprecated "Alias for [Constr.DestKO]"] - -(** {5 Simple term case analysis. } *) -val isRel : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRel]"] -val isRelN : int -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRelN]"] -val isVar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVar]"] -val isVarId : Id.t -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVarId]"] -val isInd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isInd]"] -val isEvar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar]"] -val isMeta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isMeta]"] -val isEvar_or_Meta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"] -val isSort : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isSort]"] -val isCast : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCast]"] -val isApp : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isApp]"] -val isLambda : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isLambda]"] -val isLetIn : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isletIn]"] -val isProd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProp]"] -val isConst : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConst]"] -val isConstruct : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConstruct]"] -val isFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isFix]"] -val isCoFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCoFix]"] -val isCase : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCase]"] -val isProj : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProj]"] - -val is_Prop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Prop]"] -val is_Set : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Set]"] -val isprop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isprop]"] -val is_Type : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Type]"] -val iskind : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_kind]"] -val is_small : Sorts.t -> bool -[@@ocaml.deprecated "Alias for [Constr.is_small]"] - - -(** {5 Term destructors } *) -(** Destructor operations are partial functions and - @raise DestKO if the term has not the expected form. *) - -(** Destructs a de Bruijn index *) -val destRel : constr -> int -[@@ocaml.deprecated "Alias for [Constr.destRel]"] - -(** Destructs an existential variable *) -val destMeta : constr -> metavariable -[@@ocaml.deprecated "Alias for [Constr.destMeta]"] - -(** Destructs a variable *) -val destVar : constr -> Id.t -[@@ocaml.deprecated "Alias for [Constr.destVar]"] - -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) -val destSort : constr -> Sorts.t -[@@ocaml.deprecated "Alias for [Constr.destSort]"] - -(** Destructs a casted term *) -val destCast : constr -> constr * cast_kind * constr -[@@ocaml.deprecated "Alias for [Constr.destCast]"] - -(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> Name.t * types * types -[@@ocaml.deprecated "Alias for [Constr.destProd]"] - -(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> Name.t * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLambda]"] - -(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> Name.t * constr * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLetIn]"] - -(** Destructs an application *) -val destApp : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApp]"] - -(** Obsolete synonym of destApp *) -val destApplication : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApplication]"] - -(** Decompose any term as an applicative term; the list of args can be empty *) -val decompose_app : constr -> constr * constr list -[@@ocaml.deprecated "Alias for [Constr.decompose_app]"] - -(** Same as [decompose_app], but returns an array. *) -val decompose_appvect : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] - -(** Destructs a constant *) -val destConst : constr -> Constant.t Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConst]"] - -(** Destructs an existential variable *) -val destEvar : constr -> existential -[@@ocaml.deprecated "Alias for [Constr.destEvar]"] - -(** Destructs a (co)inductive type *) -val destInd : constr -> inductive Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destInd]"] - -(** Destructs a constructor *) -val destConstruct : constr -> constructor Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConstruct]"] - -(** Destructs a [match c as x in I args return P with ... | -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 -[@@ocaml.deprecated "Alias for [Constr.destCase]"] - -(** Destructs a projection *) -val destProj : constr -> Projection.t * constr -[@@ocaml.deprecated "Alias for [Constr.destProj]"] - -(** Destructs the {% $ %}i{% $ %}th function of the block - [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} - with f{_ 2} ctx{_ 2} = b{_ 2} - ... - with f{_ n} ctx{_ n} = b{_ n}], - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -val destFix : constr -> fixpoint -[@@ocaml.deprecated "Alias for [Constr.destFix]"] - -val destCoFix : constr -> cofixpoint -[@@ocaml.deprecated "Alias for [Constr.destCoFix]"] - (** {5 Derived constructors} *) (** non-dependent product [t1 -> t2], an alias for @@ -349,242 +189,14 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type -(** {5 Redeclaration of stuff from module [Sorts]} *) - -val set_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.set"] - -val prop_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.prop"] - -val type1_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.type1"] - -val sorts_ord : Sorts.t -> Sorts.t -> int -[@@ocaml.deprecated "Alias for Sorts.compare"] - -val is_prop_sort : Sorts.t -> bool -[@@ocaml.deprecated "Alias for Sorts.is_prop"] - -val family_of_sort : Sorts.t -> Sorts.family -[@@ocaml.deprecated "Alias for Sorts.family"] - -(** {5 Redeclaration of stuff from module [Constr]} - - See module [Constr] for further info. *) - -(** {6 Term constructors. } *) - -val mkRel : int -> constr -[@@ocaml.deprecated "Alias for Constr.mkRel"] -val mkVar : Id.t -> constr -[@@ocaml.deprecated "Alias for Constr.mkVar"] -val mkMeta : metavariable -> constr -[@@ocaml.deprecated "Alias for Constr.mkMeta"] -val mkEvar : existential -> constr -[@@ocaml.deprecated "Alias for Constr.mkEvar"] -val mkSort : Sorts.t -> types -[@@ocaml.deprecated "Alias for Constr.mkSort"] -val mkProp : types -[@@ocaml.deprecated "Alias for Constr.mkProp"] -val mkSet : types -[@@ocaml.deprecated "Alias for Constr.mkSet"] -val mkType : Univ.Universe.t -> types -[@@ocaml.deprecated "Alias for Constr.mkType"] -val mkCast : constr * cast_kind * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProd : Name.t * types * types -> types -[@@ocaml.deprecated "Alias for Constr"] -val mkLambda : Name.t * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkLetIn : Name.t * constr * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkApp : constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConst : Constant.t -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProj : Projection.t * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkInd : inductive -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstruct : constructor -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstU : Constant.t Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkIndU : inductive Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructU : constructor Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructUi : (pinductive * int) -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr.mkCase"] -val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkFix"] -val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkCoFix"] - -(** {6 Aliases} *) - -val eq_constr : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.equal"] - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"] - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"] - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"] - -val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -[@@ocaml.deprecated "Alias for Constr.kind"] - -val compare : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Constr.compare]"] - -val constr_ord : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Term.compare]"] - -val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a -[@@ocaml.deprecated "Alias for [Constr.fold]"] - -val map_constr : (constr -> constr) -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map]"] - -val map_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] - -val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] -val univ_of_sort : Sorts.t -> Univ.Universe.t -[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] -val sort_of_univ : Univ.Universe.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"] - -val iter_constr : (constr -> unit) -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter]"] - -val iter_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] - -val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.compare_head]"] - -type constr = Constr.constr -[@@ocaml.deprecated "Alias for Constr.t"] - -(** Alias types, for compatibility. *) - -type types = Constr.types -[@@ocaml.deprecated "Alias for Constr.types"] - +(* Deprecated *) type contents = Sorts.contents = Pos | Null [@@ocaml.deprecated "Alias for Sorts.contents"] +type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] + type sorts = Sorts.t = | Prop of Sorts.contents (** Prop and Set *) | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] - -type sorts_family = Sorts.family = InProp | InSet | InType -[@@ocaml.deprecated "Alias for Sorts.family"] - -type 'a puniverses = 'a Univ.puniverses -[@@ocaml.deprecated "Alias for Constr.puniverses"] - -(** Simply type aliases *) -type pconstant = Constr.pconstant -[@@ocaml.deprecated "Alias for Constr.pconstant"] -type pinductive = Constr.pinductive -[@@ocaml.deprecated "Alias for Constr.pinductive"] -type pconstructor = Constr.pconstructor -[@@ocaml.deprecated "Alias for Constr.pconstructor"] -type existential_key = Evar.t -[@@ocaml.deprecated "Alias for Evar.t"] -type existential = Constr.existential -[@@ocaml.deprecated "Alias for Constr.existential"] -type metavariable = Constr.metavariable -[@@ocaml.deprecated "Alias for Constr.metavariable"] - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -[@@ocaml.deprecated "Alias for Constr.case_style"] - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style } -[@@ocaml.deprecated "Alias for Constr.case_printing"] - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : Constr.case_printing - } -[@@ocaml.deprecated "Alias for Constr.case_info"] - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast -[@@ocaml.deprecated "Alias for Constr.cast_kind"] - -type rec_declaration = Constr.rec_declaration -[@@ocaml.deprecated "Alias for Constr.rec_declaration"] -type fixpoint = Constr.fixpoint -[@@ocaml.deprecated "Alias for Constr.fixpoint"] -type cofixpoint = Constr.cofixpoint -[@@ocaml.deprecated "Alias for Constr.cofixpoint"] -type 'constr pexistential = 'constr Constr.pexistential -[@@ocaml.deprecated "Alias for Constr.pexistential"] -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -[@@ocaml.deprecated "Alias for Constr.prec_declaration"] -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -[@@ocaml.deprecated "Alias for Constr.pfixpoint"] -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -[@@ocaml.deprecated "Alias for Constr.pcofixpoint"] - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of Constr.metavariable - | Evar of 'constr Constr.pexistential - | Sort of 'sort - | Cast of 'constr * Constr.cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of Constr.case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) Constr.pfixpoint - | CoFix of ('constr, 'types) Constr.pcofixpoint - | Proj of Projection.t * 'constr -[@@ocaml.deprecated "Alias for Constr.kind_of_term"] - -type values = Vmvalues.values -[@@ocaml.deprecated "Alias for Vmvalues.values"] - -val hash_constr : Constr.constr -> int -[@@ocaml.deprecated "Alias for Constr.hash"] - -val hcons_sorts : Sorts.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.hcons]"] - -val hcons_constr : Constr.constr -> Constr.constr -[@@ocaml.deprecated "Alias for [Constr.hcons]"] - -val hcons_types : Constr.types -> Constr.types -[@@ocaml.deprecated "Alias for [Constr.hcons]"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index be2f8df7d..bad449731 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } - | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (Some (id, kns, pbs)) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | _ -> assert false - in - let univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Monomorphic_const ctx - | Polymorphic_ind auctx -> Polymorphic_const auctx - | Cumulative_ind acumi -> - Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) - in - let term, typ = pb.proj_eta in - { - Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); - cook_type = typ; - cook_proj = Some pb; - cook_universes = univs; - cook_inline = false; - cook_context = None; - } - let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = @@ -458,35 +428,12 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> compile_constant_body env univs def - | Some pb -> - (* The compilation of primitive projections is a bit tricky, because - they refer to themselves (the body of p looks like fun c => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - compile_constant_body env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; const_inline_code = result.cook_inline; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be4c0e1ec..34ed2afb2 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -221,7 +221,7 @@ let check_cast env c ct k expected_type = try match k with | VMcast -> - vm_conv CUMUL env ct expected_type + Vconv.vm_conv CUMUL env ct expected_type | DEFAULTcast -> default_conv ~l2r:false CUMUL env ct expected_type | REVERTcast -> @@ -301,7 +301,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(MutInd.equal pb.proj_ind (fst ind)); + assert(eq_ind pb.proj_ind ind); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: CList.rev args) ty @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 85b2cfffd..546f2d2b4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Projection.t puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e6b27077b..4a9467de5 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g = let () = cleanup_universes g in raise e -let add_universe vlev strict g = +let add_universe_gen vlev g = try let _arcv = UMap.find vlev g.entries in raise AlreadyDeclared @@ -520,8 +520,14 @@ let add_universe vlev strict g = } in let entries = UMap.add vlev (Canonical v) g.entries in - let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in - insert_edge strict (get_set_arc g) v g + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v + +let add_universe vlev strict g = + let g, v = add_universe_gen vlev g in + insert_edge strict (get_set_arc g) v g + +let add_universe_unconstrained vlev g = + fst (add_universe_gen vlev g) exception Found_explanation of explanation @@ -696,6 +702,9 @@ let enforce_univ_lt u v g = error_inconsistency Lt u v (get_explanation false v u g) let empty_universes = + { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + +let initial_universes = let set_arc = Canonical { univ = Level.set; ltle = LMap.empty; @@ -718,9 +727,6 @@ let empty_universes = let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in enforce_univ_lt Level.prop Level.set empty -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries let enforce_constraint cst g = @@ -780,6 +786,42 @@ let constraints_of_universes g = let csts = UMap.fold constraints_of g.entries Constraint.empty in csts, UF.partition uf +(* domain g.entries = kept + removed *) +let constraints_for ~kept g = + (* rmap: partial map from canonical universes to kept universes *) + let rmap, csts = LSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if LSet.mem arcu.univ kept then + LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts + else + match LMap.find arcu.univ rmap with + | v -> rmap, enforce_eq_level u v csts + | exception Not_found -> LMap.add arcu.univ u rmap, csts) + kept (LMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match LMap.find v.univ rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept universe *) + let todo = LMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + LSet.fold (fun u csts -> + let arc = repr g u in + LMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index cca2eb472..e6dd629e4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -49,13 +49,15 @@ exception AlreadyDeclared val add_universe : Level.t -> bool -> t -> t +(** Add a universe without (Prop,Set) <= u *) +val add_universe_unconstrained : Level.t -> t -> t + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t (** The empty graph of universes *) val empty_universes : t -[@@ocaml.deprecated "Use UGraph.initial_universes"] val sort_universes : t -> t @@ -64,6 +66,12 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +(** [constraints_for ~kept g] returns the constraints about the + universes [kept] in [g] up to transitivity. + + eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) +val constraints_for : kept:LSet.t -> t -> Constraint.t + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f11803b67..4e4168922 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -6,9 +6,6 @@ open Vm open Vmvalues open Csymtable -let val_of_constr env c = - val_of_constr (pre_env env) c - (* Test la structure des piles *) let compare_zipper z1 z2 = @@ -185,8 +182,18 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu = !rcu else raise NotConvertible +let warn_bytecode_compiler_failed = + let open Pp in + CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" + (fun () -> strbrk "Bytecode compiler failed, " ++ + strbrk "falling back to standard conversion") + let vm_conv_gen cv_pb env univs t1 t2 = - try + if not Coq_config.bytecode_compiler then + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2 + else + try let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) @@ -204,5 +211,3 @@ let vm_conv cv_pb env t1 t2 = if not b then let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () - -let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 620f6b5e8..1a3184898 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constr -open Environ open Reduction (********************************************************************** @@ -19,6 +18,3 @@ val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function - -(** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 7a703e653..8524c44d2 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -297,7 +297,6 @@ let rec obj_of_str_const str = match str with | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p | Const_b0 tag -> Obj.repr tag | Const_bn(tag, args) -> let len = Array.length args in @@ -355,6 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c) let val_of_evar evk = val_of_idkey (EvarKey evk) external val_of_annot_switch : annot_switch -> values = "%identity" +external val_of_proj_name : Constant.t -> values = "%identity" (*************************************************) (** Operations manipulating data types ***********) diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 550791b2c..08d05a038 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -112,6 +112,7 @@ val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values external val_of_annot_switch : annot_switch -> values = "%identity" +external val_of_proj_name : Constant.t -> values = "%identity" (** Destructors *) |