Store the {struct} inductive type in native fixpoint AST.

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