diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 3 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 37 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 2 |
3 files changed, 21 insertions, 21 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 94ed288d2d..ebb3c2cd73 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1280,9 +1280,6 @@ let ml_of_instance instance u = | Lmakeblock (prefix,(cn,_u),_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) - | Lconstruct (prefix, (cn,u)) -> - let uargs = ml_of_instance env.env_univ u in - mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index ec3a7b893d..d88be94b39 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -42,8 +42,6 @@ type lambda = | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor Name.t, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) - (* A partially applied constructor *) | Luint of Uint63.t | Lval of Nativevalues.t | Lsort of Sorts.t @@ -121,7 +119,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 _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam + | Llazy | Lforce | Lmeta _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -222,7 +220,7 @@ let lam_subst_args subst args = let can_subst lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _ - | Lconstruct _ | Lmeta _ | Levar _ -> true + | Lmeta _ | Levar _ -> true | _ -> false let can_merge_if bt bf = @@ -337,9 +335,20 @@ let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) (* Translation of constructors *) +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 + let args = make_args arity 1 in + Llam(ids, Lmakeblock (prefix, cstr, tag, args)) -let makeblock env cn u tag args = - if Array.for_all is_value args && Array.length args > 0 then +(* [nparams] is the number of parameters still expected *) +let makeblock env cn u tag nparams arity args = + let nargs = Array.length args in + if nparams > 0 || nargs < arity then + 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 let args = Array.map get_value args in Lval (Nativevalues.mk_block tag args) else @@ -573,16 +582,12 @@ and lambda_of_app cache env sigma f args = mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) end | Construct (c,u) -> - let tag, nparams, arity = Cache.get_construct_info cache env c in - let expected = nparams + arity in - let nargs = Array.length args in - let prefix = get_mind_prefix env (fst (fst c)) in - if Int.equal nargs expected then - let args = lambda_of_args cache env sigma nparams args in - makeblock env c u tag args - else - let args = lambda_of_args cache env sigma 0 args in - mkLapp (Lconstruct (prefix, (c,u))) args + let tag, nparams, arity = Cache.get_construct_info cache env c in + let nargs = Array.length args in + if nparams < nargs then (* got all parameters *) + let args = lambda_of_args cache env sigma nparams args in + makeblock env c u tag 0 arity args + else makeblock env c u tag (nparams - nargs) arity empty_args | _ -> let f = lambda_of_constr cache env sigma f in let args = lambda_of_args cache env sigma 0 args in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index b0de257a27..687789e82b 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -36,8 +36,6 @@ type lambda = | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor Name.t, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) - (* A partially applied constructor *) | Luint of Uint63.t | Lval of Nativevalues.t | Lsort of Sorts.t |