1 files changed, 63 insertions, 18 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1f6effba6..bd659a471 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -48,6 +48,7 @@ type gname =
   | Gind of string * inductive (* prefix, inductive name *)
   | Gconstruct of string * constructor (* prefix, constructor name *)
   | Gconstant of string * constant (* prefix, constant name *)
+  | Gproj of string * constant (* prefix, constant name *)
   | Gcase of label option * int
   | Gpred of label option * int
   | Gfixtype of label option * int
@@ -95,6 +96,7 @@ let gname_hash gn = match gn with
 | Ginternal s -> combinesmall 9 (String.hash s)
 | Grel i -> combinesmall 10 (Int.hash i)
 | Gnamed id -> combinesmall 11 (Id.hash id)
+| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p))
 
 let case_ctr = ref (-1)
 
@@ -253,6 +255,7 @@ type primitive =
   | Mk_cofix of int
   | Mk_rel of int
   | Mk_var of identifier
+  | Mk_proj
   | Is_accu
   | Is_int
   | Cast_accu
@@ -298,6 +301,8 @@ let eq_primitive p1 p2 =
   | Force_cofix, Force_cofix -> true
   | Mk_meta, Mk_meta -> true
   | Mk_evar, Mk_evar -> true
+  | Mk_proj, Mk_proj -> true
+
   | _ -> false
 
 let primitive_hash = function
@@ -344,6 +349,7 @@ let primitive_hash = function
   | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim)
   | Coq_primitive (prim, Some (prefix,kn)) ->
      combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
+  | Mk_proj -> 38
 
 type mllambda =
   | MLlocal        of lname 
@@ -1002,6 +1008,7 @@ let compile_prim decl cond paux =
   | Lapp(f,args) ->
       MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
   | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c))
+  | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c))
   | Lprim _ ->
       let decl,cond,paux = extract_prim (ml_of_lam env l) t in
       compile_prim decl cond paux
@@ -1461,6 +1468,8 @@ let string_of_gname g =
       Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
   | Gconstant (prefix, c) ->
       Format.sprintf "%sconst_%s" prefix (string_of_con c)
+  | Gproj (prefix, c) ->
+      Format.sprintf "%sproj_%s" prefix (string_of_con c)
   | Gcase (l,i) ->
       Format.sprintf "case_%s_%i" (string_of_label_def l) i
   | Gpred (l,i) ->
@@ -1518,12 +1527,12 @@ let pp_mllam fmt l =
     | MLif(t,l1,l2) ->
 	Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
 	  pp_mllam t pp_mllam l1 pp_mllam l2 
-    | MLmatch (asw, c, accu_br, br) ->
-	let mind,i = asw.asw_ind in
-    let prefix = asw.asw_prefix in
-	let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
-	Format.fprintf fmt 
-	  "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
+    | MLmatch (annot, c, accu_br, br) ->
+	  let mind,i = annot.asw_ind in
+      let prefix = annot.asw_prefix in
+	  let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
+	  Format.fprintf fmt 
+	    "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
 	  pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
 	  
     | MLconstruct(prefix,c,args) ->
@@ -1626,6 +1635,7 @@ let pp_mllam fmt l =
     | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
     | Mk_var id ->
         Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
+    | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_accu -> Format.fprintf fmt "is_accu"
     | Is_int -> Format.fprintf fmt "is_int"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
@@ -1758,9 +1768,11 @@ and compile_named env sigma auxdefs id =
   | None -> 
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
-let compile_constant env sigma prefix ~interactive con body =
-  match body with
-  | Def t ->
+let compile_constant env sigma prefix ~interactive con cb =
+  match cb.const_proj with
+  | None ->
+    begin match cb.const_body with
+    | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
       if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
@@ -1778,11 +1790,42 @@ let compile_constant env sigma prefix ~interactive con body =
       in
       if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
       code, name
-  | _ -> 
+    | _ -> 
+        let i = push_symbol (SymbConst con) in
+        [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
+	  if interactive then LinkedInteractive prefix
+	  else Linked prefix
+    end
+  | Some pb ->
+      let mind = pb.proj_ind in
+      let ind = (mind,0) in
+      let mib = lookup_mind mind env in
+      let oib = mib.mind_packets.(0) in
+      let tbl = oib.mind_reloc_tbl in 
+      (* Building info *)
+      let prefix = get_mind_prefix env mind in
+      let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; 
+		 ci_cstr_nargs = [|0|];
+		 ci_cstr_ndecls = [||] (*FIXME*);
+		 ci_pp_info = { ind_nargs = 0; style = RegularStyle } } in
+      let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
+		  asw_reloc = tbl; asw_finite = true } in
+      let c_uid = fresh_lname Anonymous in
+      let _, arity = tbl.(0) in
+      let ci_uid = fresh_lname Anonymous in
+      let cargs = Array.init arity
+        (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None)
+      in
       let i = push_symbol (SymbConst con) in
-      [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
-      if interactive then LinkedInteractive prefix
-      else Linked prefix
+      let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in
+      let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in
+      let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+      let gn = Gproj ("",con) in
+      let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in
+      let arg = fargs.(pb.proj_npars) in
+        Glet(Gconstant ("",con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
+          arg|])))::
+            [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
 
 let loaded_native_files = ref ([] : string list)
 
@@ -1858,8 +1901,8 @@ let compile_mind_deps env prefix ~interactive
    reverse order, as well as linking information updates *)
 let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
-  | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
-  | Const c ->
+  | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
+  | Const (c,u) ->
       let c = get_allias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
@@ -1873,12 +1916,14 @@ let rec compile_deps env sigma prefix ~interactive init t =
         | _ -> init
       in
       let code, name =
-	compile_constant env sigma prefix ~interactive c cb.const_body
+	compile_constant env sigma prefix ~interactive c cb
       in
       let comp_stack = code@comp_stack in
       let const_updates = Cmap_env.add c (nameref, name) const_updates in
       comp_stack, (mind_updates, const_updates)
-  | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind
+  | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
+  | Proj (p,c) ->
+      compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|]))
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
@@ -1888,7 +1933,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =
       compile_constant ~interactive:false env empty_evars prefix
-        con cb.const_body
+        con cb
     in
     gl@acc