summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /interp
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml65
-rw-r--r--interp/constrextern.mli2
-rw-r--r--interp/constrintern.ml704
-rw-r--r--interp/constrintern.mli73
-rw-r--r--interp/coqlib.ml5
-rw-r--r--interp/coqlib.mli8
-rw-r--r--interp/dumpglob.ml9
-rw-r--r--interp/dumpglob.mli3
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/genarg.mli2
-rw-r--r--interp/implicit_quantifiers.ml39
-rw-r--r--interp/implicit_quantifiers.mli4
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/modintern.mli2
-rw-r--r--interp/notation.ml5
-rw-r--r--interp/notation.mli2
-rw-r--r--interp/ppextend.ml3
-rw-r--r--interp/ppextend.mli3
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/syntax_def.ml6
-rw-r--r--interp/syntax_def.mli2
-rw-r--r--interp/topconstr.ml588
-rw-r--r--interp/topconstr.mli76
24 files changed, 948 insertions, 661 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 77a79883..b2b21925 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
(*i*)
open Pp
@@ -178,9 +178,10 @@ let rec check_same_type ty1 ty2 =
check_same_type b1 b2
| CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
check_same_type a1 a2
- | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+ | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when n1=n2 ->
List.iter2 check_same_type e1 e2;
- List.iter2 (List.iter2 check_same_type) el1 el2
+ List.iter2 (List.iter2 check_same_type) el1 el2;
+ List.iter2 check_same_fix_binder bl1 bl2
| CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
check_same_type e1 e2
@@ -287,7 +288,7 @@ and spaces ntn n =
if n = String.length ntn then []
else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-let expand_curly_brackets loc mknot ntn (l,ll) =
+let expand_curly_brackets loc mknot ntn l =
let ntn' = ref ntn in
let rec expand_ntn i =
function
@@ -300,12 +301,12 @@ let expand_curly_brackets loc mknot ntn (l,ll) =
ntn' :=
String.sub !ntn' 0 p ^ "_" ^
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
- mknot (loc,"{ _ }",([a],[])) end
+ mknot (loc,"{ _ }",[a]) end
else a in
a' :: expand_ntn (i+1) l in
let l = expand_ntn 0 l in
(* side effect *)
- mknot (loc,!ntn',(l,ll))
+ mknot (loc,!ntn',l)
let destPrim = function CPrim(_,t) -> Some t | _ -> None
let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -313,32 +314,34 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
then expand_curly_brackets loc mknot ntn l
- else match ntn,List.map destprim (fst l),(snd l) with
+ else match ntn,List.map destprim l with
(* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
- | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
- mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
+ | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
+ mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
| _ ->
match decompose_notation_key ntn, l with
- | [Terminal "-"; Terminal x], ([],[]) ->
+ | [Terminal "-"; Terminal x], [] ->
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- with _ -> mknot (loc,ntn,([],[])))
- | [Terminal x], ([],[]) ->
+ with _ -> mknot (loc,ntn,[]))
+ | [Terminal x], [] ->
(try mkprim (loc, Numeral (Bigint.of_string x))
- with _ -> mknot (loc,ntn,([],[])))
+ with _ -> mknot (loc,ntn,[]))
| _ ->
mknot (loc,ntn,l)
-let make_notation loc ntn l =
+let make_notation loc ntn (terms,termlists,binders as subst) =
+ if termlists <> [] or binders <> [] then CNotation (loc,ntn,subst) else
make_notation_gen loc ntn
- (fun (loc,ntn,l) -> CNotation (loc,ntn,l))
+ (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
(fun (loc,p) -> CPrim (loc,p))
- destPrim l
+ destPrim terms
-let make_pat_notation loc ntn l =
+let make_pat_notation loc ntn (terms,termlists as subst) =
+ if termlists <> [] then CPatNotation (loc,ntn,subst) else
make_notation_gen loc ntn
- (fun (loc,ntn,l) -> CPatNotation (loc,ntn,l))
+ (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[])))
(fun (loc,p) -> CPatPrim (loc,p))
- destPatPrim l
+ destPatPrim terms
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -686,10 +689,10 @@ let rec extern inctx scopes vars r =
let na' = match na,tm with
Anonymous, RVar (_,id) when
rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
- -> Some Anonymous
+ -> Some (dummy_loc,Anonymous)
| Anonymous, _ -> None
| Name id, RVar (_,id') when id=id' -> None
- | Name _, _ -> Some na in
+ | Name _, _ -> Some (dummy_loc,na) in
(sub_extern false scopes vars tm,
(na',Option.map (fun (loc,ind,n,nal) ->
let params = list_tabulate
@@ -703,15 +706,15 @@ let rec extern inctx scopes vars r =
CCases (loc,sty,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
- CLetTuple (loc,nal,
- (Option.map (fun _ -> na) typopt,
+ CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
+ (Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
- (Option.map (fun _ -> na) typopt,
+ (Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
@@ -836,7 +839,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
- let subst,substlist = match_aconstr t pat in
+ let terms,termlists,binders = match_aconstr t pat in
(* Try availability of interpretation ... *)
let e =
match keyrule with
@@ -851,17 +854,21 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern (* assuming no overloading: *) true
(scopt,scl@scopes') vars c)
- subst in
+ terms in
let ll =
List.map (fun (c,(scopt,scl)) ->
List.map (extern true (scopt,scl@scopes') vars) c)
- substlist in
- insert_delimiters (make_notation loc ntn (l,ll)) key)
+ termlists in
+ let bll =
+ List.map (fun (bl,(scopt,scl)) ->
+ snd (extern_local_binder (scopt,scl@scopes') vars bl))
+ binders in
+ insert_delimiters (make_notation loc ntn (l,ll,bll)) key)
| SynDefRule kn ->
let l =
List.map (fun (c,(scopt,scl)) ->
extern true (scopt,scl@scopes) vars c, None)
- subst in
+ terms in
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
if l = [] then a else CApp (loc,(None,a),l) in
if args = [] then e
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 5f170bdc..248abeda 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: constrextern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Util
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0fed211d..3bf556f1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -28,7 +28,10 @@ open Inductiveops
(* 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_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
@@ -45,19 +48,12 @@ type var_internalization_data =
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)
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
@@ -92,9 +88,9 @@ let global_reference_in_absolute_module dir id =
constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
(**********************************************************************)
-(* Internalisation errors *)
+(* Internalization errors *)
-type internalisation_error =
+type internalization_error =
| VariableCapture of identifier
| WrongExplicitImplicit
| IllegalMetavariable
@@ -104,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"
@@ -146,7 +142,7 @@ let explain_bad_explicitation_number n po =
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
@@ -171,30 +167,26 @@ let error_inductive_parameter_not_implicit loc =
(* Pre-computing the implicit arguments and arguments scopes needed *)
(* for interpretation *)
-let empty_internalization_env = ([],[])
+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
+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 *)
@@ -216,18 +208,18 @@ let expand_notation_string ntn n =
(* 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
@@ -250,43 +242,219 @@ let make_current_scope = function
| (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
- 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 " 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)
+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 &
+ 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))=
+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 _,na = coerce_to_name (fst (List.assoc id subst)) in
+ 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), Name id'
@@ -294,17 +462,18 @@ 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
+ 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)
@@ -312,83 +481,96 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
(* Happens for local notation joint with inductive/fixpoint defs *)
RVar (loc,id)
end
- | AList (x,_,iter,terminator,lassoc) ->
+ | 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
+ 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 ->
anomaly "Inconsistent substitution of recursive notation")
- | AHole (Evd.BinderType (Name id as na)) ->
+ | AHole (Evd.BinderType (Name id as na)) ->
let na =
- try snd (coerce_to_name (fst (List.assoc id subst)))
+ try snd (coerce_to_name (fst (List.assoc id terms)))
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 as fullargs) = contract_notation ntn fullargs in
- let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+ | 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 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
+ 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), 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
@@ -398,7 +580,7 @@ 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 *)
@@ -443,7 +625,7 @@ let intern_reference ref =
(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 =
+let intern_qualid loc qid intern env lvar args =
match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
RRef (loc, ref), args
@@ -453,25 +635,25 @@ let intern_qualid loc qid intern env args =
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
+ 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
+ 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 = qualid_of_ident id in
try
- let r,args2 = intern_non_secvar_qualid loc qid intern env args in
+ 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 *)
@@ -482,7 +664,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
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
@@ -529,14 +711,14 @@ let loc_of_lhs 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
@@ -646,7 +828,7 @@ let find_constructor ref f aliases pats scopes =
let (loc,qid) = qualid_of_reference ref in
let gref =
try locate_extended qid
- with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
+ with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in
match gref with
| SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
@@ -677,7 +859,7 @@ let find_constructor ref f aliases pats scopes =
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
@@ -686,7 +868,7 @@ 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 ++
@@ -696,7 +878,7 @@ let maybe_constructor ref f aliases 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*)
@@ -813,7 +995,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
intern_pat scopes aliases tmp_scope a
| CPatNotation (loc, ntn, fullargs) ->
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
+ 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
@@ -849,116 +1032,6 @@ 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 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_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.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_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 =
@@ -1030,7 +1103,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),_ =
@@ -1044,17 +1117,16 @@ 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 f =
- let idx = Option.default 0 (index_of_annot bl n) in
- let before, after = list_chop idx bl in
+ 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 = f (intern (ids', unb, tmp_scope, scopes)) in
- let n' = Option.map (fun _ -> List.length before) n 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) =
@@ -1082,7 +1154,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) ->
@@ -1107,15 +1179,15 @@ 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)],[]))
+ | 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) ->
@@ -1138,8 +1210,8 @@ 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
+ | 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 =
@@ -1177,7 +1249,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
@@ -1191,7 +1263,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| 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) ->
@@ -1252,27 +1324,27 @@ 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)
+ 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
@@ -1280,24 +1352,22 @@ let internalise sigma globalenv env allow_patvar lvar c =
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
+ 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 ->
+ | (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
+ 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
@@ -1345,9 +1415,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
try
intern env c
with
- InternalisationError (loc,e) ->
+ InternalizationError (loc,e) ->
user_err_loc (loc,"internalize",
- explain_internalisation_error e)
+ explain_internalization_error e)
(**************************************************************************)
(* Functions to translate constr_expr into rawconstr *)
@@ -1359,11 +1429,11 @@ let extract_ids env =
Idset.empty
let intern_gen isarity sigma env
- ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
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
@@ -1374,8 +1444,8 @@ 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)
+ InternalizationError (loc,e) ->
+ user_err_loc (loc,"internalize",explain_internalization_error e)
type manual_implicits = (explicitation * (bool * bool * bool)) list
@@ -1384,7 +1454,7 @@ 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=([],[]))
+ ?(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
@@ -1392,10 +1462,10 @@ 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 =
+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 =
@@ -1423,34 +1493,35 @@ let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
- env ?(impls=([],[])) kind c =
+ env ?(impls=[]) kind c =
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
+ 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 =
+ env ?(impls=[]) c typ =
interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(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 ?(fail_evar=true) env ?(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 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 =
+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
type ltac_sign = identifier list * unbound_ltac_var_map
@@ -1459,19 +1530,20 @@ 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, [])
+ 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 *)
@@ -1489,14 +1561,14 @@ 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_rawcontext_gen understand_type understand_judgment env bl =
@@ -1522,15 +1594,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params =
- let bl = intern_context fail_anonymous sigma env params in
+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 interp_context ?(fail_anonymous=false) sigma env params =
+let interp_context ?(global_level=false) sigma env params =
interp_context_gen (Default.understand_type sigma)
- (Default.understand_judgment sigma) ~fail_anonymous sigma env params
+ (Default.understand_judgment sigma) ~global_level sigma env params
-let interp_context_evars ?(fail_anonymous=false) evdref 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) ~fail_anonymous !evdref env params
+ (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index ebee4eda..acb13a8b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
(*i*)
open Names
@@ -30,45 +30,45 @@ open Pretyping
- check all variables are bound
- make absolute the references to global objets
- resolution of symbolic notations using scopes
- - insert existential variables for implicit arguments
+ - insertion of implicit arguments
*)
-(* To interpret implicits and arg scopes of recursive variables while
- internalizing inductive types and recursive definitions, and also
+(* To interpret implicit arguments and arg scopes of recursive variables
+ while internalizing inductive types and recursive definitions, and also
projection while typing records.
the third and fourth arguments associate a list of implicit
positions and scopes to identifiers declared in the [rel_context]
of [env] *)
-type var_internalization_type = Inductive | Recursive | Method
+type var_internalization_type =
+ | Inductive of identifier list (* list of params *)
+ | Recursive
+ | Method
type var_internalization_data =
var_internalization_type *
+ (* type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
identifier list *
- Impargs.implicits_list *
- scope_name option list
+ (* 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) *)
+ Impargs.implicits_list * (* signature of impargs of the variable *)
+ scope_name option list (* subscopes of the args of the variable *)
(* A map of free variables to their implicit arguments and scopes *)
type internalization_env =
(identifier * var_internalization_data) list
(* Contains also a list of identifiers to automatically apply to the variables*)
-type full_internalization_env =
- identifier list * internalization_env
-
-val empty_internalization_env : full_internalization_env
+val empty_internalization_env : internalization_env
val compute_internalization_data : env -> var_internalization_type ->
types -> Impargs.manual_explicitation list -> var_internalization_data
-val set_internalization_env_params :
- internalization_env -> identifier list -> full_internalization_env
-
-val compute_full_internalization_env : env ->
- var_internalization_type ->
- identifier list -> identifier list -> types list ->
- Impargs.manual_explicitation list list -> full_internalization_env
+val compute_internalization_env : env -> var_internalization_type ->
+ identifier list -> types list -> Impargs.manual_explicitation list list ->
+ internalization_env
type manual_implicits = (explicitation * (bool * bool * bool)) list
@@ -83,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
val intern_type : evar_map -> env -> constr_expr -> rawconstr
val intern_gen : bool -> evar_map -> env ->
- ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+ ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> rawconstr
val intern_pattern : env -> cases_pattern_expr ->
@@ -97,7 +97,7 @@ val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder
(* Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
- ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+ ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
(* Particular instances *)
@@ -105,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env ->
val interp_constr : evar_map -> env ->
constr_expr -> constr
-val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
- constr_expr -> types
+val interp_type : evar_map -> env -> ?impls:internalization_env ->
+ constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr
-val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
constr_expr -> types -> constr
(* Accepting evars and giving back the manual implicits in addition. *)
val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
- ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
+ ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
- env -> ?impls:full_internalization_env ->
+ env -> ?impls:internalization_env ->
constr_expr -> types * manual_implicits
val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
- env -> ?impls:full_internalization_env ->
+ env -> ?impls:internalization_env ->
constr_expr -> constr * manual_implicits
val interp_casted_constr_evars : evar_map ref -> env ->
- ?impls:full_internalization_env -> constr_expr -> types -> constr
+ ?impls:internalization_env -> constr_expr -> types -> constr
-val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env ->
+val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
constr_expr -> types
(*s Build a judgment *)
@@ -160,13 +160,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
val interp_context_gen : (env -> rawconstr -> types) ->
(env -> rawconstr -> unsafe_judgment) ->
- ?fail_anonymous:bool ->
+ ?global_level:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context : ?fail_anonymous:bool ->
+val interp_context : ?global_level:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context_evars : ?fail_anonymous:bool ->
+val interp_context_evars : ?global_level:bool ->
evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
@@ -177,10 +177,15 @@ val construct_reference : named_context -> identifier -> constr
val global_reference : identifier -> constr
val global_reference_in_absolute_module : dir_path -> identifier -> constr
-(* Interprets into a abbreviatable constr *)
+(* Interprets a term as the left-hand side of a notation; the boolean
+ list is a set and this set is [true] for a variable occurring in
+ term position, [false] for a variable occurring in binding
+ position; [true;false] if in both kinds of position *)
-val interp_aconstr : ?impls:full_internalization_env ->
- identifier list * identifier list -> constr_expr -> interpretation
+val interp_aconstr : ?impls:internalization_env ->
+ (identifier * notation_var_internalization_type) list ->
+ (identifier * identifier) list -> constr_expr ->
+ (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index dbec915d..0848ccc7 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: coqlib.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Util
open Pp
@@ -182,14 +182,11 @@ type coq_bool_data = {
andb_prop : constr;
andb_true_intro : constr}
-type 'a delayed = unit -> 'a
-
let build_bool_type () =
{ andb = init_constant ["Datatypes"] "andb";
andb_prop = init_constant ["Datatypes"] "andb_prop";
andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
-
let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 12791139..81cc3baa 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: coqlib.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Names
@@ -14,6 +14,7 @@ open Libnames
open Nametab
open Term
open Pattern
+open Util
(*i*)
(*s This module collects the global references, constructions and
@@ -86,9 +87,8 @@ val glob_jmeq : global_reference
at compile time. Therefore, we can only provide methods to build
them at runtime. This is the purpose of the [constr delayed] and
[constr_pattern delayed] types. Objects of this time needs to be
- applied to [()] to get the actual constr or pattern at runtime *)
-
-type 'a delayed = unit -> 'a
+ forced with [delayed_force] to get the actual constr or pattern
+ at runtime. *)
type coq_bool_data = {
andb : constr;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index ec02146e..0a42b78b 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *)
(* Dump of globalization (to be used by coqdoc) *)
@@ -161,13 +161,6 @@ let dump_name (loc, n) sec ty =
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
-let dump_local_binder b sec ty =
- if dump () then
- match b with
- | Topconstr.LocalRawAssum (nl, _, _) ->
- List.iter (fun x -> dump_name x sec ty) nl
- | Topconstr.LocalRawDef _ -> ()
-
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 2d5b1468..049bad5a 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: dumpglob.mli 13328 2010-07-26 11:05:30Z herbelin $ *)
val open_glob_file : string -> unit
@@ -39,7 +39,6 @@ val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation
val dump_binding : Util.loc -> Names.Idset.elt -> unit
val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit
-val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index a6a042d6..310420aa 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: genarg.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/interp/genarg.mli b/interp/genarg.mli
index f410e1ed..9c9096bb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: genarg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Util
open Names
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 73e3910a..22075654 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: implicit_quantifiers.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Names
@@ -93,7 +93,7 @@ let is_freevar ids env x =
with _ -> not (is_global x)
with _ -> true
-(* Auxilliary functions for the inference of implicitly quantified variables. *)
+(* Auxiliary functions for the inference of implicitly quantified variables. *)
let ungeneralizable loc id =
user_err_loc (loc, "Generalization",
@@ -110,7 +110,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
in
let rec aux bdvars l c = match c with
| CRef (Ident (loc,id)) -> found loc id bdvars l
- | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
+ | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) ->
fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
| c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
in aux bound l c
@@ -297,19 +297,28 @@ let implicit_application env ?(allow_partial=true) f ty =
CAppExpl (loc, (None, id), args), avoid
in c, avoid
-let implicits_of_rawterm l =
+let implicits_of_rawterm ?(with_products=true) l =
let rec aux i c =
- match c with
- RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
- let rest = aux (succ i) b in
- if bk = Implicit then
- let name =
- match na with
- Name id -> Some id
- | Anonymous -> None
- in
- (ExplByPos (i, name), (true, true, true)) :: rest
- else rest
+ let abs loc na bk t b =
+ let rest = aux (succ i) b in
+ if bk = Implicit then
+ let name =
+ match na with
+ | Name id -> Some id
+ | Anonymous -> None
+ in
+ (ExplByPos (i, name), (true, true, true)) :: rest
+ else rest
+ in
+ match c with
+ | RProd (loc, na, bk, t, b) ->
+ if with_products then abs loc na bk t b
+ else
+ (if bk = Implicit then
+ msg_warning (str "Ignoring implicit status of product binder " ++
+ pr_name na ++ str " and following binders");
+ [])
+ | RLambda (loc, na, bk, t, b) -> abs loc na bk t b
| RLetIn (loc, na, t, b) -> aux i b
| _ -> []
in aux 1 l
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 315541e2..b8f6594a 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: implicit_quantifiers.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Names
@@ -46,7 +46,7 @@ val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
val combine_params_freevar :
Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/modintern.ml b/interp/modintern.ml
index f414adab..bed5597e 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: modintern.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 304db5be..1cf8a5bd 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: modintern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Declarations
diff --git a/interp/notation.ml b/interp/notation.ml
index 4a89dbd7..fe9d8b6d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
(*i*)
open Util
@@ -209,7 +209,8 @@ let cases_pattern_key = function
let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
- | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args)
+ | AList (_,_,AApp (ARef ref,args),_,_)
+ | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args)
| ARef ref -> RefKey(make_gr ref), None
| _ -> Oth, None
diff --git a/interp/notation.mli b/interp/notation.mli
index 533ccb76..72b576eb 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: notation.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Util
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 653aefed..618f8320 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ *)
+(*i $Id: ppextend.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
(*i*)
open Pp
@@ -53,6 +53,7 @@ let ppcmd_of_cut = function
type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
+ | UnpBinderListMetaVar of int * bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing list
| UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 7b988786..6c386162 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: ppextend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
(*i*)
open Pp
@@ -43,6 +43,7 @@ val ppcmd_of_cut : ppcut -> std_ppcmds
type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
+ | UnpBinderListMetaVar of int * bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing list
| UnpCut of ppcut
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7f9b35a6..2225bb6e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: reserve.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Reserved names *)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index e1853a74..613ba830 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: reserve.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Util
open Names
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index e6bb468e..77b34d4f 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: syntax_def.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
open Util
open Pp
@@ -76,8 +76,8 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr
(* Coercions to the general format of notation that also supports
variables bound to list of expressions *)
-let in_pat (ids,ac) = ((ids,[]),ac)
-let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
+let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
+let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 49e74b65..33d4c5d3 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: syntax_def.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Util
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5911f667..b8a90088 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: topconstr.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
(*i*)
open Pp
@@ -36,6 +36,7 @@ type aconstr =
(* Part only in rawconstr *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
+ | ABinderList of identifier * identifier * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
@@ -50,6 +51,21 @@ type aconstr =
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+type notation_var_instance_type =
+ | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+
+type notation_var_internalization_type =
+ | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+
+type interpretation =
+ (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
@@ -69,6 +85,16 @@ let rec cases_pattern_fold_map loc g e = function
let rec subst_rawvars l = function
| RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
+ | RProd (loc,Name id,bk,t,c) ->
+ let id =
+ try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+ with Not_found -> id in
+ RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
+ | RLambda (loc,Name id,bk,t,c) ->
+ let id =
+ try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+ with Not_found -> id in
+ RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
| r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *)
let ldots_var = id_of_string ".."
@@ -82,6 +108,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
subst_rawvars outerl it
+ | ABinderList (x,y,iter,tail) ->
+ let t = f e tail in let it = f e iter in
+ let innerl = [(ldots_var,t);(x,RVar(loc,y))] in
+ let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
+ let outerl = [(ldots_var,inner)] in
+ subst_rawvars outerl it
| ALambda (na,ty,c) ->
let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
| AProd (na,ty,c) ->
@@ -134,72 +166,135 @@ let rec rawconstr_of_aconstr loc x =
(****************************************************************************)
(* Translating a rawconstr into a notation, interpreting recursive patterns *)
-let add_name r = function
- | Anonymous -> ()
- | Name id -> r := id :: !r
+let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
+let add_name r = function Anonymous -> () | Name id -> add_id r id
-let has_ldots =
- List.exists
- (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
-
-let compare_rawconstr f t1 t2 = match t1,t2 with
- | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2
- | RVar (_,v1), RVar (_,v2) -> v1 = v2
- | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
- | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
- f ty1 ty2 & f c1 c2
+let split_at_recursive_part c =
+ let sub = ref None in
+ let rec aux = function
+ | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var ->
+ if !sub <> None then
+ (* Not narrowed enough to find only one recursive part *)
+ raise Not_found
+ else
+ (sub := Some c;
+ if l = [] then RVar (loc,ldots_var)
+ else RApp (loc0,RVar (loc,ldots_var),l))
+ | c -> map_rawconstr aux c in
+ let outer_iterator = aux c in
+ match !sub with
+ | None -> (* No recursive pattern found *) raise Not_found
+ | Some c ->
+ match outer_iterator with
+ | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found
+ | _ -> outer_iterator, c
+
+let on_true_do b f c = if b then (f c; b) else b
+
+let compare_rawconstr f add t1 t2 = match t1,t2 with
+ | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2
+ | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
+ | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
+ | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
| RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
- f ty1 ty2 & f c1 c2
+ on_true_do (f ty1 ty2 & f c1 c2) add na1
| RHole _, RHole _ -> true
| RSort (_,s1), RSort (_,s2) -> s1 = s2
- | (RLetIn _ | RCases _ | RRec _ | RDynamic _
+ | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 ->
+ on_true_do (f b1 b2 & f c1 c2) add na1
+ | (RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
- | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
+ | _,(RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
-> error "Unsupported construction in recursive notations."
- | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
+ | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _
+ | RHole _ | RSort _ | RLetIn _), _
-> false
-let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
+let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2
+
+let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1)
-let discriminate_patterns foundvars nl l1 l2 =
+let check_is_hole id = function RHole _ -> () | t ->
+ user_err_loc (loc_of_rawconstr t,"",
+ strbrk "In recursive notation with binders, " ++ pr_id id ++
+ strbrk " is expected to come without type.")
+
+let compare_recursive_parts found f (iterator,subc) =
let diff = ref None in
- let rec aux n c1 c2 = match c1,c2 with
- | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
- if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
- else
- !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
- or (error
- "Both ends of the recursive pattern differ in more than one place")
- | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
- let l = list_map2_i aux 0 l1 l2 in
- if not (List.for_all ((=) true) l) then
- error "Both ends of the recursive pattern differ.";
- match !diff with
- | None -> error "Both ends of the recursive pattern are the same."
- | Some (x,y,_ as discr) ->
- List.iter (fun id ->
- if List.mem id !foundvars
- then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part.");
- foundvars := id::!foundvars) [x;y];
- discr
+ let terminator = ref None in
+ let rec aux c1 c2 = match c1,c2 with
+ | RVar(_,v), term when v = ldots_var ->
+ (* We found the pattern *)
+ assert (!terminator = None); terminator := Some term;
+ true
+ | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var ->
+ (* We found the pattern, but there are extra arguments *)
+ (* (this allows e.g. alternative (recursive) notation of application) *)
+ assert (!terminator = None); terminator := Some term;
+ list_for_all2eq aux l1 l2
+ | RVar (_,x), RVar (_,y) when x<>y ->
+ (* We found the position where it differs *)
+ let lassoc = (!terminator <> None) in
+ let x,y = if lassoc then y,x else x,y in
+ !diff = None && (diff := Some (x,y,Some lassoc); true)
+ | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term)
+ | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) ->
+ (* We found a binding position where it differs *)
+ check_is_hole y t_x;
+ check_is_hole y t_y;
+ !diff = None && (diff := Some (x,y,None); aux c term)
+ | _ ->
+ compare_rawconstr aux (add_name found) c1 c2 in
+ if aux iterator subc then
+ match !diff with
+ | None ->
+ let loc1 = loc_of_rawconstr iterator in
+ let loc2 = loc_of_rawconstr (Option.get !terminator) in
+ (* Here, we would need a loc made of several parts ... *)
+ user_err_loc (subtract_loc loc1 loc2,"",
+ str "Both ends of the recursive pattern are the same.")
+ | Some (x,y,Some lassoc) ->
+ let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+ let iterator =
+ f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator
+ else iterator) in
+ (* found have been collected by compare_constr *)
+ found := newfound;
+ AList (x,y,iterator,f (Option.get !terminator),lassoc)
+ | Some (x,y,None) ->
+ let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
+ let iterator = f iterator in
+ (* found have been collected by compare_constr *)
+ found := newfound;
+ ABinderList (x,y,iterator,f (Option.get !terminator))
+ else
+ raise Not_found
let aconstr_and_vars_of_rawconstr a =
- let found = ref [] in
- let rec aux = function
- | RVar (_,id) -> found := id::!found; AVar id
- | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
- | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
- (* Special case for alternative (recursive) notation of application *)
- let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
- found := ldots_var :: !found; assert lassoc;
- AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
+ let found = ref ([],[],[]) in
+ let rec aux c =
+ let keepfound = !found in
+ (* n^2 complexity but small and done only once per notation *)
+ try compare_recursive_parts found aux' (split_at_recursive_part c)
+ with Not_found ->
+ found := keepfound;
+ match c with
+ | RApp (_,RVar (loc,f),[c]) when f = ldots_var ->
+ (* Fall on the second part of the recursive pattern w/o having
+ found the first part *)
+ user_err_loc (loc,"",
+ str "Cannot find where the recursive pattern starts.")
+ | c ->
+ aux' c
+ and aux' = function
+ | RVar (_,id) -> add_id found id; AVar id
| RApp (_,g,args) -> AApp (aux g, List.map aux args)
| RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
| RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
| RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
| RCases (_,sty,rtntypopt,tml,eqnl) ->
- let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
+ let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
ACases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
@@ -215,7 +310,7 @@ let aconstr_and_vars_of_rawconstr a =
add_name found na;
AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
| RRec (_,fk,idl,dll,tl,bl) ->
- Array.iter (fun id -> found := id::!found) idl;
+ Array.iter (add_id found) idl;
let dll = Array.map (List.map (fun (na,bk,oc,b) ->
if bk <> Explicit then
error "Binders marked as implicit not allowed in notations.";
@@ -231,51 +326,61 @@ let aconstr_and_vars_of_rawconstr a =
| RDynamic _ | REvar _ ->
error "Existential variables not allowed in notations."
- (* Recognizing recursive notations *)
- and terminator_of_pat f1 ll1 lr1 = function
- | RApp (loc,f2,l2) ->
- if not (eq_rawconstr f1 f2) then errorlabstrm ""
- (strbrk "Cannot recognize the same head to both ends of the recursive pattern.");
- let nl = List.length ll1 in
- let nr = List.length lr1 in
- if List.length l2 <> nl + nr + 1 then
- error "Both ends of the recursive pattern have different lengths.";
- let ll2,l2' = list_chop nl l2 in
- let t = List.hd l2' and lr2 = List.tl l2' in
- let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
- let iter =
- if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
- else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
- (if order then y else x),(if order then x else y), aux iter, aux t, order
- | _ -> error "One end of the recursive pattern is not an application."
-
- and make_aconstr_list f args =
- let rec find_patterns acc = function
- | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
- (* We've found the recursive part *)
- let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
- AList (x,y,iter,term,lassoc)
- | a::l -> find_patterns (a::acc) l
- | [] -> error "Ill-formed recursive notation."
- in find_patterns [] args
-
in
let t = aux a in
(* Side effect *)
t, !found
-let aconstr_of_rawconstr vars a =
- let a,foundvars = aconstr_and_vars_of_rawconstr a in
- let check_type x =
- if not (List.mem x foundvars) then
- error ((string_of_id x)^" is unbound in the right-hand-side.") in
- List.iter check_type vars;
+let rec list_rev_mem_assoc x = function
+ | [] -> false
+ | (_,x')::l -> x = x' || list_rev_mem_assoc x l
+
+let check_variables vars recvars (found,foundrec,foundrecbinding) =
+ let useless_vars = List.map snd recvars in
+ let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in
+ let check_recvar x =
+ if List.mem x found then
+ errorlabstrm "" (pr_id x ++
+ strbrk " should only be used in the recursive part of a pattern.") in
+ List.iter (fun (x,y) -> check_recvar x; check_recvar y)
+ (foundrec@foundrecbinding);
+ let check_bound x =
+ if not (List.mem x found) then
+ if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding
+ or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding
+ then
+ error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.")
+ else
+ error ((string_of_id x)^" is unbound in the right-hand side.") in
+ let check_pair s x y where =
+ if not (List.mem (x,y) where) then
+ errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
+ str " position as part of a recursive pattern.") in
+ let check_type (x,typ) =
+ match typ with
+ | NtnInternTypeConstr ->
+ begin
+ try check_pair "term" x (List.assoc x recvars) foundrec
+ with Not_found -> check_bound x
+ end
+ | NtnInternTypeBinder ->
+ begin
+ try check_pair "binding" x (List.assoc x recvars) foundrecbinding
+ with Not_found -> check_bound x
+ end
+ | NtnInternTypeIdent -> check_bound x in
+ List.iter check_type vars
+
+let aconstr_of_rawconstr vars recvars a =
+ let a,found = aconstr_and_vars_of_rawconstr a in
+ check_variables vars recvars found;
a
(* Substitution of kernel names, avoiding a list of bound identifiers *)
let aconstr_of_constr avoiding t =
- aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
+ aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t)
let rec subst_pat subst pat =
match pat with
@@ -319,6 +424,12 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 && r2' == r2 then raw else
AProd (n,r1',r2')
+ | ABinderList (id1,id2,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1
+ and r2' = subst_aconstr subst bound r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ABinderList (id1,id2,r1',r2')
+
| ALetIn (n,r1,r2) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
@@ -396,7 +507,7 @@ let rec subst_aconstr subst bound raw =
ACast (r1',CastCoerce)
let subst_interpretation subst (metas,pat) =
- let bound = List.map fst (fst metas @ snd metas) in
+ let bound = List.map fst metas in
(metas,subst_aconstr subst bound pat)
let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
@@ -434,7 +545,7 @@ let rec alpha_var id1 id2 = function
let alpha_eq_val (x,y) = x = y
-let bind_env alp (sigma,sigmalist as fullsigma) var v =
+let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
try
let vvar = List.assoc var sigma in
if alpha_eq_val (v,vvar) then fullsigma
@@ -443,7 +554,10 @@ let bind_env alp (sigma,sigmalist as fullsigma) var v =
(* Check that no capture of binding variables occur *)
if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
(* TODO: handle the case of multiple occs in different scopes *)
- ((var,v)::sigma,sigmalist)
+ ((var,v)::sigma,sigmalist,sigmabinders)
+
+let bind_binder (sigma,sigmalist,sigmabinders) x bl =
+ (sigma,sigmalist,(x,List.rev bl)::sigmabinders)
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
@@ -458,13 +572,9 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
| Some t1, Some t2 -> f sigma t1 t2
| _ -> raise No_match
-let rawconstr_of_name = function
- | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
- | Name id -> RVar (dummy_loc,id)
-
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
- | (na,Name id2) when List.mem id2 metas ->
- alp, bind_env alp sigma id2 (rawconstr_of_name na)
+ | (Name id1,Name id2) when List.mem id2 (fst metas) ->
+ alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
| (Name id1,Name id2) -> (id1,id2)::alp,sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
@@ -482,33 +592,80 @@ let adjust_application_n n loc f l =
let l1,l2 = list_chop (List.length l - n) l in
if l1 = [] then f,l else RApp (loc,f,l1), l2
-let match_alist match_fun metas sigma l1 l2 x iter termin lassoc =
- (* match the iterator at least once *)
- let sigmavar,sigmalist =
- List.fold_left2 (match_fun (ldots_var::metas)) sigma l1 l2 in
- (* Recover the recursive position *)
- let rest = List.assoc ldots_var sigmavar in
- (* Recover the first element *)
- let t1 = List.assoc x sigmavar in
- let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
- (* try to find the remaining elements or the terminator *)
- let rec match_alist_tail metas sigma acc rest =
+let glue_letin_with_decls = true
+
+let rec match_iterated_binders islambda decls = function
+ | RLambda (_,na,bk,t,b) when islambda ->
+ match_iterated_binders islambda ((na,bk,None,t)::decls) b
+ | RProd (_,(Name _ as na),bk,t,b) when not islambda ->
+ match_iterated_binders islambda ((na,bk,None,t)::decls) b
+ | RLetIn (loc,na,c,b) when glue_letin_with_decls ->
+ match_iterated_binders islambda
+ ((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b
+ | b -> (decls,b)
+
+let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
+ (List.remove_assoc x sigmavar,sigmalist,sigmabinders)
+
+let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
+ let rec aux sigma acc rest =
try
- let sigmavar,sigmalist = match_fun (ldots_var::metas) sigma rest iter in
- let rest = List.assoc ldots_var sigmavar in
- let t = List.assoc x sigmavar in
- let sigmavar =
- List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
- match_alist_tail metas (sigmavar,sigmalist) (t::acc) rest
- with No_match ->
- List.rev acc, match_fun metas (sigmavar,sigmalist) rest termin in
- let tl,(sigmavar,sigmalist) = match_alist_tail metas sigma [t1] rest in
- (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
-
-let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
- | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
+ let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
+ let rest = List.assoc ldots_var (pi1 sigma) in
+ let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in
+ let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+ aux sigma (b::acc) rest
+ with No_match when acc <> [] ->
+ acc, match_fun metas sigma rest termin in
+ let bl,sigma = aux sigma [] rest in
+ bind_binder sigma x bl
+
+let match_alist match_fun metas sigma rest x iter termin lassoc =
+ let rec aux sigma acc rest =
+ try
+ let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
+ let rest = List.assoc ldots_var (pi1 sigma) in
+ let t = List.assoc x (pi1 sigma) in
+ let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+ aux sigma (t::acc) rest
+ with No_match when acc <> [] ->
+ acc, match_fun metas sigma rest termin in
+ let l,sigma = aux sigma [] rest in
+ (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
+
+let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with
+
+ (* Matching notation variable *)
+ | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1
+
+ (* Matching recursive notations for terms *)
+ | r1, AList (x,_,iter,termin,lassoc) ->
+ match_alist (match_ alp) metas sigma r1 x iter termin lassoc
+
+ (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
+ | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)->
+ let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
+ (* TODO: address the possibility that termin is a Lambda itself *)
+ match_ alp metas (bind_binder sigma x decls) b termin
+ | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin)
+ when na1 <> Anonymous ->
+ let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
+ (* TODO: address the possibility that termin is a Prod itself *)
+ match_ alp metas (bind_binder sigma x decls) b termin
+ (* Matching recursive notations for binders: general case *)
+ | r, ABinderList (x,_,iter,termin) ->
+ match_abinderlist_with_app (match_ alp) metas sigma r x iter termin
+
+ (* Matching individual binders as part of a recursive pattern *)
+ | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas ->
+ match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+ | RProd (_,na,bk,t,b1), AProd (Name id,_,b2)
+ when List.mem id blmetas & na <> Anonymous ->
+ match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+
+ (* Matching compositionally *)
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
- | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
+ | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
| RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
| RApp (loc,f1,l1), AApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
@@ -519,11 +676,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
else f1,l1, f2, l2 in
List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
- | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
- when List.length l1 >= List.length l2 ->
- let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
- match_alist (match_ alp)
- metas sigma (f1::l1) (f2::l2) x iter termin lassoc
| RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
@@ -588,38 +740,36 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
(alp,sigma) patl1 patl2 in
match_ alp metas sigma rhs1 rhs2
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-type interpretation =
- (* regular vars of notation / recursive parts of notation / body *)
- ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
-
-let match_aconstr c ((metas_scl,metaslist_scl),pat) =
- let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
- let subst,substlist = match_ [] vars ([],[]) c pat in
+let match_aconstr c (metas,pat) =
+ let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+ let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
+ let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in
(* Reorder canonically the substitution *)
let find x =
- try List.assoc x subst
+ try List.assoc x terms
with Not_found ->
(* Happens for binders bound to Anonymous *)
(* Find a better way to propagate Anonymous... *)
RVar (dummy_loc,x) in
- List.map (fun (x,scl) -> (find x,scl)) metas_scl,
- List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
+ List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
+ match typ with
+ | NtnTypeConstr ->
+ ((find x, scl)::terms',termlists',binders')
+ | NtnTypeConstrList ->
+ (terms',(List.assoc x termlists,scl)::termlists',binders')
+ | NtnTypeBinderList ->
+ (terms',termlists',(List.assoc x binders,scl)::binders'))
+ metas ([],[],[])
(* Matching cases pattern *)
-let bind_env_cases_pattern (sigma,sigmalist as fullsigma) var v =
+let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
try
let vvar = List.assoc var sigma in
if v=vvar then fullsigma else raise No_match
with Not_found ->
(* TODO: handle the case of multiple occs in different scopes *)
- (var,v)::sigma,sigmalist
+ (var,v)::sigma,sigmalist,x
let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1
@@ -639,26 +789,21 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
(* All parameters must be _ *)
List.iter (function AHole _ -> () | _ -> raise No_match) p2;
List.fold_left2 (match_cases_pattern metas) sigma args1 args2
- | PatCstr (loc,(ind,_ as r1),args1,_),
- AList (x,_,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
- when r1 = r2 ->
- let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
- assert (List.length args1 + nparams = List.length l2);
- let (p2,args2) = list_chop nparams l2 in
- List.iter (function AHole _ -> () | _ -> raise No_match) p2;
- match_alist match_cases_pattern
- metas sigma args1 args2 x iter termin lassoc
+ | r1, AList (x,_,iter,termin,lassoc) ->
+ match_alist (fun (metas,_) -> match_cases_pattern metas)
+ (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc
| _ -> raise No_match
-let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
- let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
- let subst,substlist = match_cases_pattern vars ([],[]) c pat in
+let match_aconstr_cases_pattern c (metas,pat) =
+ let vars = List.map fst metas in
+ let terms,termlists,() = match_cases_pattern vars ([],[],()) c pat in
(* Reorder canonically the substitution *)
- let find x subst =
- try List.assoc x subst
- with Not_found -> anomaly "match_aconstr_cases_pattern" in
- List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
- List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
+ List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
+ match typ with
+ | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists')
+ | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists')
+ | NtnTypeBinderList -> assert false)
+ metas ([],[])
(**********************************************************************)
(*s Concrete syntax for terms *)
@@ -675,19 +820,20 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
-type 'a notation_substitution =
- 'a list * (* for recursive notations: *) 'a list list
-
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
- | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
+ | CPatNotation of loc * notation * cases_pattern_notation_substitution
| CPatPrim of loc * prim_token
- | CPatRecord of loc * (reference * cases_pattern_expr) list
+ | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
| CPatDelimiters of loc * string * cases_pattern_expr
+and cases_pattern_notation_substitution =
+ cases_pattern_expr list * (** for constr subterms *)
+ cases_pattern_expr list list (** for recursive notations *)
+
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fix_expr list
@@ -701,18 +847,18 @@ type constr_expr =
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
- (constr_expr * (name option * constr_expr option)) list *
+ (constr_expr * (name located option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
- | CLetTuple of loc * name list * (name option * constr_expr option) *
+ | CLetTuple of loc * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
- | CIf of loc * constr_expr * (name option * constr_expr option)
+ | CIf of loc * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
- | CNotation of loc * notation * constr_expr notation_substitution
+ | CNotation of loc * notation * constr_notation_substitution
| CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
@@ -721,14 +867,6 @@ type constr_expr =
and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-and local_binder =
- | LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * binder_kind * constr_expr
-
-and typeclass_constraint = name located * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
@@ -737,6 +875,19 @@ and recursion_order_expr =
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
+and local_binder =
+ | LocalRawDef of name located * constr_expr
+ | LocalRawAssum of name located list * binder_kind * constr_expr
+
+and constr_notation_substitution =
+ constr_expr list * (* for constr subterms *)
+ constr_expr list list * (* for recursive notations *)
+ local_binder list list (* for binders subexpressions *)
+
+type typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
+
type constr_pattern_expr = constr_expr
(***********************)
@@ -789,6 +940,15 @@ let cases_pattern_expr_loc = function
| CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
+let local_binder_loc = function
+ | LocalRawAssum ((loc,_)::_,_,t)
+ | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
+ | LocalRawAssum ([],_,_) -> assert false
+
+let local_binders_loc bll =
+ if bll = [] then dummy_loc else
+ join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+
let occur_var_constr_ref id = function
| Ident (loc,id') -> id = id'
| Qualid _ -> false
@@ -798,7 +958,7 @@ let ids_of_cases_indtype =
let rec vars_of = function
(* We deal only with the regular cases *)
| CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
- | CNotation (_,_,(l,[]))
+ | CNotation (_,_,(l,[],[]))
(* assume the ntn is applicative and does not instantiate the head !! *)
| CAppExpl (_,_,l) -> List.fold_left add_var [] l
| CDelimiters(_,_,c) -> vars_of c
@@ -809,7 +969,7 @@ let ids_of_cases_tomatch tms =
List.fold_right
(fun (_,(ona,indnal)) l ->
Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
- indnal (Option.fold_right name_cons ona l))
+ indnal (Option.fold_right (down_located name_cons) ona l))
tms []
let is_constructor id =
@@ -849,7 +1009,7 @@ let rec fold_local_binders g f n acc b = function
f n (fold_local_binders g f n' acc b l) t
| LocalRawDef ((_,na),t)::l ->
f n (fold_local_binders g f (name_fold g na n) acc b l) t
- | _ ->
+ | [] ->
f n acc b
let fold_constr_expr_with_binders g f n acc = function
@@ -860,7 +1020,11 @@ let fold_constr_expr_with_binders g f n acc = function
| CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
| CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
| CCast (loc,a,CastCoerce) -> f n acc a
- | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
+ | CNotation (_,_,(l,ll,bll)) ->
+ (* The following is an approximation: we don't know exactly if
+ an ident is binding nor to which subterms bindings apply *)
+ let acc = List.fold_left (f n) acc (l@List.flatten ll) in
+ List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll
| CGeneralization (_,_,_,c) -> f n acc c
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
@@ -874,11 +1038,12 @@ let fold_constr_expr_with_binders g f n acc = function
let ids = ids_of_pattern_list patl in
f (Idset.fold g ids n) acc rhs) bl acc
| CLetTuple (loc,nal,(ona,po),b,c) ->
- let n' = List.fold_right (name_fold g) nal n in
- f (Option.fold_right (name_fold g) ona n') (f n acc b) c
+ let n' = List.fold_right (down_located (name_fold g)) nal n in
+ f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
| CIf (_,c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
- Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
+ Option.fold_left
+ (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
| CFix (loc,_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -961,21 +1126,29 @@ let coerce_to_name = function
(* Interpret the index of a recursion order annotation *)
-let index_of_annot bl na =
+let split_at_annot bl na =
let names = List.map snd (names_of_local_assums bl) in
match na with
| None ->
- if names = [] then error "A fixpoint needs at least one parameter."
- else None
+ if names = [] then error "A fixpoint needs at least one parameter."
+ else [], bl
| Some (loc, id) ->
- try Some (list_index0 (Name id) names)
- with Not_found ->
- user_err_loc(loc,"",
- str "No parameter named " ++ Nameops.pr_id id ++ str".")
+ let rec aux acc = function
+ | LocalRawAssum (bls, k, t) as x :: rest ->
+ let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
+ if r = [] then aux (x :: acc) rest
+ else
+ (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
+ LocalRawAssum (r, k, t) :: rest)
+ | LocalRawDef _ as x :: rest -> aux (x :: acc) rest
+ | [] ->
+ user_err_loc(loc,"",
+ str "No parameter named " ++ Nameops.pr_id id ++ str".")
+ in aux [] bl
(* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
+let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -1005,8 +1178,10 @@ let map_constr_expr_with_binders g f e = function
| CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
| CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
| CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
- | CNotation (loc,n,(l,ll)) ->
- CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
+ | CNotation (loc,n,(l,ll,bll)) ->
+ (* This is an approximation because we don't know what binds what *)
+ CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll,
+ List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
| CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
@@ -1019,11 +1194,11 @@ let map_constr_expr_with_binders g f e = function
let po = Option.map (f (List.fold_right g ids e)) rtnpo in
CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
- let e' = List.fold_right (name_fold g) nal e in
- let e'' = Option.fold_right (name_fold g) ona e in
+ let e' = List.fold_right (down_located (name_fold g)) nal e in
+ let e'' = Option.fold_right (down_located (name_fold g)) ona e in
CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (loc,c,(ona,po),b1,b2) ->
- let e' = Option.fold_right (name_fold g) ona e in
+ let e' = Option.fold_right (down_located (name_fold g)) ona e in
CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
@@ -1067,16 +1242,21 @@ type 'a module_signature =
| Check of 'a list (* ... <: T1 <: T2, possibly empty *)
(* Returns the ranges of locs of the notation that are not occupied by args *)
-(* and which are them occupied by proper symbols of the notation (or spaces) *)
+(* and which are then occupied by proper symbols of the notation (or spaces) *)
-let locs_of_notation f loc (args,argslist) ntn =
+let locs_of_notation loc locs ntn =
let (bl,el) = Util.unloc loc in
+ let locs = List.map Util.unloc locs in
let rec aux pos = function
| [] -> if pos = el then [] else [(pos,el-1)]
- | a::l ->
- let ba,ea = Util.unloc (f a) in
- if pos = ba then aux ea l else (pos,ba-1)::aux ea l
- in aux bl (args@List.flatten argslist)
+ | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+ in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs)
+
+let ntn_loc loc (args,argslist,binderslist) =
+ locs_of_notation loc
+ (List.map constr_loc (args@List.flatten argslist)@
+ List.map local_binders_loc binderslist)
-let ntn_loc = locs_of_notation constr_loc
-let patntn_loc = locs_of_notation cases_pattern_expr_loc
+let patntn_loc loc (args,argslist) =
+ locs_of_notation loc
+ (List.map cases_pattern_expr_loc (args@List.flatten argslist))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0918a4de..5e49d2ea 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: topconstr.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Pp
@@ -32,6 +32,7 @@ type aconstr =
(* Part only in [rawconstr] *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
+ | ABinderList of identifier * identifier * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
@@ -46,11 +47,34 @@ type aconstr =
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an aconstr: in a recursive pattern x..y,
+ x carries the sequence of objects bound to the list x..y *)
+type notation_var_instance_type =
+ | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as an aconstr:
+ in a recursive pattern x..y, both x and y carry the individual type
+ of each element of the list x..y *)
+type notation_var_internalization_type =
+ | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+ (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+
(**********************************************************************)
(* Translate a rawconstr into a notation given the list of variables *)
(* bound by the notation; also interpret recursive patterns *)
-val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+val aconstr_of_rawconstr :
+ (identifier * notation_var_internalization_type) list ->
+ (identifier * identifier) list -> rawconstr -> aconstr
(* Name of the special identifier used to encode recursive notations *)
val ldots_var : identifier
@@ -68,23 +92,14 @@ val rawconstr_of_aconstr_with_binders : loc ->
val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
(**********************************************************************)
-(* [match_aconstr metas] matches a rawconstr against an aconstr with *)
-(* metavariables in [metas]; raise [No_match] if the matching fails *)
+(* [match_aconstr] matches a rawconstr against a notation *)
+(* interpretation raise [No_match] if the matching fails *)
exception No_match
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-type interpretation =
- (* regular vars of notation / recursive parts of notation / body *)
- ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
-
val match_aconstr : rawconstr -> interpretation ->
- (rawconstr * subscopes) list * (rawconstr list * subscopes) list
+ (rawconstr * subscopes) list * (rawconstr list * subscopes) list *
+ (rawdecl list * subscopes) list
val match_aconstr_cases_pattern : cases_pattern -> interpretation ->
(cases_pattern * subscopes) list * (cases_pattern list * subscopes) list
@@ -113,19 +128,20 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
-type 'a notation_substitution =
- 'a list * (* for recursive notations: *) 'a list list
-
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
- | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
+ | CPatNotation of loc * notation * cases_pattern_notation_substitution
| CPatPrim of loc * prim_token
| CPatRecord of Util.loc * (reference * cases_pattern_expr) list
| CPatDelimiters of loc * string * cases_pattern_expr
+and cases_pattern_notation_substitution =
+ cases_pattern_expr list * (** for constr subterms *)
+ cases_pattern_expr list list (** for recursive notations *)
+
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fix_expr list
@@ -139,18 +155,18 @@ type constr_expr =
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
- (constr_expr * (name option * constr_expr option)) list *
+ (constr_expr * (name located option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
- | CLetTuple of loc * name list * (name option * constr_expr option) *
+ | CLetTuple of loc * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
- | CIf of loc * constr_expr * (name option * constr_expr option)
+ | CIf of loc * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
- | CNotation of loc * notation * constr_expr notation_substitution
+ | CNotation of loc * notation * constr_notation_substitution
| CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
@@ -172,6 +188,11 @@ and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
+and constr_notation_substitution =
+ constr_expr list * (** for constr subterms *)
+ constr_expr list list * (** for recursive notations *)
+ local_binder list list (** for binders subexpressions *)
+
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -185,6 +206,8 @@ val constr_loc : constr_expr -> loc
val cases_pattern_expr_loc : cases_pattern_expr -> loc
+val local_binders_loc : local_binder list -> loc
+
val replace_vars_constr_expr :
(identifier * identifier) list -> constr_expr -> constr_expr
@@ -208,7 +231,7 @@ val coerce_reference_to_id : reference -> identifier
val coerce_to_id : constr_expr -> identifier located
val coerce_to_name : constr_expr -> name located
-val index_of_annot : local_binder list -> identifier located option -> int option
+val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
@@ -256,7 +279,6 @@ type 'a module_signature =
| Check of 'a list (* ... <: T1 <: T2, possibly empty *)
val ntn_loc :
- Util.loc -> constr_expr notation_substitution -> string -> (int * int) list
+ Util.loc -> constr_notation_substitution -> string -> (int * int) list
val patntn_loc :
- Util.loc -> cases_pattern_expr notation_substitution -> string ->
- (int * int) list
+ Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 08:10:52 +0000