diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | intf/notation_term.ml | 5 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 25 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 8 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 93 |
6 files changed, 100 insertions, 44 deletions
@@ -1,3 +1,10 @@ +To be inserted at the proper place: + +Notations + +- Recursive notations with the recursive pattern repeating on the + right (e.g. "( x ; .. ; y ; z )") now supported. + Changes beyond V8.6 =================== diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0fa0afdad..cee96040b 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -83,9 +83,10 @@ type notation_interp_env = { type grammar_constr_prod_item = | GramConstrTerminal of Tok.t | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool + | GramConstrListMark of int * bool * int (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) + concat with last parsed list when true; additionally release + the p last items as if they were parsed autonomously *) type notation_grammar = { notgram_level : int; diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d4043f31e..ec422c58d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -354,7 +354,7 @@ type (_, _) ty_symbol = type ('self, _, 'r) ty_rule = | TyStop : ('self, 'r, 'r) ty_rule | TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule -| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule +| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule type 'r gen_eval = Loc.t -> 'r env -> 'r @@ -368,18 +368,27 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> | TyNext (rem, TyNonTerm (forpat, e, _, true)) -> fun f env v -> ty_eval rem f (push_item forpat e env v) -| TyMark (n, b, rem) -> +| TyMark (n, b, p, rem) -> fun f env -> let heads, constrs = List.chop n env.constrs in - let constrlists = - if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists - else heads :: env.constrlists + let constrlists, constrs = + if b then + (* We rearrange constrs = c1..cn rem and constrlists = [d1..dr e1..ep] rem' into + constrs = e1..ep rem and constrlists [c1..cn d1..dr] rem' *) + let constrlist = List.hd env.constrlists in + let constrlist, tail = List.chop (List.length constrlist - p) constrlist in + (heads @ constrlist) :: List.tl env.constrlists, tail @ constrs + else + (* We rearrange constrs = c1..cn e1..ep rem into + constrs = e1..ep rem and add a constr list [c1..cn] *) + let constrlist, tail = List.chop (n - p) heads in + constrlist :: env.constrlists, tail @ constrs in ty_eval rem f { env with constrs; constrlists; } let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function | TyStop -> Stop -| TyMark (_, _, r) -> ty_erase r +| TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) | TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) @@ -398,9 +407,9 @@ let make_ty_rule assoc from forpat prods = let s = symbol_of_entry assoc from e in let bind = match var with None -> false | Some _ -> true in AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) - | GramConstrListMark (n, b) :: rem -> + | GramConstrListMark (n, b, p) :: rem -> let AnyTyRule r = make_ty_rule rem in - AnyTyRule (TyMark (n, b, r)) + AnyTyRule (TyMark (n, b, p, r)) in make_ty_rule (List.rev prods) diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index ffea0819a..a9ae74fd6 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -109,3 +109,9 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) +{0, 1} + : nat * nat +{0, 1, 2} + : nat * (nat * nat) +{0, 1, 2, 3} + : nat * (nat * (nat * nat)) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 250aecafd..dee0f70f7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -160,3 +160,11 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). + +(**********************************************************************) +(* Test recursive notations with the recursive pattern repeated on the right *) + +Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). +Check {0,1}. +Check {0,1,2}. +Check {0,1,2,3}. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f5b31e89d..c0974d0a7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -615,46 +615,71 @@ let define_keywords = function let distribute a ll = List.map (fun l -> a @ l) ll - (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep) - as many times as expected in [n] argument *) -let rec expand_list_rule typ tkl x n i hds ll = - if Int.equal i n then + (* Expand LIST1(t,sep);sep;t;...;t (with the trailing pattern + occurring p times, possibly p=0) into the combination of + t;sep;t;...;t;sep;t (p+1 times) + t;sep;t;...;t;sep;t;sep;t (p+2 times) + ... + t;sep;t;...;t;sep;t;...;t;sep;t (p+n times) + t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) + +let expand_list_rule typ tkl x n p ll = + let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let tks = List.map (fun x -> GramConstrTerminal x) tkl in + let rec aux i hds ll = + if i < p then aux (i+1) (main :: tks @ hds) ll + else if Int.equal i (p+n) then let hds = - GramConstrListMark (n,true) :: hds + GramConstrListMark (p+n,true,p) :: hds @ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in distribute hds ll else - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in - let tks = List.map (fun x -> GramConstrTerminal x) tkl in - distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @ - expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll + distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @ + aux (i+1) (main :: tks @ hds) ll in + aux 0 [] ll + +let is_constr_typ typ x etyps = + match List.assoc x etyps with + | ETConstr typ' -> typ = typ' + | _ -> false + +let include_possible_similar_trailing_pattern typ etyps sl l = + let rec aux n = function + | Terminal s :: sl, Terminal s'::l' when s = s' -> aux n (sl,l') + | [], NonTerminal x ::l' when is_constr_typ typ x etyps -> try_aux n l' + | _ -> raise Exit + and try_aux n l = + try aux (n+1) (sl,l) + with Exit -> n,l in + try_aux 0 l let make_production etyps symbols = - let prod = - List.fold_right - (fun t ll -> match t with - | NonTerminal m -> - let typ = List.assoc m etyps in - distribute [GramConstrNonTerminal (typ, Some m)] ll - | Terminal s -> - distribute [GramConstrTerminal (CLexer.terminal s)] ll - | Break _ -> - ll - | SProdList (x,sl) -> - let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] - | Break _ -> [] - | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in - match List.assoc x etyps with - | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll - | ETBinder o -> - distribute - [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll - | _ -> - user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.")) - symbols [[]] in - List.map define_keywords prod + let rec aux = function + | [] -> [[]] + | NonTerminal m :: l -> + let typ = List.assoc m etyps in + distribute [GramConstrNonTerminal (typ, Some m)] (aux l) + | Terminal s :: l -> + distribute [GramConstrTerminal (CLexer.terminal s)] (aux l) + | Break _ :: l -> + aux l + | SProdList (x,sl) :: l -> + let tkl = List.flatten + (List.map (function Terminal s -> [CLexer.terminal s] + | Break _ -> [] + | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in + match List.assoc x etyps with + | ETConstr typ -> + let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in + expand_list_rule typ tkl x 1 p (aux l') + | ETBinder o -> + distribute + [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] (aux l) + | _ -> + user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in + let prods = aux symbols in + List.map define_keywords prods let rec find_symbols c_current c_next c_last = function | [] -> [] |