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 1be3e6511..29e33d349 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 9cbf4077e..8c5ab0ecb 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 ddbde9d38..0a121dc32 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 1bf493e2c..1590a2141 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 93fd61f02..3271ac145 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 d9998c89e..745ef311b 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 ac46dc583..d5435f0c3 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 2535a64d3..0d9334a50 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 49ab68bea..8fd90ec36 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 a316b4492..83e566041 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 1c31cc041..a03a67db8 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 d4bf461b3..a822f92eb 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 519035682..d31448ee1 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