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>

1 files changed, 10 insertions, 9 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 67c605ea1d..c15486ea10 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -304,9 +304,9 @@ let rec extract_type env sg db j c args =
 	   | (Info, TypeScheme) ->
                let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in
                (match (lookup_constant kn env).const_body with
-		  | Undef _ | OpaqueDef _ -> mlt
-                  | Def _ when is_custom (ConstRef kn) -> mlt
-		  | Def lbody ->
+                 | Undef _ | OpaqueDef _ | Primitive _ -> mlt
+                 | Def _ when is_custom (ConstRef kn) -> mlt
+                 | Def lbody ->
                       let newc = applistc (get_body lbody) args in
                       let mlt' = extract_type env sg db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
@@ -318,7 +318,7 @@ let rec extract_type env sg db j c args =
 	   | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
                (match (lookup_constant kn env).const_body with
-		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
+                 | Undef _  | OpaqueDef _ | Primitive _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
                       let newc = applistc (get_body lbody) args in
@@ -346,7 +346,7 @@ let rec extract_type env sg db j c args =
             | (Info, TypeScheme) ->
               extract_type_app env sg db (r, type_sign env sg ty) args
             | (Info, Default) -> Tunknown))
-    | Cast _ | LetIn _ | Construct _ -> assert false
+    | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
@@ -564,7 +564,7 @@ and mlt_env env r = match r with
   | ConstRef kn ->
      let cb = Environ.lookup_constant kn env in
      match cb.const_body with
-     | Undef _ | OpaqueDef _ -> None
+     | Undef _ | OpaqueDef _ | Primitive _ -> None
      | Def l_body ->
         match lookup_typedef kn cb with
         | Some _ as o -> o
@@ -683,6 +683,7 @@ let rec extract_term env sg mle mlt c args =
        let vty = extract_type env sg [] 0 ty [] in
        let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in
        extract_app env sg mle mlt extract_var args
+    | Int i -> assert (args = []); MLuint i
     | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
@@ -1063,7 +1064,7 @@ let extract_constant env kn cb =
     | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
         (match cb.const_body with
-	  | Undef _ -> warn_info (); mk_typ_ax ()
+          | Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
              (match Recordops.find_primitive_projection kn with
               | None -> mk_typ (get_body c)
@@ -1079,7 +1080,7 @@ let extract_constant env kn cb =
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
-	  | Undef _ -> warn_info (); mk_ax ()
+          | Primitive _ | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
              (match Recordops.find_primitive_projection kn with
               | None -> mk_def (get_body c)
@@ -1107,7 +1108,7 @@ let extract_constant_spec env kn cb =
     | (Info, TypeScheme) ->
         let s,vl = type_sign_vl env sg typ in
 	(match cb.const_body with
-	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
+          | Undef _ | OpaqueDef _ | Primitive _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
               let body = get_body body in