summaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml1303
1 files changed, 739 insertions, 564 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c8faf911..524448a6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,18 +1,19 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
+(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *)
open Pp
open Util
open Flags
open Names
open Nameops
+open Namegen
open Libnames
open Impargs
open Rawterm
@@ -24,73 +25,35 @@ 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 of identifier list (* list of params *)
+ | 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.implicit_status list *
+ (* subscopes of the args of the variable *)
+ scope_name option list
+
+type internalization_env =
+ (identifier * var_internalization_data) list
type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
let interning_grammar = ref false
(* Historically for parsing grammar rules, but in fact used only for
- translator, v7 parsing, and unstrict tactic internalisation *)
+ translator, v7 parsing, and unstrict tactic internalization *)
let for_grammar f x =
interning_grammar := true;
let a = f x in
@@ -98,9 +61,36 @@ let for_grammar f x =
a
(**********************************************************************)
-(* Internalisation errors *)
+(* 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))
+
+(**********************************************************************)
+(* Internalization errors *)
-type internalisation_error =
+type internalization_error =
| VariableCapture of identifier
| WrongExplicitImplicit
| IllegalMetavariable
@@ -110,7 +100,7 @@ type internalisation_error =
| BadPatternsNumber of int * int
| BadExplicitationNumber of explicitation * int option
-exception InternalisationError of loc * internalisation_error
+exception InternalizationError of loc * internalization_error
let explain_variable_capture id =
str "The variable " ++ pr_id id ++ str " occurs in its type"
@@ -126,7 +116,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,16 +133,16 @@ 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 =
+let explain_internalization_error e =
let pp = match e with
| VariableCapture id -> explain_variable_capture id
| WrongExplicitImplicit -> explain_wrong_explicit_implicit
@@ -164,13 +154,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 +164,31 @@ 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 compute_explicitable_implicit imps = function
+ | Inductive params ->
+ (* In inductive types, the parameters are fixed implicit arguments *)
+ let sub_impl,_ = list_chop (List.length params) imps in
+ let sub_impl' = List.filter is_status_implicit sub_impl in
+ List.map name_of_implicit sub_impl'
+ | Recursive | Method ->
+ (* Unable to know in advance what the implicit arguments will be *)
+ []
+
+let compute_internalization_data env ty typ impl =
+ let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in
+ let expls_impl = compute_explicitable_implicit impl ty in
+ (ty, expls_impl, impl, compute_arguments_scope typ)
+
+let compute_internalization_env env ty =
+ list_map3
+ (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+
+(**********************************************************************)
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
@@ -191,31 +201,31 @@ 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
(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
(* Remark: expansion of squash at definition is done in metasyntax.ml *)
-let contract_notation ntn (l,ll) =
+let contract_notation ntn (l,ll,bll) =
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 ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',(l,ll)
+ !ntn',(l,ll,bll)
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,133 +237,344 @@ 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 &
- 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.")
- else
- idscopes := Some (scopt,scopes)
+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 "]"
+
+let error_inconsistent_scope loc id scopes1 scopes2 =
+ user_err_loc (loc,"set_var_scope",
+ pr_id id ++ str " is used both in " ++
+ pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2)
+
+let error_expect_constr_notation_type loc id =
+ user_err_loc (loc,"",
+ pr_id id ++ str " is bound in the notation to a term variable.")
+
+let error_expect_binder_notation_type loc id =
+ user_err_loc (loc,"",
+ pr_id id ++
+ str " is expected to occur in binding position in the right-hand side.")
+
+let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
+ try
+ let idscopes,typ = List.assoc id ntnvars in
+ if !idscopes <> None &
+ (* scopes have no effect on the interpretation of identifiers, hence
+ we can tolerate having a variable occurring several times in
+ different scopes: *) typ <> NtnInternTypeIdent &
+ make_current_scope (Option.get !idscopes)
+ <> make_current_scope (scopt,scopes) then
+ error_inconsistent_scope loc id
+ (make_current_scope (Option.get !idscopes))
+ (make_current_scope (scopt,scopes))
+ else
+ idscopes := Some (scopt,scopes);
+ match typ with
+ | NtnInternTypeBinder ->
+ if istermvar then error_expect_binder_notation_type loc id
+ | NtnInternTypeConstr ->
+ (* We need sometimes to parse idents at a constr level for
+ factorization and we cannot enforce this constraint:
+ if not istermvar then error_expect_constr_notation_type loc id *)
+ ()
+ | NtnInternTypeIdent -> ()
+ with Not_found ->
+ (* Not in a notation *)
+ ()
+
+let set_type_scope (ids,unb,tmp_scope,scopes) =
+ (ids,unb,Some Notation.type_scope,scopes)
+
+let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
+ (ids,unb,None,scopes)
+
+let rec it_mkRProd env body =
+ match env with
+ (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+ | [] -> body
+
+let rec it_mkRLambda env body =
+ match env with
+ (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+ | [] -> body
+
+(**********************************************************************)
+(* Utilities for binders *)
+
+let check_capture loc ty = function
+ | Name id when occur_var_constr_expr id ty ->
+ raise (InternalizationError (loc,VariableCapture id))
+ | _ ->
+ ()
+
+let locate_if_isevar loc na = function
+ | RHole _ ->
+ (try match na with
+ | Name id -> Reserve.find_reserved_type id
+ | Anonymous -> raise Not_found
+ with Not_found -> RHole (loc, Evd.BinderType na))
+ | x -> x
+
+let check_hidden_implicit_parameters id (_,_,_,impls) =
+ if List.exists (function
+ | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
+ | _ -> false) impls
+ then
+ errorlabstrm "" (strbrk "A parameter of an inductive type " ++
+ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
+
+let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
+ function
+ | loc,Anonymous ->
+ if global_level then
+ user_err_loc (loc,"", str "Anonymous variables not allowed");
+ env
+ | loc,Name id ->
+ check_hidden_implicit_parameters id lvar;
+ set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars);
+ if global_level then Dumpglob.dump_definition (loc,id) true "var"
+ else Dumpglob.dump_binding loc id;
+ (Idset.add id ids,unb,tmpsc,scopes)
+
+let intern_generalized_binder ?(global_level=false) intern_type lvar
+ (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
+ 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.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
+ let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level 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 global_level then na
+ else
+ 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 Name name
+ | _ -> na
+ in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl
+
+let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function
+ | LocalRawAssum(nal,bk,ty) ->
+ (match bk with
+ | Default k ->
+ let (loc,na) = List.hd nal in
+ (* TODO: fail if several names with different implicit types *)
+ let ty = locate_if_isevar loc na (intern_type env ty) in
+ List.fold_left
+ (fun (env,bl) na ->
+ (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+ (env,bl) nal
+ | Generalized (b,b',t) ->
+ let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
+ env, b @ bl)
+ | LocalRawDef((loc,na as locna),def) ->
+ (push_name_env lvar env locna,
+ (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+
+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.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
+ || List.mem Notation.type_scope scopes -> true
+ | _ -> false
+ 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 ->
+ 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) ->
+ let env' = push_name_env lvar env (loc, Name id) in
+ (env', abs lid acc)) fvs (env,c)
+ in c'
+
+let iterate_binder intern lvar (env,bl) = function
+ | LocalRawAssum(nal,bk,ty) ->
+ let intern_type env = intern (set_type_scope env) in
+ (match bk with
+ | Default k ->
+ let (loc,na) = List.hd nal in
+ (* TODO: fail if several names with different implicit types *)
+ let ty = intern_type env ty in
+ let ty = locate_if_isevar loc na ty in
+ List.fold_left
+ (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+ (env,bl) nal
+ | Generalized (b,b',t) ->
+ let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
+ env, b @ bl)
+ | LocalRawDef((loc,na as locna),def) ->
+ (push_name_env lvar env locna,
+ (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
(**********************************************************************)
(* Syntax extensions *)
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
+let option_mem_assoc id = function
+ | Some (id',c) -> id = id'
+ | None -> false
+
+let find_fresh_name renaming (terms,termlists,binders) id =
+ let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) terms in
+ let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) termlists) in
+ let fvs3 = List.map snd renaming in
+ (* TODO binders *)
+ let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
+ next_ident_away id fvs
+
+let traverse_binder (terms,_,_ as subst)
+ (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 terms)) 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) *)
- let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
- let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in
- let fvs3 = List.map snd renaming in
- let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
- let id' = next_ident_away id fvs in
+ let id' = find_fresh_name renaming subst id 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
| x -> map_rawconstr (subst_iterator y t) x
-let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
- let (renaming,(ids,unb,_,scopes)) = infos in
- let subinfos = renaming,(ids,unb,None,scopes) in
- match c with
- | AVar id ->
+let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
+ let (terms,termlists,binders) = subst in
+ let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c =
+ let subinfos = renaming,(ids,unb,None,scopes) in
+ match c with
+ | AVar id ->
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
- let (a,(scopt,subscopes)) = List.assoc id subst in
- interp (ids,unb,scopt,subscopes@scopes) a
- with Not_found ->
- try
+ try
+ let (a,(scopt,subscopes)) = List.assoc id terms in
+ intern (ids,unb,scopt,subscopes@scopes) a
+ 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
+ | AList (x,_,iter,terminator,lassoc) ->
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (l,(scopt,subscopes)) = List.assoc x substlist in
- let termin =
- subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
- List.fold_right (fun a t ->
+ let (l,(scopt,subscopes)) = List.assoc x termlists in
+ let termin = aux subst' subinfos terminator in
+ List.fold_right (fun a t ->
subst_iterator ldots_var t
- (subst_aconstr_in_rawconstr loc interp
- ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
+ (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter))
(if lassoc then List.rev l else l) termin
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
- | 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 (((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
-
-let set_type_scope (ids,unb,tmp_scope,scopes) =
- (ids,unb,Some Notation.type_scope,scopes)
-
-let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
- (ids,unb,None,scopes)
-
-let rec it_mkRProd env body =
- match env with
- (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
- | [] -> body
-
-let rec it_mkRLambda env body =
- match env with
- (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
- | [] -> body
+ | AHole (Evd.BinderType (Name id as na)) ->
+ let na =
+ try snd (coerce_to_name (fst (List.assoc id terms)))
+ with Not_found -> na in
+ RHole (loc,Evd.BinderType na)
+ | ABinderList (x,_,iter,terminator) ->
+ (try
+ (* All elements of the list are in scopes (scopt,subscopes) *)
+ let (bl,(scopt,subscopes)) = List.assoc x binders in
+ let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in
+ let termin = aux subst' (renaming,env) terminator in
+ List.fold_left (fun t binder ->
+ subst_iterator ldots_var t
+ (aux (terms,Some(x,binder)) subinfos iter))
+ termin bl
+ with Not_found ->
+ anomaly "Inconsistent substitution of recursive notation")
+ | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
+ let (na,bk,_,t) = snd (Option.get binderopt) in
+ RProd (loc,na,bk,t,aux subst' infos c')
+ | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
+ let (na,bk,_,t) = snd (Option.get binderopt) in
+ RLambda (loc,na,bk,t,aux subst' infos c')
+ | t ->
+ rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+ (aux subst') subinfos t
+ in aux (terms,None) infos c
+
+let split_by_type ids =
+ List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
+ match typ with
+ | NtnTypeConstr -> ((x,scl)::l1,l2,l3)
+ | NtnTypeConstrList -> (l1,(x,scl)::l2,l3)
+ | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[])
+
+let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l
+
+let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs =
+ let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
+ let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+ Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
+ let ids,idsl,idsbl = split_by_type ids in
+ let terms = make_subst ids args in
+ let termlists = make_subst idsl argslist in
+ let binders = make_subst idsbl bll in
+ subst_aconstr_in_rawconstr loc intern lvar
+ (terms,termlists,binders) ([],env) c
(**********************************************************************)
(* Discriminating between bound variables and global references *)
-(* [vars1] is a set of name to avoid (used for the tactic language);
- [vars2] is the set of global variables, env is the set of variables
- abstracted until this point *)
-
let string_of_ty = function
- | Inductive -> "ind"
+ | Inductive _ -> "ind"
| Recursive -> "def"
| Method -> "meth"
-let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
- let (vars1,unbndltacvars) = ltacvars in
+let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id =
+ let (ltacvars,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
- (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+ let ty,expl_impls,impls,argsc = List.assoc id impls in
+ let expl_impls = List.map
+ (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
- Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
- RVar (loc,id), impl, argsc, l
+ Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
+ RVar (loc,id), make_implicits_list impls, argsc, expl_impls
with Not_found ->
- (* Is [id] bound in current env or is an ltac var bound to constr *)
- if Idset.mem id env or List.mem id vars1
+ (* Is [id] bound in current term or is an ltac var bound to constr *)
+ if Idset.mem id ids or List.mem id ltacvars
then
RVar (loc,id), [], [], []
(* Is [id] a notation variable *)
- else if List.mem_assoc id vars3
+ else if List.mem_assoc id ntnvars
+ then
+ (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], [])
+ (* Is [id] the special variable for recursive notations *)
+ else if ntnvars <> [] && id = ldots_var
then
- (set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
+ 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
@@ -362,18 +583,26 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
with Not_found ->
(* Is [id] a goal or section variable *)
- let _ = Sign.lookup_named id vars2 in
+ let _ = Sign.lookup_named id namedctxvars in
try
(* [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.map (drop_first_implicits n) (implicits_of_global ref),
+ list_skipn_at_least n (find_arguments_scope ref),[]
| x -> x,[],[],[]
let error_not_enough_arguments loc =
@@ -386,63 +615,65 @@ 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
+let intern_qualid loc qid intern env lvar args =
+ 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
+ let subst = make_subst ids (List.map fst args1) in
+ subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2
(* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env args =
- match intern_qualid loc qid intern env args with
+let intern_non_secvar_qualid loc qid intern env lvar args =
+ match intern_qualid loc qid intern env lvar args with
| RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
| r -> r
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
+ let r,args2 = intern_qualid loc qid intern env lvar args in
+ 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
+ let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
+ 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)
- (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r
+ (Idset.empty,false,None,[]) (vars,[],[],[]) [] r
in r
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,28 +704,28 @@ 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 =
match has_duplicate ids with
| Some id ->
- raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id))
+ raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
| None ->
()
(* Match the number of pattern against the number of matched args *)
let check_number_of_pattern loc n l =
let p = List.length l in
- if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
+ if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
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 +747,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 +756,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 +781,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 +800,42 @@ 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")
+ | AHole _ -> ([],[[], PatVar (loc,Anonymous)])
| 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
- with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
+ try locate_extended qid
+ with Not_found -> raise (InternalizationError (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,21 +849,21 @@ 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
let find_pattern_variable = function
| Ident (loc,id) -> id
- | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
+ | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
let maybe_constructor ref f aliases scopes =
try
@@ -636,24 +872,117 @@ let maybe_constructor ref f aliases scopes =
ConstrPat (c,idspl1)
with
(* patt var does not exists globally *)
- | InternalisationError _ -> VarPat (find_pattern_variable ref)
+ | InternalizationError _ -> VarPat (find_pattern_variable ref)
(* patt var also exists globally but does not satisfy preconditions *)
| (Environ.NotEvaluableConst _ | Not_found) ->
if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
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))
+ raise (InternalizationError (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 +998,10 @@ 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 (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+ let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
+ let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+ let (ids',idsl',_) = split_by_type ids' in
+ 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 +1010,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
@@ -707,133 +1036,24 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
(ids,List.flatten pl')
(**********************************************************************)
-(* Fix and CoFix *)
-
-(**********************************************************************)
-(* Utilities for binders *)
-
-let check_capture loc ty = function
- | Name id when occur_var_constr_expr id ty ->
- raise (InternalisationError (loc,VariableCapture id))
- | _ ->
- ()
-
-let locate_if_isevar loc na = function
- | RHole _ ->
- (try match na with
- | Name id -> Reserve.find_reserved_type id
- | Anonymous -> raise Not_found
- with Not_found -> RHole (loc, Evd.BinderType na))
- | x -> x
-
-let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
- if List.mem id indnames then
- errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
- 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 ->
- if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
- env
- | 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 ->
- if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
- env
- | 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
- 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 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
- else
- 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 Name name
- | _ -> na
- in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
-
-let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
- | LocalRawAssum(nal,bk,ty) ->
- (match bk with
- | Default k ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
- let ty = locate_if_isevar loc na (intern_type env ty) in
- List.fold_left
- (fun ((ids,unb,ts,sc),bl) (_,na) ->
- ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
- (env,bl) nal
- | Generalized (b,b',t) ->
- let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in
- env, b @ bl)
- | LocalRawDef((loc,na),def) ->
- ((name_fold Idset.add na ids,unb,ts,sc),
- (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
-
-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 =
- match ak with
- | Some AbsPi -> true
- | None when tmp_scope = Some Notation.type_scope
- || List.mem Notation.type_scope scopes -> true
- | _ -> false
- 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 ->
- 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) ->
- let env' = push_loc_name_env lvar env loc (Name id) in
- (env', abs lid acc)) fvs (env,c)
- in c'
-
-(**********************************************************************)
(* Utilities for application *)
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 +1062,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 +1089,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
@@ -887,7 +1107,7 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Main loop *)
-let internalise sigma globalenv env allow_patvar lvar c =
+let internalize sigma globalenv env allow_patvar lvar c =
let rec intern (ids,unb,tmp_scope,scopes as env) = function
| CRef ref as x ->
let (c,imp,subscopes,l),_ =
@@ -901,41 +1121,32 @@ let internalise sigma globalenv env allow_patvar lvar c =
let n =
try list_index0 iddef lf
with Not_found ->
- raise (InternalisationError (locid,UnboundFixName (false,iddef)))
+ raise (InternalizationError (locid,UnboundFixName (false,iddef)))
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 before, after = list_chop idx bl in
+ let intern_ro_arg f =
+ let before, after = split_at_annot bl n 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 n' = Option.map (fun _ -> List.length before) n in
+ let ro = f (intern (ids', unb, tmp_scope, scopes)) in
+ let n' = Option.map (fun _ -> List.length rbefore) 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,
@@ -947,7 +1158,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let n =
try list_index0 iddef lf
with Not_found ->
- raise (InternalisationError (locid,UnboundFixName (true,iddef)))
+ raise (InternalizationError (locid,UnboundFixName (true,iddef)))
in
let idl = Array.map
(fun (id,bl,ty,bd) ->
@@ -972,21 +1183,19 @@ let internalise sigma globalenv env allow_patvar lvar c =
intern env c2
| CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
- | CLetIn (loc,(loc1,na),c1,c2) ->
- 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 ->
+ | CLetIn (loc,na,c1,c2) ->
+ RLetIn (loc, snd na, intern (reset_tmp_scope env) c1,
+ intern (push_name_env lvar env na) c2)
+ | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
+ when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
- | CNotation (_,"( _ )",([a],[])) -> intern env a
+ | CNotation (_,"( _ )",([a],[],[])) -> intern env a
| CNotation (loc,ntn,args) ->
- intern_notation intern env loc ntn args
+ intern_notation intern env lvar loc ntn args
| 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 +1203,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
@@ -1004,50 +1214,30 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (c,impargs,args_scopes,l),args =
match f with
| 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
+ | CNotation (loc,ntn,([],[],[])) ->
+ let c = intern_notation intern env lvar loc ntn ([],[],[]) in
+ 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) ->
@@ -1063,7 +1253,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let p' = Option.map (fun p ->
let env'' = List.fold_left (push_name_env lvar) env ids in
intern_type env'' p) po in
- RLetTuple (loc, nal, (na', p'), b',
+ RLetTuple (loc, List.map snd nal, (na', p'), b',
intern (List.fold_left (push_name_env lvar) env nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
@@ -1072,12 +1262,12 @@ 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)
| CPatVar (loc, _) ->
- raise (InternalisationError (loc,IllegalMetavariable))
+ raise (InternalizationError (loc,IllegalMetavariable))
| CEvar (loc, n, l) ->
REvar (loc, n, Option.map (List.map (intern env)) l)
| CSort (loc, s) ->
@@ -1091,12 +1281,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 +1315,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
@@ -1138,62 +1328,61 @@ let internalise sigma globalenv env allow_patvar lvar c =
if List.length l <> nindargs then
error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
let nal = List.map (function
- | RHole loc -> Anonymous
- | RVar (_,id) -> Name id
+ | RHole (loc,_) -> loc,Anonymous
+ | RVar (loc,id) -> loc,Name id
| 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
+ if List.exists (fun (_,na) -> na <> Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
- realnal, Some (loc,ind,nparams,realnal)
- | None ->
+ realnal, Some (loc,ind,nparams,List.map snd realnal)
+ | None ->
[], None in
let na = match tm', na with
- | RVar (_,id), None when Idset.mem id vars -> Name id
- | RRef (loc, VarRef id), None -> Name id
- | _, None -> Anonymous
- | _, Some na -> na in
- (tm',(na,typ)), na::ids
-
+ | RVar (loc,id), None when Idset.mem id vars -> loc,Name id
+ | RRef (loc, VarRef id), None -> loc,Name id
+ | _, None -> dummy_loc,Anonymous
+ | _, Some (loc,na) -> loc,na in
+ (tm',(snd na,typ)), na::ids
+
and iterate_prod loc2 env bk ty body nal =
let rec default env bk = function
- | (loc1,na)::nal ->
+ | (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+ let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
RProd (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern_type env body
in
match bk with
| Default b -> default env b nal
- | Generalized (b,b',t) ->
- let env, ibind = intern_generalized_binder intern_type lvar
- env [] (List.hd nal) b b' t ty in
+ | 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
- | (loc1,na)::nal ->
+
+ and iterate_lam loc2 env bk ty body nal =
+ let rec default env bk = function
+ | (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+ let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
RLambda (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern env body
in match bk with
| Default b -> default env b nal
- | Generalized (b, b', t) ->
- let env, ibind = intern_generalized_binder intern_type lvar
- env [] (List.hd nal) b b' t ty in
+ | 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 l = select_impargs_size (List.length args) l in
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 +1393,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,52 +1416,50 @@ 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)
+ InternalizationError (loc,e) ->
+ user_err_loc (loc,"internalize",
+ explain_internalization_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=([],[]))
+ ?(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,[])
+ internalize 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
- InternalisationError (loc,e) ->
- user_err_loc (loc,"internalize",explain_internalisation_error e)
-
+ intern_cases_pattern env [] ([],[]) None patt
+ with
+ InternalizationError (loc,e) ->
+ user_err_loc (loc,"internalize",explain_internalization_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
- ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+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
Default.understand_gen kind sigma env c
@@ -1280,73 +1467,88 @@ let interp_gen kind sigma env
let interp_constr sigma env c =
interp_gen (OfType None) sigma env c
-let interp_type sigma env ?(impls=([],[])) c =
+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
+let interp_casted_constr sigma env ?(impls=[]) c typ =
+ 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
- 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 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
- env ?(impls=([],[])) c typ =
- interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
+let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
+ env ?(impls=[]) kind c =
+ let evdref =
+ match evdref with
+ | None -> ref Evd.empty
+ | Some evdref -> evdref
+ in
+ let istype = kind = IsType in
+ let c = intern_gen istype ~impls !evdref env c in
+ let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in
+ Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
+
+let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
+ env ?(impls=[]) c typ =
+ 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_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+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
-let interp_type_evars evdref env ?(impls=([],[])) c =
+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 recvars 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
+ let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
+ let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, [])
+ 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
+ let a = aconstr_of_rawconstr vars recvars c in
+ (* Splits variables into those that are binding, bound, or both *)
+ (* binding and bound *)
+ let out_scope = function None -> None,[] | Some (a,l) -> a,l in
+ let vars = List.map (fun (id,(sc,typ)) -> (id,(out_scope !sc,typ))) vl 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) ->
- (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
- list_chop (List.length vars) vl, a
+ vars, a
(* Interpret binders and contexts *)
@@ -1356,7 +1558,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'
@@ -1364,17 +1566,17 @@ open Environ
open Term
let my_intern_constr sigma env lvar acc c =
- internalise sigma env acc false lvar c
+ internalize sigma env acc false lvar c
let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-let intern_context fail_anonymous sigma env params =
- let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
+let intern_context global_level sigma env params =
+ let lvar = (([],[]),Environ.named_context env, [], []) in
snd (List.fold_left
- (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
+ (intern_local_binder_aux ~global_level (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 +1585,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 +1599,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 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
-
-let is_global id =
- try
- let _ = locate_reference (make_short_qualid id) in true
- with Not_found ->
- false
+let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params =
+ let bl = intern_context global_level sigma env params in
+ interp_rawcontext_gen understand_type understand_judgment env bl
-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 ?(global_level=false) sigma env params =
+ interp_context_gen (Default.understand_type sigma)
+ (Default.understand_judgment sigma) ~global_level sigma env params
+let interp_context_evars ?(global_level=false) evdref env params =
+ interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+ (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:14:01 +0000