diff options
| author | Maxime Dénès | 2018-02-16 01:02:17 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-04 13:12:40 +0000 |
| commit | e43b1768d0f8399f426b92f4dfe31955daceb1a4 (patch) | |
| tree | d46d10f8893205750e7238e69512736243315ef6 /checker/values.ml | |
| parent | a1b7f53a68c9ccae637f2c357fbe50a09e211a4a (diff) | |
Primitive integers
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/checker/values.ml b/checker/values.ml index 1afe764ca4..7ca2dc8050 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -34,6 +34,7 @@ type value = | Dyn | Proxy of value ref + | Uint63 let fix (f : value -> value) : value = let self = ref Any in @@ -151,7 +152,8 @@ let rec v_constr = [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) - [|v_proj;v_constr|] (* Proj *) + [|v_proj;v_constr|]; (* Proj *) + [|Uint63|] (* Int *) |]) and v_prec = Tuple ("prec_declaration", @@ -214,9 +216,12 @@ let v_oracle = let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] +let v_primitive = + v_enum "primitive" 25 + let v_cst_def = v_sum "constant_def" 0 - [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] @@ -288,6 +293,20 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Opt v_bool; v_typing_flags|] +let v_prim_ind = v_enum "prim_ind" 4 + +let v_prim_type = v_enum "prim_type" 1 + +let v_retro_action = + v_sum "retro_action" 0 [| + [|v_prim_ind; v_ind|]; + [|v_prim_type; v_cst|]; + [|v_cst|]; + |] + +let v_retroknowledge = + v_sum "module_retroknowledge" 1 [|[|List v_retro_action|]|] + let rec v_mae = Sum ("module_alg_expr",0, [|[|v_mp|]; (* SEBident *) @@ -318,7 +337,7 @@ and v_impl = and v_noimpl = v_unit and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|]) and v_modtype = Tuple ("module_type_body", [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) |