diff options
author | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-11 09:45:49 +0000 |
---|---|---|
committer | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-11 09:45:49 +0000 |
commit | 351c92f5c61082e9e8f5e1c9364f1836416f17d3 (patch) | |
tree | be7231293698b96e95a79c41745d452aeb5aa2b2 /kernel/nativelambda.ml | |
parent | 846879625d0f51457fc9fb51d7e936548de16dcf (diff) |
Fixing bug in native compiler with let patterns in fixpoint definitions.
Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n.
Was raising an "index out of bounds" exception at compile-time.
Nota: this construction is still incorrectly handled by the VM.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r-- | kernel/nativelambda.ml | 14 |
1 files changed, 14 insertions, 0 deletions
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 |