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, 58 insertions, 47 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 858c6685fd..85bf11806e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -129,7 +129,7 @@ let pr_qualid = pr_qualid
 let pr_expl_args pr (a,expl) =
   match expl with
   | None -> pr (lapp,L) a
-  | Some (_,ExplByPos n) ->
+  | Some (_,ExplByPos (n,_id)) ->
       anomaly("Explicitation by position not implemented")
   | Some (_,ExplByName id) -> 
       str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
@@ -206,30 +206,41 @@ let pr_eqn pr (loc,pl,rhs) =
 
 let begin_of_binder = function
     LocalRawDef((loc,_),_) -> fst (unloc loc)
-  | LocalRawAssum((loc,_)::_,_) -> fst (unloc loc)
+  | LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc)
   | _ -> assert false
 
 let begin_of_binders = function
   | b::_ -> begin_of_binder b
   | _ -> 0
 
-let pr_binder many pr (nal,t) =
+let surround_binder k p = 
+  match k with
+      Default Explicit -> hov 1 (str"(" ++ p ++ str")")
+    | Default Implicit -> hov 1 (str"`" ++ p ++ str"`")
+    | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+
+let surround_implicit k p =
+  match k with
+      Default Explicit -> p
+    | Default Implicit -> (str"`" ++ p ++ str"`")
+    | TypeClass b -> (str"[" ++ p ++ str"]")
+
+let pr_binder many pr (nal,k,t) =
   match t with
   | CHole _ -> prlist_with_sep spc pr_lname nal
   | _ ->
     let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
-    hov 1 (if many then surround s else s)
+      hov 1 (if many then surround_binder k s else surround_implicit k s)
 
 let pr_binder_among_many pr_c = function
-  | LocalRawAssum (nal,t) ->
-      pr_binder true pr_c (nal,t)
+  | LocalRawAssum (nal,k,t) ->
+      pr_binder true pr_c (nal,k,t)
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, CastConv (_,t)) -> c, t
         | _ -> c, CHole dummy_loc in
-      hov 1 (surround
-        (pr_lname na ++ pr_opt_type pr_c topt ++
-         str":=" ++ cut() ++ pr_c c))
+      hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
+         str":=" ++ cut() ++ pr_c c)
 
 let pr_undelimited_binders pr_c =
   prlist_with_sep spc (pr_binder_among_many pr_c)
@@ -237,8 +248,8 @@ let pr_undelimited_binders pr_c =
 let pr_delimited_binders kw pr_c bl =
   let n = begin_of_binders bl in
   match bl with
-  | [LocalRawAssum (nal,t)] ->
-      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t)
+  | [LocalRawAssum (nal,k,t)] ->
+      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
   | LocalRawAssum _ :: _ as bdl ->
       pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
   | _ -> assert false
@@ -249,9 +260,9 @@ let rec extract_prod_binders = function
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CProdN (loc,[],c) ->
       extract_prod_binders c
-  | CProdN (loc,(nal,t)::bl,c) ->
+  | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
-      LocalRawAssum (nal,t) :: bl, c
+      LocalRawAssum (nal,bk,t) :: bl, c
   | c -> [], c
 
 let rec extract_lam_binders = function
@@ -260,15 +271,15 @@ let rec extract_lam_binders = function
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CLambdaN (loc,[],c) ->
       extract_lam_binders c
-  | CLambdaN (loc,(nal,t)::bl,c) ->
+  | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
-      LocalRawAssum (nal,t) :: bl, c
+      LocalRawAssum (nal,bk,t) :: bl, c
   | c -> [], c
     
 let split_lambda = function
-  | CLambdaN (loc,[[na],t],c) -> (na,t,c)
-  | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
-  | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
+  | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
+  | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+  | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
 let rename na na' t c =
