Backport Program Instance into Instance. Proper early error message if

trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...


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

7 files changed, 109 insertions, 41 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index f605988440..fb15e41b6a 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -151,6 +151,17 @@ let new_instance ctx (instid, bk, cl) props =
 	    let cl = Option.get (class_of_constr c) in
 	      cl, ctx, [])
   in
+  let id = 
+    match snd instid with
+	Name id -> 
+	  let sp = Lib.make_path id in
+	    if Nametab.exists_cci sp then
+	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+	    id
+      | Anonymous -> 
+	  let i = Nameops.add_suffix k.cl_name "_instance_0" in
+	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
+  in
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
@@ -192,13 +203,6 @@ let new_instance ctx (instid, bk, cl) props =
       Evarutil.nf_isevar !isevars t
   in
   isevars := undefined_evars !isevars;
-  let id =
-    match snd instid with
-	Name id -> id
-      | Anonymous -> 
-	  let i = Nameops.add_suffix k.cl_name "_instance_" in
-	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
-  in
   let imps = 
     Util.list_map_i 
       (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index b7777e6222..a6639abbcf 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -156,7 +156,7 @@ let declare_definition prg =
   let gr = ConstRef c in
     if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
       Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
-    print_message (definition_message c);
+    print_message (Subtac_utils.definition_message c);
     prg.prg_hook c;
     c
 
@@ -217,7 +217,7 @@ let declare_obligation obl body =
   let constant = Declare.declare_constant obl.obl_name 
     (DefinitionEntry ce,IsProof Property)
   in
-    print_message (definition_message constant);
+    print_message (Subtac_utils.definition_message constant);
     { obl with obl_body = Some (mkConst constant) }
       
 let try_tactics obls = 
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 9aa4451870..5939f840fc 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -397,3 +397,6 @@ TACTIC EXTEND typeclasses_eauto
 	let evd' = resolve_argument_typeclasses d (mode, depth) env evd false false in
 	  Refiner.tclEVARS (Evd.evars_of evd') gl ]
 END
+
+let _ = 
+  Classes.refine_ref := Refine.refine
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 8c8c8c67c7..cd7737d06d 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -130,6 +130,11 @@ Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv
 Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
+Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
+  reflexive_partial_app_morphism.
+
+Existing Instance setoid_partial_app_morphism.
+
 Definition type_eq : relation Type :=
   fun x y => x = y.
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1d5280a490..ec2c950486 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -356,10 +356,17 @@ let destClassApp cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
     | _ -> raise Not_found
 
+let refine_ref = ref (fun _ -> assert(false))
+
+open Pp
+
+let ($$) g f = fun x -> g (f x)
+
 let new_instance ctx (instid, bk, cl) props =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-
+  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
+  let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass = 
     match bk with
       | Explicit ->
@@ -388,8 +395,14 @@ let new_instance ctx (instid, bk, cl) props =
 
       | Implicit -> cl
   in
+  let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
+  let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
+  let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in
+  let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
+  let ctx, avoid = name_typeclass_binders bound ctx in
+  let ctx = List.rev_append gen_ctx ctx in
   let k, ctx', subst = 
-    let c = abstract_constr_expr tclass ctx in
+    let c = Command.generalize_constr_expr tclass ctx in
     let _imps, c' = interp_type_evars isevars env c in
     let ctx, c = decompose_named_assum c' in
       (match kind_of_term c with 
@@ -400,22 +413,45 @@ let new_instance ctx (instid, bk, cl) props =
 	    let cl = Option.get (class_of_constr c) in
 	      cl, ctx, [])
   in
+  let id = 
+    match snd instid with
+	Name id -> 
+	  let sp = Lib.make_path id in
+	    if Nametab.exists_cci sp then
+	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+	    id
+      | Anonymous -> 
+	  let i = Nameops.add_suffix k.cl_name "_instance_0" in
+	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
+  in
   let env' = push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
   isevars := resolve_typeclasses env sigma !isevars;
   let sigma = Evd.evars_of !isevars in
-  let env' = Evarutil.nf_env_evar sigma env' in
   let substctx = Typeclasses.nf_substitution sigma subst in
-  let subst, propsctx = 
+  let subst, _propsctx = 
     let props = 
       List.map (fun (x, l, d) -> 
-	Topconstr.abstract_constr_expr d (binders_of_lidents l))
+	x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
 	props
     in
-      if List.length props <> List.length k.cl_props then 
-	mismatched_props env' props k.cl_props;
-      type_ctx_instance isevars env' k.cl_props props substctx
+      if List.length props > List.length k.cl_props then 
+	mismatched_props env' (List.map snd props) k.cl_props;
+      let props, rest = 
+	List.fold_left
+	  (fun (props, rest) (id,_,_) -> 
+	    try 
+	      let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		c :: props, rest'
+	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+	  ([], props) k.cl_props
+      in
+	if rest <> [] then 
+	  unbound_method env' k.cl_name (fst (List.hd rest))
+	else
+	  type_ctx_instance isevars env' k.cl_props props substctx
   in
   let app = 
     applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
@@ -423,33 +459,49 @@ let new_instance ctx (instid, bk, cl) props =
   let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
   isevars := Evarutil.nf_evar_defs !isevars;
   let term = Evarutil.nf_isevar !isevars term in
-  let cdecl = 
-    let kind = IsDefinition Instance in
-    let entry = 
-      { const_entry_body   = term;
-	const_entry_type   = None;
-	const_entry_opaque = false;
-	const_entry_boxed  = false }
-    in DefinitionEntry entry, kind
+  let termtype = 
+    let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
+    let t = it_mkNamedProd_or_LetIn app ctx' in
+      Evarutil.nf_isevar !isevars t
   in
-  let id, cst =
-    let instid = 
-      match snd instid with
-	  Name id -> id
-	| Anonymous -> 
-	    let i = Nameops.add_suffix k.cl_name "_instance_" in
-	      Termops.next_global_ident_away false i (Termops.ids_of_context env)
+  let imps = 
+    Util.list_map_i 
+      (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
+      1 ctx'
+  in
+  let hook cst = 
+    let inst = 
+      { is_class = k;
+	is_name = id;
+	is_impl = cst;
+      }
     in
-      instid, Declare.declare_constant instid cdecl
-  in 
-  let inst = 
-    { is_class = k;
-      is_name = id;
-      is_impl = cst;
-    }
+      add_instance_hint id;
+      Impargs.declare_manual_implicits false (ConstRef cst) false imps;
+      Typeclasses.add_instance inst
   in
-    add_instance_hint id;
-    add_instance inst
+  let evm = Evd.evars_of (undefined_evars !isevars) in
+    if evm = Evd.empty then
+      let cdecl = 
+	let kind = IsDefinition Instance in
+	let entry = 
+	  { const_entry_body   = term;
+	    const_entry_type   = Some termtype;
+	    const_entry_opaque = false;
+	    const_entry_boxed  = false }
+	in DefinitionEntry entry, kind
+      in
+      let kn = Declare.declare_constant id cdecl in
+	Flags.if_verbose Command.definition_message id;
+	hook kn
+    else
+      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
+	Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+	  (!refine_ref (evm, term));
+	Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ()
+
+    
      
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 015bdce5c3..f305fc805e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -67,6 +67,8 @@ val solve_evars_by_tac :     env ->
   Proof_type.tactic ->
   Evd.evar_defs
 
+val refine_ref : (open_constr -> Proof_type.tactic) ref
+
 val decompose_named_assum : types -> named_context * types
 
 val push_named_context : named_context -> env -> env
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d587fabf77..7ec29e0f59 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,6 +30,8 @@ open Redexpr
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
+val definition_message : identifier -> unit
+
 val declare_definition : identifier -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> declaration_hook -> unit