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

6 files changed, 210 insertions, 78 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 2eb22b177..b39cdedda 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -742,9 +742,15 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
+let pr_cs_pattern = function  
+    Const_cs c -> pr_global c
+  | Prod_cs -> str "_ -> _"
+  | Default_cs -> str "_"
+  | Sort_cs s -> pr_sort_family s
+
 let print_canonical_projections () =
-  prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
-  (match r2 with Some sr2 -> pr_global sr2 | None -> str " _") ++ 
+  prlist_with_sep pr_fnl 
+    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ 
     str " <- " ++ 
     pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
     (canonical_projections ())
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
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
new file mode 100644
index 000000000..8e613dcaa
--- /dev/null
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -0,0 +1,144 @@
+Section group_morphism.
+
+(* An example with default canonical structures *)
+
+Variable A B : Type.
+Variable plusA : A -> A -> A.
+Variable plusB : B -> B -> B.
+Variable zeroA : A.
+Variable zeroB : B.
+Variable eqA : A -> A -> Prop.
+Variable eqB : B -> B -> Prop.
+Variable phi : A -> B.
+
+Record img := {
+  ia : A;
+  ib :> B;
+  prf : phi ia = ib
+}.
+
+Parameter eq_img : forall (i1:img) (i2:img),
+  eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
+
+Lemma phi_img (a:A) : img.
+  intro a.
+  exists  a (phi a).
+  refine ( refl_equal _).
+Defined.
+Canonical Structure phi_img.
+
+Lemma zero_img : img.
+  exists zeroA zeroB.
+  admit.
+Defined.
+Canonical Structure zero_img.
+
+Lemma plus_img : img -> img -> img.
+intros i1 i2.
+exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)).
+admit.
+Defined.
+Canonical Structure plus_img.
+
+(* Print Canonical Projections. *)
+
+Goal forall a1 a2, eqA (plusA a1 zeroA) a2.
+  intros a1 a2.
+  refine  (eq_img _ _  _).
+change (eqB (plusB (phi a1) zeroB) (phi a2)).
+Admitted.
+
+End group_morphism.
+
+Open Scope type_scope.
+
+Section type_reification.
+
+Inductive term :Type := 
+   Fun : term -> term -> term
+ | Prod : term -> term -> term
+ | Bool : term
+ | SET :term
+ | PROP :term
+ | TYPE :term
+ | Var : Type -> term.
+
+Fixpoint interp (t:term) := 
+  match t with 
+    Bool => bool
+  | SET => Set
+  | PROP => Prop
+  | TYPE => Type   
+  | Fun a b => interp a -> interp b
+  | Prod a b => interp a * interp b
+  | Var x => x
+end.
+
+Record interp_pair :Type := 
+  { repr:>term;
+    abs:>Type;
+    link: abs = interp repr }.
+
+Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
+proof.
+let a:interp_pair,b:interp_pair.
+reconsider thesis as (a * b = interp a * interp b).
+thus thesis by (link a),(link b).
+end proof.
+Qed.
+
+Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
+proof.
+let a:interp_pair,b:interp_pair.
+reconsider thesis as ((a -> b) = (interp a -> interp b)).
+thus thesis using rewrite (link a);rewrite (link b);reflexivity.
+end proof.
+Qed.
+
+Canonical Structure ProdCan (a b:interp_pair) := 
+  Build_interp_pair (Prod a b) (a * b) (prod_interp a b).
+
+Canonical Structure FunCan (a b:interp_pair) := 
+  Build_interp_pair (Fun a b) (a -> b) (fun_interp a b).
+
+Canonical Structure BoolCan := 
+  Build_interp_pair Bool bool (refl_equal _).
+
+Canonical Structure VarCan (x:Type) := 
+  Build_interp_pair (Var x) x (refl_equal _).
+
+Canonical Structure SetCan := 
+  Build_interp_pair SET Set (refl_equal _).
+
+Canonical Structure PropCan := 
+  Build_interp_pair PROP Prop (refl_equal _).
+
+Canonical Structure TypeCan := 
+  Build_interp_pair TYPE Type (refl_equal _).
+
+(* Print Canonical Projections. *)
+
+Variable A:Type.
+
+Variable Inhabited: term -> Prop.
+
+Variable Inhabited_correct: forall p, Inhabited (repr p)  -> abs p.
+
+Lemma L : Prop * A -> bool * (Type -> Set) .
+refine (Inhabited_correct _ _).
+change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
+Admitted.
+
+Check L : abs _ .
+
+End type_reification.
+
+
+
+
+
+
+
+
+ 
+
diff --git a/test-suite/success/DefaultCanonicalStructure.v b/test-suite/success/DefaultCanonicalStructure.v
deleted file mode 100644
index f21ea7c8a..000000000
--- a/test-suite/success/DefaultCanonicalStructure.v
+++ /dev/null
@@ -1,49 +0,0 @@
-
-(* An example with default canonical structures *)
-
-Variable A B : Type.
-Variable plusA : A -> A -> A.
-Variable plusB : B -> B -> B.
-Variable zeroA : A.
-Variable zeroB : B.
-Variable eqA : A -> A -> Prop.
-Variable eqB : B -> B -> Prop.
-Variable phi : A -> B.
-
-Set Implicit Arguments.
-
-Record img := {
-  ia : A;
-  ib :> B;
-  prf : phi ia = ib
-}.
-
-Parameter eq_img : forall (i1:img) (i2:img),
-  eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
-
-Lemma phi_img (a:A) : img.
-  intro a.
-  exists  a (phi a).
-  refine ( refl_equal _).
-Defined.
-Canonical Structure phi_img.
-
-Lemma zero_img : img.
-  exists zeroA zeroB.
-  admit.
-Defined.
-Canonical Structure zero_img.
-
-Lemma plus_img : img -> img -> img.
-intros i1 i2.
-exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)).
-admit.
-Defined.
-Canonical Structure plus_img.
-
-Print Canonical Projections.
-
-Goal forall a1 a2, eqA (plusA a1 zeroA) a2.
-  intros a1 a2.
-  refine  (eq_img _ _  _); simpl.
-Admitted.