aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vm.ml')
-rw-r--r--kernel/vm.ml197
1 files changed, 133 insertions, 64 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml
index eacd803fd..64ddc4376 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,17 +160,98 @@ type whd =
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
+ | Vuniv_level of Univ.universe_level
+
+(************************************************)
+(* Abstract machine *****************************)
+(************************************************)
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+ "coq_interprete_ml"
+
+
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i =
+ if 0 <= i && i < (nargs args) then
+ val_of_obj (Obj.field (Obj.repr args) (i+2))
+ else invalid_arg
+ ("Vm.arg size = "^(string_of_int (nargs args))^
+ " acces "^(string_of_int i))
+
+(* Apply a value to arguments contained in [vargs] *)
+let apply_arguments vf vargs =
+ let n = nargs vargs in
+ if Int.equal n 0 then vf
+ else
+ begin
+ push_ra stop;
+ push_arguments vargs;
+ interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+ end
+
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+ let n = Array.length varray in
+ if Int.equal n 0 then vf
+ else
+ begin
+ push_ra stop;
+ push_vstack varray;
+ interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+ end
(*************************************************)
(* Destructors ***********************************)
(*************************************************)
+let uni_lvl_val (v : values) : Univ.universe_level =
+ 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)
+
let rec whd_accu a stk =
let stk =
if Int.equal (Obj.size a) 2 then stk
else Zapp (Obj.obj a) :: stk in
let at = Obj.field a 1 in
match Obj.tag at with
+ | i when Int.equal i type_atom_tag ->
+ begin match stk with
+ | [Zapp args] ->
+ let u = ref (Obj.obj (Obj.field at 0)) in
+ for i = 0 to nargs args - 1 do
+ u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
+ done;
+ Vsort (Type !u)
+ | _ -> assert false
+ end
| i when i <= max_atom_tag ->
Vatom_stk(Obj.magic at, stk)
| i when Int.equal i proj_tag ->
@@ -199,7 +281,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,67 +296,19 @@ 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)
-
-(************************************************)
-(* Abstrct machine ******************************)
-(************************************************)
-
-(* gestion de la pile *)
-external push_ra : tcode -> unit = "coq_push_ra"
-external push_val : values -> unit = "coq_push_val"
-external push_arguments : arguments -> unit = "coq_push_arguments"
-external push_vstack : vstack -> unit = "coq_push_vstack"
-
-
-(* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
- "coq_interprete_ml"
-
-
-
-(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i =
- if 0 <= i && i < (nargs args) then
- val_of_obj (Obj.field (Obj.repr args) (i+2))
- else invalid_arg
- ("Vm.arg size = "^(string_of_int (nargs args))^
- " acces "^(string_of_int i))
-
-(* Apply a value to arguments contained in [vargs] *)
-let apply_arguments vf vargs =
- let n = nargs vargs in
- if Int.equal n 0 then vf
- else
- begin
- push_ra stop;
- push_arguments vargs;
- interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
- end
-
-(* Apply value [vf] to an array of argument values [varray] *)
-let apply_varray vf varray =
- let n = Array.length varray in
- if Int.equal n 0 then vf
- else
- begin
- push_ra stop;
- push_vstack varray;
- interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
- end
+ else
+ Vconstr_block(Obj.obj o)
(**********************************************)
(* Constructors *******************************)
@@ -299,6 +335,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 +355,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 +644,34 @@ 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 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 ")")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:57:19 +0000