Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 44 insertions, 58 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9abee4d4..9af7e769 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 11065 2008-06-06 22:39:43Z msozeau $ *)
+(* $Id: constrintern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -50,7 +50,7 @@ let for_grammar f x =
 type internalisation_error =
   | VariableCapture of identifier
   | WrongExplicitImplicit
-  | NegativeMetavariable
+  | IllegalMetavariable
   | NotAConstructor of reference
   | UnboundFixName of bool * identifier
   | NonLinearPattern of identifier
@@ -66,8 +66,8 @@ let explain_wrong_explicit_implicit =
   str "Found an explicitly given implicit argument but was expecting" ++
   fnl () ++ str "a regular one"
 
-let explain_negative_metavariable =
-  str "Metavariable numbers must be positive"
+let explain_illegal_metavariable =
+  str "Metavariables allowed only in patterns"
 
 let explain_not_a_constructor ref =
   str "Unknown constructor: " ++ pr_reference ref
@@ -99,24 +99,26 @@ let explain_bad_explicitation_number n po =
       str "Bad explicitation name: found " ++ pr_id id ++ 
       str" but was expecting " ++ s
 
-let explain_internalisation_error = function
+let explain_internalisation_error e =
+  let pp = match e with
   | VariableCapture id -> explain_variable_capture id
   | WrongExplicitImplicit -> explain_wrong_explicit_implicit
-  | NegativeMetavariable -> explain_negative_metavariable
+  | IllegalMetavariable -> explain_illegal_metavariable
   | NotAConstructor ref -> explain_not_a_constructor ref
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
-  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
+  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
+  pp ++ str "."
 
 let error_unbound_patvar loc n =
   user_err_loc
     (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
-      str " is unbound")
+      str " is unbound.")
 
 let error_bad_inductive_type loc =
   user_err_loc (loc,"",str 
-    "This should be an inductive type applied to names or \"_\"")
+    "This should be an inductive type applied to names or \"_\".")
 
 let error_inductive_parameter_not_implicit loc =
   user_err_loc (loc,"", str
@@ -324,7 +326,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
     make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
-      pr_id id ++ str " already occurs in a different scope")
+      pr_id id ++ str " already occurs in a different scope.")
   else
     idscopes := Some (scopt,scopes)
 
@@ -444,7 +446,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   try
     match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"intern_var",
-	  str "variable " ++ pr_id id ++ str " should be bound to a term")
+	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
   (* Is [id] a goal or section variable *)
@@ -463,14 +465,14 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
-  user_err_loc (loc,"",str "Abbreviation is not applied enough")
+  user_err_loc (loc,"",str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let l = List.filter (fun (a,b) -> b <> None) l in
   if l <> [] then
     let loc = fst (Option.get (snd (List.hd l))) in
     user_err_loc
-      (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+     (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
@@ -580,7 +582,7 @@ let check_number_of_pattern loc n l =
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
     user_err_loc (loc, "", str 
-    "The components of this disjunctive pattern must bind the same variables")
+    "The components of this disjunctive pattern must bind the same variables.")
 
 let check_constructor_length env loc cstr pl pl0 =
   let n = List.length pl + List.length pl0 in
@@ -607,7 +609,7 @@ let message_redundant_alias (id1,id2) =
 (* Expanding notations *)
 
 let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern")
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
 
 let chop_aconstr_constructor loc (ind,k) args =
   let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -815,9 +817,9 @@ let locate_if_isevar loc na = function
 
 let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
-    errorlabstrm "" (str "A parameter or name of an inductive type " ++
-    pr_id id ++ str " must not be used as a bound variable in the type \
-of its constructor")
+    errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
+    pr_id id ++ strbrk " must not be used as a bound variable in the type \
+of its constructor.")
 
 let push_name_env lvar (ids,tmpsc,scopes as env) = function
   | Anonymous -> env 
@@ -840,11 +842,9 @@ let intern_typeclass_binders intern_type lvar env bl =
 	(env, (na,bk,None,ty)::bl))
     env bl
 
