aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/vm_printers.ml7
-rw-r--r--kernel/byterun/coq_interp.c34
-rw-r--r--kernel/byterun/coq_values.h17
-rw-r--r--kernel/cbytecodes.ml57
-rw-r--r--kernel/cbytecodes.mli31
-rw-r--r--kernel/cbytegen.ml250
-rw-r--r--kernel/cbytegen.mli10
-rw-r--r--kernel/cemitcodes.ml23
-rw-r--r--kernel/cemitcodes.mli4
-rw-r--r--kernel/csymtable.ml30
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/mod_typing.ml10
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/term_typing.ml39
-rw-r--r--kernel/univ.ml7
-rw-r--r--kernel/univ.mli3
-rw-r--r--kernel/vars.ml4
-rw-r--r--kernel/vars.mli2
-rw-r--r--kernel/vconv.ml50
-rw-r--r--kernel/vm.ml112
-rw-r--r--kernel/vm.mli11
-rw-r--r--pretyping/vnorm.ml96
23 files changed, 578 insertions, 225 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 802b0f9d8..272df7b42 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -13,7 +13,7 @@ let ppripos (ri,pos) =
("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
| Reloc_const _ ->
print_string "structured constant\n"
- | Reloc_getglobal (kn,_) ->
+ | Reloc_getglobal kn ->
print_string ("getglob "^(string_of_con kn)^"\n"));
print_flush ()
@@ -30,7 +30,7 @@ let ppsort = function
let print_idkey idk =
match idk with
- | ConstKey (sp,_) ->
+ | ConstKey sp ->
print_string "Cons(";
print_string (string_of_con sp);
print_string ")"
@@ -61,7 +61,8 @@ and ppstack s =
and ppatom a =
match a with
| Aid idk -> print_idkey idk
- | Aind((sp,i),_) -> print_string "Ind(";
+ | Atype u -> print_string "Type(...)"
+ | Aind(sp,i) -> print_string "Ind(";
print_string (string_of_mind sp);
print_string ","; print_int i;
print_string ")"
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0553a5ed7..dc571699e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -341,6 +341,7 @@ value coq_interprete
/* Fallthrough */
Instruct(ENVACC){
print_instr("ENVACC");
+ print_int(*pc);
accu = Field(coq_env, *pc++);
Next;
}
@@ -371,6 +372,10 @@ value coq_interprete
sp[1] = (value)pc;
sp[2] = coq_env;
sp[3] = Val_long(coq_extra_args);
+ print_instr("call stack=");
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ print_lint(sp[3]);
pc = Code_val(accu);
coq_env = accu;
coq_extra_args = 0;
@@ -458,6 +463,7 @@ value coq_interprete
sp[0] = arg1;
sp[1] = arg2;
pc = Code_val(accu);
+ print_lint(accu);
coq_env = accu;
coq_extra_args += 1;
goto check_stacks;
@@ -481,11 +487,18 @@ value coq_interprete
print_instr("RETURN");
print_int(*pc);
sp += *pc++;
+ print_instr("stack=");
+ print_lint(sp[0]);
+ print_lint(sp[1]);
+ print_lint(sp[2]);
if (coq_extra_args > 0) {
+ print_instr("extra args > 0");
+ print_lint(coq_extra_args);
coq_extra_args--;
pc = Code_val(accu);
coq_env = accu;
} else {
+ print_instr("extra args = 0");
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -585,7 +598,10 @@ value coq_interprete
Alloc_small(accu, 1 + nvars, Closure_tag);
Code_val(accu) = pc + *pc;
pc++;
- for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
sp += nvars;
Next;
}
@@ -720,6 +736,7 @@ value coq_interprete
/* Fallthrough */
Instruct(GETGLOBAL){
print_instr("GETGLOBAL");
+ print_int(*pc);
accu = Field(coq_global_data, *pc);
pc++;
Next;
@@ -732,7 +749,7 @@ value coq_interprete
tag_t tag = *pc++;
mlsize_t i;
value block;
- print_instr("MAKEBLOCK");
+ print_instr("MAKEBLOCK, tag=");
Alloc_small(block, wosize, tag);
Field(block, 0) = accu;
for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -743,7 +760,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK1");
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
Alloc_small(block, 1, tag);
Field(block, 0) = accu;
accu = block;
@@ -753,7 +771,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK2");
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
Alloc_small(block, 2, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -764,7 +783,8 @@ value coq_interprete
Instruct(MAKEBLOCK3) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK3");
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
Alloc_small(block, 3, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -776,7 +796,8 @@ value coq_interprete
Instruct(MAKEBLOCK4) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK4");
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
Alloc_small(block, 4, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -940,6 +961,7 @@ value coq_interprete
/* Fallthrough */
Instruct(CONSTINT) {
print_instr("CONSTINT");
+ print_int(*pc);
accu = Val_int(*pc);
pc++;
Next;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 80100da71..bb0f0eb5e 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,22 +17,17 @@
#define Default_tag 0
#define Accu_tag 0
-
-
#define ATOM_ID_TAG 0
#define ATOM_INDUCTIVE_TAG 1
-#define ATOM_PROJ_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#define ATOM_TYPE_TAG 2
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
/* Les blocs accumulate */
#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#endif /* _COQ_VALUES_ */
-
-
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 448bf8544..b13b0607b 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -19,13 +19,12 @@ type tag = int
let accu_tag = 0
-let max_atom_tag = 1
-let proj_tag = 2
-let fix_app_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-
+let max_atom_tag = 2
+let proj_tag = 3
+let fix_app_tag = 4
+let switch_tag = 5
+let cofix_tag = 6
+let cofix_evaluated_tag = 7
(* It would be great if OCaml exported this value,
So fixme if this happens in a new version of OCaml *)
@@ -33,10 +32,12 @@ let last_variant_tag = 245
type structured_constant =
| Const_sorts of sorts
- | Const_ind of pinductive
+ | 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.universe_level
+ | Const_type of Univ.universe
type reloc_table = (tag * int) array
@@ -71,7 +72,8 @@ type instruction =
| Kclosure of Label.t * int
| Kclosurerec of int * int * Label.t array * Label.t array
| Kclosurecofix of int * int * Label.t array * Label.t array
- | Kgetglobal of pconstant
+ (* nb fv, init, lbl types, lbl bodies *)
+ | Kgetglobal of constant
| Kconst of structured_constant
| Kmakeblock of int * tag
| Kmakeprod
@@ -127,7 +129,10 @@ type instruction =
and bytecodes = instruction list
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+ | FVnamed of Id.t
+ | FVrel of int
+ | FVuniv_var of int
type fv = fv_elem array
@@ -145,18 +150,17 @@ type vm_env = {
type comp_env = {
- nb_stack : int; (* nbre de variables sur la pile *)
- in_stack : int list; (* position dans la pile *)
- nb_rec : int; (* nbre de fonctions mutuellement *)
- (* recursives = nbr *)
+ nb_uni_stack : int ; (* number of universes on the stack, *)
+ (* universes are always at the bottom. *)
+ nb_stack : int; (* number of variables on the stack *)
+ in_stack : int list; (* position in the stack *)
+ nb_rec : int; (* number of mutually recursive functions *)
pos_rec : instruction list; (* instruction d'acces pour les variables *)
(* de point fix ou de cofix *)
offset : int;
- in_env : vm_env ref
+ in_env : vm_env ref (* The free variables of the expression *)
}
-
-
(* --- Pretty print *)
open Pp
open Util
@@ -169,14 +173,24 @@ let pp_sort s =
let rec pp_struct_const = function
| Const_sorts s -> pp_sort s
- | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+ | Const_ind (mind, i) -> pr_mind 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)
+ | Const_univ_level l -> Univ.Level.pr l
+ | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
let pp_lbl lbl = str "L" ++ int lbl
+let pp_pcon (id,u) =
+ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+
+let pp_fv_elem = function
+ | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
+ | FVrel i -> str "Rel(" ++ int i ++ str ")"
+ | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+
let rec pp_instr i =
match i with
| Klabel _ | Ksequence _ -> assert false
@@ -210,8 +224,7 @@ let rec pp_instr i =
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
str " bodies = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
- | Kgetglobal (id,u) ->
- str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+ | Kgetglobal idu -> str "getglobal " ++ pr_con idu
| Kconst sc ->
str "const " ++ pp_struct_const sc
| Kmakeblock(n, m) ->
@@ -269,10 +282,6 @@ and pp_bytecodes c =
| i :: c ->
tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
-let dump_bytecode c =
- pperrnl (pp_bytecodes c);
- flush_all()
-
(*spiwack: moved this type in this file because I needed it for
retroknowledge which can't depend from cbytegen *)
type block =
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03d638305..c35ef6920 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -22,14 +22,18 @@ val switch_tag : tag
val cofix_tag : tag
val cofix_evaluated_tag : tag
-val last_variant_tag : tag
+val last_variant_tag : tag
type structured_constant =
| Const_sorts of sorts
- | Const_ind of pinductive
+ | 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.universe_level
+ | Const_type of Univ.universe
+
+val pp_struct_const : structured_constant -> Pp.std_ppcmds
type reloc_table = (tag * int) array
@@ -64,9 +68,11 @@ type instruction =
(** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(** nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of pconstant (** accu = coq_global_data[c] *)
+ | Kgetglobal of constant
| Kconst of structured_constant
- | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *)
+ | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
+ ** is accu, all others are popped from
+ ** the top of the stack *)
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
| Kswitch of Label.t array * Label.t array (** consts,blocks *)
@@ -120,7 +126,10 @@ type instruction =
and bytecodes = instruction list
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+ FVnamed of Id.t
+| FVrel of int
+| FVuniv_var of int
type fv = fv_elem array
@@ -129,26 +138,28 @@ type fv = fv_elem array
closed terms. *)
exception NotClosed
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Cbytegen because I needed them
for the retroknowledge *)
type vm_env = {
- size : int; (** longueur de la liste [n] *)
+ size : int; (** length of the list [n] *)
fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
}
type comp_env = {
+ nb_uni_stack : int ; (** number of universes on the stack *)
nb_stack : int; (** number of variables on the stack *)
in_stack : int list; (** position in the stack *)
nb_rec : int; (** number of mutually recursive functions *)
- (** recursives = nbr *)
+ (** (= nbr) *)
pos_rec : instruction list; (** instruction d'acces pour les variables *)
(** de point fix ou de cofix *)
offset : int;
- in_env : vm_env ref
+ in_env : vm_env ref (** the variables that are accessed *)
}
-val dump_bytecode : bytecodes -> unit
+val pp_bytecodes : bytecodes -> Pp.std_ppcmds
+val pp_fv_elem : fv_elem -> Pp.std_ppcmds
(*spiwack: moved this here because I needed it for retroknowledge *)
type block =
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 3462694d6..f9f72efdb 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -96,13 +96,14 @@ let empty_fv = { size= 0; fv_rev = [] }
let fv r = !(r.in_env)
-let empty_comp_env ()=
- { nb_stack = 0;
+let empty_comp_env ?(univs=0) ()=
+ { nb_uni_stack = univs;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
offset = 0;
- in_env = ref empty_fv;
+ in_env = ref empty_fv
}
(*i Creation functions for comp_env *)
@@ -110,8 +111,9 @@ let empty_comp_env ()=
let rec add_param n sz l =
if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
-let comp_env_fun arity =
- { nb_stack = arity;
+let comp_env_fun ?(univs=0) arity =
+ { nb_uni_stack = univs ;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = 0;
pos_rec = [];
@@ -120,8 +122,9 @@ let comp_env_fun arity =
}
-let comp_env_fix_type rfv =
- { nb_stack = 0;
+let comp_env_fix_type rfv =
+ { nb_uni_stack = 0;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
@@ -134,7 +137,8 @@ let comp_env_fix ndef curr_pos arity rfv =
for i = ndef downto 1 do
prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
done;
- { nb_stack = arity;
+ { nb_uni_stack = 0;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = ndef;
pos_rec = !prec;
@@ -143,7 +147,8 @@ let comp_env_fix ndef curr_pos arity rfv =
}
let comp_env_cofix_type ndef rfv =
- { nb_stack = 0;
+ { nb_uni_stack = 0;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
@@ -156,7 +161,8 @@ let comp_env_cofix ndef arity rfv =
for i = 1 to ndef do
prec := Kenvacc i :: !prec
done;
- { nb_stack = arity;
+ { nb_uni_stack = 0;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = ndef;
pos_rec = !prec;
@@ -168,7 +174,7 @@ let comp_env_cofix ndef arity rfv =
let push_param n sz r =
{ r with
nb_stack = r.nb_stack + n;
- in_stack = add_param n sz r.in_stack }
+ in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack }
(* [push_local sz r] add a new variable on the stack at position [sz] *)
let push_local sz r =
@@ -176,8 +182,6 @@ let push_local sz r =
nb_stack = r.nb_stack + 1;
in_stack = (sz + 1) :: r.in_stack }
-
-
(*i Compilation of variables *)
let find_at f l =
let rec aux n = function
@@ -214,6 +218,37 @@ let pos_rel i r sz =
r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
Kenvacc(r.offset + pos)
+(*
+let pos_poly_inst idu r =
+ let env = !(r.in_env) in
+ let f = function
+ | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i
+ | _ -> false
+ in
+ try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+ with Not_found ->
+ let pos = env.size in
+ let db = FVpoly_inst idu in
+ r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
+ Kenvacc(r.offset + pos)
+*)
+
+let pos_universe_var i r sz =
+ if i < r.nb_uni_stack then
+ Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
+ else
+ let env = !(r.in_env) in
+ let f = function
+ | FVuniv_var u -> Int.equal i u
+ | _ -> false
+ in
+ try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+ with Not_found ->
+ let pos = env.size in
+ let db = FVuniv_var i in
+ r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+ Kenvacc(r.offset + pos)
+
(*i Examination of the continuation *)
(* Discard all instructions up to the next label. *)
@@ -459,7 +494,8 @@ let rec str_const c =
end
| _ -> Bconstr c
end
- | Ind ind -> Bstrconst (Const_ind ind)
+ | Ind (ind,_) ->
+ Bstrconst (Const_ind ind)
| Construct (((kn,j),i),u) ->
begin
(* spiwack: tries first to apply the run-time compilation
@@ -513,6 +549,7 @@ let compile_fv_elem reloc 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
let rec compile_fv reloc l sz cont =
match l with
@@ -524,18 +561,21 @@ let rec compile_fv reloc l sz cont =
(* Compiling constants *)
-let rec get_alias env (kn,u as p) =
+let rec get_alias env kn =
let cb = lookup_constant kn env in
let tps = cb.const_body_code in
match tps with
- | None -> p
+ | None -> kn
| Some tps ->
(match Cemitcodes.force tps with
- | BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u')
- | _ -> p)
+ | BCalias kn' -> get_alias env kn'
+ | _ -> kn)
(* Compiling expressions *)
+type ('a,'b) sum = Inl of 'a | Inr of 'b
+
+(* sz is the size of the local stack *)
let rec compile_constr reloc c sz cont =
match kind_of_term c with
| Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
@@ -552,9 +592,40 @@ let rec compile_constr reloc c sz cont =
| Rel i -> pos_rel i reloc sz :: cont
| Var id -> pos_named id reloc :: cont
| Const (kn,u) -> compile_const reloc kn u [||] sz cont
- | Sort _ | Ind _ | Construct _ ->
+ | Ind (i,u) ->
+ if Univ.Instance.is_empty u then
compile_str_cst reloc (str_const c) sz cont
-
+ else
+ comp_app compile_str_cst compile_universe reloc
+ (str_const c)
+ (Univ.Instance.to_array u)
+ sz
+ cont
+ | Sort (Prop _) | Construct _ ->
+ compile_str_cst reloc (str_const c) sz cont
+ | Sort (Type u) ->
+ begin
+ let levels = Univ.Universe.levels u in
+ if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels
+ then
+ (** TODO(gmalecha): Fix this **)
+ (** NOTE: This relies on the order of iteration to be consistent
+ **)
+ let level_vars =
+ List.map_filter (fun x -> Univ.Level.var_index x)
+ (Univ.LSet.elements levels)
+ in
+ let compile_get_univ reloc idx sz cont =
+ compile_fv_elem reloc (FVuniv_var idx) sz cont
+ in
+ comp_app compile_str_cst compile_get_univ reloc
+ (Bstrconst (Const_type u))
+ (Array.of_list level_vars)
+ sz
+ cont
+ else
+ compile_str_cst reloc (str_const c) sz cont
+ end
| LetIn(_,xb,_,body) ->
compile_constr reloc xb sz
(Kpush ::
@@ -663,7 +734,9 @@ let rec compile_constr reloc c sz cont =
let lbl_sw = Label.create () in
let sz_b,branch,is_tailcall =
match branch1 with
- | Kreturn k -> assert (Int.equal k sz); sz, branch1, true
+ | Kreturn k ->
+ assert (Int.equal k sz) ;
+ sz, branch1, true
| _ -> sz+3, Kjump, false
in
let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -745,6 +818,19 @@ and compile_str_cst reloc sc sz 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 =
+ let kn = get_alias !global_env kn in
+ 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
+
+and compile_universe reloc uni sz cont =
+ match Univ.Level.var_index uni with
+ | None -> Kconst (Const_univ_level uni) :: cont
+ | Some idx -> pos_universe_var idx reloc sz :: cont
+
and compile_const =
fun reloc-> fun kn u -> fun args -> fun sz -> fun cont ->
let nargs = Array.length args in
@@ -756,31 +842,83 @@ and compile_const =
(mkConstU (kn,u)) reloc args sz cont
with Not_found ->
if Int.equal nargs 0 then
- Kgetglobal (get_alias !global_env (kn, u)) :: cont
+ compile_get_global reloc (kn,u) sz cont
else
- comp_app (fun _ _ _ cont ->
- Kgetglobal (get_alias !global_env (kn,u)) :: cont)
- compile_constr reloc () args sz cont
-
-let compile fail_on_error env c =
+ if Univ.Instance.is_empty u then
+ (* normal compilation *)
+ comp_app (fun _ _ sz cont ->
+ compile_get_global reloc (kn,u) sz cont)
+ compile_constr reloc () args sz cont
+ else
+ let compile_either reloc constr_or_uni sz cont =
+ match constr_or_uni with
+ | Inl cst -> compile_constr reloc cst sz cont
+ | Inr uni -> compile_universe reloc uni sz cont
+ in
+ (** TODO(gmalecha): This can be more efficient **)
+ let all =
+ Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @
+ List.map (fun x -> Inl x) (Array.to_list args))
+ in
+ comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+ compile_either reloc () all sz cont
+
+let is_univ_copy max u =
+ let u = Univ.Instance.to_array u in
+ if Array.length u = max then
+ Array.fold_left_i (fun i acc u ->
+ if acc then
+ match Univ.Level.var_index u with
+ | None -> false
+ | Some l -> l = i
+ else false) true u
+ else
+ false
+
+let dump_bytecodes init code fvs =
+ let open Pp in
+ (str "code =" ++ fnl () ++
+ pp_bytecodes init ++ fnl () ++
+ pp_bytecodes code ++ fnl () ++
+ str "fv = " ++
+ prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
+ fnl ())
+
+let compile fail_on_error ?universes:(universes=0) env c =
set_global_env env;
init_fun_code ();
Label.reset_label_counter ();
- let reloc = empty_comp_env () in
- try
- let init_code = compile_constr reloc c 0 [Kstop] in
- let fv = List.rev (!(reloc.in_env).fv_rev) in
- let pp_v v =
- match v with
- | FVnamed id -> Pp.str (Id.to_string id)
- | FVrel i -> Pp.str (string_of_int i)
+ let cont = [Kstop] in
+ try
+ let reloc, init_code =
+ if Int.equal universes 0 then
+ let reloc = empty_comp_env () in
+ reloc, compile_constr reloc c 0 cont
+ else
+ (* We are going to generate a lambda, but merge the universe closure
+ * with the function closure if it exists.
+ *)
+ let reloc = empty_comp_env () in
+ let arity , body =
+ match kind_of_term c with
+ | Lambda _ ->
+ let params, body = decompose_lam c in
+ List.length params , body
+ | _ -> 0 , c
+ in
+ let full_arity = arity + universes in
+ let r_fun = comp_env_fun ~univs:universes arity in
+ let lbl_fun = Label.create () in
+ let cont_fun =
+ compile_constr r_fun body full_arity [Kreturn full_arity]
+ in
+ fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
+ let fv = fv r_fun in
+ reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont)
in
- let open Pp in
- if !Flags.dump_bytecode then
- (dump_bytecode init_code;
- dump_bytecode !fun_code;
- Pp.msg_debug (Pp.str "fv = " ++
- Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ()));
+ let fv = List.rev (!(reloc.in_env).fv_rev) in
+ (if !Flags.dump_bytecode then
+ Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
@@ -789,28 +927,33 @@ let compile fail_on_error env c =
Id.print tname ++ str str_max_constructors));
None)
-let compile_constant_body fail_on_error env = function
+let compile_constant_body fail_on_error env univs = function
| Undef _ | OpaqueDef _ -> Some BCconstant
| Def sb ->
let body = Mod_subst.force_constr sb in
+ let instance_size =
+ match univs with
+ | None -> 0
+ | Some univ -> Univ.UContext.size univ
+ in
match kind_of_term body with
- | Const (kn',u) ->
+ | Const (kn',u) when is_univ_copy instance_size u ->
(* we use the canonical name of the constant*)
let con= constant_of_kn (canonical_con kn') in
- Some (BCalias (get_alias env (con,u)))
+ Some (BCalias (get_alias env con))
| _ ->
- let res = compile fail_on_error env body in
+ let res = compile fail_on_error ~universes:instance_size env body in
Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
-let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u)
+let compile_alias kn = BCalias (constant_of_kn (canonical_con kn))
(* spiwack: additional function which allow different part of compilation of the
31-bit integers *)
let make_areconst n else_lbl cont =
- if n <=0 then
+ if n <= 0 then
cont
else
Kareconst (n, else_lbl)::cont
@@ -902,14 +1045,14 @@ let op2_compilation op =
3/ if at least one is not, branches to the normal behavior:
Kgetglobal (get_alias !global_env kn) *)
let op_compilation n op =
- let code_construct kn cont =
+ let code_construct reloc 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]*)
- Kgetglobal (get_alias !global_env kn)::
- Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
+ compile_get_global reloc 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)];
@@ -926,12 +1069,11 @@ let op_compilation n op =
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs = n and non-tailcall cont*)
- Kgetglobal (get_alias !global_env kn)::
- Kapply n::labeled_cont)))
+ compile_get_global reloc kn sz (Kapply n::labeled_cont))))
else if Int.equal nargs 0 then
- code_construct kn cont
+ code_construct reloc kn sz cont
else
- comp_app (fun _ _ _ cont -> code_construct kn cont)
+ comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
compile_constr reloc () args sz cont
let int31_escape_before_match fc cont =
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 1128f0d0b..c0f48641c 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -4,17 +4,17 @@ open Term
open Declarations
open Pre_env
-
+(** Should only be used for monomorphic terms *)
val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
- env -> constr -> (bytecodes * bytecodes * fv) option
+ ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
(** init, fun, fv *)
-val compile_constant_body : bool ->
- env -> constant_def -> body_code option
+val compile_constant_body : bool ->
+ env -> constant_universes option -> constant_def -> body_code option
(** Shortcut of the previous function used during module strengthening *)
-val compile_alias : pconstant -> body_code
+val compile_alias : Names.constant -> body_code
(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 9b275cb6c..2a70d0b1b 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -19,7 +19,7 @@ open Mod_subst
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of pconstant
+ | Reloc_getglobal of Names.constant
type patch = reloc_info * int
@@ -127,11 +127,11 @@ let slot_for_const c =
enter (Reloc_const c);
out_int 0
-and slot_for_annot a =
+let slot_for_annot a =
enter (Reloc_annot a);
out_int 0
-and slot_for_getglobal p =
+let slot_for_getglobal p =
enter (Reloc_getglobal p);
out_int 0
@@ -190,7 +190,7 @@ let emit_instr = function
Array.iter (out_label_with_orig org) lbl_bodies
| Kgetglobal q ->
out opGETGLOBAL; slot_for_getglobal q
- | Kconst((Const_b0 i)) ->
+ | Kconst (Const_b0 i) ->
if i >= 0 && i <= 3
then out (opCONST0 + i)
else (out opCONSTINT; out_int i)
@@ -310,7 +310,7 @@ let rec subst_strcst s sc =
| Const_sorts _ | Const_b0 _ -> 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,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
+ | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
let subst_patch s (ri,pos) =
match ri with
@@ -319,7 +319,7 @@ let subst_patch s (ri,pos) =
let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
(Reloc_annot {a with ci = ci},pos)
| Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
+ | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
@@ -328,12 +328,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
type body_code =
| BCdefined of to_patch
- | BCalias of pconstant
+ | BCalias of Names.constant
| BCconstant
type to_patch_substituted =
| PBCdefined of to_patch substituted
-| PBCalias of pconstant substituted
+| PBCalias of Names.constant substituted
| PBCconstant
let from_val = function
@@ -343,7 +343,7 @@ let from_val = function
let force = function
| PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCalias cu -> BCalias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
| PBCconstant -> BCconstant
let subst_to_patch_subst s = function
@@ -373,8 +373,3 @@ let to_memory (init_code, fun_code, fv) =
| Label_undefined patchlist ->
assert (patchlist = []))) !label_table;
(code, reloc, fv)
-
-
-
-
-
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 54b92b912..10f3a6087 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of constant Univ.puniverses
+ | Reloc_getglobal of constant
type patch = reloc_info * int
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
| BCdefined of to_patch
- | BCalias of constant Univ.puniverses
+ | BCalias of constant
| BCconstant
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b3f0ba5b5..28f0fa4f2 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -58,7 +58,7 @@ let set_global v =
let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
| Const_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| 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
@@ -67,18 +67,24 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_bn (t1, a1), Const_bn (t2, a2) ->
Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
let rec hash_structured_constant c =
let open Hashset.Combine in
match c with
| Const_sorts s -> combinesmall 1 (Sorts.hash s)
- | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
+ | 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_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)
+ | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
@@ -124,7 +130,7 @@ exception NotEvaluated
let key rk =
match !rk with
| None -> raise NotEvaluated
- | Some k -> (*Pp.msgnl (str"found at: "++int k);*)
+ | Some k ->
try Ephemeron.get k
with Ephemeron.InvalidKey -> raise NotEvaluated
@@ -148,23 +154,22 @@ let slot_for_annot key =
AnnotTable.add annot_tbl key n;
n
-let rec slot_for_getglobal env (kn,u) =
+let rec slot_for_getglobal env kn =
let (cb,(_,rk)) = lookup_constant_key kn env in
try key rk
with NotEvaluated ->
(* Pp.msgnl(str"not yet evaluated");*)
let pos =
match cb.const_body_code with
- | None -> set_global (val_of_constant (kn,u))
+ | None -> set_global (val_of_constant kn)
| Some code ->
match Cemitcodes.force code with
| BCdefined(code,pl,fv) ->
- if Univ.Instance.is_empty u then
- let v = eval_to_patch env (code,pl,fv) in
- set_global v
- else set_global (val_of_constant (kn,u))
+ let v = eval_to_patch env (code,pl,fv) in
+ set_global v
| BCalias kn' -> slot_for_getglobal env kn'
- | BCconstant -> set_global (val_of_constant (kn,u)) in
+ | BCconstant -> set_global (val_of_constant kn)
+ in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (Ephemeron.create pos);
pos
@@ -197,6 +202,8 @@ and slot_for_fv env fv =
fill_fv_cache rv i val_of_rel env_of_rel b
| Some (v, _) -> v
end
+ | FVuniv_var idu ->
+ assert false
and eval_to_patch env (buff,pl,fv) =
(* copy code *before* patching because of nested evaluations:
@@ -214,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) =
List.iter patch pl;
let vm_env = Array.map (slot_for_fv env) fv in
let tc = tcode_of_code buff (length buff) in
-(*Pp.msgnl (str"execute code");*)
eval_tcode tc vm_env
and val_of_constr env c =
@@ -232,5 +238,3 @@ and val_of_constr env c =
let set_transparent_const kn = () (* !?! *)
let set_opaque_const kn = () (* !?! *)
-
-
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9f6ea522a..dfe6cc85b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -250,7 +250,7 @@ type unsafe_type_judgment = {
(** {6 Compilation of global declaration } *)
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
+val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option
exception Hyp_not_found
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index c03c5175f..bd7ee7b33 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -126,11 +126,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
in
let def = Def (Mod_subst.from_val c') in
+(* let ctx' = Univ.UContext.make (newus, cst) in *)
+ let univs =
+ if cb.const_polymorphic then Some cb.const_universes
+ else None
+ in
let cb' =
{ cb with
const_body = def;
- const_universes = univs;
- const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) }
+ const_universes = ctx ;
+ const_body_code = Option.map Cemitcodes.from_val
+ (compile_constant_body env' univs def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index f0cb65c96..cbb796331 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -335,7 +335,7 @@ let strengthen_const mp_from l cb resolver =
in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
+ const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 263befd21..4d033bc99 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) =
| None -> p
| Some tps ->
match Cemitcodes.force tps with
- | Cemitcodes.BCalias kn' -> get_alias env kn'
+ | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
| _ -> p
(*i Global environment *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b6df8f454..cab99077f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -258,33 +258,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
check declared inferred) lc) in
let tps =
- (* FIXME: incompleteness of the bytecode vm: we compile polymorphic
- constants like opaque definitions. *)
- if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
- else
- let res =
- match proj with
- | None -> compile_constant_body env def
- | Some pb ->
+ let res =
+ let comp_univs = if poly then Some univs else None in
+ match proj with
+ | None -> compile_constant_body env comp_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 = proj;
- const_body_code = None;
- const_polymorphic = poly;
- const_universes = univs;
- const_inline_code = inline_code }
- in
- let env = add_constant kn cb env in
- compile_constant_body env def
- in Option.map Cemitcodes.from_val res
+ let cb =
+ { const_hyps = hyps;
+ const_body = def;
+ const_type = typ;
+ const_proj = proj;
+ const_body_code = None;
+ const_polymorphic = poly;
+ const_universes = univs;
+ const_inline_code = inline_code }
+ in
+ let env = add_constant kn cb env in
+ compile_constant_body env comp_univs def
+ in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
diff --git a/kernel/univ.ml b/kernel/univ.ml
index c0bd3bacd..064dde3a6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1754,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') =
f x y && Instance.equal u u'
(** A context of universe levels with universe constraints,
- representiong local universe variables and constraints *)
+ representing local universe variables and constraints *)
module UContext =
struct
@@ -1778,8 +1778,11 @@ struct
let union (univs, cst) (univs', cst') =
Instance.append univs univs', Constraint.union cst cst'
-
+
let dest x = x
+
+ let size (x,_) = Instance.length x
+
end
type universe_context = UContext.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index cbaf7e546..c926c57bd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -343,6 +343,9 @@ sig
(** Keeps the order of the instances *)
val union : t -> t -> t
+ (* the number of universes in the context *)
+ val size : t -> int
+
end
type universe_context = UContext.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 88c1e1038..a800e2531 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -337,5 +337,5 @@ let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else map_rel_context (fun x -> subst_instance_constr s x) ctx
-type id_key = pconstant tableKey
-let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
+type id_key = constant tableKey
+let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdd4603b5..c0fbeeb6e 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -88,5 +88,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_
val subst_instance_constr : universe_instance -> constr -> constr
val subst_instance_context : universe_instance -> rel_context -> rel_context
-type id_key = pconstant tableKey
+type id_key = constant tableKey
val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2f6be0601..e0d968848 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 cu =
else conv_whd env pb k (whd_val v1) (whd_val v2) cu
and conv_whd env pb k whd1 whd2 cu =
+(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
match whd1, whd2 with
| Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
+ | Vuniv_level _ , _
+ | _ , Vuniv_level _ ->
+ (** Both of these are invalid since universes are handled via
+ ** special cases in the code.
+ **)
+ assert false
| Vprod p1, Vprod p2 ->
let cu = conv_val env CONV k (dom p1) (dom p2) cu in
conv_fun env pb k (codom p1) (codom p2) cu
@@ -81,26 +88,53 @@ and conv_whd env pb k whd1 whd2 cu =
and conv_atom env pb k a1 stk1 a2 stk2 cu =
+(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
match a1, a2 with
- | Aind ind1, Aind ind2 ->
- if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
+ | Aind ((mi,i) as ind1) , Aind ind2 ->
+ if eq_ind ind1 ind2 && compare_stack stk1 stk2
then
- conv_stack env k stk1 stk2 cu
+ if Environ.polymorphic_ind ind1 env
+ then
+ let mib = Environ.lookup_mind mi env in
+ let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+ match stk1 , stk2 with
+ | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+ assert (ulen <= nargs args1) ;
+ assert (ulen <= nargs args2) ;
+ for i = 0 to ulen - 1 do
+ let a1 = uni_lvl_val (arg args1 i) in
+ let a2 = uni_lvl_val (arg args2 i) in
+ let result = Univ.Level.equal a1 a2 in
+ if not result
+ then raise NotConvertible
+ done ;
+ conv_arguments env ~from:ulen k args1 args2
+ (conv_stack env k stk1' stk2' cu)
+ | _ -> raise NotConvertible
+ else
+ conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
+ | Atype u1 , Atype u2 ->
+ let u1 = Vm.instantiate_universe u1 stk1 in
+ let u2 = Vm.instantiate_universe u2 stk2 in
+ sort_cmp_universes env pb (Type u1) (Type u2) cu
+ | Atype _ , Aid _
+ | Atype _ , Aind _
+ | Aid _ , Atype _
| Aind _, _ | Aid _, _ -> raise NotConvertible
-and conv_stack env k stk1 stk2 cu =
+and conv_stack env ?from:(from=0) k stk1 stk2 cu =
match stk1, stk2 with
| [], [] -> cu
| Zapp args1 :: stk1, Zapp args2 :: stk2 ->
- conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
+ conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu)
| Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
conv_stack env k stk1 stk2
- (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
+ (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu))
| Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
if check_switch sw1 sw2 then
let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
@@ -144,13 +178,13 @@ and conv_cofix env k cf1 cf2 cu =
conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
else raise NotConvertible
-and conv_arguments env k args1 args2 cu =
+and conv_arguments env ?from:(from=0) k args1 args2 cu =
if args1 == args2 then cu
else
let n = nargs args1 in
if Int.equal n (nargs args2) then
let rcu = ref cu in
- for i = 0 to n - 1 do
+ for i = from to n - 1 do
rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
done;
!rcu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index eacd803fd..858f546c6 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -121,12 +121,12 @@ type vswitch = {
(* *)
(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
-(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *)
-(* -- 3_[accu|proj name] : a projection blocked by an accu *)
-(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *)
-(* -- 5_[accu|vswitch] : a match blocked by an accu *)
-(* -- 6_[fcofix] : a cofix function *)
-(* -- 7_[fcofix|val] : a cofix function, val represent the value *)
+(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *)
+(* -- 10_[accu|proj name] : a projection blocked by an accu *)
+(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *)
+(* -- 12_[accu|vswitch] : a match blocked by an accu *)
+(* -- 13_[fcofix] : a cofix function *)
+(* -- 14_[fcofix|val] : a cofix function, val represent the value *)
(* of the function applied to arg1 ... argn *)
(* The [arguments] type, which is abstracted as an array, represents : *)
(* tag[ _ | _ |v1|... | vn] *)
@@ -136,7 +136,8 @@ type vswitch = {
type atom =
| Aid of Vars.id_key
- | Aind of pinductive
+ | Aind of inductive
+ | Atype of Univ.universe
(* Zippers *)
@@ -159,6 +160,7 @@ type whd =
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
+ | Vuniv_level of Univ.universe_level
(*************************************************)
(* Destructors ***********************************)
@@ -199,7 +201,9 @@ let rec whd_accu a stk =
| [Zapp args] -> Vcofix(vcofix, res, Some args)
| _ -> assert false
end
- | _ -> assert false
+ | tg ->
+ Errors.anomaly
+ Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg)
external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
@@ -212,22 +216,45 @@ let whd_val : values -> whd =
if tag = accu_tag then
(
if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
- else
+ else
if is_accumulate (fun_code o) then whd_accu o []
- else (Vprod(Obj.obj o)))
+ else Vprod(Obj.obj o))
else
if tag = Obj.closure_tag || tag = Obj.infix_tag then
- ( match kind_of_closure o with
+ (match kind_of_closure o with
| 0 -> Vfun(Obj.obj o)
| 1 -> Vfix(Obj.obj o, None)
| 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
| 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
| _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
- else
- Vconstr_block(Obj.obj o)
-
+ else
+ Vconstr_block(Obj.obj o)
+
+let uni_lvl_val : values -> Univ.universe_level =
+ fun v ->
+ let whd = Obj.magic v in
+ match whd with
+ | Vuniv_level lvl -> lvl
+ | _ ->
+ let pr =
+ let open Pp in
+ match whd with
+ | Vsort _ -> str "Vsort"
+ | Vprod _ -> str "Vprod"
+ | Vfun _ -> str "Vfun"
+ | Vfix _ -> str "Vfix"
+ | Vcofix _ -> str "Vcofix"
+ | Vconstr_const i -> str "Vconstr_const"
+ | Vconstr_block b -> str "Vconstr_block"
+ | Vatom_stk (a,stk) -> str "Vatom_stk"
+ | _ -> assert false
+ in
+ Errors.anomaly
+ Pp.( strbrk "Parsing virtual machine value expected universe level, got "
+ ++ pr)
+
(************************************************)
-(* Abstrct machine ******************************)
+(* Abstract machine *****************************)
(************************************************)
(* gestion de la pile *)
@@ -299,6 +326,8 @@ let rec obj_of_str_const str =
Obj.set_field res i (obj_of_str_const args.(i))
done;
res
+ | Const_univ_level l -> Obj.repr (Vuniv_level l)
+ | Const_type u -> obj_of_atom (Atype u)
let val_of_obj o = ((Obj.obj o) : values)
@@ -317,11 +346,11 @@ let val_of_proj kn v =
module IdKeyHash =
struct
- type t = pconstant tableKey
- let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
+ type t = constant tableKey
+ let equal = Names.eq_table_key Constant.equal
open Hashset.Combine
let hash = function
- | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
+ | ConstKey c -> combinesmall 1 (Constant.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
end
@@ -606,3 +635,50 @@ let apply_whd k whd =
interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
| Vatom_stk(a,stk) ->
apply_stack (val_of_atom a) stk v
+ | Vuniv_level lvl -> assert false
+
+let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe =
+ match stk with
+ | [] -> u
+ | [Zapp args] ->
+ assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ;
+ let _,mp = Univ.LSet.fold (fun key (i,mp) ->
+ let u = uni_lvl_val (arg args i) in
+ (i+1, Univ.LMap.add key (Univ.Universe.make u) mp))
+ (Univ.Universe.levels u)
+ (0,Univ.LMap.empty) in
+ let subst = Univ.make_subst mp in
+ Univ.subst_univs_universe subst u
+ | _ ->
+ Errors.anomaly Pp.(str "ill-formed universe")
+
+
+let rec pr_atom a =
+ Pp.(match a with
+ | Aid c -> str "Aid(" ++ (match c with
+ | ConstKey c -> Names.pr_con c
+ | RelKey i -> str "#" ++ int i
+ | _ -> str "...") ++ str ")"
+ | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")"
+ | Atype _ -> str "Atype(")
+and pr_whd w =
+ Pp.(match w with
+ | Vsort _ -> str "Vsort"
+ | Vprod _ -> str "Vprod"
+ | Vfun _ -> str "Vfun"
+ | Vfix _ -> str "Vfix"
+ | Vcofix _ -> str "Vcofix"
+ | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
+ | Vconstr_block b -> str "Vconstr_block"
+ | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
+ | Vuniv_level _ -> assert false)
+and pr_stack stk =
+ Pp.(match stk with
+ | [] -> str "[]"
+ | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk)
+and pr_zipper z =
+ Pp.(match z with
+ | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
+ | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
+ | Zswitch s -> str "Zswitch(...)"
+ | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")")
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 045d02333..bc1978663 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -22,7 +22,8 @@ type arguments
type atom =
| Aid of Vars.id_key
- | Aind of pinductive
+ | Aind of inductive
+ | Atype of Univ.universe
(** Zippers *)
@@ -45,19 +46,25 @@ type whd =
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
+ | Vuniv_level of Univ.universe_level
+
+val pr_atom : atom -> Pp.std_ppcmds
+val pr_whd : whd -> Pp.std_ppcmds
(** Constructors *)
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
val val_of_named : Id.t -> values
-val val_of_constant : pconstant -> values
+val val_of_constant : constant -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
(** Destructors *)
val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.universe_level
+val instantiate_universe : Univ.universe -> stack -> Univ.universe
(** Arguments *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 46af784dd..b9c1a5a1c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
-let constr_type_of_idkey env idkey =
- match idkey with
- | ConstKey cst ->
- let const_type = Typeops.type_of_constant_in env cst in
- mkConstU cst, const_type
- | VarKey id ->
- let (_,_,ty) = lookup_named id env in
- mkVar id, ty
- | RelKey i ->
- let n = (nb_rel env - i) in
- let (_,_,ty) = lookup_rel n env in
- mkRel n, lift n ty
-
let type_of_ind env (ind, u) =
type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
@@ -164,9 +151,11 @@ and nf_whd env whd typ =
let t = ta.(i) in
let _, args = nf_args env vargs t in
mkApp(cfd,args)
- | Vconstr_const n -> construct_of_constr_const env n typ
+ | Vconstr_const n ->
+ construct_of_constr_const env n typ
| Vconstr_block b ->
let tag = btag b in
+ let x = tag in
let (tag,ofs) =
if tag = Cbytecodes.last_variant_tag then
match whd_val (bfield b 0) with
@@ -177,22 +166,80 @@ and nf_whd env whd typ =
let args = nf_bargs env b ofs ctyp in
mkApp(capp,args)
| Vatom_stk(Aid idkey, stk) ->
- let c,typ = constr_type_of_idkey env idkey in
- nf_stk env c typ stk
- | Vatom_stk(Aind ind, stk) ->
- nf_stk env (mkIndU ind) (type_of_ind env ind) stk
+ constr_type_of_idkey env idkey stk nf_stk
+(*let c,typ = constr_type_of_idkey env idkey in
+ nf_stk env c typ stk *)
+ | Vatom_stk(Aind ((mi,i) as ind), stk) ->
+ if Environ.polymorphic_ind ind env then
+ let mib = Environ.lookup_mind mi env in
+ let ulen = Univ.UContext.size mib.mind_universes in
+ match stk with
+ | Zapp args :: stk' ->
+ assert (ulen <= nargs args) ;
+ let inst =
+ Array.init ulen (fun i -> Vm.uni_lvl_val (arg args i))
+ in
+ let pind = (ind, Univ.Instance.of_array inst) in
+ nf_stk ~from:ulen env (mkIndU pind) (type_of_ind env pind) stk
+ | _ -> assert false
+ else
+ let pind = (ind, Univ.Instance.empty) in
+ nf_stk env (mkIndU pind) (type_of_ind env pind) stk
+ | Vatom_stk(Atype u, stk) ->
+ mkSort (Type (Vm.instantiate_universe u stk))
+ | Vuniv_level lvl ->
+ assert false
+
+and constr_type_of_idkey env (idkey : Vars.id_key) stk cont =
+ match idkey with
+ | ConstKey cst ->
+ if Environ.polymorphic_constant cst env then
+ let cbody = Environ.lookup_constant cst env in
+ match stk with
+ | Zapp vargs :: stk' ->
+ let uargs = Univ.UContext.size cbody.const_universes in
+ assert (Vm.nargs vargs >= uargs) ;
+ let uary = Array.init uargs (fun i -> Vm.uni_lvl_val (Vm.arg vargs i)) in
+ let ui = Univ.Instance.of_array uary in
+ let ucst = (cst, ui) in
+ let const_type = Typeops.type_of_constant_in env ucst in
+ if uargs < Vm.nargs vargs then
+ let t, args = nf_args env vargs ~from:uargs const_type in
+ cont env (mkApp (mkConstU ucst, args)) t stk'
+ else
+ cont env (mkConstU ucst) const_type stk'
+ | _ -> assert false
+ else
+ begin
+ let ucst = (cst, Univ.Instance.empty) in
+ let const_type = Typeops.type_of_constant_in env ucst in
+ cont env (mkConstU ucst) const_type stk
+ end
+ | VarKey id ->
+ let (_,_,ty) = lookup_named id env in
+ cont env (mkVar id) ty stk
+ | RelKey i ->
+ let n = (nb_rel env - i) in
+ let (_,_,ty) = lookup_rel n env in
+ cont env (mkRel n) (lift n ty) stk
-and nf_stk env c t stk =
+and nf_stk ?from:(from=0) env c t stk =
match stk with
| [] -> c
| Zapp vargs :: stk ->
- let t, args = nf_args env vargs t in
- nf_stk env (mkApp(c,args)) t stk
+ if nargs vargs >= from then
+ let t, args = nf_args ~from:from env vargs t in
+ nf_stk env (mkApp(c,args)) t stk
+ else
+ let rest = from - nargs vargs in
+ nf_stk ~from:rest env c t stk
| Zfix (f,vargs) :: stk ->
+ assert (from = 0) ;
let fa, typ = nf_fix_app env f vargs in
let _,_,codom = decompose_prod env typ in
nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
| Zswitch sw :: stk ->
+ assert (from = 0) ;
let ((mind,_ as ind), u), allargs = find_rectype_a env t in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
@@ -215,6 +262,7 @@ and nf_stk env c t stk =
let ci = case_info sw in
nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
| Zproj p :: stk ->
+ assert (from = 0) ;
let p' = Projection.make p true in
let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
nf_stk env (mkProj(p',c)) ty stk
@@ -240,14 +288,14 @@ and nf_predicate env ind mip params v pT =
true, mkLambda(name,dom,body)
| _, _ -> false, nf_val env v crazy_type
-and nf_args env vargs t =
+and nf_args env vargs ?from:(f=0) t =
let t = ref t in
- let len = nargs vargs in
+ let len = nargs vargs - f in
let args =
Array.init len
(fun i ->
let _,dom,codom = decompose_prod env !t in
- let c = nf_val env (arg vargs i) dom in
+ let c = nf_val env (arg vargs (f+i)) dom in
t := subst1 c codom; c) in
!t,args
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 09:11:21 +0000