diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/checker/values.ml b/checker/values.ml index df6a9136c8..ed730cff8e 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -34,7 +34,7 @@ type value = | Dyn | Proxy of value ref - | Uint63 + | Int64 | Float64 let fix (f : value -> value) : value = @@ -129,6 +129,9 @@ let v_cast = v_enum "cast_kind" 4 let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|] let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] +let v_uint63 = + if Sys.word_size == 64 then Int else Int64 + let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) @@ -148,7 +151,7 @@ let rec v_constr = [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) - [|Uint63|]; (* Int *) + [|v_uint63|]; (* Int *) [|Float64|] (* Int *) |]) @@ -225,7 +228,7 @@ let v_oracle = |] let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] + v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -235,7 +238,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |