diff options
| -rw-r--r-- | kernel/nativecode.ml | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 22 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 2 |
3 files changed, 21 insertions, 5 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c8572eec3..2cbe9cd22 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1767,7 +1767,7 @@ let compile_constant env sigma prefix ~interactive con body = | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in - let is_lazy = is_lazy t in + let is_lazy = is_lazy prefix t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index c9733c5fd..acf115466 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -499,8 +499,24 @@ module Renv = r end -let is_lazy t = (* APPROXIMATION *) - isApp t || isLetIn t +(* What about pattern matching ?*) +let is_lazy prefix t = + match kind_of_term t with + | App (f,args) -> + begin match kind_of_term f with + | Construct c -> + let entry = mkInd (fst c) in + (try + let _ = + Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + entry prefix c Llazy; + in + false + with Not_found -> true) + | _ -> true + end + | LetIn _ -> true + | _ -> false let evar_value sigma ev = sigma.evars_val ev @@ -642,7 +658,7 @@ and lambda_of_app env sigma f args = else let prefix = get_const_prefix !global_env kn in let t = - if is_lazy (Mod_subst.force_constr csubst) then + if is_lazy prefix (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, kn)|] else Lconst (prefix, kn) in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index da1a07d5d..a2763626c 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -23,7 +23,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Names.name array * lambda val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda -val is_lazy : constr -> bool +val is_lazy : prefix -> constr -> bool val mk_lazy : lambda -> lambda val get_allias : env -> constant -> constant |