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>

5 files changed, 14 insertions, 6 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3b95423067..8da30bd9c9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -763,12 +763,13 @@ let build_proof
 	      end
 	  | Cast(t,_,_) ->
 	      build_proof do_finalize {dyn_infos with info = t} g
-	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
 	      do_finalize dyn_infos g
 	  | App(_,_) ->
 	      let f,args = decompose_app sigma dyn_infos.info in
 	      begin
 		match EConstr.kind sigma f with
+      | Int _ -> user_err Pp.(str "integer cannot be applied")
 		  | App _ -> assert false (* we have collected all the app in decompose_app *)
 		  | Proj _ -> assert false (*FIXME*)
 		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4b6caea70d..02964d7ba5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -478,7 +478,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
-    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ ->
+    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
     | GApp(_,_) ->
@@ -588,6 +588,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
+            | GInt _ -> user_err Pp.(str "Cannot apply an integer")
 	end (* end of the application treatement *)
 
     | GLambda(n,_,t,b) ->
@@ -1221,7 +1222,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
    TODO: Find a valid way to deal with implicit arguments here!
 *)
 let rec compute_cst_params relnames params gt = DAst.with_val (function
-  | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
+  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params
   | GApp(f,args) ->
     begin match DAst.get f with
     | GVar relname' when Id.Set.mem relname' relnames ->
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
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3a04c753ea..d9b0330e2b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -201,7 +201,7 @@ let is_rec names =
   let check_id id names =  Id.Set.mem id names in
   let rec lookup names gt = match DAst.get gt with
     | GVar(id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ -> false
     | GCast(b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
     | GIf(b,_,lhs,rhs) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 38f27f760b..1b5286dce4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -306,6 +306,7 @@ let check_not_nested sigma forbidden e =
   let rec check_not_nested e =  
     match EConstr.kind sigma e with 
       | Rel _ -> ()
+      | Int _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
         then user_err ~hdr:"Recdef.check_not_nested"
@@ -487,7 +488,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
           | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
-    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
       let new_continuation_tac = 
 	jinfo.otherS () expr_info continuation_tac in
       new_continuation_tac expr_info g
@@ -1294,6 +1295,7 @@ let is_opaque_constant c =
     | Declarations.OpaqueDef _ -> Proof_global.Opaque
     | Declarations.Undef _ -> Proof_global.Opaque
     | Declarations.Def _ -> Proof_global.Transparent
+    | Declarations.Primitive _ -> Proof_global.Opaque
 
 let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)