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

3 files changed, 105 insertions, 44 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index c33738644..8ea183509 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -38,6 +38,7 @@ type definition_object_kind =
   | Scheme
   | StructureComponent
   | IdentityCoercion
+  | Instance
 
 type strength = locality_flag (* For compatibility *)
 
@@ -97,5 +98,5 @@ let string_of_definition_kind (l,boxed,d) =
   | Global, Example -> "Example"
   | Local, (CanonicalStructure|Example) ->
       anomaly "Unsupported local definition kind"
-  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion)
+  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Instance)
       -> anomaly "Internal definition kind"
diff --git a/library/impargs.ml b/library/impargs.ml
index 479936c88..4272f413a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -117,7 +117,7 @@ type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
-  | Manual
+  | Manual of bool
 
 let argument_less = function
   | Hyp n, Hyp n' -> n<n'
@@ -137,7 +137,7 @@ let update pos rig (na,st) =
       | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
-      | Some Manual -> assert false
+      | Some (Manual _) -> assert false
   else
     match st with
       | None -> DepFlex pos
@@ -147,7 +147,7 @@ let update pos rig (na,st) =
           if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
       | Some (DepFlex fpos as x) ->
           if argument_less (pos,fpos) then DepFlex pos else x
-      | Some Manual -> assert false
+      | Some (Manual _) -> assert false
   in na, Some e
 
 (* modified is_rigid_reference with a truncated env *)
@@ -197,12 +197,20 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let compute_implicits_gen strict strongly_strict revpat contextual env t =
+let concrete_name avoid_flags l env_names n all c =
+  if n = Anonymous & noccurn 1 c then
+    (Anonymous,l)
+  else
+    let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
+    let idopt = if not all && noccurn 1 c then Anonymous else Name fresh_id in
+    (idopt, fresh_id::l)
+
+let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = Termops.concrete_name None avoid names na b in
+	  let na',avoid' = concrete_name None avoid names na all b in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ -> 
@@ -214,7 +222,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual env t =
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
     | Prod (na,a,b) ->
-	let na',avoid = Termops.concrete_name None [] [] na b in
+	let na',avoid = concrete_name None [] [] na all b in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	Array.to_list v
     | _ -> []
