Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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