summaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml776
1 files changed, 437 insertions, 339 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c8faf911..b5604cf7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
open Flags
open Names
open Nameops
+open Namegen
open Libnames
open Impargs
open Rawterm
@@ -24,66 +25,32 @@ open Nametab
open Notation
open Inductiveops
-open Decl_kinds
-
-let type_of_logical_kind =
- function
- | IsDefinition def ->
- (match def with
- | Definition -> "def"
- | Coercion -> "coe"
- | SubClass -> "subclass"
- | CanonicalStructure -> "canonstruc"
- | Example -> "ex"
- | Fixpoint -> "def"
- | CoFixpoint -> "def"
- | Scheme -> "scheme"
- | StructureComponent -> "proj"
- | IdentityCoercion -> "coe"
- | Instance -> "inst"
- | Method -> "meth")
- | IsAssumption a ->
- (match a with
- | Definitional -> "defax"
- | Logical -> "prfax"
- | Conjectural -> "prfax")
- | IsProof th ->
- (match th with
- | Theorem
- | Lemma
- | Fact
- | Remark
- | Property
- | Proposition
- | Corollary -> "thm")
-
-let type_of_global_ref gr =
- if Typeclasses.is_class gr then
- "class"
- else
- match gr with
- | ConstRef cst ->
- type_of_logical_kind (Decls.constant_kind cst)
- | VarRef v ->
- "var" ^ type_of_logical_kind (Decls.variable_kind v)
- | IndRef ind ->
- let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record then
- if mib.Declarations.mind_finite then "rec"
- else "corec"
- else if mib.Declarations.mind_finite then "ind"
- else "coind"
- | ConstructRef _ -> "constr"
-
-(* To interpret implicits and arg scopes of recursive variables in
- inductive types and recursive definitions *)
-type var_internalisation_type = Inductive | Recursive | Method
-
-type var_internalisation_data =
- var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
-
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+(* To interpret implicits and arg scopes of variables in inductive
+ types and recursive definitions and of projection names in records *)
+
+type var_internalization_type = Inductive | Recursive | Method
+
+type var_internalization_data =
+ (* type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ var_internalization_type *
+ (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+ in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+ identifier list *
+ (* signature of impargs of the variable *)
+ Impargs.implicits_list *
+ (* subscopes of the args of the variable *)
+ scope_name option list
+
+type internalization_env =
+ (identifier * var_internalization_data) list
+
+type full_internalization_env =
+ (* a superset of the list of variables that may be automatically
+ inserted and that must not occur as binders *)
+ identifier list *
+ (* mapping of the variables to their internalization data *)
+ internalization_env
type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
@@ -98,6 +65,33 @@ let for_grammar f x =
a
(**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+ Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
+
+let is_global id =
+ try
+ let _ = locate_reference (qualid_of_ident id) in true
+ with Not_found ->
+ false
+
+let global_reference_of_reference ref =
+ locate_reference (snd (qualid_of_reference ref))
+
+let global_reference id =
+ constr_of_global (locate_reference (qualid_of_ident id))
+
+let construct_reference ctx id =
+ try
+ Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+ with Not_found ->
+ global_reference id
+
+let global_reference_in_absolute_module dir id =
+ constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+
+(**********************************************************************)
(* Internalisation errors *)
type internalisation_error =
@@ -126,7 +120,7 @@ let explain_not_a_constructor ref =
str "Unknown constructor: " ++ pr_reference ref
let explain_unbound_fix_name is_cofix id =
- str "The name" ++ spc () ++ pr_id id ++
+ str "The name" ++ spc () ++ pr_id id ++
spc () ++ str "is not bound in the corresponding" ++ spc () ++
str (if is_cofix then "co" else "") ++ str "fixpoint definition"
@@ -143,13 +137,13 @@ let explain_bad_explicitation_number n po =
let s = match po with
| None -> str "a regular argument"
| Some p -> int p in
- str "Bad explicitation number: found " ++ int n ++
+ str "Bad explicitation number: found " ++ int n ++
str" but was expecting " ++ s
| ExplByName id ->
let s = match po with
| None -> str "a regular argument"
| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
- str "Bad explicitation name: found " ++ pr_id id ++
+ str "Bad explicitation name: found " ++ pr_id id ++
str" but was expecting " ++ s
let explain_internalisation_error e =
@@ -164,13 +158,8 @@ let explain_internalisation_error e =
| 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.")
-
let error_bad_inductive_type loc =
- user_err_loc (loc,"",str
+ user_err_loc (loc,"",str
"This should be an inductive type applied to names or \"_\".")
let error_inductive_parameter_not_implicit loc =
@@ -179,6 +168,35 @@ let error_inductive_parameter_not_implicit loc =
"the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
(**********************************************************************)
+(* Pre-computing the implicit arguments and arguments scopes needed *)
+(* for interpretation *)
+
+let empty_internalization_env = ([],[])
+
+let set_internalization_env_params ienv params =
+ let nparams = List.length params in
+ if nparams = 0 then
+ ([],ienv)
+ else
+ let ienv_with_implicit_params =
+ List.map (fun (id,(ty,_,impl,scopes)) ->
+ let sub_impl,_ = list_chop nparams impl in
+ let sub_impl' = List.filter is_status_implicit sub_impl in
+ (id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in
+ (params, ienv_with_implicit_params)
+
+let compute_internalization_data env ty typ impls =
+ let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in
+ (ty, [], impl, compute_arguments_scope typ)
+
+let compute_full_internalization_env env ty params idl typl impll =
+ set_internalization_env_params
+ (list_map3
+ (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+ idl typl impll)
+ params
+
+(**********************************************************************)
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
@@ -191,8 +209,8 @@ and spaces ntn n =
let expand_notation_string ntn n =
let pos = List.nth (wildcards ntn 0) n in
let hd = if pos = 0 then "" else String.sub ntn 0 pos in
- let tl =
- if pos = String.length ntn then ""
+ let tl =
+ if pos = String.length ntn then ""
else String.sub ntn (pos+1) (String.length ntn - pos -1) in
hd ^ "{ _ }" ^ tl
@@ -202,7 +220,7 @@ let contract_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CNotation (_,"{ _ }",([a],[])) :: l ->
+ | CNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -215,7 +233,7 @@ let contract_pat_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CPatNotation (_,"{ _ }",([a],[])) :: l ->
+ | CPatNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -227,26 +245,40 @@ let contract_pat_notation ntn (l,ll) =
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
-let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
+let make_current_scope = function
+ | (Some tmp_scope,(sc::_ as scopes)) when sc = tmp_scope -> scopes
+ | (Some tmp_scope,scopes) -> tmp_scope::scopes
+ | None,scopes -> scopes
let set_var_scope loc id (_,_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
- if !idscopes <> None &
+ if !idscopes <> None &
make_current_scope (Option.get !idscopes)
<> make_current_scope (scopt,scopes) then
+ let pr_scope_stack = function
+ | [] -> str "the empty scope stack"
+ | [a] -> str "scope " ++ str a
+ | l -> str "scope stack " ++
+ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in
user_err_loc (loc,"set_var_scope",
- pr_id id ++ str " already occurs in a different scope.")
+ pr_id id ++ str " is used both in " ++
+ pr_scope_stack (make_current_scope (Option.get !idscopes)) ++
+ strbrk " and in " ++
+ pr_scope_stack (make_current_scope (scopt,scopes)))
else
idscopes := Some (scopt,scopes)
(**********************************************************************)
(* Syntax extensions *)
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))=
+ function
+ | Anonymous -> (renaming,env),Anonymous
+ | Name id ->
try
(* Binders bound in the notation are considered first-order objects *)
- let _,id' = coerce_to_id (fst (List.assoc id subst)) in
- (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
+ let _,na = coerce_to_name (fst (List.assoc id subst)) in
+ (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -256,7 +288,7 @@ let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) i
let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
let id' = next_ident_away id fvs in
let renaming' = if id=id' then renaming else (id,id')::renaming in
- (renaming',env), id'
+ (renaming',env), Name id'
let rec subst_iterator y t = function
| RVar (_,id) as x -> if id = y then t else x
@@ -270,40 +302,45 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
interp (ids,unb,scopt,subscopes@scopes) a
- with Not_found ->
- try
+ with Not_found ->
+ try
RVar (loc,List.assoc id renaming)
- with Not_found ->
+ with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
RVar (loc,id)
end
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
- let termin =
+ let termin =
subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
- List.fold_right (fun a t ->
+ List.fold_right (fun a t ->
subst_iterator ldots_var t
- (subst_aconstr_in_rawconstr loc interp
+ (subst_aconstr_in_rawconstr loc interp
((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
(if lassoc then List.rev l else l) termin
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
+ | AHole (Evd.BinderType (Name id as na)) ->
+ let na =
+ try snd (coerce_to_name (fst (List.assoc id subst)))
+ with Not_found -> na in
+ RHole (loc,Evd.BinderType na)
| t ->
rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
(subst_aconstr_in_rawconstr loc interp sub) subinfos t
let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
- let ntn,(args,argslist) = contract_notation ntn fullargs in
+ let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
- let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
- subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
+ Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
+ let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+ let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
+ subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
let set_type_scope (ids,unb,tmp_scope,scopes) =
(ids,unb,Some Notation.type_scope,scopes)
@@ -337,8 +374,8 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
let (vars1,unbndltacvars) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
- let ty, l,impl,argsc = List.assoc id impls in
- let l = List.map
+ let ty,l,impl,argsc = List.assoc id impls in
+ let l = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
@@ -353,7 +390,6 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
then
(set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
else
-
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
try
match List.assoc id unbndltacvars with
@@ -367,13 +403,21 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
let ref = VarRef id in
- RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+ let impls = implicits_of_global ref in
+ let scopes = find_arguments_scope ref in
+ Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+ RRef (loc, ref), impls, scopes, []
with _ ->
(* [id] a goal variable *)
RVar (loc,id), [], [], []
-
-let find_appl_head_data (_,_,_,(_,impls)) = function
+
+let find_appl_head_data = function
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+ | RApp (_,RRef (_,ref),l) as x
+ when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
+ let n = List.length l in
+ x,list_skipn_at_least n (implicits_of_global ref),
+ list_skipn_at_least n (find_arguments_scope ref),[]
| x -> x,[],[],[]
let error_not_enough_arguments loc =
@@ -386,23 +430,31 @@ let check_no_explicitation l =
user_err_loc
(loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
+let dump_extended_global loc = function
+ | TrueGlobal ref -> Dumpglob.add_glob loc ref
+ | SynDef sp -> Dumpglob.add_glob_kn loc sp
+
+let intern_extended_global_of_qualid (loc,qid) =
+ try let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+ with Not_found -> error_global_not_found_loc loc qid
+
+let intern_reference ref =
+ Smartlocate.global_of_extended_global
+ (intern_extended_global_of_qualid (qualid_of_reference ref))
+
(* Is it a global reference or a syntactic definition? *)
let intern_qualid loc qid intern env args =
- try match Nametab.extended_locate qid with
+ match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
- Dumpglob.add_glob loc ref;
RRef (loc, ref), args
- | SyntacticDef sp ->
- Dumpglob.add_glob_kn loc sp;
- let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
+ | SynDef sp ->
+ let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments loc;
let args1,args2 = list_chop nids args in
check_no_explicitation args1;
let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
- with Not_found ->
- error_global_not_found_loc loc qid
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env args =
@@ -413,20 +465,20 @@ let intern_non_secvar_qualid loc qid intern env args =
let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
| Qualid (loc, qid) ->
let r,args2 = intern_qualid loc qid intern env args in
- find_appl_head_data lvar r, args2
+ find_appl_head_data r, args2
| Ident (loc, id) ->
try intern_var env lvar loc id, args
- with Not_found ->
- let qid = make_short_qualid id in
+ with Not_found ->
+ let qid = qualid_of_ident id in
try
let r,args2 = intern_non_secvar_qualid loc qid intern env args in
- find_appl_head_data lvar r, args2
+ find_appl_head_data r, args2
with e ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || unb then
(RVar (loc,id), [], [], []),args
else raise e
-
+
let interp_reference vars r =
let (r,_,_,_),_ =
intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
@@ -437,12 +489,6 @@ let apply_scope_env (ids,unb,_,scopes) = function
| [] -> (ids,unb,None,scopes), []
| sc::scl -> (ids,unb,sc,scopes), scl
-let rec adjust_scopes env scopes = function
- | [] -> []
- | a::args ->
- let (enva,scopes) = apply_scope_env env scopes in
- enva :: adjust_scopes env scopes args
-
let rec simple_adjust_scopes n = function
| [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
@@ -473,11 +519,11 @@ let simple_product_of_cases_patterns pl =
pl [[],[]]
(* Check linearity of pattern-matching *)
-let rec has_duplicate = function
+let rec has_duplicate = function
| [] -> None
| x::l -> if List.mem x l then (Some x) else has_duplicate l
-let loc_of_lhs lhs =
+let loc_of_lhs lhs =
join_loc (fst (List.hd lhs)) (fst (list_last lhs))
let check_linearity lhs ids =
@@ -494,7 +540,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
+ user_err_loc (loc, "", str
"The components of this disjunctive pattern must bind the same variables.")
let check_constructor_length env loc cstr pl pl0 =
@@ -516,7 +562,7 @@ let alias_of = function
| (id::_,_) -> Name id
let message_redundant_alias (id1,id2) =
- if_verbose warning
+ if_verbose warning
("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
(* Expanding notations *)
@@ -525,12 +571,16 @@ let error_invalid_pattern_notation loc =
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
- if nparams > List.length args then error_invalid_pattern_notation loc;
- let params,args = list_chop nparams args in
- List.iter (function AHole _ -> ()
- | _ -> error_invalid_pattern_notation loc) params;
- args
+ if List.length args = 0 then (* Tolerance for a @id notation *) args else
+ begin
+ let mib,_ = Global.lookup_inductive ind in
+ let nparams = mib.Declarations.mind_nparams in
+ if nparams > List.length args then error_invalid_pattern_notation loc;
+ let params,args = list_chop nparams args in
+ List.iter (function AHole _ -> ()
+ | _ -> error_invalid_pattern_notation loc) params;
+ args
+ end
let rec subst_pat_iterator y t (subst,p) = match p with
| PatVar (_,id) as x ->
@@ -546,10 +596,10 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
intern (subscopes@scopes) ([],[]) scopt a
- with Not_found ->
+ with Not_found ->
if id = ldots_var then [], [[], PatVar (loc,Name id)] else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
(*
@@ -565,41 +615,41 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
let args = chop_aconstr_constructor loc cstr args in
let idslpll = List.map (aux Anonymous fullsubst) args in
let ids',pll = product_of_cases_patterns [] idslpll in
- let pl' = List.map (fun (asubst,pl) ->
+ let pl' = List.map (fun (asubst,pl) ->
asubst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
let termin = aux Anonymous fullsubst terminator in
let idsl,v =
- List.fold_right (fun a (tids,t) ->
+ List.fold_right (fun a (tids,t) ->
let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
let pll = List.map (subst_pat_iterator ldots_var t) u in
tids@uids, List.flatten pll)
(if lassoc then List.rev l else l) termin in
idsl, List.map (fun ((asubst, pl) as x) ->
match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t -> error_invalid_pattern_notation loc
in aux alias fullsubst a
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
- | ConstrPat of constructor * (identifier list *
+ | ConstrPat of constructor * (identifier list *
((identifier * identifier) list * cases_pattern) list) list
| VarPat of identifier
let find_constructor ref f aliases pats scopes =
let (loc,qid) = qualid_of_reference ref in
let gref =
- try extended_locate qid
+ try locate_extended qid
with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
match gref with
- | SyntacticDef sp ->
- let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+ | SynDef sp ->
+ let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
| ARef (ConstructRef cstr) ->
assert (vars=[]);
@@ -613,14 +663,14 @@ let find_constructor ref f aliases pats scopes =
let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
-
+
| TrueGlobal r ->
let rec unf = function
| ConstRef cst ->
let v = Environ.constant_value (Global.env()) cst in
unf (global_of_constr v)
- | ConstructRef cstr ->
- Dumpglob.add_glob loc r;
+ | ConstructRef cstr ->
+ Dumpglob.add_glob loc r;
cstr, [], pats
| _ -> raise Not_found
in unf r
@@ -643,17 +693,110 @@ let maybe_constructor ref f aliases scopes =
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
-let mustbe_constructor loc ref f aliases patl scopes =
+let mustbe_constructor loc ref f aliases patl scopes =
try find_constructor ref f aliases patl scopes
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
+let sort_fields mode loc l completer =
+(*mode=false if pattern and true if constructor*)
+ match l with
+ | [] -> None
+ | (refer, value)::rem ->
+ let (nparams, (* the number of parameters *)
+ base_constructor, (* the reference constructor of the record *)
+ (max, (* number of params *)
+ (first_index, (* index of the first field of the record *)
+ list_proj))) (* list of projections *)
+ =
+ let record =
+ try Recordops.find_projection
+ (global_reference_of_reference refer)
+ with Not_found ->
+ user_err_loc (loc, "intern", str"Not a projection")
+ in
+ (* elimination of the first field from the projections *)
+ let rec build_patt l m i acc =
+ match l with
+ | [] -> (i, acc)
+ | (Some name) :: b->
+ (match m with
+ | [] -> anomaly "Number of projections mismatch"
+ | (_, regular)::tm ->
+ let boolean = not regular in
+ if ConstRef name = global_reference_of_reference refer
+ then
+ if boolean && mode then
+ user_err_loc (loc, "", str"No local fields allowed in a record construction.")
+ else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
+ else
+ build_patt b tm (if boolean&&mode then i else i + 1)
+ (if boolean && mode then acc
+ else fst acc, (i, ConstRef name) :: snd acc))
+ | None :: b-> (* we don't want anonymous fields *)
+ if mode then
+ user_err_loc (loc, "", str "This record contains anonymous fields.")
+ else build_patt b m (i+1) acc
+ (* anonymous arguments don't appear in m *)
+ in
+ let ind = record.Recordops.s_CONST in
+ try (* insertion of Constextern.reference_global *)
+ (record.Recordops.s_EXPECTEDPARAM,
+ Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef ind)),
+ build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
+ with Not_found -> anomaly "Environment corruption for records."
+ in
+ (* now we want to have all fields of the pattern indexed by their place in
+ the constructor *)
+ let rec sf patts accpatt =
+ match patts with
+ | [] -> accpatt
+ | p::q->
+ let refer, patt = p in
+ let rec add_patt l acc =
+ match l with
+ | [] ->
+ user_err_loc
+ (loc, "",
+ str "This record contains fields of different records.")
+ | (i, a) :: b->
+ if global_reference_of_reference refer = a
+ then (i,List.rev_append acc l)
+ else add_patt b ((i,a)::acc)
+ in
+ let (index, projs) = add_patt (snd accpatt) [] in
+ sf q ((index, patt)::fst accpatt, projs) in
+ let (unsorted_indexed_pattern, remainings) =
+ sf rem ([first_index, value], list_proj) in
+ (* we sort them *)
+ let sorted_indexed_pattern =
+ List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in
+ (* a function to complete with wildcards *)
+ let rec complete_list n l =
+ if n <= 1 then l else complete_list (n-1) (completer n l) in
+ (* a function to remove indice *)
+ let rec clean_list l i acc =
+ match l with
+ | [] -> complete_list (max - i) acc
+ | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
+ in
+ Some (nparams, base_constructor,
+ List.rev (clean_list sorted_indexed_pattern 0 []))
+
let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
- let intern_pat = intern_cases_pattern genv in
+ let intern_pat = intern_cases_pattern genv in
match pat with
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
intern_pat scopes aliases' tmp_scope p
+ | CPatRecord (loc, l) ->
+ let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
+ let self_patt =
+ match sorted_fields with
+ | None -> CPatAtom (loc, None)
+ | Some (_, head, pl) -> CPatCstr(loc, head, pl)
+ in
+ intern_pat scopes aliases tmp_scope self_patt
| CPatCstr (loc, head, pl) ->
let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
check_constructor_length genv loc c idslpl1 pl2;
@@ -669,9 +812,9 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
| CPatNotation (_,"( _ )",([a],[])) ->
intern_pat scopes aliases tmp_scope a
| CPatNotation (loc, ntn, fullargs) ->
- let ntn,(args,argsl) = contract_pat_notation ntn fullargs in
+ let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+ Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
let ids'',pl =
@@ -680,9 +823,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
in ids@ids'', pl
| CPatPrim (loc, p) ->
let a = alias_of aliases in
- let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+ let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
(tmp_scope,scopes) in
- Dumpglob.dump_notation_location (fst (unloc loc)) df;
(ids,[asubst,c])
| CPatDelimiters (loc, key, e) ->
intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -719,10 +861,10 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ ->
+ | RHole _ ->
(try match na with
| Name id -> Reserve.find_reserved_type id
- | Anonymous -> raise Not_found
+ | Anonymous -> raise Not_found
with Not_found -> RHole (loc, Evd.BinderType na))
| x -> x
@@ -732,43 +874,44 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
(Idset.add id ids, unb,tmpsc,scopes)
let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
Dumpglob.dump_binding loc id;
(Idset.add id ids,unb,tmpsc,scopes)
let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
(ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
- let ty =
- if t then ty else
+ let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in
+ let ty, ids' =
+ if t then ty, ids else
Implicit_quantifiers.implicit_application ids
Implicit_quantifiers.combine_params_freevar ty
in
let ty' = intern_type (ids,true,tmpsc,sc) ty in
- let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty' in
+ let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
let na = match na with
- | Anonymous ->
- if fail_anonymous then na
+ | Anonymous ->
+ if fail_anonymous then na
else
- let name =
- let id =
+ let name =
+ let id =
match ty with
| CApp (_, (_, CRef (Ident (loc,id))), _) -> id
| _ -> id_of_string "H"
- in Implicit_quantifiers.make_fresh ids (Global.env ()) id
+ in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
| _ -> na
in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
@@ -793,26 +936,26 @@ let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((id
let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
let c = intern (ids,true,tmp_scope,scopes) c in
- let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
- let env', c' =
- let abs =
- let pi =
+ let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
+ let env', c' =
+ let abs =
+ let pi =
match ak with
| Some AbsPi -> true
- | None when tmp_scope = Some Notation.type_scope
+ | None when tmp_scope = Some Notation.type_scope
|| List.mem Notation.type_scope scopes -> true
| _ -> false
- in
+ in
if pi then
(fun (id, loc') acc ->
RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
else
- (fun (id, loc') acc ->
+ (fun (id, loc') acc ->
RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
in
- List.fold_right (fun (id, loc as lid) (env, acc) ->
+ List.fold_right (fun (id, loc as lid) (env, acc) ->
let env' = push_loc_name_env lvar env loc (Name id) in
- (env', abs lid acc)) fvs (env,c)
+ (env', abs lid acc)) fvs (env,c)
in c'
(**********************************************************************)
@@ -820,20 +963,20 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a
let merge_impargs l args =
List.fold_right (fun a l ->
- match a with
- | (_,Some (_,(ExplByName id as x))) when
+ match a with
+ | (_,Some (_,(ExplByName id as x))) when
List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
| _ -> a::l)
- l args
+ l args
-let check_projection isproj nargs r =
+let check_projection isproj nargs r =
match (r,isproj) with
| RRef (loc, ref), Some _ ->
(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.");
- with Not_found ->
+ 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.")
@@ -842,9 +985,9 @@ let check_projection isproj nargs r =
let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
-let set_hole_implicit i = function
- | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
- | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
+let set_hole_implicit i b = function
+ | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
+ | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
| _ -> anomaly "Only refs have implicits"
let exists_implicit_name id =
@@ -869,7 +1012,7 @@ let extract_explicit_arg imps args =
id
| ExplByPos (p,_id) ->
let id =
- try
+ try
let imp = List.nth imps (p-1) in
if not (is_status_implicit imp) then failwith "imp";
name_of_implicit imp
@@ -905,37 +1048,29 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
- let intern_ro_arg c f =
- let idx =
- match n with
- Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
- | None -> 0
- in
+ let intern_ro_arg f =
+ let idx = Option.default 0 (index_of_annot bl n) in
let before, after = list_chop idx bl in
let ((ids',_,_,_) as env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
- let ro =
- match c with
- | None -> RStructRec
- | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c')
- in
+ let ro = f (intern (ids', unb, tmp_scope, scopes)) in
let n' = Option.map (fun _ -> List.length before) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, ((ids',_,_,_),rbl) =
- (match order with
- | CStructRec ->
- intern_ro_arg None (fun _ -> RStructRec)
- | CWfRec c ->
- intern_ro_arg (Some c) (fun r -> RWfRec r)
- | CMeasureRec c ->
- intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+ match order with
+ | CStructRec ->
+ intern_ro_arg (fun _ -> RStructRec)
+ | CWfRec c ->
+ intern_ro_arg (fun f -> RWfRec (f c))
+ | CMeasureRec (m,r) ->
+ intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
in
let ids'' = List.fold_right Idset.add lf ids' in
- ((n, ro), List.rev rbl,
+ ((n, ro), List.rev rbl,
intern_type (ids',unb,tmp_scope,scopes) ty,
intern (ids'',unb,None,scopes) bd)) dl in
- RRec (loc,RFix
+ RRec (loc,RFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -976,7 +1111,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
intern (push_loc_name_env lvar env loc1 na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
- when Bigint.is_strictly_pos p ->
+ when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",([a],[])) -> intern env a
| CNotation (loc,ntn,args) ->
@@ -984,9 +1119,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CGeneralization (loc,b,a,c) ->
intern_generalization intern env lvar loc b a c
| CPrim (loc, p) ->
- let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (fst (unloc loc)) df;
- c
+ fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
| CDelimiters (loc, key, e) ->
intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
@@ -994,6 +1127,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env lvar args ref in
check_projection isproj (List.length args) f;
+ (* Rem: RApp(_,f,[]) stands for @f *)
RApp (loc, f, intern_args env args_scopes (List.map fst args))
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
@@ -1006,48 +1140,28 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CRef ref -> intern_applied_reference intern env lvar args ref
| CNotation (loc,ntn,([],[])) ->
let c = intern_notation intern env loc ntn ([],[]) in
- find_appl_head_data lvar c, args
+ find_appl_head_data c, args
| x -> (intern env f,[],[],[]), args in
- let args =
+ let args =
intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
- (match c with
+ (match c with
(* Now compact "(f args') args" *)
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
| _ -> RApp (loc, c, args))
- | CRecord (loc, w, fs) ->
- let id, _ = List.hd fs in
- let record =
- let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
- match id with
- | RRef (loc, ref) ->
- (try Recordops.find_projection ref
- with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
- | c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
- in
- let args =
- let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
- let fields, rest =
- List.fold_left (fun (args, rest as acc) (na, b) ->
- if b then
- try
- let id = out_name na in
- let _, t = List.assoc id rest in
- t :: args, List.remove_assoc id rest
- with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
- else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
- in
- if rest <> [] then
- let id, (loc, t) = List.hd rest in
- user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
- else pars @ List.rev fields
- in
- let constrname =
- Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
- in
- let app = CAppExpl (loc, (None, constrname), args) in
+ | CRecord (loc, _, fs) ->
+ let cargs =
+ sort_fields true loc fs
+ (fun k l -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: l)
+ in
+ begin
+ match cargs with
+ | None -> user_err_loc (loc, "intern", str"No constructor inference.")
+ | Some (n, constrname, args) ->
+ let pars = list_make n (CHole (loc, None)) in
+ let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
intern env app
-
+ end
| CCases (loc, sty, rtnpo, tms, eqns) ->
let tms,env' = List.fold_right
(fun citm (inds,env) ->
@@ -1072,7 +1186,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let env'' = List.fold_left (push_name_env lvar) env ids in
intern_type env'' p) po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
- | CHole (loc, k) ->
+ | CHole (loc, k) ->
RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
@@ -1091,12 +1205,12 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_type env = intern (set_type_scope env)
- and intern_local_binder env bind =
+ and intern_local_binder env bind =
intern_local_binder_aux intern intern_type lvar env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern scopes n (loc,pl) =
- let idsl_pll =
+ let idsl_pll =
List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
@@ -1125,7 +1239,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
let tm' = intern env tm in
let ids,typ = match t with
- | Some t ->
+ | Some t ->
let tids = ids_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
let t = intern_type (tids,unb,None,scopes) t in
@@ -1145,7 +1259,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
if List.exists ((<>) Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
realnal, Some (loc,ind,nparams,realnal)
- | None ->
+ | None ->
[], None in
let na = match tm', na with
| RVar (_,id), None when Idset.mem id vars -> Name id
@@ -1153,7 +1267,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
-
+
and iterate_prod loc2 env bk ty body nal =
let rec default env bk = function
| (loc1,na)::nal ->
@@ -1165,14 +1279,14 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
match bk with
| Default b -> default env b nal
- | Generalized (b,b',t) ->
+ | Generalized (b,b',t) ->
let env, ibind = intern_generalized_binder intern_type lvar
env [] (List.hd nal) b b' t ty in
let body = intern_type env body in
it_mkRProd ibind body
-
- and iterate_lam loc2 env bk ty body nal =
- let rec default env bk = function
+
+ and iterate_lam loc2 env bk ty body nal =
+ let rec default env bk = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
let body = default (push_loc_name_env lvar env loc1 na) bk nal in
@@ -1181,19 +1295,19 @@ let internalise sigma globalenv env allow_patvar lvar c =
| [] -> intern env body
in match bk with
| Default b -> default env b nal
- | Generalized (b, b', t) ->
+ | Generalized (b, b', t) ->
let env, ibind = intern_generalized_binder intern_type lvar
env [] (List.hd nal) b b' t ty in
let body = intern env body in
it_mkRLambda ibind body
-
+
and intern_impargs c env l subscopes args =
let eargs, rargs = extract_explicit_arg l args in
let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
match (impl,rargs) with
| (imp::impl', rargs) when is_status_implicit imp ->
- begin try
+ begin try
let id = name_of_implicit imp in
let (_,a) = List.assoc id eargs in
let eargs' = List.remove_assoc id eargs in
@@ -1204,16 +1318,16 @@ let internalise sigma globalenv env allow_patvar lvar c =
(* with implicit arguments if maximal insertion is set *)
[]
else
- RHole (set_hole_implicit (n,get_implicit_name n l) c) ::
+ RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
aux (n+1) impl' subscopes' eargs rargs
end
| (imp::impl', a::rargs') ->
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
- | (imp::impl', []) ->
- if eargs <> [] then
+ | (imp::impl', []) ->
+ 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 " ++
+ arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
| ([], rargs) ->
@@ -1227,51 +1341,49 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (enva,subscopes) = apply_scope_env env subscopes in
(intern enva a) :: (intern_args env subscopes args)
- in
- try
+ in
+ try
intern env c
with
InternalisationError (loc,e) ->
- user_err_loc (loc,"internalize",explain_internalisation_error e)
+ user_err_loc (loc,"internalize",
+ explain_internalisation_error e)
(**************************************************************************)
(* Functions to translate constr_expr into rawconstr *)
(**************************************************************************)
let extract_ids env =
- List.fold_right Idset.add
+ List.fold_right Idset.add
(Termops.ids_of_rel_context (Environ.rel_context env))
Idset.empty
let intern_gen isarity sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- let tmp_scope =
+ let tmp_scope =
if isarity then Some Notation.type_scope else None in
internalise sigma env (extract_ids env, false, tmp_scope,[])
allow_patvar (ltacvars,Environ.named_context env, [], impls) c
-
-let intern_constr sigma env c = intern_gen false sigma env c
-let intern_type sigma env c = intern_gen true sigma env c
+let intern_constr sigma env c = intern_gen false sigma env c
+
+let intern_type sigma env c = intern_gen true sigma env c
let intern_pattern env patt =
try
- intern_cases_pattern env [] ([],[]) None patt
- with
+ intern_cases_pattern env [] ([],[]) None patt
+ with
InternalisationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalisation_error e)
-let intern_ltac isarity ltacvars sigma env c =
- intern_gen isarity sigma env ~ltacvars:ltacvars c
-
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
(*********************************************************************)
(* Functions to parse and interpret constructions *)
-let interp_gen kind sigma env
+let interp_gen kind sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
@@ -1284,39 +1396,56 @@ let interp_type sigma env ?(impls=([],[])) c =
interp_gen IsType sigma env ~impls c
let interp_casted_constr sigma env ?(impls=([],[])) c typ =
- interp_gen (OfType (Some typ)) sigma env ~impls c
+ interp_gen (OfType (Some typ)) sigma env ~impls c
let interp_open_constr sigma env c =
Default.understand_tcc sigma env (intern_constr sigma env c)
+let interp_open_constr_patvar sigma env c =
+ let raw = intern_gen false sigma env c ~allow_patvar:true in
+ let sigma = ref (Evd.create_evar_defs sigma) in
+ let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in
+ let rec patvar_to_evar r = match r with
+ | RPatVar (loc,(_,id)) ->
+ ( try Gmap.find id !evars
+ with Not_found ->
+ let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
+ let ev = Evarutil.e_new_evar sigma env ev in
+ let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
+ evars := Gmap.add id rev !evars;
+ rev
+ )
+ | _ -> map_rawconstr patvar_to_evar r in
+ let raw = patvar_to_evar raw in
+ Default.understand_tcc !sigma env raw
+
let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
-let interp_constr_evars_gen_impls ?evdref
+let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
env ?(impls=([],[])) kind c =
- match evdref with
- | None ->
- let c = intern_gen (kind=IsType) ~impls Evd.empty env 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 = Implicit_quantifiers.implicits_of_rawterm c in
- Default.understand_tcc_evars evdref env kind c, imps
+ let evdref =
+ match evdref with
+ | None -> ref Evd.empty
+ | Some evdref -> evdref
+ in
+ let c = intern_gen (kind=IsType) ~impls !evdref env c in
+ let imps = Implicit_quantifiers.implicits_of_rawterm c in
+ Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
- let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
- Default.understand_tcc_evars evdref env kind c
-
-let interp_casted_constr_evars_impls ?evdref
+let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
env ?(impls=([],[])) c typ =
- interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
+ interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
-let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ?evdref env IsType ~impls c
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
-let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
+
+let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+ let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
+ Default.understand_tcc_evars evdref env kind c
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
@@ -1324,27 +1453,23 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
let interp_type_evars evdref env ?(impls=([],[])) c =
interp_constr_evars_gen evdref env IsType ~impls c
-let interp_constr_judgment_evars evdref env c =
- Default.understand_judgment_tcc evdref env
- (intern_constr (Evd.evars_of !evdref) env c)
-
type ltac_sign = identifier list * unbound_ltac_var_map
let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
pattern_of_rawconstr c
-let interp_aconstr impls (vars,varslist) a =
+let interp_aconstr ?(impls=([],[])) (vars,varslist) a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
- false (([],[]),Environ.named_context env,vl,([],impls)) a in
+ false (([],[]),Environ.named_context env,vl,impls) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a = aconstr_of_rawconstr vars c in
(* Returns [a] and the ordered list of variables with their scopes *)
(* Variables occurring in binders have no relevant scope since bound *)
- let vl = List.map (fun (id,r) ->
+ let vl = List.map (fun (id,r) ->
(id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
list_chop (List.length vars) vl, a
@@ -1356,7 +1481,7 @@ let interp_binder sigma env na t =
Default.understand_type sigma env t'
let interp_binder_evars evdref env na t =
- let t = intern_gen true (Evd.evars_of !evdref) env t in
+ let t = intern_gen true !evdref env t in
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
Default.understand_tcc_evars evdref env IsType t'
@@ -1374,7 +1499,7 @@ let intern_context fail_anonymous sigma env params =
(intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
((extract_ids env,false,None,[]), []) params)
-let interp_context_gen understand_type understand_judgment env bl =
+let interp_rawcontext_gen understand_type understand_judgment env bl =
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
@@ -1383,10 +1508,10 @@ let interp_context_gen understand_type understand_judgment env bl =
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
let t = understand_type env t' in
let d = (na,None,t) in
- let impls =
+ let impls =
if k = Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
- (ExplByPos (n, na), (true, true)) :: impls
+ (ExplByPos (n, na), (true, true, true)) :: impls
else impls
in
(push_rel d env, d::params, succ n, impls)
@@ -1397,42 +1522,15 @@ let interp_context_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context ?(fail_anonymous=false) sigma env params =
+let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params =
let bl = intern_context fail_anonymous sigma env params in
- interp_context_gen (Default.understand_type sigma)
- (Default.understand_judgment sigma) env bl
-
-let interp_context_evars ?(fail_anonymous=false) evdref env params =
- let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in
- interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
- (Default.understand_judgment_tcc evdref) env bl
-
-(**********************************************************************)
-(* Locating reference, possibly via an abbreviation *)
-
-let locate_reference qid =
- match Nametab.extended_locate qid with
- | TrueGlobal ref -> ref
- | SyntacticDef kn ->
- match Syntax_def.search_syntactic_definition dummy_loc kn with
- | [],ARef ref -> ref
- | _ -> raise Not_found
+ interp_rawcontext_gen understand_type understand_judgment env bl
-let is_global id =
- try
- let _ = locate_reference (make_short_qualid id) in true
- with Not_found ->
- false
-
-let global_reference id =
- constr_of_global (locate_reference (make_short_qualid id))
-
-let construct_reference ctx id =
- try
- Term.mkVar (let _ = Sign.lookup_named id ctx in id)
- with Not_found ->
- global_reference id
-
-let global_reference_in_absolute_module dir id =
- constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
+let interp_context ?(fail_anonymous=false) sigma env params =
+ interp_context_gen (Default.understand_type sigma)
+ (Default.understand_judgment sigma) ~fail_anonymous sigma env params
+let interp_context_evars ?(fail_anonymous=false) evdref env params =
+ interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+ (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:15:50 +0000