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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/prettyp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 408bd5f60b..e0403a9f97 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -193,7 +193,7 @@ let opacity env = | ConstRef cst -> let cb = Environ.lookup_constant cst env in (match cb.const_body with - | Undef _ -> None + | Undef _ | Primitive _ -> None | OpaqueDef _ -> Some FullyOpaque | Def _ -> Some (TransparentMaybeOpacified @@ -558,7 +558,7 @@ let print_constant with_values sep sp udecl = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with @@ -724,7 +724,10 @@ let print_full_pure_context env sigma = | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ - pr_lconstr_env env sigma (Mod_subst.force_constr c)) + pr_lconstr_env env sigma (Mod_subst.force_constr c) + | Primitive _ -> + str "Primitive " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in |