summaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml102
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:16:37 +0000