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, 40 insertions, 21 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 05ee50daf5..445555251e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -46,21 +46,21 @@ open Goptions
 open Mod_subst
 open Evd
 
-let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
+let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
+let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
 
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+  | LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl
         (abstract_constr_expr c bl)
 
 let rec generalize_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+  | LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl
         (generalize_constr_expr c bl)
 
 let rec under_binders env f n c =
@@ -103,10 +103,13 @@ let definition_message id =
 let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
   let sigma = Evd.empty in
   let env = Global.env() in
-  match comtypopt with
+    match comtypopt with
       None -> 
 	let b = abstract_constr_expr com bl in
-	let j = interp_constr_judgment sigma env b in
+	let ib = intern_constr sigma env b in
+	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+  	let j = Default.understand_judgment sigma env ib in
+	  imps,
 	{ const_entry_body = j.uj_val;
 	  const_entry_type = None;
           const_entry_opaque = opacity;
@@ -115,7 +118,10 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
 	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
-	let (body,typ) = destSubCast (interp_constr sigma env b) in
+	let ib = intern_gen false sigma env b in
+	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+	let (body,typ) = destSubCast (Default.understand_gen (OfType None) sigma env ib) in
+	  imps,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity;
@@ -130,15 +136,18 @@ let red_constant_entry bl ce = function
 	  (local_binders_length bl)
 	  body }
 
-let declare_global_definition ident ce local =
+let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
-  if local = Local && Flags.is_verbose() then
-    msg_warning (pr_id ident ++ str" is declared as a global definition");
-  definition_message ident;
-  ConstRef kn
+  let gr = ConstRef kn in
+    if Impargs.is_implicit_args () || imps <> [] then
+      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    if local = Local && Flags.is_verbose() then
+      msg_warning (pr_id ident ++ str" is declared as a global definition");
+    definition_message ident;
+    gr
 
 let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
-  let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
+  let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
   let ce' = red_constant_entry bl ce red_option in
   let r = match local with
     | Local when Lib.sections_are_opened () ->
@@ -152,7 +161,7 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
              str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
-        declare_global_definition ident ce' local in
+        declare_global_definition ident ce' local imps in
   hook local r
 
 let syntax_definition ident c local onlyparse =
@@ -550,8 +559,8 @@ let eq_constr_expr c1 c2 =
 
 (* Very syntactical equality *)
 let eq_local_binder d1 d2 = match d1,d2 with
-  | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) ->
-      List.length nal1 = List.length nal2 &&
+  | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
+      List.length nal1 = List.length nal2 && k1 = k2 &&
       List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
       eq_constr_expr c1 c2
   | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
@@ -742,7 +751,7 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix boxed kind f def t =
+let declare_fix boxed kind f def t imps =
   let ce = {
     const_entry_body = def;
     const_entry_type = Some t;
@@ -750,7 +759,11 @@ let declare_fix boxed kind f def t =
     const_entry_boxed = boxed
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
-  ConstRef kn
+  let gr = ConstRef kn in
+    if Impargs.is_implicit_args () || imps <> [] then
+      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    gr
+
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -766,6 +779,7 @@ let compute_possible_guardness_evidences (n,_) fixl fixtype =
 	 but doing it properly involves delta-reduction, and it finally 
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
+      (* FIXME, local_binders_length does not give the size of the final product if typeclasses are used *)
       let m = local_binders_length fixl.fix_binders in
       let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
       list_map_i (fun i _ -> i) 0 ctx
@@ -778,6 +792,11 @@ let interp_recursive fixkind l boxed =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let fiximps = 
+    List.map 
+      (fun x -> Implicit_quantifiers.implicits_of_binders x.fix_binders) 
+      fixl 
+  in
   let fixctxs = List.map (interp_fix_context evdref env) fixl in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
@@ -816,7 +835,7 @@ let interp_recursive fixkind l boxed =
   in
 
   (* Declare the recursive definitions *)
-  ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes);
+  ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps);
   if_verbose ppnl (recursive_message kind indexes fixnames);
 
   (* Declare notations *)