@@ -279,13 +290,13 @@ let rename na na' t c =
   
 let split_product na' = function
   | CArrow (loc,t,c) -> (na',t,c)
-  | CProdN (loc,[[na],t],c) -> rename na na' t c
-  | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
-  | CProdN (loc,(na::nal,t)::bl,c) ->
-      rename na na' t (CProdN(loc,(nal,t)::bl,c))
+  | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
+  | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,bk,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let merge_binders (na1,ty1) cofun (na2,ty2) codom =
+let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
   let na =
     match snd na1, snd na2 with
         Anonymous, Name id ->
@@ -306,42 +317,42 @@ let merge_binders (na1,ty1) cofun (na2,ty2) codom =
       | _ ->
           Constrextern.check_same_type ty1 ty2;
           ty2 in
-  (LocalRawAssum ([na],ty), codom)
+  (LocalRawAssum ([na],bk1,ty), codom)
             
 let rec strip_domain bvar cofun c =
   match c with
     | CArrow(loc,a,b) ->
-        merge_binders bvar cofun ((dummy_loc,Anonymous),a) b
-    | CProdN(loc,[([na],ty)],c') ->
-        merge_binders bvar cofun (na,ty) c'
-    | CProdN(loc,([na],ty)::bl,c') ->
-        merge_binders bvar cofun (na,ty) (CProdN(loc,bl,c'))
-    | CProdN(loc,(na::nal,ty)::bl,c') ->
-        merge_binders bvar cofun (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
+        merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b
+    | CProdN(loc,[([na],bk,ty)],c') ->
+        merge_binders bvar cofun (na,bk,ty) c'
+    | CProdN(loc,([na],bk,ty)::bl,c') ->
+        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c'))
+    | CProdN(loc,(na::nal,bk,ty)::bl,c') ->
+        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c'))
     | _ -> failwith "not a product"
 
 (* Note: binder sharing is lost *)
-let rec strip_domains (nal,ty) cofun c =
+let rec strip_domains (nal,bk,ty) cofun c =
   match nal with
       [] -> assert false
     | [na] ->
-        let bnd, c' = strip_domain (na,ty) cofun c in
+        let bnd, c' = strip_domain (na,bk,ty) cofun c in
         ([bnd],None,c')
     | na::nal ->
-        let f = CLambdaN(dummy_loc,[(nal,ty)],cofun) in
-        let bnd, c1 = strip_domain (na,ty) f c in
+        let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in
+        let bnd, c1 = strip_domain (na,bk,ty) f c in
         (try
-          let bl, rest, c2 = strip_domains (nal,ty) cofun c1 in
+          let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in
           (bnd::bl, rest, c2)
-        with Failure _ -> ([bnd],Some (nal,ty), c1))
+        with Failure _ -> ([bnd],Some (nal,bk,ty), c1))
 
 (* Re-share binders *)
 let rec factorize_binders = function
   | ([] | [_] as l) -> l
-  | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') ->
+  | LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') ->
       (try
 	let _ = Constrextern.check_same_type ty ty' in
-	factorize_binders (LocalRawAssum (nal@nal',ty)::l)
+	factorize_binders (LocalRawAssum (nal@nal',k,ty)::l)
       with _ ->
 	d :: factorize_binders l')
   | d :: l -> d :: factorize_binders l
@@ -370,7 +381,7 @@ let rec split_fix n typ def =
     let (na,_,def) = split_lambda def in
     let (na,t,typ) = split_product na typ in
     let (bl,typ,def) = split_fix (n-1) typ def in
-    (LocalRawAssum ([na],t)::bl,typ,def)
+    (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
 
 let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   let pr_body =
@@ -601,27 +612,27 @@ let rec strip_context n iscast t =
   if n = 0 then
     [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
   else match t with
-    | CLambdaN (loc,(nal,t)::bll,c) ->
+    | CLambdaN (loc,(nal,bk,t)::bll,c) ->
 	let n' = List.length nal in
 	if n' > n then
 	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+	  [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c)
 	else
 	let bl', c = strip_context (n-n') iscast
 	  (if bll=[] then c else CLambdaN (loc,bll,c)) in
-	LocalRawAssum (nal,t) :: bl', c 
-    | CProdN (loc,(nal,t)::bll,c) ->
+	LocalRawAssum (nal,bk,t) :: bl', c 
+    | CProdN (loc,(nal,bk,t)::bll,c) ->
 	let n' = List.length nal in
 	if n' > n then
 	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,t)], CProdN (loc,(nal2,t)::bll,c)
+	  [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c)
 	else
 	let bl', c = strip_context (n-n') iscast
 	  (if bll=[] then c else CProdN (loc,bll,c)) in
-	LocalRawAssum (nal,t) :: bl', c 
+	LocalRawAssum (nal,bk,t) :: bl', c 
     | CArrow (loc,t,c) ->
 	let bl', c = strip_context (n-1) iscast c in
-	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
+	LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c
     | CCast (_,c,_) -> strip_context n false c
     | CLetIn (_,na,b,c) -> 
 	let bl', c = strip_context (n-1) iscast c in