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, 125 insertions, 180 deletions

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 1e4dbfd418..5c21a5ec25 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -5,13 +5,44 @@ open Term
 open Constr
 open Declarations
 open Vmvalues
-open Cbytecodes
-open Cinstr
 open Environ
 open Pp
 
 let pr_con sp = str(Names.Label.to_string (Constant.label sp))
 
+type lambda =
+  | Lrel          of Name.t * int
+  | Lvar          of Id.t
+  | Levar         of Evar.t * lambda array
+  | Lprod         of lambda * lambda
+  | Llam          of Name.t array * lambda
+  | Llet          of Name.t * lambda * lambda
+  | Lapp          of lambda * lambda array
+  | Lconst        of pconstant
+  | Lprim         of pconstant option * CPrimitives.t * lambda array
+        (* No check if None *)
+  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
+  | Lif           of lambda * lambda * lambda
+  | Lfix          of (int array * int) * fix_decl
+  | Lcofix        of int * fix_decl
+  | Lint          of int
+  | Lmakeblock    of int * lambda array
+  | Luint         of Uint63.t
+  | Lval          of structured_values
+  | Lsort         of Sorts.t
+  | Lind          of pinductive
+  | Lproj         of Projection.Repr.t * lambda
+
+(* We separate branches for constant and non-constant constructors. If the OCaml
+   limitation on non-constant constructors is reached, remaining branches are
+   stored in [extra_branches]. *)
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t array * lambda) array }
+(*    extra_branches : (name array * lambda) array } *)
+
+and fix_decl =  Name.t array * lambda array * lambda array
+
 (** Printing **)
 
 let pp_names ids =
@@ -77,6 +108,10 @@ let rec pp_lam lam =
                   pp_names ids ++ str " => " ++ pp_lam c)
                (Array.to_list branches.nonconstant_branches)))
          ++ cut() ++ str "end")
+  | Lif (t, bt, bf) ->
+      v 0 (str "(if " ++ pp_lam t ++
+             cut () ++ str "then " ++ pp_lam bt ++
+             cut() ++ str "else " ++ pp_lam bf ++ str ")")
   | Lfix((t,i),(lna,tl,bl)) ->
     let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in
     hov 1
@@ -104,22 +139,26 @@ let rec pp_lam lam =
       (str "(makeblock " ++ int tag ++ spc() ++
        prlist_with_sep spc pp_lam (Array.to_list args) ++
        str")")
+  | Luint i -> str (Uint63.to_string i)
   | Lval _ -> str "values"
   | Lsort s -> pp_sort s
   | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
-  | Lprim((kn,_u),_ar,_op,args) ->
-    hov 1
-      (str "(PRIM " ++ pr_con kn ++  spc() ++
-       prlist_with_sep spc pp_lam  (Array.to_list args) ++
-       str")")
+  | Lprim(Some (kn,_u),_op,args) ->
+     hov 1
+         (str "(PRIM " ++ pr_con kn ++  spc() ++
+            prlist_with_sep spc pp_lam  (Array.to_list args) ++
+            str")")
+  | Lprim(None,op,args) ->
+     hov 1
+         (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++  spc() ++
+            prlist_with_sep spc pp_lam (Array.to_list args) ++
+            str")")
   | Lproj(p,arg) ->
     hov 1
       (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
        ++ str ")")
   | Lint i ->
     Pp.(str "(int:" ++ int i ++ str ")")
-  | Luint _ ->
-    str "(uint)"
 
 (*s Constructors *)
 
@@ -151,9 +190,9 @@ let shift subst = subs_shft (1, subst)
 
 (* A generic map function *)
 
-let rec map_lam_with_binders g f n lam =
+let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> lam
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
@@ -192,6 +231,11 @@ let rec map_lam_with_binders g f n lam =
     in
     if t == t' && a == a' && branches == branches' then lam else
       Lcase(ci,rtbl,t',a',branches')
+  | Lif(t,bt,bf) ->
+      let t' = f n t in
+      let bt' = f n bt in
+      let bf' = f n bf in
+      if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
   | Lfix(init,(ids,ltypes,lbodies)) ->
     let ltypes' = Array.Smart.map (f n) ltypes in
     let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
@@ -205,25 +249,12 @@ let rec map_lam_with_binders g f n lam =
   | Lmakeblock(tag,args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lmakeblock(tag,args')
-  | Lprim(kn,ar,op,args) ->
+  | Lprim(kn,op,args) ->
     let args' = Array.Smart.map (f n) args in
-    if args == args' then lam else Lprim(kn,ar,op,args')
+    if args == args' then lam else Lprim(kn,op,args')
   | Lproj(p,arg) ->
     let arg' = f n arg in
     if arg == arg' then lam else Lproj(p,arg')
