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, 18 insertions, 16 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 612be05e3..97f7c1d97 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -139,8 +139,8 @@ type newfixpoint_expr =
 let rec abstract_rawconstr c = function
   | [] -> c
   | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
-  | Topconstr.LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
+  | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
         (abstract_rawconstr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
@@ -213,7 +213,7 @@ let rec is_rec names =
     | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b)  -> 
+    | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
 	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
     | RLetTuple(_,nal,_,t,b) -> lookup names t || 
 	lookup 
@@ -434,7 +434,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
       | None -> 
 	  begin
 	    match args with 
-	      | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x 
+	      | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x 
 	      | _ -> error "Recursive argument must be specified" 
 	  end
       | Some wf_args -> 
@@ -442,7 +442,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 	    match 
 	      List.find 
 		(function 
-		   | Topconstr.LocalRawAssum(l,t) -> 
+		   | Topconstr.LocalRawAssum(l,k,t) -> 
 		       List.exists 
 			 (function (_,Name id) -> id =  wf_args | _ -> false) 
 			 l 
@@ -450,7 +450,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 		)
 		args 
 	    with 
-	      | Topconstr.LocalRawAssum(_,t)  ->	    t,wf_args
+	      | Topconstr.LocalRawAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false 
 	  with Not_found -> assert false 
   in
@@ -462,7 +462,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
   let fun_from_mes = 
     let applied_mes = 
       Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg])    in
-    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) 
+    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) 
   in
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -570,11 +570,11 @@ let rec add_args id new_args b =
       CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) -> 
       CProdN(loc,
-	     List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, 
+	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, 
 	     add_args id new_args  b1)
   | CLambdaN(loc,nal,b1) -> 
       CLambdaN(loc,
-	       List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, 
+	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal, 
 	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) -> 
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
@@ -644,13 +644,15 @@ let rec chop_n_arrow n t =
 	      let new_n =
 		let rec aux (n:int) = function 
 		    [] -> n
-		| (nal,t'')::nal_ta' -> 
+		| (nal,k,t'')::nal_ta' -> 
 		    let nal_l = List.length nal in 
 		    if n >= nal_l
 		    then 
 		      aux (n - nal_l) nal_ta'
 		    else 
-		      let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t')
+		      let new_t' = 
+			Topconstr.CProdN(dummy_loc,
+					((snd (list_chop n nal)),k,t'')::nal_ta',t')
 		      in 
 		      raise (Stop new_t')
 		in
@@ -668,12 +670,12 @@ let rec get_args b t : Topconstr.local_binder list *
     | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
 	begin
 	  let n = 
-	    (List.fold_left (fun n (nal,_) -> 
+	    (List.fold_left (fun n (nal,_,_) -> 
 			       n+List.length nal) 0 nal_ta )
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-	  (List.map (fun (nal,ta) -> 
-		       (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
+	  (List.map (fun (nal,k,ta) -> 
+		       (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' 
 	end
     | _ -> [],b,t
 
@@ -716,7 +718,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function 
 				 | Topconstr.LocalRawDef (na,_)-> []
-				 | Topconstr.LocalRawAssum (nal,_) -> nal
+				 | Topconstr.LocalRawAssum (nal,_,_) -> nal
 			      )
 			      bl
 			   )
@@ -730,7 +732,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
-			      	 | Topconstr.LocalRawAssum (nal,_) -> 
+			      	 | Topconstr.LocalRawAssum (nal,_,_) -> 
 				     List.map 
 				       (fun (loc,n) -> 
 					  CRef(Libnames.Ident(loc, Nameops.out_name n)))