Backport fixes in Instance declarations to Program Instance.

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

2 files changed, 108 insertions, 136 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index fe25dc6fc..5c9deab8d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -29,40 +30,6 @@ open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
-let interp_binder_evars evdref env na t =
-  let t = Constrintern.intern_gen true ( !evdref) env t in
-    SPretyping.understand_tcc_evars evdref env IsType t
-
-let interp_binders_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) ((loc, i), t) ->
-      let n = Name i in
-      let t' = interp_binder_evars isevars env n t in
-      let d = (i,None,t') in
-	(push_named d env, i :: ids, d::params))
-    (env, avoid, []) l
-
-let interp_typeclass_context_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) (iid, bk, cl) ->
-      let t' = interp_binder_evars isevars env (snd iid) cl in
-      let i = match snd iid with
-	| Anonymous -> Namegen.next_name_away (Namegen.named_hd env t' Anonymous) ids
-	| Name id -> id
-      in
-      let d = (i,None,t') in
-	(push_named d env, i :: ids, d::params))
-    (env, avoid, []) l
-
-let interp_constrs_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, ids, params) t ->
-      let t' = interp_binder_evars isevars env Anonymous t in
-      let id = Namegen.next_name_away (Namegen.named_hd env t' Anonymous) ids in
-      let d = (id,None,t') in
-	(push_named d env, id :: ids, d::params))
-    (env, avoid, []) l
-
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
   SPretyping.understand_tcc_evars evdref env kind
     (intern_gen (kind=IsType) ~impls ( !evdref) env c)
@@ -70,31 +37,29 @@ let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
 let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
-let type_ctx_instance isevars env ctx inst subst =
-  List.fold_left2
-    (fun (subst, instctx) (na, _, t) ce ->
-      let t' = substl subst t in
-      let c = interp_casted_constr_evars isevars env ce t' in
-      isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
-      let d = na, Some c, t' in
-	c :: subst, d :: instctx)
-    (subst, []) (List.rev ctx) inst
-
-let type_class_instance_params isevars env id n ctx inst subst =
-  List.fold_left2
-    (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
-      let c = interp_casted_constr_evars isevars env ce t' in
-      let d = na, Some c, t' in
-	(na, c) :: subst, d :: instctx)
-    (subst, []) (List.rev ctx) inst
+let interp_context_evars evdref env params =
+  Constrintern.interp_context_gen
+    (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t)
+    (SPretyping.understand_judgment_tcc evdref) !evdref env params
 
-let substitution_of_constrs ctx cstrs =
-  List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
+let type_ctx_instance evars env ctx inst subst =
+  let rec aux (subst, instctx) l = function
+    (na, b, t) :: ctx ->
+      let t' = substl subst t in
+      let c', l =
+	match b with
+	| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
+	| Some b -> substl subst b, l
+      in
+       evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
+       let d = na, Some c', t' in
+	aux (c' :: subst, d :: instctx) l ctx
+    | [] -> subst
+  in aux (subst, []) inst (List.rev ctx)
 
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
-  let isevars = ref Evd.empty in
+  let evars = ref Evd.empty in
   let tclass, _ =
     match bk with
     | Implicit ->
@@ -113,12 +78,22 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
       | Explicit -> cl, Idset.empty
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
-  let k, ctx', imps, subst =
-    let c = Topconstr.prod_constr_expr tclass ctx in
-    let c', imps = interp_type_evars_impls ~evdref:isevars env c in
-    let ctx, c = decompose_prod_assum c' in
-    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
-      cl, ctx, imps, (List.rev args)
+  let k, cty, ctx', ctx, len, imps, subst =
+    let (env', ctx), imps = interp_context_evars evars env ctx in
+    let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+    let len = List.length ctx in
+    let imps = imps @ Impargs.lift_implicits len imps' in
+    let ctx', c = decompose_prod_assum c' in
+    let ctx'' = ctx' @ ctx in
+    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+    let _, args = 
+      List.fold_right (fun (na, b, t) (args, args') ->
+	match b with
+	| None -> (List.tl args, List.hd args :: args')
+	| Some b -> (args, substl args' b :: args'))
+	(snd cl.cl_context) (args, [])
+    in
+      cl, c', ctx', ctx, len, imps, args
   in
   let id =
     match snd instid with
@@ -131,79 +106,77 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
 	  Namegen.next_global_ident_away i (Termops.ids_of_context env)
   in
-  let env' = push_rel_context ctx' env in
-  isevars := Evarutil.nf_evar_map !isevars;
-  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
-  let sigma =  !isevars in
+  let env' = push_rel_context ctx env in
+  evars := Evarutil.nf_evar_map !evars;
+  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
+  let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
-  let subst =
-    let props =
-      match props with
-      | CRecord (loc, _, fs) ->
-	  if List.length fs > List.length k.cl_props then
-	    Classes.mismatched_props env' (List.map snd fs) k.cl_props;
-	  fs
-      | _ ->
-	  if List.length k.cl_props <> 1 then
-	    errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
-	  else [Ident (dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
-    in
-      match k.cl_props with
-      | [(na,b,ty)] ->
-	  let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
-	  let ty' = substl subst ty in
-	  let c = interp_casted_constr_evars isevars env' term ty' in
-	    c :: subst
-      | _ ->
-	  let get_id (idref, c) =
-	    match idref with
-	      | Ident id' -> id'
-	      | _ ->
-		  errorlabstrm "new_instance"
-		    (Pp.str "only local structures are managed")
-	  in
-	  let props, rest =
-	    List.fold_left
-	      (fun (props, rest) (id,_,_) ->
-		 try
-		   let (loc_mid, c) =
-		     List.find (fun elt -> Name (snd (get_id elt)) = id) rest
-		   in
-		   let rest' =
-		     List.filter (fun elt -> Name (snd (get_id elt)) <> id) rest
-		   in
-		   match loc_mid with
-		     | Ident (loc, mid) ->
-			 Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
-			 c :: props, rest'
-		     | _ -> errorlabstrm "new_instance"
-			 (Pp.str "only local structures are managed")
-		 with Not_found ->
-		   (CHole (Util.dummy_loc, None) :: props), rest)
-	      ([], props) k.cl_props
-	  in
-	    if rest <> [] then
-	      unbound_method env' k.cl_impl (get_id (List.hd rest))
-	    else
-	      fst (type_ctx_instance isevars env' k.cl_props props subst)
+  let props =
+    match props with
+    | CRecord (loc, _, fs) ->
+	if List.length fs > List.length k.cl_props then
+	  Classes.mismatched_props env' (List.map snd fs) k.cl_props;
+	Inl fs
+    | _ -> Inr props
   in
-  let subst = List.fold_left2
-    (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
-    [] subst (k.cl_props @ snd k.cl_context)
+  let subst =
+    match props with
+    | Inr term ->
+	let c = interp_casted_constr_evars evars env' term cty in
+	  Inr (c, subst)
+    | Inl props ->
+	let get_id =
+	  function
+	    | Ident id' -> id'
+	    | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled")
+	in
+	let props, rest =
+	  List.fold_left
+	    (fun (props, rest) (id,b,_) ->
+	      if b = None then
+		try
+		  let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
+		  let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
+		  let (loc, mid) = get_id loc_mid in
+		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+		    c :: props, rest'
+		with Not_found ->
+		  (CHole (Util.dummy_loc, None) :: props), rest
+	      else props, rest)
+	    ([], props) k.cl_props
+	in
+	  if rest <> [] then
+	    unbound_method env' k.cl_impl (get_id (fst (List.hd rest)))
+	  else
+	    Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
+  in	  
+  evars := Evarutil.nf_evar_map !evars;
+  let term, termtype =
+    match subst with
+    | Inl subst ->
+	let subst = List.fold_left2
+	  (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+	  [] subst (k.cl_props @ snd k.cl_context)
+	in
+	let app, ty_constr = instance_constructor k subst in
+	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+	let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
+	  term, termtype
+    | Inr (def, subst) ->
+	let termtype = it_mkProd_or_LetIn cty ctx in
+	let term = Termops.it_mkLambda_or_LetIn def ctx in
+	  term, termtype
   in
-  let inst_constr, ty_constr = instance_constructor k subst in
-  isevars := Evarutil.nf_evar_map !isevars;
-  let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
-  and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
+  let termtype = Evarutil.nf_isevar !evars termtype in
+  let term = Evarutil.nf_isevar !evars term in
+  evars := undefined_evars !evars;
+  Evarutil.check_evars env Evd.empty !evars termtype;
+  let hook vis gr =
+    let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+    let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
+      Impargs.declare_manual_implicits false gr ~enriching:false imps;
+      Typeclasses.add_instance inst
   in
-    isevars := undefined_evars !isevars;
-    Evarutil.check_evars env Evd.empty !isevars termtype;
-    let hook vis gr =
-      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
-	Impargs.declare_manual_implicits false gr ~enriching:false imps;
-	Typeclasses.add_instance inst
-    in
-    let evm = Subtac_utils.evars_of_term !isevars Evd.empty term in
-    let obls, _, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
-      id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
+  let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
+  let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
+    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 4b575da90..ee78ff68a 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -25,12 +25,11 @@ open Classes
 (*i*)
 
 val type_ctx_instance :     Evd.evar_map ref ->
-    Environ.env ->
+  Environ.env ->
     ('a * Term.constr option * Term.constr) list ->
     Topconstr.constr_expr list ->
     Term.constr list ->
-    Term.constr list *
-    ('a * Term.constr option * Term.constr) list
+    Term.constr list
 
 val new_instance :
   ?global:bool ->