diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-16 22:17:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 08:02:45 +0100 |
| commit | 9f5586d88880cbb98c92edfe9c33c76564f1a19c (patch) | |
| tree | 6de2a171eff5706b0e4ce9268554b84a922f12b3 /kernel/nativevalues.ml | |
| parent | 4985f0ff99278beb3b934f86edf1398659c611a8 (diff) | |
Make native compiler handle universe polymorphic definitions.
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 098c59e82..d7a219505 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -49,8 +49,8 @@ let eq_rec_pos = Array.equal Int.equal type atom = | Arel of int - | Aconstant of constant - | Aind of inductive + | Aconstant of pconstant + | Aind of pinductive | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) @@ -106,14 +106,19 @@ let mk_rels_accu lvl len = let napply (f:t) (args: t array) = Array.fold_left (fun f a -> f a) f args -let mk_constant_accu kn = - mk_accu (Aconstant kn) +let mk_constant_accu kn u = + mk_accu (Aconstant (kn,Univ.Instance.of_array u)) -let mk_ind_accu s = - mk_accu (Aind s) +let mk_ind_accu ind u = + mk_accu (Aind (ind,Univ.Instance.of_array u)) -let mk_sort_accu s = - mk_accu (Asort s) +let mk_sort_accu s u = + match s with + | Prop _ -> mk_accu (Asort s) + | Type s -> + let u = Univ.Instance.of_array u in + let s = Univ.subst_instance_universe u s in + mk_accu (Asort (Type s)) let mk_var_accu id = mk_accu (Avar id) |