-  | Luint u ->
-    let u' = map_uint g f n u in
-    if u == u' then lam else Luint u'
-
-and map_uint _g f n u =
-  match u with
-  | UintVal _ -> u
-  | UintDigits(args) ->
-    let args' = Array.Smart.map (f n) args in
-    if args == args' then u else UintDigits(args')
-  | UintDecomp(a) ->
-    let a' = f n a in
-    if a == a' then u else UintDecomp(a')
 
 (*s Lift and substitution *)
 
@@ -271,28 +302,58 @@ let lam_subst_args subst args =
 
 let can_subst lam =
   match lam with
-  | Lrel _ | Lvar _ | Lconst _
+  | Lrel _ | Lvar _ | Lconst _ | Luint _
   | Lval _ | Lsort _ | Lind _ -> true
   | _ -> false
 
+
+let can_merge_if bt bf =
+  match bt, bf with
+  | Llam(_idst,_), Llam(_idsf,_) -> true
+  | _ -> false
+
+let merge_if t bt bf =
+  let (idst,bodyt) = decompose_Llam bt in
+  let (idsf,bodyf) = decompose_Llam bf in
+  let nt = Array.length idst in
+  let nf = Array.length idsf in
+  let common,idst,idsf =
+    if nt = nf then idst, [||], [||]
+    else
+      if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
+      else idsf, Array.sub idst nf (nt - nf), [||] in
+  Llam(common,
+       Lif(lam_lift (Array.length common) t,
+           mkLlam idst bodyt,
+           mkLlam idsf bodyf))
+
+
 let rec simplify subst lam =
   match lam with
   | Lrel(id,i) -> lam_subst_rel lam id i subst
 
   | Llet(id,def,body) ->
-    let def' = simplify subst def in
-    if can_subst def' then simplify (cons def' subst) body
-    else
-      let body' = simplify (lift subst) body in
-      if def == def' && body == body' then lam
-      else Llet(id,def',body')
+      let def' = simplify subst def in
+      if can_subst def' then simplify (cons def' subst) body
+      else
+        let body' = simplify (lift subst) body in
+        if def == def' && body == body' then lam
+        else Llet(id,def',body')
 
   | Lapp(f,args) ->
-    begin match simplify_app subst f subst args with
+      begin match simplify_app subst f subst args with
       | Lapp(f',args') when f == f' && args == args' -> lam
       | lam' -> lam'
-    end
+      end
 
