Added default canonical structures (see example in test-suite)

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

5 files changed, 91 insertions, 19 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6712af8b9..2eb22b177 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -744,7 +744,9 @@ let print_path_between cls clt =
 
 let print_canonical_projections () =
   prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
-    pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+  (match r2 with Some sr2 -> pr_global sr2 | None -> str " _") ++ 
+    str " <- " ++ 
+    pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
     (canonical_projections ())
 
 (*************************************************************************)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 93e1c1157..55625232b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -115,15 +115,22 @@ let apprec_nohdbeta env evd c =
 let check_conv_record (t1,l1) (t2,l2) =
   try
     let proji = global_of_constr t1 in
-    let cstr = global_of_constr t2 in
-    let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
-      lookup_canonical_conversion (proji, cstr) 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 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
-    c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1
+    c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
+    (n,applist(t2,l2))
   with _ -> 
     raise Not_found
 
@@ -466,14 +473,15 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
 	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
 
-and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
-  let (evd',ks) =
+and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = 
+  let (evd',ks,_) =
     List.fold_left
-      (fun (i,ks) b ->
+      (fun (i,ks,m) b ->
+	 if m=0 then (i,t2::ks, n-1) else
 	 let dloc = (dummy_loc,InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
-	 (i', ev :: ks))
-      (evd,[]) bs
+	 (i', ev :: ks, n - 1))
+      (evd,[],n) bs
   in
   ise_and evd'
     [(fun i ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4b93388d6..73ff31180 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -115,12 +115,13 @@ that maps the pair (Li,ci) to the following data
 
 type obj_typ = {
   o_DEF : constr;
+  o_INJ : int;      (* position of trivial argument (negative= none) *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
   o_TCOMPS : constr list } (* ordered *)
 
 let object_table =
-  (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
+  (ref [] : ((global_reference * global_reference option) * obj_typ) list ref)
 
 let canonical_projections () = !object_table
 
@@ -128,14 +129,15 @@ let keep_true_projections projs kinds =
   map_succeed (function (p,true) -> p | _ -> failwith "")
     (List.combine projs kinds)
 
-(* Intended to always success *)
+(* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let v = mkConst con in
   let c = Environ.constant_value (Global.env()) con in
   let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
   let lt = List.rev (List.map snd lt) in
   let args = snd (decompose_app t) in
-  let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in
+  let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = 
+    lookup_structure ind in
   let params, projs = list_chop p args in
   let lpj = keep_true_projections lpj kl in
   let lps = List.combine lpj projs in
@@ -145,12 +147,22 @@ let compute_canonical_projections (con,ind) =
 	 match spopt with
            | Some proji_sp ->
 	       let c, args = decompose_app t in
-	       (try (ConstRef proji_sp, global_of_constr c, args) :: l
-                with Not_found -> l)
+		 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
 	   | _ -> l)
       [] lps in
-  List.map (fun (refi,c,argj) ->
-    (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj})
+  List.map (fun (refi,c,inj,argj) ->
+    (refi,c),{o_DEF=v; o_INJ=inj; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj})
     comp
 
 let open_canonical_structure i (_,o) =
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index c8942b5d4..321584b5b 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -38,11 +38,12 @@ val find_projection_nparams : global_reference -> int
 
 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) -> obj_typ
+val lookup_canonical_conversion : (global_reference * global_reference option) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val canonical_projections : unit -> 
-  ((global_reference * global_reference) * obj_typ) list
+  ((global_reference * global_reference option) * obj_typ) list
diff --git a/test-suite/success/DefaultCanonicalStructure.v b/test-suite/success/DefaultCanonicalStructure.v
new file mode 100644
index 000000000..f21ea7c8a
--- /dev/null
+++ b/test-suite/success/DefaultCanonicalStructure.v
@@ -0,0 +1,49 @@
+
+(* 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.