aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativeinstr.mli2
-rw-r--r--kernel/nativelambda.ml24
3 files changed, 24 insertions, 4 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8d69eacbc..b09cd3f79 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1142,7 +1142,7 @@ let ml_of_instance instance u =
mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
| Lif(t,bt,bf) ->
MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
- | Lfix ((rec_pos,start), (ids, tt, tb)) ->
+ | Lfix ((rec_pos, inds, start), (ids, tt, tb)) ->
(* let type_f fvt = [| type fix |]
let norm_f1 fv f1 .. fn params1 = body1
..
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index eaad8ee0c..5075bd3d1 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -36,7 +36,7 @@ and lambda =
| Lcase of annot_sw * lambda * lambda * lam_branches
(* annotations, term being matched, accu, branches *)
| Lif of lambda * lambda * lambda
- | Lfix of (int array * int) * fix_decl
+ | Lfix of (int array * (string * inductive) array * int) * fix_decl
| Lcofix of int * fix_decl (* must be in eta-expanded form *)
| Lmakeblock of prefix * pconstructor * int * lambda array
(* prefix, constructor name, constructor tag, arguments *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b6d75437c..a5cdd0a19 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -397,6 +397,20 @@ let empty_evars =
let empty_ids = [||]
+(** Extract the inductive type over which a fixpoint is decreasing *)
+let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with
+| Prod (na, dom, t) ->
+ if Int.equal i 0 then
+ let dom = Reduction.whd_all env dom in
+ let (dom, _) = decompose_appvect dom in
+ match kind dom with
+ | Ind (ind, _) -> ind
+ | _ -> assert false
+ else
+ let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in
+ get_fix_struct env (i - 1) t
+| _ -> assert false
+
let rec lambda_of_constr cache env sigma c =
match kind c with
| Meta mv ->
@@ -497,11 +511,17 @@ let rec lambda_of_constr cache env sigma c =
let bs = Array.mapi mk_branch branches in
Lcase(annot_sw, lt, la, bs)
- | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
+ | Fix((pos, i), (names,type_bodies,rec_bodies)) ->
let ltypes = lambda_of_args cache env sigma 0 type_bodies in
+ let map i t =
+ let ind = get_fix_struct env i t in
+ let prefix = get_mind_prefix env (fst ind) in
+ (prefix, ind)
+ in
+ let inds = Array.map2 map pos type_bodies in
let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in
let lbodies = lambda_of_args cache env sigma 0 rec_bodies in
- Lfix(rec_init, (names, ltypes, lbodies))
+ Lfix((pos, inds, i), (names, ltypes, lbodies))
| CoFix(init,(names,type_bodies,rec_bodies)) ->
let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in