From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- printing/ppconstr.ml | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c58d9eb9a..873505940 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -86,8 +86,8 @@ let tag_var = tag Tag.variable open Notation - let print_hunks n pr pr_binders (terms, termlists, binders) unps = - let env = ref terms and envlist = ref termlists and bll = ref binders in + let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = + let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in (* Warning: @@ -102,6 +102,11 @@ let tag_var = tag Tag.variable let pp2 = aux l in let pp1 = pr (n, prec) c in return unp pp1 pp2 + | UnpBinderMetaVar (_, prec) as unp :: l -> + let c = pop bl in + let pp2 = aux l in + let pp1 = pr_patt (n, prec) c in + return unp pp1 pp2 | UnpListMetaVar (_, prec, sl) as unp :: l -> let cl = pop envlist in let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in @@ -127,9 +132,9 @@ let tag_var = tag Tag.variable in aux unps - let pr_notation pr pr_binders s env = + let pr_notation pr pr_patt pr_binders s env = let unpl, level = find_notation_printing_rule s in - print_hunks level pr pr_binders env unpl, level + print_hunks level pr pr_patt pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -263,8 +268,8 @@ let tag_var = tag Tag.variable in str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec - | CPatAlias (p, id) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las + | CPatAlias (p, na) -> + pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom @@ -292,7 +297,7 @@ let tag_var = tag Tag.variable pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> - let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not @@ -658,10 +663,10 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[])) -> + | CNotation ("( _ )",([t],[],[],[])) -> return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) | CNotation (s,env) -> - pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env + pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) | CPrim p -> -- cgit v1.2.3