Merge PR #6914: Primitive integers

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

10 files changed, 43 insertions, 23 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b0f6301192..b59e3b608c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -147,7 +147,7 @@ let check_fix env sg cb i =
           | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
-    | Undef _ | OpaqueDef _ -> raise Impossible
+    | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible
 
 let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
   Array.equal Name.equal na1 na2 &&
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
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 97fe9f24d5..a3cd92d556 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -214,6 +214,8 @@ let rec pp_expr par env args =
     | MLmagic a ->
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
+    | MLuint _ ->
+      pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
 
 and pp_cons_pat par r ppl =
   pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index e43c47d050..f88d29e9ed 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -155,6 +155,10 @@ let rec json_expr env = function
       ("value", json_expr env a)
     ]
   | MLaxiom -> json_dict [("what", json_str "expr:axiom")]
+  | MLuint i -> json_dict [
+      ("what", json_str "expr:int");
+      ("int", json_str (Uint63.to_string i))
+    ]
 
 and json_one_pat env (ids,p,t) =
   let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index ce920ad6a0..b7f80d543b 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -126,6 +126,7 @@ and ml_ast =
   | MLdummy  of kill_reason
   | MLaxiom
   | MLmagic  of ml_ast
+  | MLuint of Uint63.t
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index ce920ad6a0..9df0f4964e 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -126,6 +126,7 @@ and ml_ast =
   | MLdummy  of kill_reason
   | MLaxiom
   | MLmagic  of ml_ast
+  | MLuint   of Uint63.t
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9f5c1f1a17..2432887673 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -66,7 +66,8 @@ let rec eq_ml_type t1 t2 = match t1, t2 with
 | Tdummy k1, Tdummy k2 -> k1 == k2
 | Tunknown, Tunknown -> true
 | Taxiom, Taxiom -> true
-| _ -> false
+| (Tarr _ | Tglob _ | Tvar _ | Tvar' _ | Tmeta _ | Tdummy _ | Tunknown | Taxiom), _
+  -> false
 
 and eq_ml_meta m1 m2 =
  Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
@@ -107,7 +108,7 @@ let rec type_occurs alpha t =
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
   | Tglob (r,l) -> List.exists (type_occurs alpha) l
-  | _ -> false
+  | (Tdummy _ | Tvar _ | Tvar' _ | Taxiom | Tunknown) -> false
 
 (*s Most General Unificator *)
 
@@ -310,7 +311,7 @@ let isMLdummy = function MLdummy _ -> true | _ -> false
 
 let sign_of_id = function
   | Dummy -> Kill Kprop
-  | _ -> Keep
+  | (Id _ | Tmp _) -> Keep
 
 (* Classification of signatures *)
 
@@ -370,7 +371,10 @@ let eq_ml_ident i1 i2 = match i1, i2 with
 | Dummy, Dummy -> true
 | Id id1, Id id2 -> Id.equal id1 id2
 | Tmp id1, Tmp id2 -> Id.equal id1 id2
-| _ -> false
+| Dummy, (Id _ | Tmp _)
+| Id _, (Dummy | Tmp _)
+| Tmp _, (Dummy | Id _)
+  -> false
 
 let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLrel i1, MLrel i2 ->
@@ -394,7 +398,8 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLdummy k1, MLdummy k2 -> k1 == k2
 | MLaxiom, MLaxiom -> true
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
-| _ -> false
+| MLuint i1, MLuint i2 -> Uint63.equal i1 i2
+| _, _ -> false
 
 and eq_ml_pattern p1 p2 = match p1, p2 with
 | Pcons (gr1, p1), Pcons (gr2, p2) ->
@@ -426,7 +431,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> ()
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
   in iter 0
 
 (*s Map over asts. *)
@@ -445,7 +450,7 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -463,7 +468,7 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
 
 (*s Iter over asts. *)
 
@@ -477,7 +482,7 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom  -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -513,7 +518,7 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
   in nb 1
 
 (* Replace unused variables by _ *)
@@ -565,7 +570,7 @@ let dump_unused_vars a =
        let b' = ren env b in
        if b' == b then a else MLmagic b'
 
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a
 
     and ren_branch env ((ids,p,b) as tr) =
       let occs = List.map (fun _ -> ref false) ids in
@@ -1398,7 +1403,7 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b398bc07a0..654695c232 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -108,7 +108,7 @@ let ast_iter_references do_term do_cons do_type a =
 	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy _ | MLaxiom | MLmagic _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 96d8760404..8940aedd6d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -310,6 +310,10 @@ let rec pp_expr par env args =
 		apply2
 		  (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
 			pp_pat env pv))))
+    | MLuint i ->
+        assert (args=[]);
+        str "(" ++ str (Uint63.compile i) ++ str ")"
+
 
 and pp_record_proj par env typ t pv args =
   (* Can a match be printed as a mere record projection ? *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 76a0c74068..6aa3a6220e 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -129,6 +129,8 @@ let rec pp_expr env args =
     | MLmagic a ->
 	pp_expr env args a
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
+    | MLuint _ ->
+      paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->