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 /plugins/funind/glob_termops.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 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5b45a8dbed..13ff19a46b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -106,6 +106,7 @@ let change_vars = | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x + | GInt _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) @@ -285,6 +286,7 @@ let rec alpha_rt excluded rt = ) | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ + | GInt _ | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, @@ -344,6 +346,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + | GInt _ -> false ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -434,6 +437,7 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ | GHole _ as rt -> rt + | GInt _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) @@ -516,7 +520,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map = DAst.map (function - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt | GVar id as rt -> begin try |