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, 34 insertions, 28 deletions

diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index e8cce47adb..0c03c1e619 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -12,8 +12,8 @@ let idmap_is_empty m = m = Idmap.empty
 let mkRRef ref = RRef(dummy_loc,ref)
 let mkRVar id = RVar(dummy_loc,id)
 let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
 let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
@@ -26,7 +26,7 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 *)
 let raw_decompose_prod = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,t)::args) b 
   | rt -> args,rt
   in
@@ -34,7 +34,7 @@ let raw_decompose_prod =
 
 let raw_decompose_prod_or_letin = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,None,Some t)::args) b 
   | RLetIn(_,n,t,b) -> 
       raw_decompose_prod ((n,Some t,None)::args) b 
@@ -58,7 +58,7 @@ let raw_decompose_prod_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,t)::args) b 
 	| rt -> args,rt
   in
@@ -70,7 +70,7 @@ let raw_decompose_prod_or_letin_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,None,Some t)::args) b 
 	| RLetIn(_,n,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,Some t,None)::args) b 
@@ -135,15 +135,17 @@ let change_vars =
 	       change_vars mapping rt',
 	       List.map (change_vars mapping) rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
@@ -261,21 +263,21 @@ let rec alpha_rt excluded rt =
   let new_rt = 
     match rt with   
       | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
-      | RLambda(loc,Anonymous,t,b) -> 
+      | RLambda(loc,Anonymous,k,t,b) -> 
 	  let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in 
 	  let new_excluded = new_id :: excluded in 
 	  let new_t = alpha_rt new_excluded t in 
 	  let new_b = alpha_rt new_excluded b in 
-	  RLambda(loc,Name new_id,new_t,new_b)
-      | RProd(loc,Anonymous,t,b) -> 
+	  RLambda(loc,Name new_id,k,new_t,new_b)
+      | RProd(loc,Anonymous,k,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
-	RProd(loc,Anonymous,new_t,new_b)
+	RProd(loc,Anonymous,k,new_t,new_b)
     | RLetIn(loc,Anonymous,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
 	RLetIn(loc,Anonymous,new_t,new_b)
-    | RLambda(loc,Name id,t,b) -> 
+    | RLambda(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
 	  if new_id = id 
@@ -287,8 +289,8 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in 
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RLambda(loc,Name new_id,new_t,new_b)
-    | RProd(loc,Name id,t,b) -> 
+	RLambda(loc,Name new_id,k,new_t,new_b)
+    | RProd(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let new_excluded = new_id::excluded in 
 	let t,b = 
@@ -300,7 +302,7 @@ let rec alpha_rt excluded rt =
 	in
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RProd(loc,Name new_id,new_t,new_b)
+	RProd(loc,Name new_id,k,new_t,new_b)
     | RLetIn(loc,Name id,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
@@ -389,7 +391,7 @@ let is_free_in id =
     | REvar _ -> false
     | RPatVar _ -> false
     | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+    | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> id_ord id' id <> 0
@@ -460,17 +462,19 @@ let replace_var_by_term x_id term =
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RProd(loc,name,t,b) -> 
+      | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
@@ -590,8 +594,8 @@ let ids_of_rawterm c =
       | RVar (_,id) -> id::acc
       | RApp (loc,g,args) -> 
           ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
-      | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
       | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
       | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
@@ -622,15 +626,17 @@ let zeta_normalize =
 	       zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  zeta_normalize_term t,
 		  zeta_normalize_term b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
-		name, 		  
+		name, 		
+	        k,
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
@@ -691,8 +697,8 @@ let expand_as =
 	    with Not_found -> rt 
 	  end
       | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
-      | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
-      | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+      | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
+      | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
       | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
       | RLetTuple(loc,nal,(na,po),v,b) ->
 	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),