Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses

........
  r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Comment grammar error
........
  r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
  
  The initial Type Classes patch.
  This patch introduces type classes and instance definitions a la Haskell.
  Technically, it uses the implicit arguments mechanism which was extended a bit. 
  The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
  It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). 
........
  r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix interface
........
  r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix more xlate code
........
  r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
  r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Bug fixes in Instance decls.
........
  r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
  
  Streamline typeclass context implementation, prepare for class binders in proof statements.
........
  r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
  
  Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
  r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
  
  Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
  r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
  
  Stupid bug
........
  r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
  r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
  r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
  
  Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
  New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
  Other bugs related to naming in typeclasses fixed. 
........
  r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
  
  Progress on setoids using type classes, recognize setoid equalities in hyps better.
  Streamline implementation to return more information when resolving setoids (return the results setoid).
........
  r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
  
  Syntax change, more like Coq
........
  r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
  
  Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
  r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
  
  Work on type classes based rewrite tactic.
........
  r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
  
  Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
  r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
  
  Forgot to add a file
........
  r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
  
  Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and 
  implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
  r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
  
  Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. 
  Add useful tactics to Program.Subsets.
........


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

1 files changed, 311 insertions, 0 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
new file mode 100644
index 0000000000..b0e7cb1470
--- /dev/null
+++ b/pretyping/typeclasses.ml
@@ -0,0 +1,311 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Typeclasses_errors
+(*i*)
+
+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 rels = constr list
+
+(* This module defines type-classes *)
+type typeclass = {
+  cl_name : identifier; (* Name of the class *)
+  cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *)
+  cl_super : named_context; (* Superclasses applied to some of the params *)
+  cl_params : named_context; (* Context of the parameters (usually types) *)
+(*   cl_defs : named_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
+  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
+  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+}
+
+type typeclasses = (identifier, typeclass) Gmap.t
+
+type instance = {
+  is_class: typeclass;
+  is_name: identifier; (* Name of the instance *)
+(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
+(*   is_super: named_context; (\* The corresponding superclasses *\) *)
+(*   is_defs: named_context; (\* Context of the definitions, instanciated *\) *)
+  is_impl: constant; 
+(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
+}
+
+type instances = (identifier, instance list) Gmap.t
+    
+let classes : typeclasses ref = ref Gmap.empty
+
+let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty
+  
+let instances : instances ref = ref Gmap.empty
+  
+let freeze () = !classes, !methods, !instances
+
+let unfreeze (cl,m,is) = 
+  classes:=cl;
+  methods:=m;
+  instances:=is
+    
+let init () =
+  classes:= Gmap.empty; 
+  methods:= Gmap.empty;
+  instances:= Gmap.empty
+    
+let _ = 
+  Summary.declare_summary "classes_and_instances"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = true;
+      Summary.survive_section = true }
+
+let gmap_merge old ne =
+  Gmap.fold (fun k v acc -> Gmap.add k v acc) ne old
+
+let gmap_list_merge old ne =
+  let ne = 
+    Gmap.fold (fun k v acc -> 
+      let oldv = try Gmap.find k old with Not_found -> [] in
+      let v' = 
+	List.fold_left (fun acc x -> 
+	  if not (List.exists (fun y -> y.is_name = x.is_name) v) then x :: acc else acc)
+	v oldv
+      in Gmap.add k v' acc)
+      ne Gmap.empty
+  in
+    Gmap.fold (fun k v acc -> 
+      let newv = try Gmap.find k ne with Not_found -> [] in
+      let v' = 
+	List.fold_left (fun acc x -> 
+	  if not (List.exists (fun y -> y.is_name = x.is_name) acc) then x :: acc else acc)
+	  newv v
+      in Gmap.add k v' acc)
+      old ne
+
+let cache (_, (cl, m, inst)) =
+  classes := gmap_merge !classes cl;
+  methods := gmap_merge !methods m;
+  instances := gmap_list_merge !instances inst
+
+open Libobject
+
+let subst (_,subst,(cl,m,inst)) = 
+  let do_subst_con c = fst (Mod_subst.subst_con subst c)
+  and do_subst c = Mod_subst.subst_mps subst c
+  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+  in
+  let do_subst_named ctx = 
+    List.map (fun (na, b, t) ->
+      (na, Option.smartmap do_subst b, do_subst t))
+      ctx
+  in
+  let subst_class cl = 
+    let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl;
+		cl_context = do_subst_named cl.cl_context;
+		cl_super = do_subst_named cl.cl_super;
+		cl_params = do_subst_named cl.cl_params;
+		cl_props = do_subst_named cl.cl_props; }
+    in if cl' = cl then cl else cl'
+  in
+  let subst_inst classes insts =
+    List.map (fun is -> 
+      { is with is_class = Gmap.find is.is_class.cl_name classes; 
+	is_impl = do_subst_con is.is_impl }) insts
+  in
+  let classes = Gmap.map subst_class cl in
+  let instances = Gmap.map (subst_inst classes) inst in
+    (classes, m, instances)
+
+let discharge (_,(cl,m,inst)) =
+  let subst_class cl = 
+    { cl with cl_impl = Lib.discharge_inductive cl.cl_impl }
+  in
+  let subst_inst classes insts =
+    List.map (fun is -> { is with is_impl = Lib.discharge_con is.is_impl;
+      is_class = Gmap.find is.is_class.cl_name classes; }) insts
+  in
+  let classes = Gmap.map subst_class cl in
+  let instances = Gmap.map (subst_inst classes) inst in
+    Some (classes, m, instances)
+  
+let (input,output) = 
+  declare_object
+    { (default_object "type classes state") with
+      cache_function = cache;
+      load_function = (fun _ -> cache);
+      open_function = (fun _ -> cache);
+      classify_function = (fun (_,x) -> Substitute x);
+      discharge_function = discharge;
+      subst_function = subst;
+      export_function = (fun x -> Some x) }
+
+let update () = 
+  Lib.add_anonymous_leaf (input (!classes, !methods, !instances))
+
+let class_methods cl =
+  List.map (function (x, _, _) -> x) cl.cl_props
+
+let add_class c = 
+  classes := Gmap.add c.cl_name c !classes;
+  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c);
+  update ()
+    
+let class_info c = 
+  Gmap.find c !classes
+
+let class_of_inductive ind = 
+  let res = Gmap.fold 
+    (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc)
+    !classes None
+  in match res with
+      None -> raise Not_found
+    | Some cl -> cl
+
+let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
+
+let gmapl_add x y m =
+  try
+    let l = Gmap.find x m in
+    Gmap.add x (y::Util.list_except y l) m
+  with Not_found ->
+    Gmap.add x [y] m
+
+let instances_of c = 
+  try Gmap.find c.cl_name !instances with Not_found -> []
+
+let add_instance i =
+  instances := gmapl_add i.is_class.cl_name i !instances;
+  update ()
+
+open Libnames
+      
+let id_of_reference r = 
+  let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id
+
+let instances r = 
+  let id = id_of_reference r in
+    try let cl = class_info id in instances_of cl
+    with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
+
+let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+
+let resolve_typeclass env ev evi (evd, defined as acc) =
+  if evi.evar_body = Evar_empty then
+    try
+      !solve_instanciation_problem env evd ev evi
+    with Exit -> acc
+  else acc
+
+let resolve_one_typeclass env types =
+  try
+    let evi = Evd.make_evar (Environ.named_context_val env) types in
+    let ev = 1 in
+    let evm = Evd.add Evd.empty ev evi in
+    let evd = Evd.create_evar_defs evm in
+    let evd', b = !solve_instanciation_problem env evd ev evi in
+      if b then 
+	let evm' = Evd.evars_of evd' in
+	  match Evd.evar_body (Evd.find evm' ev) with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c -> c
+      else raise Not_found
+  with Exit -> raise Not_found
+
+let resolve_one_typeclass_evd env evd types =
+  try
+    let ev = Evarutil.e_new_evar evd env types in
+    let (ev,_) = destEvar ev in
+    let evd', b =
+	!solve_instanciation_problem env !evd ev (Evd.find (Evd.evars_of !evd) ev)
+    in
+      evd := evd';
+      if b then 
+	let evm' = Evd.evars_of evd' in
+	  match Evd.evar_body (Evd.find evm' ev) with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c -> c
+      else raise Not_found
+  with Exit -> raise Not_found
+
+let method_typeclass ref = 
+  match ref with 
+    | ConstRef c -> 
+	let (_, _, l) = Names.repr_con c in
+	  class_info (Gmap.find (Names.id_of_label l) !methods)
+    | _ -> raise Not_found
+      
+let is_class ind = 
+  Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false
+  
+let is_implicit_arg k = 
+  match k with
+      ImplicitArg (ref, (n, id)) -> true
+    | InternalHole -> true
+    | _ -> false
+
+let resolve_typeclasses ?(check=true) env sigma evd =
+  let evm = Evd.evars_of evd in
+  let tc_evars = 
+    let f ev evi acc =
+      let (l, k) = Evd.evar_source ev evd in
+	if not check || is_implicit_arg k then
+	  match kind_of_term evi.evar_concl with
+	    | App(ki, args) when isInd ki -> 
+		if is_class (destInd ki) then Evd.add acc ev evi
+		else acc
+	    | _ -> acc
+	else acc
+    in Evd.fold f evm Evd.empty
+  in
+  let rec sat evars =
+    let (evars', progress) = 
+      Evd.fold 
+	(fun ev evi acc -> 
+	  if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) 
+	(Evd.evars_of evars) (evars, false) 
+    in
+      if not progress then evars'
+      else
+	sat (Evarutil.nf_evar_defs evars')
+  in sat evd
+
+let class_of_constr c = 
+  match kind_of_term c with
+      App (c, _) -> 
+	(match kind_of_term c with
+	    Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
+	  | _ -> None)
+    | _ -> None
+
+
+type substitution = (identifier * constr) list
+
+let substitution_of_named_context isevars env id n subst l = 
+  List.fold_right
+    (fun (na, _, t) subst -> 
+      let t' = replace_vars subst t in
+      let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' in
+	(na, b) :: subst)
+    l subst
+
+let nf_substitution sigma subst = 
+  List.map (function (na, c) -> na, Reductionops.nf_evar sigma c) subst