@@ -227,54 +235,79 @@ let rec prepare_implicits f = function
       Some (id,imp,set_maximality imps' f.maximal) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
+let compute_implicits_flags env f all t = 
+  compute_implicits_gen 
+    f.strict f.strongly_strict f.reversible_pattern f.contextual all env t
+    
 let compute_implicits_auto env f t =
-  let l =
-    compute_implicits_gen 
-      f.strict f.strongly_strict f.reversible_pattern f.contextual env t in
-  prepare_implicits f l
+  let l = compute_implicits_flags env f false t in
+    prepare_implicits f l
 
 let compute_implicits env t = compute_implicits_auto env !implicit_args t
 
 let set_implicit id imp insmax =
-  (id,(match imp with None -> Manual | Some imp -> imp),insmax)
+  (id,(match imp with None -> Manual false | Some imp -> imp),insmax)
+
+let merge_imps f = function 
+    None -> Some (Manual f)
+  | x -> x
 
-let compute_manual_implicits flags ref l =
+let rec assoc_by_pos k = function
+    (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl
+  | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
+  | [] -> raise Not_found
+
+let compute_manual_implicits flags ref enriching l =
   let t = Global.type_of_global ref in
+  let env = Global.env () in
   let autoimps =
-    compute_implicits_gen false false false true (Global.env()) t in
+    if enriching then compute_implicits_flags env flags true t
+    else compute_implicits_gen false false false true true env t in
   let n = List.length autoimps in
+  let try_forced k l =
+    try 
+      let (id, (b, f)), l' = assoc_by_pos k l in
+	if f then
+	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
+	    l', Some (id,Manual f,b)
+	else l, None
+    with Not_found -> l, None
+  in
   if not (list_distinct l) then 
     error ("Some parameters are referred more than once");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
   | (Name id,imp)::imps ->
-      let l',m =
+      let l',imp,m =
 	try 
-	  let b = List.assoc (ExplByName id) l in
-	  List.remove_assoc (ExplByName id) l, Some b
+	  let (b, f) = List.assoc (ExplByName id) l in
+	  List.remove_assoc (ExplByName id) l, merge_imps f imp,Some b
 	with Not_found ->
 	try 
-	  let b = List.assoc (ExplByPos k) l in
-	  List.remove_assoc (ExplByPos k) l, Some b
+	  let (id, (b, f)), l' = assoc_by_pos k l in
+	    l', merge_imps f imp,Some b
 	with Not_found ->
-	l, None in
+	  l,imp, if enriching && imp <> None then Some flags.maximal else None
+      in
       let imps' = merge (k+1) l' imps in
       let m = Option.map (set_maximality imps') m in
       Option.map (set_implicit id imp) m :: imps'
-  | (Anonymous,_imp)::imps -> 
-      None :: merge (k+1) l imps
+  | (Anonymous,imp)::imps ->
+      let l', forced = try_forced k l in
+	forced :: merge (k+1) l' imps
   | [] when l = [] -> []
-  | _ ->
+  | [] ->
       match List.hd l with
-      | ExplByName id,_ ->
-	  error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
-      | ExplByPos i,_ ->
-	  if i<1 or i>n then 
-	    error ("Bad implicit argument number: "^(string_of_int i))
-	  else
-	    errorlabstrm ""
-	      (str "Cannot set implicit argument number " ++ int i ++
-	      str ": it has no name") in
+	| ExplByName id,b ->
+	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+	| ExplByPos (i,_id),_t ->
+	    if i<1 or i>n then 
+	      error ("Bad implicit argument number: "^(string_of_int i))
+	    else
+	      errorlabstrm ""
+		(str "Cannot set implicit argument number " ++ int i ++
+		    str ": it has no name")
+  in
   merge 1 l autoimps
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
@@ -297,7 +330,11 @@ let maximal_insertion_of = function
   | Some (_,_,b) -> b
   | None -> anomaly "Not an implicit argument"
 
-(* [in_ctx] means we now the expected type, [n] is the index of the argument *)
+let forced_implicit = function
+  | Some (_,Manual b,_) -> b
+  | _ -> false
+
+(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
   | None -> false
   | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
@@ -306,7 +343,7 @@ let is_inferable_implicit in_ctx n = function
   | Some (_,DepRigid Conclusion,_) -> in_ctx
   | Some (_,DepFlex Conclusion,_) -> false
   | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual,_) -> true
+  | Some (_,Manual _,_) -> true
 
 let positions_of_implicits =
   let rec aux n = function
@@ -368,11 +405,24 @@ let compute_global_implicits flags = function
   | ConstructRef ((kn,i),j) -> 
       let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
 
+(* Merge a manual explicitation with an implicit_status list *)
+
+let list_split_at index l = 
+  let rec aux i acc = function
+      tl when i = index -> (List.rev acc), tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "list_split_at: Invalid argument"
+  in aux 0 [] l
+    
+let merge_impls oimpls impls =
+  let oimpls, _ = list_split_at (List.length oimpls - List.length impls) oimpls in
+    oimpls @ impls
+
 (* Caching implicits *)
 
 type implicit_interactive_request =
   | ImplAuto
-  | ImplManual of (explicitation * bool) list
+  | ImplManual of implicit_status list
 
 type implicit_discharge_request =
   | ImplNoDischarge
@@ -420,9 +470,10 @@ let rebuild_implicits (req,l) =
   | ImplInteractive (ref,flags,o) ->
       match o with
       | ImplAuto -> [ref,compute_global_implicits flags ref]
-      | ImplManual l ->
-	  error "Discharge of global manually given implicit arguments not implemented" in
-  (req,l')
+      | ImplManual l -> 
+	  let auto = compute_global_implicits flags ref in
+	  let l' = merge_impls auto l in [ref,l']
+  in (req,l')
 
 
 let (inImplicits, _) =
@@ -464,15 +515,16 @@ let declare_mib_implicits kn =
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
 
 (* Declare manual implicits *)
+type manual_explicitation = Topconstr.explicitation * (bool * bool) 
 
-let declare_manual_implicits local ref l =
+let declare_manual_implicits local ref enriching l =
   let flags = !implicit_args in
-  let l' = compute_manual_implicits flags ref l in
+  let l' = compute_manual_implicits flags ref enriching l in
   let req =
     if local or isVarRef ref then ImplNoDischarge
-    else ImplInteractive(ref,flags,ImplManual l)
+    else ImplInteractive(ref,flags,ImplManual l')
   in
-  add_anonymous_leaf (inImplicits (req,[ref,l']))
+    add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 (*s Registration as global tables *)
 
diff --git a/library/impargs.mli b/library/impargs.mli
index 8e6e25194..22c1ea23c 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -41,10 +41,13 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 type implicit_status
 type implicits_list = implicit_status list
 
+type implicit_explanation
+
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> identifier
 val maximal_insertion_of : implicit_status -> bool
+val forced_implicit : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
@@ -60,8 +63,13 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
+(* A [manual_explicitation] is a tuple of a positional or named explicitation with
+   maximal insertion and forcing flags. *)
+type manual_explicitation = Topconstr.explicitation * (bool * bool) 
+
 (* Manual declaration of which arguments are expected implicit *)
-val declare_manual_implicits : bool -> global_reference -> 
-  (Topconstr.explicitation * bool) list -> unit
+val declare_manual_implicits : bool -> global_reference -> bool ->
+  manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
+