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, 215 insertions, 0 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
new file mode 100644
index 0000000000..d9113644cb
--- /dev/null
+++ b/interp/implicit_quantifiers.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  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 Rawterm
+open Topconstr
+open Libnames
+open Typeclasses
+open Typeclasses_errors
+(*i*)
+
+(* Auxilliary functions for the inference of implicitly quantified variables. *)    
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
+  let found id bdvars l = if Idset.mem id bdvars then l else if List.mem id l then l else id :: l in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident (_,id)) -> found id bdvars l
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+  in aux bound l c
+
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition dummy_loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> raise Not_found
+
+let is_global id =
+  try 
+    let _ = locate_reference (make_short_qualid id) in true
+  with Not_found -> 
+    false
+
+let is_freevar ids env x =
+  try
+    if Idset.mem x ids then false
+    else
+      try ignore(Environ.lookup_named x env) ; false
+      with _ -> not (is_global x)
+  with _ -> true
+
+let freevars_of_ids env ids = 
+  List.filter (is_freevar env (Global.env())) ids
+
+let compute_constrs_freevars env constrs =
+  let ids = 
+    List.rev (List.fold_left 
+		 (fun acc x -> free_vars_of_constr_expr x acc) 
+		 [] constrs)
+  in freevars_of_ids env ids
+
+(* let compute_context_freevars env ctx = *)
+(*   let ids = *)
+(*     List.rev *)
+(*       (List.fold_left *)
+(* 	  (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *)
+(* 	  [] constrs) *)
+(*   in freevars_of_ids ids *)
+
+let compute_constrs_freevars_binders env constrs =
+  let elts = compute_constrs_freevars env constrs in
+    List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+      
+let ids_of_named_context_avoiding avoid l =
+  List.fold_left (fun (ids, avoid) id -> 
+    let id' = Nameops.next_ident_away_from id avoid in id' :: ids, id' :: avoid) 
+    ([], avoid) (Termops.ids_of_named_context l)
+    
+let combine_params avoid applied needed =
+  let rec aux ids app need =
+    match app, need with
+	[], need -> 
+	  let need', avoid = ids_of_named_context_avoiding avoid need in
+	    List.rev ids @ (List.map mkIdentC need'), avoid
+      | x :: app, _ :: need -> aux (x :: ids) app need    
+      | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
+  in aux [] applied needed
+
+let compute_context_vars env l =
+  List.fold_left (fun l (iid, _, c) -> 
+    (match snd iid with Name i -> [i] | Anonymous -> []) @ free_vars_of_constr_expr c ~bound:env l)
+    [] l
+
+let destClassApp cl =
+  match cl with
+    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+    | _ -> raise Not_found
+
+let full_class_binders env l = 
+  let avoid = compute_context_vars env l in
+  let l', avoid =
+    List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
+      match bk with
+	  Explicit -> 
+	    let (id, l) = destClassApp cl in
+	      (try
+		  let c = class_info (snd id) in
+		  let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in
+		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
+		with Not_found -> unbound_class (Global.env ()) id)
+	| Implicit -> (x :: l', avoid))
+      ([], avoid) l
+  in List.rev l'
+      
+let constr_expr_of_constraint (kind, id) l =
+  match kind with
+    | Explicit -> CAppExpl (fst id, (None, Ident id), l)
+    | Implicit -> CApp (fst id, (None, CRef (Ident id)),
+		       List.map (fun x -> x, None) l)
+
+(*    | CApp of loc * (proj_flag * constr_expr) *  *)
+(*         (constr_expr * explicitation located option) list *)
+
+
+let constrs_of_context l =
+  List.map (fun (_, id, l) -> constr_expr_of_constraint id l) l
+
+let compute_context_freevars env ctx =
+  let bound, ids = 
+    List.fold_left 
+      (fun (bound, acc) (oid, id, x) -> 
+	let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in
+	  bound, free_vars_of_constr_expr x ~bound acc)
+      (env,[]) ctx
+  in freevars_of_ids env (List.rev ids)
+
+let resolve_class_binders env l = 
+  let ctx = full_class_binders env l in
+  let fv_ctx = 
+    let elts = compute_context_freevars env ctx in
+      List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+  in
+    fv_ctx, ctx
+
+let generalize_class_binders env l = 
+  let fv_ctx, cstrs = resolve_class_binders env l in
+    List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx,
+  List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c)) 
+    cstrs
+
+let generalize_class_binders_raw env l = 
+  let fv_ctx, cstrs = resolve_class_binders env l in
+    List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
+  List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
+
+let ctx_of_class_binders env l = 
+  let (x, y) = generalize_class_binders env l in x @ y
+	
+let implicits_of_binders l = 
+  let rec aux i l = 
+    match l with 
+	[] -> []
+      | hd :: tl -> 
+	  let res, reslen = 
+	    match hd with
+		LocalRawAssum (nal, Default Implicit, t) -> 
+		  list_map_i (fun i (_,id) ->
+		    let name =
+		      match id with
+			  Name id -> Some id
+			| Anonymous -> None
+		    in ExplByPos (i, name), (true, true))
+		    i nal, List.length nal
+	      | LocalRawAssum (nal, _, _) -> [], List.length nal
+	      | LocalRawDef _ -> [], 1
+	  in res @ (aux (i + reslen) tl)
+  in aux 1 l
+  
+let implicits_of_rawterm l = 
+  let rec aux i c = 
+    match c with
+	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
+	  let rest = aux (succ i) b in
+	    if bk = Implicit then
+	      let name =
+		match na with
+		    Name id -> Some id
+		  | Anonymous -> None
+	      in
+		(ExplByPos (i, name), (true, true)) :: rest
+	    else rest
+      | RLetIn (loc, na, t, b) -> aux i b
+      | _ -> []
+  in aux 1 l
+
+let nf_named_context sigma ctx = 
+  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+
+let nf_rel_context sigma ctx = 
+  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+    
+let nf_env sigma env = 
+  let nc' = nf_named_context sigma (Environ.named_context env) in
+  let rel' = nf_rel_context sigma (Environ.rel_context env) in
+    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)