Code cleanup in typeclasses, remove dead and duplicated code.

Change from named_context to rel_context for class params and fields.


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

1 files changed, 37 insertions, 260 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0d24a6edd..30fee26a0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -61,11 +61,12 @@ let declare_instance glob idl =
   in declare_instance_cst glob con
 	  
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 type binder_list = (identifier located * bool * constr_expr) list
 
+(* Calls to interpretation functions. *)
+
 let interp_binders_evars isevars env avoid l =
   List.fold_left
     (fun (env, ids, params) ((loc, i), t) -> 
@@ -87,33 +88,26 @@ let interp_typeclass_context_evars isevars env avoid l =
 	(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 = Nameops.next_name_away (Termops.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 raw_assum_of_binders k = 
-  List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t))
-
-let raw_assum_of_constrs k = 
-  List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t))
-
-let raw_assum_of_anonymous_constrs k = 
-  List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t))
+let interp_type_evars evdref env ?(impls=([],[])) typ =
+  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
+    imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
 
-let decl_expr_of_binders = 
-  List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t))
-      
-let rec unfold n f acc = 
-  match n with 
-    | 0 -> f 0 acc
-    | n -> unfold (n - 1) f (f n acc)
+let mk_interning_data env na impls typ =
+  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
+  in (na, ([], impl, Notation.compute_arguments_scope typ))
+    
+let interp_fields_evars isevars env avoid l =
+  List.fold_left
+    (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> 
+      let impl, t' = interp_type_evars isevars env ~impls t in
+      let data = mk_interning_data env i impl t' in
+      let d = (Name i,None,t') in
+	(push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
+    (env, [], avoid, [], ([], [])) l    
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
+
 open Topconstr
 
 let declare_implicit_proj c proj imps sub =
@@ -144,22 +138,12 @@ let declare_implicits impls subs cl =
 	if len - i <= cl.cl_params then acc
 	else 
 	  match is with
-	      None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc
+	      None | Some (_, false) -> (ExplByPos (i, Some (Nameops.out_name na)), (false, true)) :: acc
 	    | _ -> acc)
       1 [] (List.rev cl.cl_context)
   in
     Impargs.declare_manual_implicits false cl.cl_impl false indimps
       
-let rel_of_named_context subst l = 
-  List.fold_right
-    (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
-    l ([], subst)
-
-let ids_of_rel_context subst l = 
-  List.fold_right
-    (fun (id, _, t) acc -> Nameops.out_name id :: acc)
-    l subst
-
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
@@ -168,7 +152,6 @@ let degenerate_decl (na,b,t) =
     | None -> (id, Entries.LocalAssum t)
     | Some b -> (id, Entries.LocalDef b)
 
-
 let declare_structure env id idbuild params arity fields =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
@@ -192,33 +175,6 @@ let declare_structure env id idbuild params arity fields =
     Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
     rsp
 
-let interp_type_evars evdref env ?(impls=([],[])) typ =
-  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
-  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
-    imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
-
-let mk_interning_data env na impls typ =
-  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
-  in (na, ([], impl, Notation.compute_arguments_scope typ))
-    
-let interp_fields_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> 
-      let impl, t' = interp_type_evars isevars env ~impls t in
-      let data = mk_interning_data env i impl t' in
-      let d = (i,None,t') in
-	(push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
-    (env, [], avoid, [], ([], [])) l    
-
-let interp_fields_rel_evars isevars env avoid l =
-  List.fold_left
-    (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> 
-      let impl, t' = interp_type_evars isevars env ~impls t in
-      let data = mk_interning_data env i impl t' in
-      let d = (Name i,None,t') in
-	(push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
-    (env, [], avoid, [], ([], [])) l    
-
 let name_typeclass_binder avoid = function
   | LocalRawAssum ([loc, Anonymous], bk, c) ->
       let name = 
@@ -237,33 +193,7 @@ let name_typeclass_binders avoid l =
 				   b' :: binders, avoid)
       ([], avoid) l
   in List.rev l', avoid
-
-let decompose_named_assum = 
-  let rec prodec_rec subst l c =
-    match kind_of_term c with
-      | Prod (Name na,t,c) -> 
-	let decl = (na,None,substl subst t) in
-	let subst' = mkVar na :: subst in
-	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
-      | LetIn (Name na, b, t, c) ->
-	let decl = (na,Some (substl subst b),substl subst t) in
-	let subst' = mkVar na :: subst in
-	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
-      | Cast (c,_,_)      -> prodec_rec subst l c
-      | _               -> l,c
-  in prodec_rec [] []
       
-let push_named_context = 
-  List.fold_right push_named
-
-let named_of_rel_context (subst, ids, env as init) ctx =
-  Sign.fold_rel_context
-    (fun (na,c,t) (subst, avoid, env) ->
-      let id = Nameops.next_name_away na avoid in
-      let d = (id,Option.map (substl subst) c,substl subst t) in
-	(mkVar id :: subst, id::avoid, d::env))
-    ctx ~init
-    
 let new_class id par ar sup props =
   let env0 = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -294,7 +224,7 @@ let new_class id par ar sup props =
     
   (* Interpret the definitions and propositions *)
   let env_props, prop_impls, bound, ctx_props, _ = 
-    interp_fields_rel_evars isevars env_params bound props 
+    interp_fields_evars isevars env_params bound props 
   in
   let subs = List.map (fun ((loc, id), b, _) -> b) props in
   (* Instantiate evars and check all are resolved *)
@@ -344,21 +274,18 @@ let new_class id par ar sup props =
 	      IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
 			     fields (Recordops.lookup_projections kn))
   in
-  let ids = List.map pi1 (named_context env0) in
-  let (subst, ids, named_ctx_params) = named_of_rel_context ([], ids, []) ctx_params in
-  let (_, _, named_ctx_props) = named_of_rel_context (subst, ids, []) ctx_props in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
       match Typeclasses.class_of_constr t with
-      | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d)
+      | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d)
       | None -> (None, d))
-      named_ctx_params
+      ctx_params
   in
   let k =
     { cl_impl = impl;
       cl_params = List.length par;
       cl_context = ctx_context;
-      cl_props = named_ctx_props;
+      cl_props = ctx_props;
       cl_projs = projs }
   in
     declare_implicits (List.rev prop_impls) subs k;
@@ -369,64 +296,15 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
 let binders_of_lidents l =
   List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
 
-let subst_ids_in_named_context subst l =
-  let x, _ = 
-    List.fold_right
-      (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k)
-      l ([], 1)
-  in x
-    
-let subst_one_named inst ids t =
-  substnl inst 0 (substn_vars 1 ids t)
-      
-let subst_named inst subst ctx =
-  let ids = List.map (fun (id, _, _) -> id) subst in
-  let ctx' = subst_ids_in_named_context ids ctx in
-  let ctx', _ =
-    List.fold_right
-      (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
-      ctx' ([], 0)
-  in ctx'
-(*
-let infer_super_instances env params params_ctx super =
-  let super = subst_named params params_ctx super in
-    List.fold_right 
-      (fun (na, _, t) (sups, ids, supctx) -> 
-	let t = subst_one_named sups ids t in
-	let inst = 
-	  try resolve_one_typeclass env t 
-	  with Not_found -> 
-	    let cl, args = destClass t in
-	      no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args)
-	in
-	let d = (na, Some inst, t) in
-	  inst :: sups, na :: ids, d :: supctx)
-      super ([], [], [])*)
-      
-(* let evars_of_context ctx id n env = *)
-(*   List.fold_right (fun (na, _, t) (n, env, nc) ->  *)
-(*     let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *)
-(*     let d = (na, Some b, t) in *)
-(*       (succ n, push_named d env, d :: nc)) *)
-(*     ctx (n, env, []) *)
-
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
+      let t' = substl 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)
+	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-let substitution_of_constrs ctx cstrs =
-  List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
-
-let destClassApp cl =
-  match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
-    | _ -> raise Not_found
-
 let refine_ref = ref (fun _ -> assert(false))
 
 let id_of_class cl =
@@ -521,9 +399,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
   let k, ctx', imps, subst = 
     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
+    let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, List.rev (Array.to_list args)
   in
   let id = 
     match snd instid with
@@ -536,16 +414,16 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
-  let env' = push_named_context ctx' env in
+  let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses env !isevars;
   let sigma = Evd.evars_of !isevars in
-  let substctx = Typeclasses.nf_substitution sigma subst in
+  let substctx = List.map (Evarutil.nf_evar sigma) subst in
     if Lib.is_modtype () then
       begin
-	let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in
+	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
-	  let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+	  let t = it_mkProd_or_LetIn ty_constr ctx' in
 	    Evarutil.nf_isevar !isevars t
 	in
 	Evarutil.check_evars env Evd.empty !isevars termtype;
@@ -567,8 +445,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	      List.fold_left
 		(fun (props, rest) (id,_,_) -> 
 		  try 
-		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-		    let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
 		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -579,12 +457,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	      else
 		type_ctx_instance isevars env' k.cl_props props substctx
 	in
-	let app, ty_constr = instance_constructor k (List.rev_map snd subst) in
+	let app, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
-	  let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+	  let t = it_mkProd_or_LetIn ty_constr ctx' in
 	    Evarutil.nf_isevar !isevars t
 	in
-	let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
+	let term = Termops.it_mkLambda_or_LetIn app ctx' in
 	isevars := Evarutil.nf_evar_defs !isevars;
 	let term = Evarutil.nf_isevar !isevars term in
 	let evm = Evd.evars_of (undefined_evars !isevars) in
@@ -607,21 +485,6 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  end
       end
 
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-
-let solve_by_tac env evd evar evi t =
-  let goal = {it = evi; sigma = (Evd.evars_of evd) } in
-  let (res, valid) = t goal in 
-    if res.it = [] then 
-      let prooftree = valid [] in
-      let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in
-	if obls = [] then 
-	  let evd' = evars_reset_evd res.sigma evd in
-	  let evd' = evar_define evar proofterm evd' in
-	    evd', true
-	else evd, false
-    else evd, false
-
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -649,89 +512,3 @@ let context ?(hook=fun _ -> ()) l =
 	     None -> ()
 	   | Some tc -> hook (VarRef id)))
       (List.rev fullctx)
-
-open Libobject
-
-let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")
-let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation")
-  
-let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid)))
-let tactic = lazy (Tacinterp.interp tactic_expr)
-
-let _ =
-  Typeclasses.solve_instanciation_problem :=
-    (fun env evd ev evi -> 
-      Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
-      solve_by_tac env evd ev evi (Lazy.force tactic))
-
-(* let prod = lazy_fun Coqlib.build_prod *)
-
-(* let build_conjunction evm = *)
-(*   List.fold_left *)
-(*     (fun (acc, evs) (ev, evi)  -> *)
-(*       if class_of_constr evi.evar_concl <> None then *)
-(* 	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *)
-(*       else acc, Evd.add evs ev evi) *)
-(*     (Coqlib.build_coq_True (), Evd.empty) evm *)
-
-(* let destruct_conjunction evm_list evm evm' term = *)
-(*   let _, evm = *)
-(*     List.fold_right *)
-(*       (fun (ev, evi) (term, evs) -> *)
-(* 	if class_of_constr evi.evar_concl <> None then *)
-(* 	  match kind_of_term term with *)
-(* 	    | App (x, [| _ ; _ ; proof ; term |]) -> *)
-(* 		let evs' = Evd.define evs ev proof in *)
-(* 		  (term, evs') *)
-(* 	    | _ -> assert(false) *)
-(* 	else *)
-(* 	  match (Evd.find evm' ev).evar_body with *)
-(* 	      Evar_empty -> raise Not_found *)
-(* 	    | Evar_defined c -> *)
-(* 		let evs' = Evd.define evs ev c in *)
-(* 		  (term, evs')) *)
-(*       evm_list (term, evm) *)
-(*   in evm *)
- 
-(* let solve_by_tac env evd evar evi t = *)
-(*   let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
-(*   let (res, valid) = t goal in *)
-(*     if res.it = [] then *)
-(*       let prooftree = valid [] in *)
-(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
-(* 	if obls = [] then *)
-(* 	  let evd' = evars_reset_evd res.sigma evd in *)
-(* 	  let evd' = evar_define evar proofterm evd' in *)
-(* 	    evd', true *)
-(* 	else evd, false *)
-(*     else evd, false *)
-
-(* let resolve_all_typeclasses env evd = *)
-(*   let evm = Evd.evars_of evd in *)
-(*   let evm_list = Evd.to_list evm in *)
-(*   let goal, typesevm = build_conjunction evm_list in *)
-(*   let evars = ref (Evd.create_evar_defs typesevm) in *)
-(*   let term = resolve_one_typeclass_evd env evars goal in *)
-(*   let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *)
-(*     Evd.create_evar_defs evm' *)
-
-(* let _ = *)
-(*   Typeclasses.solve_instanciations_problem := *)
-(*     (fun env evd ->  *)
-(*       Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *)
-(*       resolve_all_typeclasses env evd) *)
-
-let solve_evars_by_tac env evd t =
-  let ev = make_evar empty_named_context_val mkProp in
-  let goal = {it = ev; sigma = (Evd.evars_of evd) } in
-  let (res, valid) = t goal in 
-  let evd' = evars_reset_evd res.sigma evd in
-    evd'
-(*       Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *)
-
-(* let _ = *)
-(*   Typeclasses.solve_instanciations_problem := *)
-(*     (fun env evd ->  *)
-(*       Eauto.resolve_all_evars false (true, 15) env  *)
-(* 	(fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *)
-(* 	  && class_of_constr evi.evar_concl <> None) evd) *)