aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml7
-rw-r--r--contrib/subtac/equations.ml42
-rw-r--r--interp/constrextern.ml60
-rw-r--r--interp/constrintern.ml153
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml4
-rw-r--r--interp/syntax_def.ml11
-rw-r--r--interp/syntax_def.mli8
-rw-r--r--interp/topconstr.ml83
-rw-r--r--interp/topconstr.mli20
-rw-r--r--lib/util.ml16
-rw-r--r--lib/util.mli3
-rw-r--r--parsing/egrammar.ml46
-rw-r--r--parsing/g_constr.ml44
-rw-r--r--parsing/ppconstr.ml56
-rw-r--r--parsing/ppvernac.ml4
-rw-r--r--parsing/q_coqast.ml46
-rw-r--r--tactics/decl_interp.ml4
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--test-suite/output/Notations.out4
-rw-r--r--test-suite/output/Notations.v16
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/metasyntax.ml59
24 files changed, 329 insertions, 251 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 77cde062f..561ed3d4c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -274,9 +274,11 @@ let rec xlate_match_pattern =
CT_coerce_NUM_to_MATCH_PATTERN
(CT_int_encapsulator(Bigint.to_string n))
| CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
- | CPatNotation(_, s, l) ->
+ | CPatNotation(_, s, (l,[])) ->
CT_pattern_notation(CT_string s,
CT_match_pattern_list(List.map xlate_match_pattern l))
+ | CPatNotation(_, s, (l,_)) ->
+ xlate_error "CPatNotation (recursive notation): TODO"
;;
@@ -392,7 +394,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
xlate_formula b1, xlate_formula b2)
| CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
- | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
+ | CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
+ | CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
| CPrim (_, Numeral i) ->
CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
| CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 135fcf11d..ebbb5505f 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -850,7 +850,7 @@ let ids_of_patc c ?(bound=Idset.empty) l =
in
let rec aux bdvars l c = match c with
| CRef (Ident lid) -> found lid 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
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a3393863b..add71a8b0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -190,8 +190,9 @@ 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), CNotation(_,n2,e2) when n1=n2 ->
- List.iter2 check_same_type e1 e2
+ | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+ List.iter2 check_same_type e1 e2;
+ List.iter2 (List.iter2 check_same_type) el1 el2
| CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
check_same_type e1 e2
@@ -298,7 +299,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 =
+let expand_curly_brackets loc mknot ntn (l,ll) =
let ntn' = ref ntn in
let rec expand_ntn i =
function
@@ -311,12 +312,12 @@ let expand_curly_brackets loc mknot ntn l =
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)
+ mknot (loc,!ntn',(l,ll))
let destPrim = function CPrim(_,t) -> Some t | _ -> None
let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -324,18 +325,18 @@ 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 l with
+ else match ntn,List.map destprim (fst l),(snd 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)
@@ -351,13 +352,13 @@ let make_pat_notation loc ntn l =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim l
-let bind_env sigma var v =
+let bind_env (sigma,sigmalist as fullsigma) var v =
try
let vvar = List.assoc var sigma in
- if v=vvar then sigma else raise No_match
+ 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
+ (var,v)::sigma,sigmalist
let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
@@ -378,15 +379,18 @@ 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
+ (* TODO: use recursive notations *)
| _ -> raise No_match
-let match_aconstr_cases_pattern c (metas_scl,pat) =
- let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+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
(* Reorder canonically the substitution *)
let find x subst =
- try List.assoc 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 subst,scl)) metas_scl,
+ List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -424,7 +428,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| PatCstr (loc,_,_,na),_ -> loc,na
| PatVar (loc,na),_ -> loc,na in
(* Try matching ... *)
- let subst = match_aconstr_cases_pattern t pat in
+ let subst,substlist = match_aconstr_cases_pattern t pat in
(* Try availability of interpretation ... *)
let p = match keyrule with
| NotationRule (sc,ntn) ->
@@ -438,7 +442,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
subst in
- insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
+ let ll =
+ List.map (fun (c,(scopt,scl)) ->
+ let subscope = (scopt,scl@scopes') in
+ List.map (extern_cases_pattern_in_scope subscope vars) c)
+ substlist in
+ insert_pat_delimiters loc
+ (make_pat_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let qid = shortest_qualid_of_syndef vars kn in
CPatAtom (loc,Some (Qualid (loc, qid))) in
@@ -817,7 +827,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| _, None -> t,[]
| _ -> raise No_match in
(* Try matching ... *)
- let subst = match_aconstr t pat in
+ let subst,substlist = match_aconstr t pat in
(* Try availability of interpretation ... *)
let e =
match keyrule with
@@ -833,7 +843,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
extern (* assuming no overloading: *) true
(scopt,scl@scopes') vars c)
subst in
- insert_delimiters (make_notation loc ntn l) key)
+ 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)
| SynDefRule kn ->
let l =
List.map (fun (c,(scopt,scl)) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 15c816b5b..2faa86622 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -147,31 +147,31 @@ 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 =
+let contract_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CNotation (_,"{ _ }",[a]) :: l ->
+ | CNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',l
+ !ntn',(l,ll)
-let contract_pat_notation ntn l =
+let contract_pat_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CPatNotation (_,"{ _ }",[a]) :: l ->
+ | CPatNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',l
+ !ntn',(l,ll)
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
@@ -191,7 +191,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
(**********************************************************************)
(* Syntax extensions *)
-let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,tmpsc,scopes as env)) id =
try
(* Binders bound in the notation are considered first-order objects *)
let _,id' = coerce_to_id (fst (List.assoc id subst)) in
@@ -200,22 +200,21 @@ let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
(* 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.map snd renaming in
- let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 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 renaming' = if id=id' then renaming else (id,id')::renaming in
(renaming',env), id'
-let decode_constrlist_value = function
- | CAppExpl (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
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 (renaming,(ids,_,scopes)) =
- function
+let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
+ let (renaming,(ids,_,scopes)) = infos in
+ let subinfos = renaming,(ids,None,scopes) in
+ match c with
| AVar id ->
begin
(* subst remembers the delimiters stack in the interpretation *)
@@ -233,30 +232,27 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
| AList (x,_,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (a,(scopt,subscopes)) = List.assoc x subst in
+ let (l,(scopt,subscopes)) = List.assoc x substlist in
let termin =
- subst_aconstr_in_rawconstr loc interp subst
- (renaming,(ids,None,scopes)) terminator in
- let l = decode_constrlist_value a in
+ subst_aconstr_in_rawconstr loc interp sub 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)
- (renaming,(ids,None,scopes)) iter))
+ ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
(if lassoc then List.rev l else l) termin
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t ->
- rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
- (subst_aconstr_in_rawconstr loc interp subst)
- (renaming,(ids,None,scopes)) 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 args =
- let ntn,args = contract_notation ntn args in
- let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
- let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- subst_aconstr_in_rawconstr loc intern subst ([],env) c
+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
+ Dumpglob.dump_notation_location (ntn_loc loc fullargs 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,tmp_scope,scopes) =
(ids,Some Notation.type_scope,scopes)
@@ -353,7 +349,7 @@ let intern_qualid loc qid intern env args =
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
+ subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
with Not_found ->
error_global_not_found_loc loc qid
@@ -460,8 +456,8 @@ let check_constructor_length env loc cstr pl pl0 =
(* [merge_aliases] returns the sets of all aliases encountered at this
point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,subst as _aliases) id =
- ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
+let merge_aliases (ids,asubst as _aliases) id =
+ ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst
let alias_of = function
| ([],_) -> Anonymous
@@ -483,10 +479,6 @@ let chop_aconstr_constructor loc (ind,k) args =
| _ -> error_invalid_pattern_notation loc) params;
args
-let decode_patlist_value = function
- | CPatCstr (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
let rec subst_pat_iterator y t (subst,p) = match p with
| PatVar (_,id) as x ->
if id = Name y then t else [subst,x]
@@ -495,8 +487,8 @@ let rec subst_pat_iterator y t (subst,p) = match p with
let pl = simple_product_of_cases_patterns l' in
List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
-let subst_cases_pattern loc alias intern subst scopes a =
- let rec aux alias subst = function
+let subst_cases_pattern loc alias intern fullsubst scopes a =
+ let rec aux alias (subst,substlist as fullsubst) = function
| AVar id ->
begin
(* subst remembers the delimiters stack in the interpretation *)
@@ -518,30 +510,29 @@ let subst_cases_pattern loc alias intern subst scopes a =
([],[[], PatCstr (loc,c, [], alias)])
| AApp (ARef (ConstructRef cstr),args) ->
let args = chop_aconstr_constructor loc cstr args in
- let idslpll = List.map (aux Anonymous subst) args in
+ let idslpll = List.map (aux Anonymous fullsubst) args in
let ids',pll = product_of_cases_patterns [] idslpll in
- let pl' = List.map (fun (subst,pl) ->
- subst,PatCstr (loc,cstr,pl,alias)) pll in
+ let pl' = List.map (fun (asubst,pl) ->
+ asubst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (a,(scopt,subscopes)) = List.assoc x subst in
- let termin = aux Anonymous subst terminator in
- let l = decode_patlist_value a in
+ let (l,(scopt,subscopes)) = List.assoc x substlist in
+ let termin = aux Anonymous fullsubst terminator in
let idsl,v =
List.fold_right (fun a (tids,t) ->
- let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) iter in
+ let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
let pll = List.map (subst_pat_iterator ldots_var t) u in
tids@uids, List.flatten pll)
(if lassoc then List.rev l else l) termin in
- idsl, List.map (fun ((subst, pl) as x) ->
- match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
+ idsl, List.map (fun ((asubst, pl) as x) ->
+ match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t -> error_invalid_pattern_notation loc
- in aux alias subst a
-
+ in aux alias fullsubst a
+
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
| ConstrPat of constructor * (identifier list *
@@ -566,7 +557,7 @@ let find_constructor ref f aliases pats scopes =
if List.length pats < nvars then error_not_enough_arguments loc;
let pats1,pats2 = list_chop nvars pats in
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
- let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in
+ let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
@@ -604,7 +595,7 @@ let mustbe_constructor loc ref f aliases patl scopes =
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
let intern_pat = intern_cases_pattern genv in
match pat with
| CPatAlias (loc, p, id) ->
@@ -616,28 +607,30 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
- let pl' = List.map (fun (subst,pl) ->
- (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
+ let pl' = List.map (fun (asubst,pl) ->
+ (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
ids',pl'
- | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)])
+ | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
- | CPatNotation (_,"( _ )",[a]) ->
+ | CPatNotation (_,"( _ )",([a],[])) ->
intern_pat scopes aliases tmp_scope a
- | CPatNotation (loc, ntn, args) ->
- let ntn,args = contract_pat_notation ntn args in
- let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+ | 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
+ Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
- let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes
- c
+ let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
+ let ids'',pl =
+ subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
+ scopes c
in ids@ids'', pl
| CPatPrim (loc, p) ->
let a = alias_of aliases in
let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
(tmp_scope,scopes) in
Dumpglob.dump_notation_location (fst (unloc loc)) df;
- (ids,[subst,c])
+ (ids,[asubst,c])
| CPatDelimiters (loc, key, e) ->
intern_pat (find_delimiters_scope loc key::scopes) aliases None e
| CPatAtom (loc, Some head) ->
@@ -645,13 +638,13 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
| ConstrPat (c,idspl) ->
check_constructor_length genv loc c idspl [];
let (ids',pll) = product_of_cases_patterns ids idspl in
- (ids,List.map (fun (subst,pl) ->
- (subst, PatCstr (loc,c,pl,alias_of aliases))) pll)
+ (ids,List.map (fun (asubst,pl) ->
+ (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll)
| VarPat id ->
- let ids,subst = merge_aliases aliases id in
- (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
+ let ids,asubst = merge_aliases aliases id in
+ (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
| CPatAtom (loc, None) ->
- (ids,[subst, PatVar (loc,alias_of aliases)])
+ (ids,[asubst, PatVar (loc,alias_of aliases)])
| CPatOr (loc, pl) ->
assert (pl <> []);
let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
@@ -888,10 +881,10 @@ let internalise sigma globalenv env allow_patvar lvar c =
| 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)])
+ | 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
| CPrim (loc, p) ->
@@ -915,8 +908,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 loc ntn ([],[]) in
find_appl_head_data lvar c, args
| x -> (intern env f,[],[],[]), args in
let args =
@@ -992,9 +985,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
(* Linearity implies the order in ids is irrelevant *)
check_linearity lhs eqn_ids;
let env_ids = List.fold_right Idset.add eqn_ids ids in
- List.map (fun (subst,pl) ->
- let rhs = replace_vars_constr_expr subst rhs in
- List.iter message_redundant_alias subst;
+ List.map (fun (asubst,pl) ->
+ let rhs = replace_vars_constr_expr asubst rhs in
+ List.iter message_redundant_alias asubst;
let rhs' = intern (env_ids,tmp_scope,scopes) rhs in
(loc,eqn_ids,pl,rhs')) pll
@@ -1209,19 +1202,19 @@ type ltac_sign = identifier list * unbound_ltac_var_map
let interp_constrpattern sigma env c =
pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
-let interp_aconstr impls vars a =
+let interp_aconstr impls (vars,varslist) a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
- let vl = List.map (fun id -> (id,ref None)) vars in
+ let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
let c = internalise Evd.empty (Global.env()) (extract_ids env, 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
(* Returns [a] and the ordered list of variables with their scopes *)
(* Variables occurring in binders have no relevant scope since bound *)
- List.map
- (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
- a
+ 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
(* Interpret binders and contexts *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9169e5fbf..1554d4289 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -141,8 +141,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
- interpretation
+val interp_aconstr : implicits_env -> identifier list * identifier list
+ -> constr_expr -> interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8bacbcd8c..7801f048f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
in
let rec aux bdvars l c = match c with
| CRef (Ident (_,id)) -> found 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
diff --git a/interp/notation.ml b/interp/notation.ml
index 0915304c3..b6c1bfa40 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -193,10 +193,6 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| ARef ref -> RefKey ref, None
| _ -> Oth, None
-let pattern_key = function
- | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
- | _ -> Oth
-
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 4c2b7eaef..8f303ea61 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -70,11 +70,18 @@ let (in_syntax_constant, out_syntax_constant) =
classify_function = classify_syntax_constant;
export_function = export_syntax_constant }
+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 declare_syntactic_definition local id onlyparse pat =
- let _ = add_leaf id (in_syntax_constant (local,pat,onlyparse)) in ()
+ let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
let search_syntactic_definition loc kn =
- KNmap.find kn !syntax_table
+ out_pat (KNmap.find kn !syntax_table)
let locate_global_with_alias (loc,qid) =
match Nametab.extended_locate qid with
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index bbbea07f3..1599e844b 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,10 +18,12 @@ open Libnames
(* Syntactic definitions. *)
-val declare_syntactic_definition : bool -> identifier -> bool -> interpretation
- -> unit
+type syndef_interpretation = (identifier * subscopes) list * aconstr
-val search_syntactic_definition : loc -> kernel_name -> interpretation
+val declare_syntactic_definition : bool -> identifier -> bool ->
+ syndef_interpretation -> unit
+
+val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
(* [locate_global_with_alias] locates global reference possibly following
a notation if this notation has a role of aliasing; raise Not_found
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c684c6adb..058d997e0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -389,8 +389,9 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 then raw else
ACast (r1',CastCoerce)
-let subst_interpretation subst (metas,pat) =
- (metas,subst_aconstr subst (List.map fst metas) pat)
+let subst_interpretation subst (metas,pat) =
+ let bound = List.map fst (fst metas @ snd metas) in
+ (metas,subst_aconstr subst bound pat)
let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
@@ -427,16 +428,16 @@ let rec alpha_var id1 id2 = function
let alpha_eq_val (x,y) = x = y
-let bind_env alp sigma var v =
+let bind_env alp (sigma,sigmalist as fullsigma) var v =
try
let vvar = List.assoc var sigma in
- if alpha_eq_val (v,vvar) then sigma
+ if alpha_eq_val (v,vvar) then fullsigma
else raise No_match
with Not_found ->
(* 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
+ ((var,v)::sigma,sigmalist)
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
@@ -467,6 +468,10 @@ let rec match_cases_pattern metas acc pat1 pat2 =
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
+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 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
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -481,8 +486,9 @@ 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 (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
- when List.length l1 = List.length 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 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
@@ -535,24 +541,26 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
and match_alist alp metas sigma l1 l2 x iter termin lassoc =
(* match the iterator at least once *)
- let sigma = List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
+ let sigmavar,sigmalist =
+ List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
(* Recover the recursive position *)
- let rest = List.assoc ldots_var sigma in
+ let rest = List.assoc ldots_var sigmavar in
(* Recover the first element *)
- let t1 = List.assoc x sigma in
- let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
+ 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 alp metas sigma acc rest =
try
- let sigma = match_ alp (ldots_var::metas) sigma rest iter in
- let rest = List.assoc ldots_var sigma in
- let t = List.assoc x sigma in
- let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
- match_alist_tail alp metas sigma (t::acc) rest
+ let sigmavar,sigmalist = match_ alp (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 alp metas (sigmavar,sigmalist) (t::acc) rest
with No_match ->
- List.rev acc, match_ alp metas sigma rest termin in
- let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
- (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
+ List.rev acc, match_ alp metas (sigmavar,sigmalist) rest termin in
+ let tl,(sigmavar,sigmalist) = match_alist_tail alp metas sigma [t1] rest in
+ (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
and match_binders alp metas na1 na2 sigma b1 b2 =
let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
@@ -569,19 +577,24 @@ type scope_name = string
type tmp_scope_name = scope_name
-type interpretation =
- (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+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,pat) =
- let subst = match_ [] (List.map fst metas_scl) [] c pat in
+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
(* Reorder canonically the substitution *)
- let find x subst =
+ let find x =
try List.assoc x subst
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 subst,scl)) metas_scl
+ List.map (fun (x,scl) -> (find x,scl)) metas_scl,
+ List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
(**********************************************************************)
(*s Concrete syntax for terms *)
@@ -596,12 +609,15 @@ 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 list
+ | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
@@ -628,7 +644,7 @@ type constr_expr =
| 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 list
+ | CNotation of loc * notation * constr_expr notation_substitution
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -718,7 +734,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
@@ -738,8 +754,10 @@ let is_constructor id =
let rec cases_pattern_fold_names f a = function
| CPatAlias (_,pat,id) -> f id a
- | CPatCstr (_,_,patl) | CPatOr (_,patl) | CPatNotation (_,_,patl) ->
+ | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
List.fold_left (cases_pattern_fold_names f) a patl
+ | CPatNotation (_,_,(patl,patll)) ->
+ List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)
| CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
| CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
| CPatPrim _ | CPatAtom _ -> a
@@ -776,7 +794,7 @@ 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) -> List.fold_left (f n) acc l
+ | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
@@ -887,7 +905,8 @@ 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) -> CNotation (loc,n,List.map (f e) l)
+ | CNotation (loc,n,(l,ll)) ->
+ CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
@@ -948,7 +967,7 @@ type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
-let loc_of_notation f loc args ntn =
+let loc_of_notation f loc (args,_) ntn =
if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
else snd (Util.unloc (f (List.hd args)))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index aed67975d..eb166bc25 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -77,11 +77,14 @@ type scope_name = string
type tmp_scope_name = scope_name
-type interpretation =
- (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+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 * (tmp_scope_name option * scope_name list)) list
+ (rawconstr * subscopes) list * (rawconstr list * subscopes) list
(**********************************************************************)
(* Substitution of kernel names in interpretation data *)
@@ -101,12 +104,15 @@ 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 list
+ | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
@@ -133,7 +139,7 @@ type constr_expr =
| 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 list
+ | CNotation of loc * notation * constr_expr notation_substitution
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -240,5 +246,5 @@ type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
-val ntn_loc : Util.loc -> constr_expr list -> string -> int
-val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int
+val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
+val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int
diff --git a/lib/util.ml b/lib/util.ml
index eb096c3cf..d1e24e321 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -730,13 +730,21 @@ let list_subset l1 l2 =
in
look l1
-let list_splitby p =
- let rec splitby_loop x y =
+let list_split_at p =
+ let rec split_at_loop x y =
match y with
| [] -> ([],[])
- | (a::l) -> if (p a) then (x,y) else (splitby_loop (x@[a]) l)
+ | (a::l) -> if (p a) then (x,y) else (split_at_loop (x@[a]) l)
in
- splitby_loop []
+ split_at_loop []
+
+let list_split_by p =
+ let rec split_loop = function
+ | [] -> ([],[])
+ | (a::l) ->
+ let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2)
+ in
+ split_loop
let rec list_split3 = function
| [] -> ([], [], [])
diff --git a/lib/util.mli b/lib/util.mli
index 40d6046d7..46fd7b02e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -146,7 +146,8 @@ val list_uniquize : 'a list -> 'a list
(* merges two sorted lists and preserves the uniqueness property: *)
val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
val list_subset : 'a list -> 'a list -> bool
-val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
val list_firstn : int -> 'a list -> 'a list
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index bd688bcdd..585d7ab82 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -52,58 +52,56 @@ type prod_item =
| NonTerm of constr_production_entry *
(Names.identifier * constr_production_entry) option
-type 'a action_env = (identifier * 'a) list
+type 'a action_env = 'a list * 'a list list
let make_constr_action
(f : loc -> constr_expr action_env -> constr_expr) pil =
- let rec make (env : constr_expr action_env) = function
+ let rec make (env,envlist as fullenv : constr_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
- Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
- Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
+ Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+ make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
- Gramext.action (fun (v:constr_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
+ Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
| Some (p, ETPattern) :: tl ->
failwith "Unexpected entry of type cases pattern" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_cases_pattern_action
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
- let rec make (env : cases_pattern_expr action_env) = function
+ let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
- Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun (v:reference) ->
- make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+ make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
+ make
+ (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
Gramext.action (fun (v:cases_pattern_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
+ make (env, v :: envlist) tl)
| Some (p, (ETPattern | ETOther _)) :: tl ->
failwith "Unexpected entry of type cases pattern or other" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_constr_prod_item univ assoc from forpat = function
| Term tok -> (Gramext.Stoken tok, None)
@@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt =
let extend_constr_notation (n,assoc,ntn,rule) =
(* Add the notation in constr *)
- let mkact loc env = CNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CNotation (loc,ntn,env) in
let e = get_constr_entry false (ETConstr (n,())) in
extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
(* Add the notation in cases_pattern *)
- let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CPatNotation (loc,ntn,env) in
let e = get_constr_entry true (ETConstr (n,())) in
extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
true rule
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b8dcf8e99..740ba0b34 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -202,7 +202,7 @@ GEXTEND Gram
| "("; c = operconstr LEVEL "200"; ")" ->
(match c with
CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CNotation(loc,"( _ )",[c])
+ CNotation(loc,"( _ )",([c],[]))
| _ -> c) ] ]
;
forall:
@@ -337,7 +337,7 @@ GEXTEND Gram
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CPatNotation(loc,"( _ )",[p])
+ CPatNotation(loc,"( _ )",([p],[]))
| _ -> p)
| n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
| s = string -> CPatPrim (loc, String s) ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4f266f5ca..e906fb398 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -62,36 +62,32 @@ let prec_of_prim_token = function
| Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
| String _ -> latom
-let env_assoc_value v env =
- try List.nth env (v-1)
- with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
-
-let decode_constrlist_value = function
- | CAppExpl (_,_,l) -> l
- | CApp (_,_,l) -> List.map fst l
- | _ -> anomaly "Ill-formed list argument of notation"
-
-let decode_patlist_value = function
- | CPatCstr (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
open Notation
-let rec print_hunk n decode pr env = function
- | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
- | UnpListMetaVar (e,prec,sl) ->
- prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
- (pr (n,prec)) (decode (env_assoc_value e env))
- | UnpTerminal s -> str s
- | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
- | UnpCut cut -> ppcmd_of_cut cut
-
-let pr_notation_gen decode pr s env =
+let print_hunks n pr (env,envlist) unp =
+ let env = ref env and envlist = ref envlist in
+ let pop r = let a = List.hd !r in r := List.tl !r; a in
+ let rec aux = function
+ | [] -> mt ()
+ | UnpMetaVar (_,prec) :: l ->
+ let c = pop env in pr (n,prec) c ++ aux l
+ | UnpListMetaVar (_,prec,sl) :: l ->
+ let cl = pop envlist in
+ let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+ let pp2 = aux l in
+ pp1 ++ pp2
+ | UnpTerminal s :: l -> str s ++ aux l
+ | UnpBox (b,sub) :: l ->
+ (* Keep order: side-effects *)
+ let pp1 = ppcmd_of_box b (aux sub) in
+ let pp2 = aux l in
+ pp1 ++ pp2
+ | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
+ aux unp
+
+let pr_notation pr s env =
let unpl, level = find_notation_printing_rule s in
- prlist (print_hunk level decode pr env) unpl, level
-
-let pr_notation = pr_notation_gen decode_constrlist_value
-let pr_patnotation = pr_notation_gen decode_patlist_value
+ print_hunks level pr env unpl, level
let pr_delimiters key strm =
strm ++ str ("%"^key)
@@ -179,9 +175,9 @@ let rec pr_patt sep inh p =
| CPatAtom (_,Some r) -> pr_reference r, latom
| CPatOr (_,pl) ->
hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
- | CPatNotation (_,"( _ )",[p]) ->
+ | CPatNotation (_,"( _ )",([p],[])) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
- | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
+ | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
| CPatPrim (_,p) -> pr_prim_token p, latom
| CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
in
@@ -592,7 +588,7 @@ let rec pr sep inherited a =
| CCast (_,a,CastCoerce) ->
hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
lcast
- | CNotation (_,"( _ )",[t]) ->
+ | CNotation (_,"( _ )",([t],[])) ->
pr (fun()->str"(") (max_int,L) t ++ str")", latom
| CNotation (_,s,env) -> pr_notation (pr mt) s env
| CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f779f53fb..2233bbd6a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -539,11 +539,11 @@ let rec pr_vernac = function
| VernacStartTheoremProof (ki,l,_,_) ->
let pr_statement head (id,(bl,c)) =
hov 0
- (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++
+ (head ++ pr_opt pr_lident id ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
str":" ++ pr_spc_lconstr c) in
hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
- prlist (pr_statement (str "with ")) (List.tl l))
+ prlist (pr_statement (spc () ++ str "with")) (List.tl l))
| VernacEndProof Admitted -> str"Admitted"
| VernacEndProof (Proved (opac,o)) -> (match o with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 37350af08..8407211f1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -159,9 +159,11 @@ let rec mlexpr_of_constr = function
| Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
| Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
- | Topconstr.CNotation(_,ntn,l) ->
+ | Topconstr.CNotation(_,ntn,subst) ->
<:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
- $mlexpr_of_list mlexpr_of_constr l$ >>
+ $mlexpr_of_pair
+ (mlexpr_of_list mlexpr_of_constr)
+ (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >>
| Topconstr.CPatVar (loc,n) ->
<:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
| _ -> failwith "mlexpr_of_constr: TODO"
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 2be95056e..2701566ed 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -94,8 +94,10 @@ let rec add_vars_of_simple_pattern globs = function
(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
| CPatDelimiters (_,_,p) ->
add_vars_of_simple_pattern globs p
- | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) ->
+ | CPatCstr (_,_,pl) ->
List.fold_left add_vars_of_simple_pattern globs pl
+ | CPatNotation(_,_,(pl,pll)) ->
+ List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))
| CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
| _ -> globs
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bbd9112d4..1e4f6a050 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -206,7 +206,7 @@ let onHyps find tac gl = tac (find gl) gl
after id *)
let afterHyp id gl =
- fst (list_splitby (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+ fst (list_split_at (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
(* Create a singleton clause list with the last hypothesis from then context *)
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2066a7ef3..6c69c097d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,3 +50,7 @@ Nil
: forall A : Type, list A
NIL:list nat
: list nat
+[|1, 2, 3; 4, 5, 6|]
+ : Z * Z * Z * (Z * Z * Z)
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+ : (Z -> Z -> Z -> Z) -> Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 6e637aca3..f19ba998f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -129,3 +129,19 @@ Check Nil.
Notation NIL := nil.
Check NIL : list nat.
+
+(**********************************************************************)
+(* Check notations with several recursive patterns *)
+
+Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
+ (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
+Check [|1,2,3;4,5,6|].
+
+(**********************************************************************)
+(* Test recursive notations involving applications *)
+(* Caveat: does not work for applied constant because constants are *)
+(* classified as notations for the particular constant while this *)
+(* generic application notation is classified as generic *)
+
+Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+Check fun f => {| f; 0; 1; 2 |} : Z.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ca55fb066..4682a963e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -166,9 +166,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
hook local r
let syntax_definition ident (vars,c) local onlyparse =
- let pat = interp_aconstr [] vars c in
- let onlyparse = onlyparse or Metasyntax.is_not_printable (snd pat) in
- Syntax_def.declare_syntactic_definition local ident onlyparse pat
+ let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in
+ let onlyparse = onlyparse or Metasyntax.is_not_printable pat in
+ Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b43a5eeb9..920f6f4c5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -281,22 +281,22 @@ let rec find_pattern xl = function
error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
let rec interp_list_parser hd = function
- | [] -> [], List.rev hd
+ | [] -> [], [], List.rev hd
| NonTerminal id :: tl when id = ldots_var ->
let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
- let yl,tl'' = interp_list_parser [] tl' in
- (* We remember the second copy of each recursive part variable to *)
- (* remove it afterwards *)
- y::yl, SProdList (x,sl) :: tl''
+ let yl,xl,tl'' = interp_list_parser [] tl' in
+ (* We remember each pair of variable denoting a recursive part to *)
+ (* remove the second copy of it afterwards *)
+ (y,x)::yl, x::xl, SProdList (x,sl) :: tl''
| (Terminal _ | Break _) as s :: tl ->
if hd = [] then
- let yl,tl' = interp_list_parser [] tl in
- yl, s :: tl'
+ let yl,xl,tl' = interp_list_parser [] tl in
+ yl, xl, s :: tl'
else
interp_list_parser (s::hd) tl
| NonTerminal _ as x :: tl ->
- let yl,tl' = interp_list_parser [x] tl in
- yl, List.rev_append hd tl'
+ let yl,xl,tl' = interp_list_parser [x] tl in
+ yl, xl, List.rev_append hd tl'
| SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
(* Find non-terminal tokens of notation *)
@@ -345,10 +345,20 @@ let is_numeral symbs =
let analyse_notation_tokens l =
let vars,l = raw_analyse_notation_tokens l in
- let recvars,l = interp_list_parser [] l in
- ((if recvars = [] then [] else ldots_var::recvars), vars, l)
-
-let remove_vars = List.fold_right List.remove_assoc
+ let extrarecvars,recvars,l = interp_list_parser [] l in
+ (if extrarecvars = [] then [], [], vars, l
+ else extrarecvars, recvars, list_subtract vars recvars, l)
+
+let remove_extravars extrarecvars (vars,recvars) =
+ let vars =
+ List.fold_right (fun (x,y) l ->
+ if List.mem_assoc x l <> List.mem_assoc y recvars then
+ error
+ "Two end variables of a recursive notation are not in the same scope"
+ else
+ List.remove_assoc x l)
+ extrarecvars (List.remove_assoc ldots_var vars) in
+ (vars,recvars)
(**********************************************************************)
(* Build pretty-printing rules *)
@@ -422,7 +432,7 @@ let make_hunks etyps symbols from =
| NonTerminal m :: prods ->
let i = list_index m vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let u = UnpMetaVar (i ,prec) in
+ let u = UnpMetaVar (i,prec) in
if prods <> [] && is_non_terminal (List.hd prods) then
u :: add_break 1 (make CanBreak prods)
else
@@ -814,7 +824,7 @@ let compute_syntax_data (df,modifiers) =
(* Notation defaults to NONA *)
let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
let toks = split_notation_string df in
- let (recvars,vars,symbols) = analyse_notation_tokens toks in
+ let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let need_squash = (symbols <> symbols') in
@@ -833,7 +843,7 @@ let compute_syntax_data (df,modifiers) =
let prec = (n,List.map (assoc_of_type n) typs) in
let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
let df' = (Lib.library_dp(),df) in
- let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in
+ let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
(i_data,sy_data)
(**********************************************************************)
@@ -939,14 +949,15 @@ let add_notation_in_scope local df c mods scope =
let sy_rules = make_syntax_rules sy_data in
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
(* Declare interpretation *)
- let (onlyparse,recvars,vars,df') = i_data in
- let (acvars,ac) = interp_aconstr [] vars c in
- let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in
+ let (onlyparse,extrarecvars,recvars,vars,df') = i_data in
+ let (acvars,ac) = interp_aconstr [] (vars,recvars) c in
+ let a = (remove_extravars extrarecvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
- Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+ Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
let add_notation_interpretation_core local df names c scope onlyparse =
- let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
+ let dfs = split_notation_string df in
+ let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in
(* Redeclare pa/pp rules *)
if not (is_numeral symbs) then begin
let sy_rules = recover_notation_syntax (make_notation_key symbs) in
@@ -954,10 +965,10 @@ let add_notation_interpretation_core local df names c scope onlyparse =
end;
(* Declare interpretation *)
let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
- let (acvars,ac) = interp_aconstr names vars c in
- let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
+ let (acvars,ac) = interp_aconstr names (vars,recvars) c in
+ let a = (remove_extravars extrarecvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
- Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+ Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
(* Notations without interpretation (Reserved Notation) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 04:23:15 +0000