Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.

13 files changed, 99 insertions, 32 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e65113..29e33d349b 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
     arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=2;
+  arity[ARECONST]=arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077e2..8c5ab0ecbd 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
   SWITCH, PUSHFIELDS, 
   GETFIELD0, GETFIELD1, GETFIELD, 
   SETFIELD0, SETFIELD1, SETFIELD,
+  PROJ,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ddbde9d385..0a121dc32e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -878,8 +878,32 @@ value coq_interprete
 	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
-      }	
-   
+      }
+
+
+      Instruct(PROJ){
+	print_instr("PROJ");
+	if (Is_accu (accu)) {
+	  /* Skip over the index of projected field */
+	  pc++;
+	  /* Save the argument on the stack */
+	  *--sp = accu;
+	  /* Create atom */
+	  Alloc_small(accu, 2, ATOM_PROJ_TAG);
+	  Field(accu, 0) = Field(coq_global_data, *pc);
+	  Field(accu, 1) = sp[0];
+	  sp[0] = accu;
+	  /* Create accumulator */
+	  Alloc_small(accu, 2, Accu_tag);
+	  Code_val(accu) = accumulate;
+	  Field(accu,1) = *sp++;
+	} else {
+	    accu = Field(accu, *pc++);
+	}
+	pc++;
+	Next;
+      }
+
 /* Integer constants */
 
       Instruct(CONST0){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2c0..1590a2141d 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -22,10 +22,11 @@
 #define ATOM_ID_TAG 0
 #define ATOM_IDDEF_TAG 1
 #define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
 
 
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 93fd61f02a..3271ac1458 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -31,6 +31,7 @@ let last_variant_tag = 245
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of pinductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -81,6 +82,8 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (* index of the projected argument,
+                                           name of projection *)
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
   | Kaddint31                           (* adds the int31 in the accu
@@ -167,6 +170,7 @@ let pp_sort s =
 let rec pp_struct_const = function
   | Const_sorts s -> pp_sort s
   | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+  | Const_proj p -> Constant.print p
   | Const_b0 i -> int i
   | Const_bn (i,t) ->
      int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
@@ -228,6 +232,8 @@ let rec pp_instr i =
 
   | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
+  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+
   | Kaddint31 -> str "addint31"
   | Kaddcint31 -> str "addcint31"
   | Kaddcarrycint31 -> str "addcarrycint31"
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index d9998c89e8..745ef311b0 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -25,6 +25,7 @@ val last_variant_tag : tag
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of pinductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -72,6 +73,8 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (** index of the projected argument,
+                                            name of projection *)
 
 (** spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (** jump to label, is it needed ? *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index ac46dc5833..d5435f0c37 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -540,14 +540,12 @@ let rec compile_constr reloc c sz cont =
   match kind_of_term c with
   | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
-  | Proj (p,c) -> 
-    (* compile_const reloc p [|c|] sz cont *)
-    let kn = Projection.constant p in
-    let cb = lookup_constant kn !global_env in
-      (* TODO: better representation of projections *)
-    let pb = Option.get cb.const_proj in
-    let args = Array.make pb.proj_npars mkProp in
-      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+  | Proj (p,c) ->
+     let kn = Projection.constant p in
+     let cb = lookup_constant kn !global_env in
+     let pb = Option.get cb.const_proj in
+     let n = pb.proj_arg in
+     compile_constr reloc c sz (Kproj (n,kn) :: cont)
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d3c..0d9334a50c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -225,6 +225,7 @@ let emit_instr = function
       if n <= 1 then out (opSETFIELD0+n)
       else (out opSETFIELD;out_int n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+  | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
   (* spiwack *)
   | Kbranch lbl -> out opBRANCH; out_label lbl
   | Kaddint31 -> out opADDINT31
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 49ab68beae..8fd90ec364 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -60,6 +60,8 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts _, _ -> false
 | Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
 | Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
@@ -71,11 +73,12 @@ let rec hash_structured_constant c =
   match c with
   | Const_sorts s -> combinesmall 1 (Sorts.hash s)
   | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
-  | Const_b0 t -> combinesmall 3 (Int.hash t)
+  | Const_proj p -> combinesmall 3 (Constant.hash p)
+  | Const_b0 t -> combinesmall 4 (Int.hash t)
   | Const_bn (t, a) ->
     let fold h c = combine h (hash_structured_constant c) in
     let h = Array.fold_left fold 0 a in
-    combinesmall 4 (combine (Int.hash t) h)
+    combinesmall 5 (combine (Int.hash t) h)
 
 module SConstTable = Hashtbl.Make (struct
   type t = structured_constant
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492b..83e566041f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 	match proj with
 	| None -> compile_constant_body env def
 	| Some pb ->
-	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+	(* The compilation of primitive projections is a bit tricky, because
+           they refer to themselves (the body of p looks like fun c =>
+           Proj(p,c)). We break the cycle by building an ad-hoc compilation
+           environment. A cleaner solution would be that kernel projections are
+           simply Proj(i,c) with i an int and c a constr, but we would have to
+           get rid of the compatibility layer. *)
+	   let cb =
+	     { const_hyps = hyps;
+	       const_body = def;
+	       const_type = typ;
+	       const_proj = proj;
+	       const_body_code = None;
+	       const_polymorphic = poly;
+	       const_universes = univs;
+	       const_inline_code = inline_code }
+	   in
+	   let env = add_constant kn cb env in
+	   compile_constant_body env def
       in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
@@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_universes = univs;
     const_inline_code = inline_code }
 
-
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc0414..a03a67db8b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
   | Zfix(f1,args1), Zfix(f2,args2) ->  Int.equal (nargs args1) (nargs args2)
-  | Zswitch _, Zswitch _ -> true
-  | _ , _ -> false
+  | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+  | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
 
 let rec compare_stack stk1 stk2 =
   match stk1, stk2 with
@@ -81,7 +81,10 @@ and conv_whd env pb k whd1 whd2 cu =
       conv_whd env pb k whd1 (force_whd v stk) cu
   | Vatom_stk(Aiddef(_,v),stk), _ ->
       conv_whd env pb k (force_whd v stk) whd2 cu
-  | _, _ -> raise NotConvertible
+
+  | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
+  | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
@@ -110,7 +113,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
       conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
       conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
-  | _, _ -> raise NotConvertible
+  | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env k stk1 stk2 cu =
   match stk1, stk2 with
@@ -131,7 +134,11 @@ and conv_stack env k stk1 stk2 cu =
 	done;
 	conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
-  | _, _ -> raise NotConvertible
+  | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+    if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    else raise NotConvertible
+  | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+  | Zproj _ :: _, _ -> raise NotConvertible
 
 and conv_fun env pb k f1 f2 cu =
   if f1 == f2 then cu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b39..a822f92eb3 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -127,10 +127,11 @@ type vswitch = {
 (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
 (*   - representation of [accu] : tag_[....]                              *)
 (*     -- tag <= 2 : encoding atom type (sorts, free vars, etc.)          *)
-(*     -- 3_[accu|fix_app] : a fixpoint blocked by an accu                *)
-(*     -- 4_[accu|vswitch] : a match blocked by an accu                   *)
-(*     -- 5_[fcofix]       : a cofix function                             *)
-(*     -- 6_[fcofix|val]   : a cofix function, val represent the value    *)
+(*     -- 3_[accu|proj name] : a projection blocked by an accu            *)
+(*     -- 4_[accu|fix_app] : a fixpoint blocked by an accu                *)
+(*     -- 5_[accu|vswitch] : a match blocked by an accu                   *)
+(*     -- 6_[fcofix]       : a cofix function                             *)
+(*     -- 7_[fcofix|val]   : a cofix function, val represent the value    *)
 (*        of the function applied to arg1 ... argn                        *)
 (* The [arguments] type, which is abstracted as an array, represents :    *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
@@ -149,6 +150,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -176,15 +178,18 @@ let rec whd_accu a stk =
   match Obj.tag at with
   | i when i <= 2 ->
       Vatom_stk(Obj.magic at, stk)
-  | 3 (* fix_app tag *) ->
+  | 3 (* proj tag *) ->
+     let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+     whd_accu (Obj.field at 1) (zproj :: stk)
+  | 4 (* fix_app tag *) ->
       let fa = Obj.field at 1 in
       let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
-  | 4 (* switch tag  *) ->
+  | 5 (* switch tag  *) ->
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
-  | 5 (* cofix_tag *) ->
+  | 6 (* cofix_tag *) ->
       let vcfx = Obj.obj (Obj.field at 0) in
       let to_up = Obj.obj a in
       begin match stk with
@@ -192,7 +197,7 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
-  | 6 (* cofix_evaluated_tag *) ->
+  | 7 (* cofix_evaluated_tag *) ->
       let vcofix = Obj.obj (Obj.field at 0) in
       let res = Obj.obj a in
       begin match stk with
@@ -289,6 +294,7 @@ let rec obj_of_str_const str =
   match str with
   | Const_sorts s -> Obj.repr (Vsort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_proj p -> Obj.repr p
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5190356828..d31448ee13 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -34,6 +34,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list