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, 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)