aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/dune2
-rw-r--r--kernel/cPrimitives.ml76
-rw-r--r--kernel/cPrimitives.mli4
-rw-r--r--kernel/cooking.ml3
-rw-r--r--kernel/dune2
-rw-r--r--kernel/inductive.ml5
-rw-r--r--kernel/mod_subst.ml5
-rw-r--r--kernel/mod_subst.mli3
-rw-r--r--kernel/nativecode.ml5
-rw-r--r--kernel/reduction.ml41
-rw-r--r--kernel/typeops.ml19
-rw-r--r--kernel/uGraph.ml25
-rw-r--r--kernel/vars.ml8
-rw-r--r--kernel/vmbytecodes.ml6
-rw-r--r--kernel/vmbytecodes.mli1
-rw-r--r--kernel/vmbytegen.ml25
-rw-r--r--kernel/vmemitcodes.ml5
17 files changed, 97 insertions, 138 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index b14ad5c558..4d2000bb52 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,5 +1,5 @@
(library
- (name byterun)
+ (name coqrun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq-core.vm)
(foreign_stubs
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 6ef0e9fa15..9e0f574fa3 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -295,38 +295,57 @@ let types =
PITT_param 1))
in
function
- | Int63head0 | Int63tail0 -> [int_ty; int_ty]
+ | Int63head0 | Int63tail0 ->
+ [int_ty], int_ty
| Int63add | Int63sub | Int63mul
| Int63div | Int63mod
| Int63divs | Int63mods
| Int63lsr | Int63lsl | Int63asr
- | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+ | Int63land | Int63lor | Int63lxor ->
+ [int_ty; int_ty], int_ty
| Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
- [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
+ [int_ty; int_ty], PITT_ind (PIT_carry, int_ty)
| Int63mulc | Int63diveucl ->
- [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
- | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
- | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+ [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+ | Int63eq | Int63lt | Int63le | Int63lts | Int63les ->
+ [int_ty; int_ty], PITT_ind (PIT_bool, ())
+ | Int63compare | Int63compares ->
+ [int_ty; int_ty], PITT_ind (PIT_cmp, ())
| Int63div21 ->
- [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
- | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
+ [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+ | Int63addMulDiv ->
+ [int_ty; int_ty; int_ty], int_ty
| Float64opp | Float64abs | Float64sqrt
- | Float64next_up | Float64next_down -> [float_ty; float_ty]
- | Float64ofInt63 -> [int_ty; float_ty]
- | Float64normfr_mantissa -> [float_ty; int_ty]
- | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))]
- | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
- | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
- | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
- | Float64add | Float64sub | Float64mul
- | Float64div -> [float_ty; float_ty; float_ty]
- | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
- | Arraymake -> [int_ty; PITT_param 1; array_ty]
- | Arrayget -> [array_ty; int_ty; PITT_param 1]
- | Arraydefault -> [array_ty; PITT_param 1]
- | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
- | Arraycopy -> [array_ty; array_ty]
- | Arraylength -> [array_ty; int_ty]
+ | Float64next_up | Float64next_down ->
+ [float_ty], float_ty
+ | Float64ofInt63 ->
+ [int_ty], float_ty
+ | Float64normfr_mantissa ->
+ [float_ty], int_ty
+ | Float64frshiftexp ->
+ [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty))
+ | Float64eq | Float64lt | Float64le ->
+ [float_ty; float_ty], PITT_ind (PIT_bool, ())
+ | Float64compare ->
+ [float_ty; float_ty], PITT_ind (PIT_f_cmp, ())
+ | Float64classify ->
+ [float_ty], PITT_ind (PIT_f_class, ())
+ | Float64add | Float64sub | Float64mul | Float64div ->
+ [float_ty; float_ty], float_ty
+ | Float64ldshiftexp ->
+ [float_ty; int_ty], float_ty
+ | Arraymake ->
+ [int_ty; PITT_param 1], array_ty
+ | Arrayget ->
+ [array_ty; int_ty], PITT_param 1
+ | Arraydefault ->
+ [array_ty], PITT_param 1
+ | Arrayset ->
+ [array_ty; int_ty; PITT_param 1], array_ty
+ | Arraycopy ->
+ [array_ty], array_ty
+ | Arraylength ->
+ [array_ty], int_ty
let one_param =
(* currently if there's a parameter it's always this *)
@@ -460,14 +479,17 @@ type args_red = arg_kind list
(* Invariant only argument of type int63, float or an inductive can
have kind Kwhnf *)
-let arity t = let sign = types t in nparams t + List.length sign - 1
+let arity t =
+ nparams t + List.length (fst (types t))
let kind t =
let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in
let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in
- params (nparams t) @ List.map args (CList.drop_last (types t))
+ params (nparams t) @ List.map args (fst (types t))
-let types t = params t, types t
+let types t =
+ let args_ty, ret_ty = types t in
+ params t, args_ty, ret_ty
(** Special Entries for Register **)
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index de90179726..6661851d53 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -140,8 +140,8 @@ val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
val univs : t -> Univ.AUContext.t
-val types : t -> Constr.rel_context * ind_or_type list
-(** Parameters * Reduction relevant arguments and output type
+val types : t -> Constr.rel_context * ind_or_type list * ind_or_type
+(** Parameters * Reduction relevant arguments * output type
XXX we could reify universes in ind_or_type (currently polymorphic types
like array are assumed to use universe 0). *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f82b754c59..87b1a71c9d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -252,9 +252,6 @@ let cook_constant { from = cb; info } =
cook_context = Some const_hyps;
}
-(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
-(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
-
(********************************)
(* Discharging mutual inductive *)
diff --git a/kernel/dune b/kernel/dune
index 0bf51f80ec..af88e9864f 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -4,7 +4,7 @@
(public_name coq-core.kernel)
(wrapped false)
(modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
- (libraries lib byterun dynlink))
+ (libraries lib coqrun dynlink))
(executable
(name genOpcodeFiles)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index eb18d4b90e..6cb61174d3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
else
()
-(*
-let cfkey = CProfile.declare_profile "check_fix";;
-let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
-*)
-
(************************************************************************)
(* Co-fixpoints. *)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c5ac57a2cd..d2fb773dc4 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -291,6 +291,11 @@ let subst_ind sub (ind,i as indi) =
let ind' = subst_mind sub ind in
if ind' == ind then indi else ind',i
+let subst_constructor subst (ind,j as ref) =
+ let ind' = subst_ind subst ind in
+ if ind==ind' then ref
+ else (ind',j)
+
let subst_pind sub (ind,u) =
(subst_ind sub ind, u)
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 9cf270cff7..e7bfceb4de 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -127,6 +127,9 @@ val subst_mind :
val subst_ind :
substitution -> inductive -> inductive
+val subst_constructor :
+ substitution -> constructor -> constructor
+
val subst_pind : substitution -> pinductive -> pinductive
val subst_kn :
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9ce388929c..22bbcb8a65 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -994,9 +994,8 @@ let extract_prim ml_of l =
let decl = ref [] in
let cond = ref [] in
let type_args p =
- let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
- let params, sign = CPrimitives.types p in
- List.length params, Array.of_list (aux sign) in
+ let params, args_ty, _ = CPrimitives.types p in
+ List.length params, Array.of_list args_ty in
let rec aux l =
match l with
| Lprim(prefix,kn,p,args) ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1e39756d47..18c3a3ec9c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -964,7 +964,8 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
-let gen_conv cv_pb l2r reds env evars univs t1 t2 =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _ -> None)) t1 t2 =
+ let univs = Environ.universes env in
let b =
if cv_pb = CUMUL then leq_constr_univs univs t1 t2
else eq_constr_univs univs t1 t2
@@ -974,16 +975,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
()
-(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
- let univs = Environ.universes env in
- if Flags.profile then
- let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
- CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
- else gen_conv cv_pb l2r reds env evars univs
-
let conv = gen_conv CONV
-
let conv_leq = gen_conv CUMUL
let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
@@ -992,7 +984,7 @@ let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
in s
-let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env t1 t2 =
let univs = Environ.universes env in
let b, cstrs =
if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
@@ -1001,37 +993,16 @@ let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
if b then cstrs
else
let state = ((univs, Univ.Constraint.empty), inferred_universes) in
- let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
+ let ((_,cstrs), _) = clos_gen_conv ts cv_pb l2r evars env univs state t1 t2 in
cstrs
-(* Profiling *)
-let infer_conv_universes =
- if Flags.profile then
- let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
- CProfile.profile7 infer_conv_universes_key infer_conv_universes
- else infer_conv_universes
-
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env t1 t2 =
- infer_conv_universes CONV l2r evars ts env t1 t2
-
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env t1 t2 =
- infer_conv_universes CUMUL l2r evars ts env t1 t2
+let infer_conv = infer_conv_universes CONV
+let infer_conv_leq = infer_conv_universes CUMUL
let default_conv cv_pb ?l2r:_ env t1 t2 =
gen_conv cv_pb env t1 t2
let default_conv_leq = default_conv CUMUL
-(*
-let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
-let conv_leq env t1 t2 =
- CProfile.profile4 convleqkey conv_leq env t1 t2;;
-
-let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
-let conv env t1 t2 =
- CProfile.profile4 convleqkey conv env t1 t2;;
-*)
(* Application with on-the-fly reduction *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 741491c917..3a946fc03a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -644,12 +644,6 @@ let infer env constr =
let constr, t = execute env constr in
make_judge constr t
-let infer =
- if Flags.profile then
- let infer_key = CProfile.declare_profile "Fast_infer" in
- CProfile.profile2 infer_key (fun b c -> infer b c)
- else (fun b c -> infer b c)
-
let assumption_of_judgment env {uj_val=c; uj_type=t} =
infer_assumption env c t
@@ -785,15 +779,16 @@ let type_of_prim env u t =
| PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t
| PITT_param i -> Constr.mkRel (n+i)
in
- let rec nary_op n = function
- | [] -> assert false
- | [ret_ty] -> tr_type n ret_ty
+ let rec nary_op n ret_ty = function
+ | [] -> tr_type n ret_ty
| arg_ty :: r ->
- Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r)
+ Constr.mkProd (Context.nameR (Id.of_string "x"),
+ tr_type n arg_ty, nary_op (n + 1) ret_ty r)
in
- let params, sign = types t in
+ let params, args_ty, ret_ty = types t in
assert (AUContext.size (univs t) = Instance.length u);
- Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params)
+ Vars.subst_instance_constr u
+ (Term.it_mkProd_or_LetIn (nary_op 0 ret_ty args_ty) params)
let type_of_prim_or_type env u = let open CPrimitives in
function
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index b988ec40a7..6db54a3bb6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -251,28 +251,3 @@ type node = G.node =
let repr g = G.repr g.graph
let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
-
-(** Profiling *)
-
-let merge_constraints =
- if Flags.profile then
- let key = CProfile.declare_profile "merge_constraints" in
- CProfile.profile2 key merge_constraints
- else merge_constraints
-let check_constraints =
- if Flags.profile then
- let key = CProfile.declare_profile "check_constraints" in
- CProfile.profile2 key check_constraints
- else check_constraints
-
-let check_eq =
- if Flags.profile then
- let check_eq_key = CProfile.declare_profile "check_eq" in
- CProfile.profile3 check_eq_key check_eq
- else check_eq
-
-let check_leq =
- if Flags.profile then
- let check_leq_key = CProfile.declare_profile "check_leq" in
- CProfile.profile3 check_leq_key check_leq
- else check_leq
diff --git a/kernel/vars.ml b/kernel/vars.ml
index b09577d4db..b9991391c2 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -123,11 +123,6 @@ let substn_many lamv n c =
| _ -> Constr.map_with_binders succ substrec depth c in
substrec n c
-(*
-let substkey = CProfile.declare_profile "substn_many";;
-let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;;
-*)
-
let make_subst = function
| [] -> [||]
| hd :: tl ->
@@ -343,9 +338,6 @@ let univ_instantiate_constr u c =
assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
subst_instance_constr u c.univ_abstracted_value
-(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
-
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c2b087f061..b5604d0593 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -35,6 +35,7 @@ type instruction =
| Kpush
| Kpop of int
| Kpush_retaddr of Label.t
+ | Kshort_apply of int
| Kapply of int
| Kappterm of int * int
| Kreturn of int
@@ -93,6 +94,7 @@ let rec pp_instr i =
| Kpush -> str "push"
| Kpop n -> str "pop " ++ int n
| Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+ | Kshort_apply n -> str "short_apply " ++ int n
| Kapply n -> str "apply " ++ int n
| Kappterm(n, m) ->
str "appterm " ++ int n ++ str ", " ++ int m
@@ -146,8 +148,8 @@ let rec pp_instr i =
(Constant.print (fst id))
| Kcamlprim (op, lbl) ->
- str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
- pp_lbl lbl
+ str "camlcall " ++ str (CPrimitives.to_string op) ++ str ", branch " ++
+ pp_lbl lbl ++ str " on accu"
and pp_bytecodes c =
match c with
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index eeca0d2ad1..d9e2d91177 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -30,6 +30,7 @@ type instruction =
| Kpush (** sp = accu :: sp *)
| Kpop of int (** sp = skipn n sp *)
| Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+ | Kshort_apply of int (** number of arguments (arguments on top of stack) *)
| Kapply of int (** number of arguments (arguments on top of stack) *)
| Kappterm of int * int (** number of arguments, slot size *)
| Kreturn of int (** slot size *)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 7d3b3469b0..b4d97228bf 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont =
| None ->
if nargs <= 4 then
comp_args comp_arg cenv args sz
- (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
+ (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont)))
else
let lbl,cont1 = label_code cont in
Kpush_retaddr lbl ::
@@ -757,26 +757,25 @@ let rec compile_lam env cenv lam sz cont =
let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
comp_args (compile_lam env) cenv args sz cont
- | Lprim ((kn,u), op, args) when is_caml_prim op ->
+ | Lprim (kn, op, args) when is_caml_prim op ->
let arity = CPrimitives.arity op in
let nparams = CPrimitives.nparams op in
let nargs = arity - nparams in
- assert (arity = Array.length args && arity <= 4);
+ assert (arity = Array.length args && arity <= 4 && nargs >= 1);
let (jump, cont) = make_branch cont in
let lbl_default = Label.create () in
let default =
- let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in
+ let cont = [Kshort_apply arity; jump] in
+ let cont = Kpush :: compile_get_global cenv kn (sz + arity) cont in
let cont =
- if Univ.Instance.is_empty u then cont
- else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont)
- in
- Klabel lbl_default ::
- Kpush ::
- if Int.equal nparams 0 then cont
- else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont)
- in
+ if Int.equal nparams 0 then cont
+ else
+ let params = Array.sub args 0 nparams in
+ Kpush :: comp_args (compile_lam env) cenv params (sz + nargs) cont in
+ Klabel lbl_default :: cont in
fun_code := Ksequence default :: !fun_code;
- comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont)
+ let cont = Kcamlprim (op, lbl_default) :: cont in
+ comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz cont
| Lprim (kn, op, args) ->
comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont)
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index caa263432e..44e933ef26 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -300,8 +300,11 @@ let emit_instr env = function
out env opPOP; out_int env n
| Kpush_retaddr lbl ->
out env opPUSH_RETADDR; out_label env lbl
+ | Kshort_apply n ->
+ assert (1 <= n && n <= 4);
+ out env(opAPPLY1 + n - 1)
| Kapply n ->
- if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
+ out env opAPPLY; out_int env n
| Kappterm(n, sz) ->
if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
else (out env opAPPTERM; out_int env n; out_int env sz)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 17:43:22 +0000