-let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
-  let ctx = (na, b, ty) in
-  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
-  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
-    intern_typeclass_binders intern_type lvar (env,ifvs) bind
+let intern_typeclass_binder intern_type lvar (env,bl) cb =
+  let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
+    intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
     
 let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
@@ -857,8 +857,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = fu
 		(fun ((ids,ts,sc),bl) (_,na) ->
 		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
 		(env,bl) nal
-	| TypeClass b ->
-	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+	| TypeClass (b,b') ->
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
@@ -880,11 +880,11 @@ let check_projection isproj nargs r =
       (try
 	let n = Recordops.find_projection_nparams ref + 1 in
 	if nargs <> n then
-	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters");
+	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
       with Not_found -> 
 	user_err_loc
-	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
-  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
+	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
+  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
   | _, None -> ()
 
 let get_implicit_name n imps =
@@ -909,10 +909,11 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id);
+		user_err_loc
+		  (loc,"",str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str "Argument name " ++ pr_id id
-		++ str " occurs more than once");
+		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
 	      let id =
@@ -921,11 +922,12 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err_loc (loc,"",str"Wrong argument position: " ++ int p)
+		  user_err_loc
+		    (loc,"",str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str"Argument at position " ++ int p ++
-		  str " is mentioned more than once");
+		  str " is mentioned more than once.");
 	      id in
 	  ((id,(loc,a))::eargs,rargs)
   in aux args
@@ -1086,7 +1088,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
-	raise (InternalisationError (loc,NegativeMetavariable))
+	raise (InternalisationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
 	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
@@ -1149,7 +1151,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	let nal = List.map (function
 	  | RHole loc -> Anonymous
 	  | RVar (_,id) -> Name id
-	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
 	let parnal,realnal = list_chop nparams nal in
 	if List.exists ((<>) Anonymous) parnal then
 	  error_inductive_parameter_not_implicit loc;
@@ -1173,9 +1175,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     in
       match bk with
 	| Default b -> default env b nal
-	| TypeClass b -> 
+	| TypeClass (b,b') -> 
 	    let env, ibind = intern_typeclass_binder intern_type lvar
-	      (env, []) (List.hd nal) b ty in
+	      (env, []) (List.hd nal,(b,b'),ty) in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1189,9 +1191,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass b ->	  
+      | TypeClass (b, b') ->	  
 	  let env, ibind = intern_typeclass_binder intern_type lvar
-	    (env, []) (List.hd nal) b ty in
+	    (env, []) (List.hd nal,(b,b'),ty) in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
@@ -1221,7 +1223,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  if eargs <> [] then 
 	    (let (id,(loc,_)) = List.hd eargs in
 	       user_err_loc (loc,"",str "Not enough non implicit
-	    arguments to accept the argument bound to " ++ pr_id id));
+	    arguments to accept the argument bound to " ++ 
+		 pr_id id ++ str"."));
 	  []
       | ([], rargs) ->
 	  assert (eargs = []);
@@ -1275,23 +1278,6 @@ let intern_ltac isarity ltacvars sigma env c =
 
 type manual_implicits = (explicitation * (bool * bool)) list
 
-let implicits_of_rawterm l = 
-  let rec aux i c = 
-    match c with
-	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
-	  let rest = aux (succ i) b in
-	    if bk = Implicit then
-	      let name =
-		match na with
-		    Name id -> Some id
-		  | Anonymous -> None
-	      in
-		(ExplByPos (i, name), (true, true)) :: rest
-	    else rest
-      | RLetIn (loc, na, t, b) -> aux i b
-      | _ -> []
-  in aux 1 l
-
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
@@ -1321,11 +1307,11 @@ let interp_constr_evars_gen_impls ?evdref
   match evdref with 
     | None -> 
 	let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_gen kind Evd.empty env c, imps
     | Some evdref ->
 	let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_tcc_evars evdref env kind c, imps
 
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =