added products and sorts as possible heads for canonical structures

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 58 insertions, 27 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 55625232b..d80fdac9d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -115,20 +115,28 @@ let apprec_nohdbeta env evd c =
 let check_conv_record (t1,l1) (t2,l2) =
   try
     let proji = global_of_constr t1 in
-    let canon_s = 
-      begin    
-	try 
-	  let cstr = global_of_constr t2 in
-	    lookup_canonical_conversion (proji, Some cstr)
-	with _ -> lookup_canonical_conversion (proji,None)
-      end in
-    let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
-      canon_s in
+    let canon_s,l2_effective = 
+      try
+	match kind_of_term t2 with
+	    Prod (_,a,b) -> (* assert (l2=[]); *)
+      	      if dependent (mkRel 1) b then raise Not_found
+	      else lookup_canonical_conversion (proji, Prod_cs),[a;pop b]
+	  | Sort s -> 
+	      lookup_canonical_conversion 
+		(proji, Sort_cs (family_of_sort s)),[]
+	  | _ -> 
+	      let c2 = try global_of_constr t2 with _ -> raise Not_found in
+		lookup_canonical_conversion (proji, Const_cs c2),l2
+      with Not_found -> 
+	lookup_canonical_conversion (proji,Default_cs),[]
+    in
+    let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } 
+	= canon_s in
     let params1, c1, extra_args1 =
       match list_chop (List.length params) l1 with 
 	| params1, c1::extra_args1 -> params1, c1, extra_args1
 	| _ -> assert false in
-    let us2,extra_args2 = list_chop (List.length us) l2 in
+    let us2,extra_args2 = list_chop (List.length us) l2_effective in
     c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
     (n,applist(t2,l2))
   with _ -> 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 73ff31180..9681a7a63 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -120,8 +120,14 @@ type obj_typ = {
   o_TPARAMS : constr list; (* ordered *)
   o_TCOMPS : constr list } (* ordered *)
 
+type cs_pattern =
+    Const_cs of global_reference
+  | Prod_cs
+  | Sort_cs of sorts_family
+  | Default_cs
+
 let object_table =
-  (ref [] : ((global_reference * global_reference option) * obj_typ) list ref)
+  (ref [] : ((global_reference * cs_pattern) * obj_typ) list ref)
 
 let canonical_projections () = !object_table
 
@@ -129,6 +135,22 @@ let keep_true_projections projs kinds =
   map_succeed (function (p,true) -> p | _ -> failwith "")
     (List.combine projs kinds)
 
+let cs_pattern_of_constr t =
+  match kind_of_term t with
+      App (f,vargs) -> 
+	begin 
+	  try  Const_cs (global_of_constr f) , -1, Array.to_list vargs with
+	      _ -> raise Not_found 
+	end 
+    | Rel n -> Default_cs, pred n, []
+    | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b]
+    | Sort s -> Sort_cs (family_of_sort s), -1, []
+    | _ -> 
+	begin 
+	  try  Const_cs (global_of_constr t) , -1, [] with
+	      _ -> raise Not_found 
+	end 
+
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let v = mkConst con in
@@ -146,19 +168,12 @@ let compute_canonical_projections (con,ind) =
       (fun l (spopt,t) -> (* comp=components *)
 	 match spopt with
            | Some proji_sp ->
-	       let c, args = decompose_app t in
-		 begin
-		   try 
-		     let ogc,oinj = 
-		       try  Some (global_of_constr c) , -1  
-		       with _ -> 
-			 try  
-			   None,pred (destRel c) 
-			 with _ -> raise Not_found 
-		     in
-   		       ((ConstRef proji_sp, ogc,oinj , args) :: l)
-                   with Not_found -> l 
-		 end
+	       begin
+		 try 
+		   let patt, n , args = cs_pattern_of_constr t in
+		     ((ConstRef proji_sp, patt, n, args) :: l)
+		 with Not_found -> l 
+	       end
 	   | _ -> l)
       [] lps in
   List.map (fun (refi,c,inj,argj) ->
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 321584b5b..348407ae1 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -36,14 +36,22 @@ val find_projection_nparams : global_reference -> int
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)
 
+type cs_pattern =
+    Const_cs of global_reference
+  | Prod_cs 
+  | Sort_cs of sorts_family
+  | Default_cs
+
 type obj_typ = {
   o_DEF : constr;
   o_INJ : int;      (* position of trivial argument *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
   o_TCOMPS : constr list } (* ordered *)
-               
-val lookup_canonical_conversion : (global_reference * global_reference option) -> obj_typ
+
+val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+ 
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val canonical_projections : unit -> 
-  ((global_reference * global_reference option) * obj_typ) list
+  ((global_reference * cs_pattern) * obj_typ) list