+  | Lif(t,bt,bf) ->
+      let t' = simplify subst t in
+      let bt' = simplify subst bt in
+      let bf' = simplify subst bf in
+      if can_merge_if bt' bf' then merge_if t' bt' bf'
+      else
+        if t == t' && bt == bt' && bf == bf' then lam
+        else Lif(t',bt',bf')
   | _ -> map_lam_with_binders liftn simplify subst lam
 
 and simplify_app substf f substa args =
@@ -352,7 +413,7 @@ let rec occurrence k kind lam =
     if n = k then
       if kind then false else raise Not_found
     else kind
-  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ -> kind
+  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> kind
   | Levar (_, args) ->
     occurrence_args k kind args
   | Lprod(dom, codom) ->
@@ -363,7 +424,7 @@ let rec occurrence k kind lam =
     occurrence (k+1) (occurrence k kind def) body
   | Lapp(f, args) ->
     occurrence_args k (occurrence k kind f) args
-  | Lprim(_,_,_,args) | Lmakeblock(_,args) ->
+  | Lprim(_,_,args) | Lmakeblock(_,args) ->
     occurrence_args k kind args
   | Lcase(_ci,_rtbl,t,a,branches) ->
     let kind = occurrence k (occurrence k kind t) a in
@@ -374,6 +435,9 @@ let rec occurrence k kind lam =
     in
     Array.iter on_b branches.nonconstant_branches;
     !r
+  | Lif (t, bt, bf) ->
+      let kind = occurrence k kind t in
+      kind && occurrence k kind bt && occurrence k kind bf
   | Lfix(_,(ids,ltypes,lbodies))
   | Lcofix(_,(ids,ltypes,lbodies)) ->
     let kind = occurrence_args k kind ltypes in
@@ -381,17 +445,10 @@ let rec occurrence k kind lam =
     kind
   | Lproj(_,arg) ->
     occurrence k kind arg
-  | Luint u -> occurrence_uint k kind u
 
 and occurrence_args k kind args =
   Array.fold_left (occurrence k) kind args
 
-and occurrence_uint k kind u =
-  match u with
-  | UintVal _ -> kind
-  | UintDigits args -> occurrence_args k kind args
-  | UintDecomp t -> occurrence k kind t
-
 let occur_once lam =
   try let _ = occurrence 1 true lam in true
   with Not_found -> false
@@ -439,11 +496,12 @@ let check_compilable ib =
 
 let is_value lc =
   match lc with
-  | Lval _ | Lint _ -> true
+  | Lval _ | Lint _ | Luint _ -> true
   | _ -> false
 
 let get_value lc =
   match lc with
+  | Luint i -> val_of_uint i
   | Lval v -> v
   | Lint i -> val_of_int i
   | _ -> raise Not_found
@@ -491,26 +549,18 @@ let rec get_alias env kn =
 
 (* Compilation of primitive *)
 
-let _h =  Name(Id.of_string "f")
+let prim kn p args =
+  Lprim(Some kn, p, args)
 
-(*
 let expand_prim kn op arity =
   let ids = Array.make arity Anonymous in
   let args = make_args arity 1 in
   Llam(ids, prim kn op args)
-*)
 
-let compile_prim n op kn fc args =
-  if not fc then raise Not_found
-  else
-    Lprim(kn, n, op, args)
-
-    (*
-  let (nparams, arity) = CPrimitives.arity op in
-  let expected = nparams + arity in
-  if Array.length args >= expected then prim kn op args
-  else mkLapp (expand_prim kn op expected) args
-*)
+let lambda_of_prim kn op args =
+  let arity = CPrimitives.arity op in
+  if Array.length args >= arity then prim kn op args
+  else mkLapp (expand_prim kn op arity) args
 
 (*i Global environment *)
 
@@ -661,13 +711,6 @@ let rec lambda_of_constr env c =
 
     (* translation of the argument *)
     let la = lambda_of_constr env a in
-    let gr = GlobRef.IndRef ind in
-    let la =
-      try
-        Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge
-          gr la
-      with Not_found -> la
-    in
     (* translation of the type *)
     let lt = lambda_of_constr env t in
     (* translation of branches *)
@@ -713,88 +756,30 @@ let rec lambda_of_constr env c =
     let lc = lambda_of_constr env c in
     Lproj (Projection.repr p,lc)
 
+  | Int i -> Luint i
+
 and lambda_of_app env f args =
   match Constr.kind f with
-  | Const (kn,_u as c) ->
-    let kn = get_alias env.global_env kn in
-    (* spiwack: checks if there is a specific way to compile the constant
-                if there is not, Not_found is raised, and the function
-                falls back on its normal behavior *)
-    (try
-      (* We delay the compilation of arguments to avoid an exponential behavior *)
-      let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge
-          (GlobRef.ConstRef kn) in
-      let args = lambda_of_args env 0 args in
-      f args
-    with Not_found ->
-    let cb = lookup_constant kn env.global_env in
-    begin match cb.const_body with
+  | Const (kn,u as c) ->
+      let kn = get_alias env.global_env kn in
+      let cb = lookup_constant kn env.global_env in
+      begin match cb.const_body with
+      | Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args)
       | Def csubst when cb.const_inline_code ->
-        lambda_of_app env (Mod_subst.force_constr csubst) args
+          lambda_of_app env (Mod_subst.force_constr csubst) args
       | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args)
-    end)
+      end
   | Construct (c,_) ->
