diff options
| author | Maxime Dénès | 2015-01-16 22:17:03 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | 6e0b660b1e58502b7da477b9725ae8ee4f5d00ed (patch) | |
| tree | 36114b255b884e90b021876bebd49ff978c24710 /kernel/nativevalues.ml | |
| parent | a83721ac508aa96496ef95c8433bc282bca0db14 (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 098c59e823..d7a2195052 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) |