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, 89 insertions, 1 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c9acd168e8..7eb8e803b3 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,7 +12,7 @@ open CErrors
 open Util
 open Names
 open Univ
-open Sorts
+open Term
 open Constr
 open Vars
 open Declarations
@@ -187,6 +187,74 @@ let type_of_apply env func funt argsv argstv =
   in
   apply_rec 0 (inject funt)
 
+(* Type of primitive constructs *)
+let type_of_prim_type _env = function
+  | CPrimitives.PT_int63 -> Constr.mkSet
+
+let type_of_int env =
+  match env.retroknowledge.Retroknowledge.retro_int63 with
+  | Some c -> mkConst c
+  | None -> CErrors.user_err Pp.(str"The type int must be registered before this construction can be typechecked.")
+
+let type_of_prim env t =
+  let int_ty = type_of_int env in
+  let bool_ty () =
+    match env.retroknowledge.Retroknowledge.retro_bool with
+    | Some ((ind,_),_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.")
+  in
+  let compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_cmp with
+    | Some ((ind,_),_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
+  in
+  let pair_ty fst_ty snd_ty =
+    match env.retroknowledge.Retroknowledge.retro_pair with
+    | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
+    | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
+  in
+  let carry_ty int_ty =
+    match env.retroknowledge.Retroknowledge.retro_carry with
+    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
+    | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
+  in
+  let rec nary_int63_op arity ty =
+    if Int.equal arity 0 then ty
+      else Constr.mkProd(Name (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty)
+  in
+  let return_ty =
+    let open CPrimitives in
+    match t with
+    | Int63head0
+    | Int63tail0
+    | Int63add
+    | Int63sub
+    | Int63mul
+    | Int63div
+    | Int63mod
+    | Int63lsr
+    | Int63lsl
+    | Int63land
+    | Int63lor
+    | Int63lxor
+    | Int63addMulDiv -> int_ty
+    | Int63eq
+    | Int63lt
+    | Int63le -> bool_ty ()
+    | Int63mulc
+    | Int63div21
+    | Int63diveucl -> pair_ty int_ty int_ty
+    | Int63addc
+    | Int63subc
+    | Int63addCarryC
+    | Int63subCarryC -> carry_ty int_ty
+    | Int63compare -> compare_ty ()
+  in
+  nary_int63_op (CPrimitives.arity t) return_ty
+
+let judge_of_int env i =
+  make_judge (Constr.mkInt i) (type_of_int env)
+
 (* Type of product *)
 
 let sort_of_product env domsort rangsort =
@@ -468,6 +536,9 @@ let rec execute env cstr =
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
         check_cofix env cofix; fix_ty
+
+    (* Primitive types *)
+    | Int _ -> type_of_int env
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -590,3 +661,20 @@ let judge_of_case env ci pj cj lfj =
   let lf, lft = dest_judgev lfj in
   make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
              (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
+
+(* Building type of primitive operators and type *)
+
+open CPrimitives
+
+let check_primitive_type env op_t t =
+  match op_t with
+  | OT_type PT_int63 ->
+    (try
+      default_conv ~l2r:false CUMUL env mkSet t
+    with NotConvertible ->
+      CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set"))
+  | OT_op p ->
+    (try
+      default_conv ~l2r:false CUMUL env (type_of_prim env p) t
+    with NotConvertible ->
+      CErrors.user_err Pp.(str"Not the expected type for this primitive"))