diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 19 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 3 |
3 files changed, 15 insertions, 9 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d7ec2ecf72..c879cab9df 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1272,6 +1272,8 @@ let ml_of_instance instance u = (lname, paramsi, body) in MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) + | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|]) + | Lmakeblock (prefix,(cn,_u),_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index d88be94b39..02b5043135 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -39,9 +39,10 @@ type lambda = | Lif of lambda * lambda * lambda | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl + | Lint of int (* a constant constructor *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor Name.t, constructor tag, arguments *) - (* A fully applied constructor *) + (* A fully applied non-constant constructor *) | Luint of Uint63.t | Lval of Nativevalues.t | Lsort of Sorts.t @@ -119,7 +120,7 @@ let get_const_prefix env c = let map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _ - | Llazy | Lforce | Lmeta _ -> lam + | Llazy | Lforce | Lmeta _ | Lint _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -318,16 +319,13 @@ and reduce_lapp substf lids body substa largs = let is_value lc = match lc with - | Lval _ -> true - | Lmakeblock(_,_,_,args) when Array.is_empty args -> true - | Luint _ -> true + | Lval _ | Lint _ | Luint _ -> true | _ -> false let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> - Nativevalues.mk_int tag + | Lint tag -> Nativevalues.mk_int tag | Luint i -> Nativevalues.mk_uint i | _ -> raise Not_found @@ -338,6 +336,8 @@ let make_args start _end = let expand_constructor prefix cstr tag nparams arity = let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) let ids = Array.make (nparams + arity) anon in + if Int.equal arity 0 then mkLlam ids (Lint tag) + else let args = make_args arity 1 in Llam(ids, Lmakeblock (prefix, cstr, tag, args)) @@ -348,7 +348,10 @@ let makeblock env cn u tag nparams arity args = let prefix = get_mind_prefix env (fst (fst cn)) in mkLapp (expand_constructor prefix (cn,u) tag nparams arity) args else - if Array.for_all is_value args && nargs > 0 then + (* The constructor is fully applied *) + if Int.equal arity 0 then Lint tag + else + if Array.for_all is_value args then let args = Array.map get_value args in Lval (Nativevalues.mk_block tag args) else diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 687789e82b..c357819da5 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -33,9 +33,10 @@ type lambda = | Lif of lambda * lambda * lambda | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl + | Lint of int (* a constant constructor *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor Name.t, constructor tag, arguments *) - (* A fully applied constructor *) + (* A fully applied non-constant constructor *) | Luint of Uint63.t | Lval of Nativevalues.t | Lsort of Sorts.t |