Merge PR #6914: Primitive integers

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

8 files changed, 74 insertions, 5 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index 63324bff20..77e70318dd 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -106,6 +106,7 @@ end
 
 type repr =
 | RInt of int
+| RInt63 of Uint63.t
 | RBlock of (int * int) (* tag × len *)
 | RString of string
 | RPointer of int
@@ -119,6 +120,7 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
 | String of string
 
 module type Input =
@@ -255,6 +257,28 @@ let input_header64 chan =
   in
   (tag, len)
 
+let input_cstring chan : string =
+  let buff = Buffer.create 17 in
+  let rec loop () =
+    match input_char chan with
+    | '\o000' -> Buffer.contents buff
+    | c -> Buffer.add_char buff c |> loop
+  in loop ()
+
+let input_intL chan : int64 =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let ( lsl ) x y = Int64.(shift_left (of_int x) y) in
+  let ( lor ) = Int64.logor in
+  (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+  (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor (Int64.of_int p)
+
 let parse_object chan =
   let data = input_byte chan in
   if prefix_small_block <= data then
@@ -297,6 +321,11 @@ let parse_object chan =
     let addr = input_int32u chan in
     for _i = 0 to 15 do ignore (input_byte chan); done;
     RCode addr
+  | CODE_CUSTOM ->
+    begin match input_cstring chan with
+    | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan))
+    | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
+    end
   | CODE_DOUBLE_ARRAY32_LITTLE
   | CODE_DOUBLE_BIG
   | CODE_DOUBLE_LITTLE
@@ -304,8 +333,7 @@ let parse_object chan =
   | CODE_DOUBLE_ARRAY8_LITTLE
   | CODE_DOUBLE_ARRAY32_BIG
   | CODE_INFIXPOINTER
-  | CODE_CUSTOM ->
-    Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+    -> Printf.eprintf "Unhandled code %04x\n%!" data; assert false
 
 let parse chan =
   let (magic, len, _, _, size) = parse_header chan in
@@ -337,6 +365,11 @@ let parse chan =
   | RCode addr ->
     let data = Fun addr in
     data, None
+  | RInt63 i ->
+    let data = Ptr !current_object in
+    let () = LargeArray.set memory !current_object (Int63 i) in
+    let () = incr current_object in
+    data, None
   in
 
   let rec fill block off accu =
@@ -400,6 +433,7 @@ let instantiate (p, mem) =
   for i = 0 to len - 1 do
     let obj = match LargeArray.get mem i with
     | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+    | Int63 i -> Obj.repr i
     | String str -> Obj.repr str
     in
     LargeArray.set ans i obj
@@ -418,6 +452,7 @@ let instantiate (p, mem) =
       for k = 0 to Array.length blk - 1 do
         Obj.set_field obj k (get_data blk.(k))
       done
+    | Int63 _
     | String _ -> ()
   done;
   get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index d7770539df..029f595959 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -1,3 +1,4 @@
+(** Representation of data allocated on the OCaml heap. *)
 type data =
 | Int of int
 | Ptr of int
@@ -6,6 +7,7 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
 | String of string
 
 module LargeArray :
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 086dd17e39..c33c6d5d09 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -66,6 +66,7 @@ let mk_mtb mp sign delta =
 
 let rec check_module env mp mb =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
+  let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   let (_:module_signature) =
     check_signature env mb.mod_type mb.mod_mp mb.mod_delta
   in
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 6dc2953060..4a64039e30 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -16,6 +16,7 @@ let import senv clib univs digest =
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true mb.mod_constraints env in
   let env = push_context_set ~strict:true univs env in
+  let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   Mod_checking.check_module env mb.mod_mp mb;
   let (_,senv) = Safe_typing.import clib univs digest senv in senv
 
diff --git a/checker/validate.ml b/checker/validate.ml
index b85944f94f..72cf38ebe6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -86,6 +86,7 @@ let rec val_gen v ctx o = match v with
   | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
   | Dyn -> val_dyn ctx o
   | Proxy { contents = v } -> val_gen v ctx o
+  | Uint63 -> val_uint63 ctx o
 
 (* Check that an object is a tuple (or a record). vs is an array of
    value representation for each field. Its size corresponds to the
@@ -133,6 +134,10 @@ and val_array v ctx o =
     val_gen v ctx (Obj.field o i)
   done
 
+and val_uint63 ctx o =
+  if not (Uint63.is_uint63 o) then
+    fail ctx o "not a 63-bit unsigned integer"
+
 let print_frame = function
 | CtxType t -> t
 | CtxAnnot t -> t
diff --git a/checker/values.ml b/checker/values.ml
index 1afe764ca4..7ca2dc8050 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -34,6 +34,7 @@ type value =
   | Dyn
 
   | Proxy of value ref
+  | Uint63
 
 let fix (f : value -> value) : value =
   let self = ref Any in
@@ -151,7 +152,8 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_proj;v_constr|] (* Proj *)
+    [|v_proj;v_constr|]; (* Proj *)
+    [|Uint63|] (* Int *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -214,9 +216,12 @@ let v_oracle =
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
+let v_primitive =
+  v_enum "primitive" 25
+
 let v_cst_def =
   v_sum "constant_def" 0
-    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
+    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
@@ -288,6 +293,20 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Opt v_bool;
     v_typing_flags|]
 
+let v_prim_ind = v_enum "prim_ind" 4
+
+let v_prim_type = v_enum "prim_type" 1
+
+let v_retro_action =
+  v_sum "retro_action" 0 [|
+    [|v_prim_ind; v_ind|];
+    [|v_prim_type; v_cst|];
+    [|v_cst|];
+  |]
+
+let v_retroknowledge =
+  v_sum "module_retroknowledge" 1 [|[|List v_retro_action|]|]
+
 let rec v_mae =
   Sum ("module_alg_expr",0,
   [|[|v_mp|];         (* SEBident *)
@@ -318,7 +337,7 @@ and v_impl =
 and v_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|])
 and v_modtype =
   Tuple ("module_type_body",
          [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
diff --git a/checker/values.mli b/checker/values.mli
index 616b69907f..2ab8da1928 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -38,6 +38,8 @@ type value =
   | Proxy of value ref
   (** Same as the inner value, used to define recursive types *)
 
+  | Uint63
+
 (** NB: List and Opt have their own constructors to make it easy to
    define eg [let rec foo = List foo]. *)
 
diff --git a/checker/votour.ml b/checker/votour.ml
index 3c088b59b5..36014cde73 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -100,6 +100,7 @@ struct
             init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
         in
         fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
+      | Int63 _ -> k 0
       | String s ->
         let size = 2 + (String.length s / ws) in
         let () = LargeArray.set !sizes p size in
@@ -116,6 +117,7 @@ struct
   | Ptr p ->
     match LargeArray.get !memory p with
     | Struct (tag, os) -> BLOCK (tag, os)
+    | Int63 _ -> OTHER (* TODO: pretty-print int63 values *)
     | String s -> STRING s
 
   let input ch =
@@ -153,6 +155,7 @@ let rec get_name ?(extra=false) = function
   |Annot (s,v) -> s^"/"^get_name ~extra v
   |Dyn -> "<dynamic>"
   | Proxy v -> get_name ~extra !v
+  | Uint63 -> "Uint63"
 
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
@@ -257,6 +260,7 @@ let rec get_children v o pos = match v with
     end
   |Fail s -> raise Forbidden
   | Proxy v -> get_children !v o pos
+  | Uint63 -> raise Exit
 
 let get_children v o pos =
   try get_children v o pos