aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-13 10:44:40 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-13 11:20:28 +0200
commit24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 (patch)
treebdde5a56a8e3ca5b0a258ccb68a85caf498fdf56 /kernel/nativeconv.ml
parent9a4e062c92ad88c894ebbd6e20ee9d1511f24a3f (diff)
Providing a -type-in-type option for collapsing the universe hierarchy.
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml54
1 files changed, 27 insertions, 27 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 5964ed70e..c7701a8b1 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,15 +16,15 @@ open Nativecode
(** This module implements the conversion test by compiling to OCaml code *)
-let rec conv_val pb lvl v1 v2 cu =
+let rec conv_val env pb lvl v1 v2 cu =
if v1 == v2 then cu
else
match kind_of_value v1, kind_of_value v2 with
| Vaccu k1, Vaccu k2 ->
- conv_accu pb lvl k1 k2 cu
+ conv_accu env pb lvl k1 k2 cu
| Vfun f1, Vfun f2 ->
let v = mk_rel_accu lvl in
- conv_val CONV (lvl+1) (f1 v) (f2 v) cu
+ conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
| Vconst i1, Vconst i2 ->
if Int.equal i1 i2 then cu else raise NotConvertible
| Vblock b1, Vblock b2 ->
@@ -34,29 +34,29 @@ let rec conv_val pb lvl v1 v2 cu =
raise NotConvertible;
let rec aux lvl max b1 b2 i cu =
if Int.equal i max then
- conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu
+ conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
else
let cu =
- conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu in
+ conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
aux lvl max b1 b2 (i+1) cu in
aux lvl (n1-1) b1 b2 0 cu
| Vfun f1, _ ->
- conv_val CONV lvl v1 (fun x -> v2 x) cu
+ conv_val env CONV lvl v1 (fun x -> v2 x) cu
| _, Vfun f2 ->
- conv_val CONV lvl (fun x -> v1 x) v2 cu
+ conv_val env CONV lvl (fun x -> v1 x) v2 cu
| _, _ -> raise NotConvertible
-and conv_accu pb lvl k1 k2 cu =
+and conv_accu env pb lvl k1 k2 cu =
let n1 = accu_nargs k1 in
let n2 = accu_nargs k2 in
if not (Int.equal n1 n2) then raise NotConvertible;
if Int.equal n1 0 then
- conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
+ conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
else
- let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
- List.fold_right2 (conv_val CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
+ let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+ List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
-and conv_atom pb lvl a1 a2 cu =
+and conv_atom env pb lvl a1 a2 cu =
if a1 == a2 then cu
else
match a1, a2 with
@@ -70,18 +70,18 @@ and conv_atom pb lvl a1 a2 cu =
if not (eq_constant c1 c2) then raise NotConvertible;
cu
| Asort s1, Asort s2 ->
- check_sort_cmp_universes pb s1 s2 cu; cu
+ check_sort_cmp_universes env pb s1 s2 cu; cu
| Avar id1, Avar id2 ->
if not (Id.equal id1 id2) then raise NotConvertible;
cu
| Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
- let cu = conv_accu CONV lvl ac1 ac2 cu in
+ let cu = conv_accu env CONV lvl ac1 ac2 cu in
let tbl = a1.asw_reloc in
let len = Array.length tbl in
- if Int.equal len 0 then conv_val CONV lvl p1 p2 cu
+ if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
else
- let cu = conv_val CONV lvl p1 p2 cu in
+ let cu = conv_val env CONV lvl p1 p2 cu in
let max = len - 1 in
let rec aux i cu =
let tag,arity = tbl.(i) in
@@ -89,38 +89,38 @@ and conv_atom pb lvl a1 a2 cu =
if Int.equal arity 0 then mk_const tag
else mk_block tag (mk_rels_accu lvl arity) in
let bi1 = bs1 ci and bi2 = bs2 ci in
- if Int.equal i max then conv_val CONV (lvl + arity) bi1 bi2 cu
- else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in
+ if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+ else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
aux 0 cu
| Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
if f1 == f2 then cu
- else conv_fix lvl t1 f1 t2 f2 cu
+ else conv_fix env lvl t1 f1 t2 f2 cu
| (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
(Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
if not (Int.equal s1 s2) then raise NotConvertible;
if f1 == f2 then cu
else
if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
- else conv_fix lvl t1 f1 t2 f2 cu
+ else conv_fix env lvl t1 f1 t2 f2 cu
| Aprod(_,d1,c1), Aprod(_,d2,c2) ->
- let cu = conv_val CONV lvl d1 d2 cu in
+ let cu = conv_val env CONV lvl d1 d2 cu in
let v = mk_rel_accu lvl in
- conv_val pb (lvl + 1) (d1 v) (d2 v) cu
+ conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
| _, _ -> raise NotConvertible
(* Precondition length t1 = length f1 = length f2 = length t2 *)
-and conv_fix lvl t1 f1 t2 f2 cu =
+and conv_fix env lvl t1 f1 t2 f2 cu =
let len = Array.length f1 in
let max = len - 1 in
let fargs = mk_rels_accu lvl len in
let flvl = lvl + len in
let rec aux i cu =
- let cu = conv_val CONV lvl t1.(i) t2.(i) cu in
+ let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
let fi1 = napply f1.(i) fargs in
let fi2 = napply f2.(i) fargs in
- if Int.equal i max then conv_val CONV flvl fi1 fi2 cu
- else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
+ if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
+ else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
aux 0 cu
let native_conv pb sigma env t1 t2 =
@@ -144,7 +144,7 @@ let native_conv pb sigma env t1 t2 =
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Pp.msg_debug (Pp.str time_info);
(* TODO change 0 when we can have deBruijn *)
- ignore(conv_val pb 0 !rt1 !rt2 (Environ.universes env))
+ ignore(conv_val env pb 0 !rt1 !rt2 (Environ.universes env))
end
| _ -> anomaly (Pp.str "Compilation failure")