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, 17 insertions, 8 deletions

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e273891500..e8a66f1889 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -44,6 +44,7 @@ struct
     | DCase   of case_info * 't * 't * 't array
     | DFix    of int array * int * 't array * 't array
     | DCoFix  of int * 't array * 't array
+    | DInt    of Uint63.t
 
     (* special constructors only inside the left-hand side of DCtx or
        DApp. Used to encode lists of foralls/letins/apps as contexts *)
@@ -61,6 +62,7 @@ struct
     | DCase (_,t1,t2,ta) -> str "case"
     | DFix _ -> str "fix"
     | DCoFix _ -> str "cofix"
+    | DInt _ -> str "INT"
     | DCons ((t,dopt),tl) -> f t ++ (match dopt with
 	  Some t' -> str ":=" ++ f t'
 	| None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
@@ -72,7 +74,7 @@ struct
    *)
 
   let map f = function
-    | (DRel | DSort | DNil | DRef _) as c -> c
+    | (DRel | DSort | DNil | DRef _ | DInt _) as c -> c
     | DCtx (ctx,c) -> DCtx (f ctx, f c)
     | DLambda (t,c) -> DLambda (f t, f c)
     | DApp (t,u) -> DApp (f t,f u)
@@ -145,6 +147,10 @@ struct
     else c
   | DCoFix _, _ -> -1 | _, DCoFix _ -> 1
 
+  | DInt i1, DInt i2 -> Uint63.compare i1 i2
+
+  | DInt _, _ -> -1 | _, DInt _ -> 1
+
   | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) ->
      let c = cmp t1 t2 in
      if Int.equal c 0 then
@@ -157,7 +163,7 @@ struct
   | DNil, DNil -> 0
 
   let fold f acc = function
-    | (DRel | DNil | DSort | DRef _) -> acc
+    | (DRel | DNil | DSort | DRef _ | DInt _) -> acc
     | DCtx (ctx,c) -> f (f acc ctx) c
     | DLambda (t,c) -> f (f acc t) c
     | DApp (t,u) -> f (f acc t) u
@@ -169,7 +175,7 @@ struct
     | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
 
   let choose f = function
-    | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose"
+    | (DRel | DSort | DNil | DRef _ | DInt _) -> invalid_arg "choose"
     | DCtx (ctx,c) -> f ctx
     | DLambda (t,c) -> f t
     | DApp (t,u) -> f u
@@ -185,7 +191,8 @@ struct
     if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0)
     then invalid_arg "fold2:compare" else
       match c1,c2 with
-	| (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc
+        | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _
+           | DInt _, DInt _) -> acc
 	| (DCtx (c1,t1), DCtx (c2,t2)
 	  | DApp (c1,t1), DApp (c2,t2)
 	  | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
@@ -198,14 +205,15 @@ struct
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
         | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
-           | DFix _ | DCoFix _ | DCons _), _ -> assert false
+           | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false
 
   let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
     let head w = map (fun _ -> ()) w in
     if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0)
     then invalid_arg "map2_t:compare" else
       match c1,c2 with
-	| (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc ->
+        | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _
+           | DInt _, DInt _) as cc ->
 	    let (c,_) = cc in c
 	| DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
 	| DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
@@ -219,10 +227,10 @@ struct
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
         | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
-           | DFix _ | DCoFix _ | DCons _), _ -> assert false
+           | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false
 
   let terminal = function
-    | (DRel | DSort | DNil | DRef _) -> true
+    | (DRel | DSort | DNil | DRef _ | DInt _) -> true
     | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ ->
       false
 
@@ -315,6 +323,7 @@ struct
         (pat_of_constr f) (Array.map pat_of_constr ca)
     | Proj (p,c) -> 
         Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
+    | Int i -> Term (DInt i)
 
     and ctx_of_constr ctx c = match Constr.kind c with
     | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c