-    let tag, nparams, arity = Renv.get_construct_info env c in
-    let nargs = Array.length args in
-    let gr = GlobRef.ConstructRef c in
-    if Int.equal (nparams + arity) nargs then (* fully applied *)
-      (* spiwack: *)
-      (* 1/ tries to compile the constructor in an optimal way,
-            it is supposed to work only if the arguments are
-            all fully constructed, fails with Cbytecodes.NotClosed.
-            it can also raise Not_found when there is no special
-            treatment for this constructor
-            for instance: tries to to compile an integer of the
-                form I31 D1 D2 ... D31 to [D1D2...D31] as
-                a processor number (a caml number actually) *)
-      try
-        try
-          Retroknowledge.get_vm_constant_static_info
-            env.global_env.retroknowledge
-            gr args
-        with NotClosed ->
-          (* 2/ if the arguments are not all closed (this is
-                              expectingly (and it is currently the case) the only
-                              reason why this exception is raised) tries to
-                              give a clever, run-time behavior to the constructor.
-                              Raises Not_found if there is no special treatment
-                              for this integer.
-                              this is done in a lazy fashion, using the constructor
-                              Bspecial because it needs to know the continuation
-                              and such, which can't be done at this time.
-                              for instance, for int31: if one of the digit is
-                                  not closed, it's not impossible that the number
-                                  gets fully instantiated at run-time, thus to ensure
-                                  uniqueness of the representation in the vm
-                                  it is necessary to try and build a caml integer
-                                  during the execution *)
-          let rargs = Array.sub args nparams arity in
-          let args = lambda_of_args env nparams rargs in
-          Retroknowledge.get_vm_constant_dynamic_info
-            env.global_env.retroknowledge
-            gr args
-      with Not_found ->
-        (* 3/ if no special behavior is available, then the compiler
-           falls back to the normal behavior *)
+      let tag, nparams, arity = Renv.get_construct_info env c in
+      let nargs = Array.length args in
+      if nparams < nargs then (* got all parameters *)
         let args = lambda_of_args env nparams args in
         makeblock tag 0 arity args
-    else
-      let args = lambda_of_args env nparams args in
-      (* spiwack: tries first to apply the run-time compilation
-                behavior of the constructor, as in 2/ above *)
-      (try
-         (Retroknowledge.get_vm_constant_dynamic_info
-            env.global_env.retroknowledge
-            gr) args
-       with Not_found ->
-         if nparams <= nargs then (* got all parameters *)
-           makeblock tag 0 arity args
-         else (* still expecting some parameters *)
-           makeblock tag (nparams - nargs) arity empty_args)
+      else makeblock tag (nparams - nargs) arity empty_args
   | _ ->
-    let f = lambda_of_constr env f in
-    let args = lambda_of_args env 0 args in
-    mkLapp f args
+      let f = lambda_of_constr env f in
+      let args = lambda_of_args env 0 args in
+      mkLapp f args
 
 and lambda_of_args env start args =
   let nargs = Array.length args in
@@ -822,43 +807,3 @@ let lambda_of_constr ~optimize genv c =
   if !dump_lambda then
     Feedback.msg_debug (pp_lam lam);
   lam
-
-(** Retroknowledge, to be removed once we move to primitive machine integers *)
-let compile_structured_int31 fc args =
-  if not fc then raise Not_found else
-    Luint (UintVal
-    (Uint31.of_int (Array.fold_left
-       (fun temp_i -> fun t -> match kind t with
-          | Construct ((_,d),_) -> 2*temp_i+d-1
-          | _ -> raise NotClosed)
-       0 args)))
-
-let dynamic_int31_compilation fc args =
-  if not fc then raise Not_found else
-  Luint (UintDigits args)
-
-let d0 = Lint 0
-let d1 = Lint 1
-
-(* We are relying here on the tags of digits constructors *)
-let digits_from_uint i =
-  let digits = Array.make 31 d0 in
-  for k = 0 to 30 do
-    if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
-      digits.(30-k) <- d1
-  done;
-  digits
-
-let int31_escape_before_match fc t =
-  if not fc then
-    raise Not_found
-  else
-  match t with
-  | Luint (UintVal i) ->
-    let digits = digits_from_uint i in
-    Lmakeblock (1, digits)
-  | Luint (UintDigits args) ->
-    Lmakeblock (1,args)
-  | Luint (UintDecomp _) ->
-    assert false
-  | _ -> Luint (UintDecomp t)