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, 22 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1117d25079..7e288f3117 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -216,7 +216,7 @@ let rec check_same_type ty1 ty2 =
   | _ when ty1=ty2 -> ()
   | _ -> failwith "not same type"
 
-and check_same_binder (nal1,e1) (nal2,e2) =
+and check_same_binder (nal1,_,e1) (nal2,_,e2) =
   List.iter2 (fun (_,na1) (_,na2) ->
     if na1<>na2 then failwith "not same name") nal1 nal2;
   check_same_type e1 e2
@@ -224,10 +224,10 @@ and check_same_binder (nal1,e1) (nal2,e2) =
 and check_same_fix_binder bl1 bl2 =
   List.iter2 (fun b1 b2 ->
     match b1,b2 with
-        LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
-          check_same_binder (nal1,ty1) (nal2,ty2)
+        LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) ->
+          check_same_binder (nal1,k,ty1) (nal2,k',ty2)
       | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
-          check_same_binder ([na1],def1) ([na2],def2)          
+          check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
       | _ -> failwith "not same binder") bl1 bl2
 
 let same c d = try check_same_type c d; true with _ -> false
@@ -255,10 +255,10 @@ let rec same_raw c d =
   | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
   | RApp(_,f1,a1), RApp(_,f2,a2) ->
       List.iter2 same_raw (f1::a1) (f2::a2)
-  | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) ->
+  | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
       if na1 <> na2 then failwith "RLambda";
       same_raw t1 t2; same_raw m1 m2
-  | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) ->
+  | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
       if na1 <> na2 then failwith "RProd";
       same_raw t1 t2; same_raw m1 m2
   | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
@@ -283,7 +283,7 @@ let rec same_raw c d =
   | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
       if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
       array_iter2
-        (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
+        (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
           if na1<>na2 then failwith "RRec";
           Option.iter2 same_raw bd1 bd2;
           same_raw ty1 ty2)) bl1 bl2;
@@ -582,7 +582,7 @@ let rec rename_rawconstr_var id0 id1 = function
 
 let rec share_fix_binders n rbl ty def =
   match ty,def with
-      RProd(_,na0,t0,b), RLambda(_,na1,t1,m) ->
+      RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
         if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
         else
           let (na,b,m) =
@@ -672,7 +672,7 @@ let rec extern inctx scopes vars r =
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
                (List.map (sub_extern true scopes vars) args))
 
-  | RProd (loc,Anonymous,t,c) ->
+  | RProd (loc,Anonymous,_,t,c) ->
       (* Anonymous product are never factorized *)
       CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
 
@@ -680,15 +680,15 @@ let rec extern inctx scopes vars r =
       CLetIn (loc,(loc,na),sub_extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
 
-  | RProd (loc,na,t,c) ->
+  | RProd (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
-      CProdN (loc,[(dummy_loc,na)::idl,t],c)
+      CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RLambda (loc,na,t,c) ->
+  | RLambda (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
-      CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
+      CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
   | RCases (loc,rtntypopt,tml,eqns) ->
       let vars' = 
@@ -775,7 +775,7 @@ and factorize_prod scopes vars aty c =
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
-  | RProd (loc,(Name id as na),ty,c)
+  | RProd (loc,(Name id as na),bk,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
 	-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
@@ -787,7 +787,7 @@ and factorize_lambda inctx scopes vars aty c =
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
-  | RLambda (loc,na,ty,c)
+  | RLambda (loc,na,bk,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
 	-> let (nal,c) =
@@ -797,24 +797,24 @@ and factorize_lambda inctx scopes vars aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[])
-  | (na,Some bd,ty)::l ->
+  | (na,bk,Some bd,ty)::l ->
       let (ids,l) =
         extern_local_binder scopes (name_fold Idset.add na vars) l in
       (na::ids,
        LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
       
-  | (na,None,ty)::l ->
+  | (na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Idset.add na vars) l with
-          (ids,LocalRawAssum(nal,ty')::l)
+          (ids,LocalRawAssum(nal,k,ty')::l)
             when same ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::ids,
-               LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+               LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
         | (ids,l) ->
             (na::ids,
-             LocalRawAssum([(dummy_loc,na)],ty) :: l))
+             LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
@@ -927,11 +927,11 @@ let rec raw_of_pat env = function
       RApp (loc,RPatVar (loc,(true,n)),
         List.map (raw_of_pat env) args)
   | PProd (na,t,c) ->
-      RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c)
+      RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
   | PLetIn (na,t,c) ->
       RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PLambda (na,t,c) ->
-      RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+      RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
   | PIf (c,b1,b2) ->
       RIf (loc, raw_of_pat env c, (Anonymous,None), 
            raw_of_pat env b1, raw_of_pat env b2)