diff options
| -rw-r--r-- | kernel/nativecode.ml | 38 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 14 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 1 |
3 files changed, 41 insertions, 12 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6b9247476..9fee03ca1 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -615,13 +615,27 @@ let merge_branches t = let lf,env_n = push_rels (empty_env ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in + let mk_let envi (id,def) t = MLlet (id,def,t) in + let mk_lam_or_let (params,lets,env) (id,def) = + let ln,env' = push_rel env id in + match def with + | None -> (ln::params,lets,env') + | Some lam -> (params, (ln,ml_of_lam env l lam)::lets,env') + in let ml_of_fix i body = - let idsi,bodyi = decompose_Llam body in - let paramsi, envi = push_rels env_n idsi in - t_norm_f.(i) <- fresh_gnorm l; - let bodyi = ml_of_lam envi l bodyi in - t_params.(i) <- paramsi; - mkMLlam paramsi bodyi in + let varsi, bodyi = decompose_Llam_Llet body in + let paramsi,letsi,envi = + Array.fold_left mk_lam_or_let ([],[],env_n) varsi + in + let paramsi,letsi = + Array.of_list (List.rev paramsi), Array.of_list (List.rev letsi) + in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + let bodyi = Array.fold_right (mk_let envi) letsi bodyi in + mkMLlam paramsi bodyi + in let tnorm = Array.mapi ml_of_fix tb in let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in let fv_params = fv_params env_n in @@ -667,12 +681,12 @@ let merge_branches t = let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in let ml_of_fix i body = - let idsi,bodyi = decompose_Llam body in - let paramsi, envi = push_rels env_n idsi in - t_norm_f.(i) <- fresh_gnorm l; - let bodyi = ml_of_lam envi l bodyi in - t_params.(i) <- paramsi; - mkMLlam paramsi bodyi in + let idsi,bodyi = decompose_Llam body in + let paramsi, envi = push_rels env_n idsi in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + mkMLlam paramsi bodyi in let tnorm = Array.mapi ml_of_fix tb in let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in let fv_params = fv_params env_n in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 2ca274799..f530f6e2e 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -66,6 +66,20 @@ let decompose_Llam lam = | Llam(ids,body) -> ids, body | _ -> [||], lam +let rec decompose_Llam_Llet lam = + match lam with + | Llam(ids,body) -> + let vars, body = decompose_Llam_Llet body in + Array.fold_right (fun x l -> (x, None) :: l) ids vars, body + | Llet(id,def,body) -> + let vars, body = decompose_Llam_Llet body in + (id,Some def) :: vars, body + | _ -> [], lam + +let decompose_Llam_Llet lam = + let vars, body = decompose_Llam_Llet lam in + Array.of_list vars, body + (*s Operators on substitution *) let subst_id = subs_id 0 let lift = subs_lift diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 0c454256e..ada63ebb4 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -46,6 +46,7 @@ and lam_branches = (constructor * name array * lambda) array and fix_decl = name array * lambda array * lambda array 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 mk_lazy : lambda -> lambda |