From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Aug 2017 16:15:57 +0200
Subject: Moving the argument of CProdN/CLambdaN from binder_expr to
 local_binder_expr.

The motivations are:

- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
  before this patch, there is a different treatment of `Definition f
  '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
  to interpret `Definition f `pat := c : t`. With the patch, the fix
  to avoid seeing a variable named `pat` works for both `fun 'x =>
  ...` and `Definition f 'x := ...`.

The drawbacks are:

- Counterpart to reflecting the concrete syntax more closerly, there
  are more redundancies in the syntax. For instance, the case `CLetIn
  (na,b,t,c)` can appears also in the form `CProdN (CLocalDef
  (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
---
 printing/ppconstr.ml  | 68 ++-------------------------------------------------
 printing/ppconstr.mli |  8 ------
 2 files changed, 2 insertions(+), 74 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1146b42a01..c58d9eb9a6 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -394,68 +394,6 @@ let tag_var = tag Tag.variable
     if is_open then pr_delimited_binders pr_com_at sep pr_c
     else pr_undelimited_binders sep pr_c
 
-  let rec extract_prod_binders = let open CAst in function
-  (*  | CLetIn (loc,na,b,c) as x ->
-      let bl,c = extract_prod_binders c in
-      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | { v = CProdN ([],c) } ->
-      extract_prod_binders c
-    | { loc; v = CProdN ([[_,Name id],bk,t],
-              { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) }
-         when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
-      let bl,c = extract_prod_binders b in
-      CLocalPattern (loc, (p,None)) :: bl, c
-    | { loc; v = CProdN ((nal,bk,t)::bl,c) } ->
-      let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in
-      CLocalAssum (nal,bk,t) :: bl, c
-    | c -> [], c
-
-  let rec extract_lam_binders ce = let open CAst in match ce.v with
-  (*  | CLetIn (loc,na,b,c) as x ->
-      let bl,c = extract_lam_binders c in
-      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | CLambdaN ([],c) ->
-      extract_lam_binders c
-    | CLambdaN ([[_,Name id],bk,t],
-                { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} )
-         when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
-      let bl,c = extract_lam_binders b in
-      CLocalPattern (ce.loc,(p,None)) :: bl, c
-    | CLambdaN ((nal,bk,t)::bl,c) ->
-      let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in
-      CLocalAssum (nal,bk,t) :: bl, c
-    | _ -> [], ce
-
-  let split_lambda = CAst.with_loc_val (fun ?loc -> function
-    | CLambdaN ([[na],bk,t],c) -> (na,t,c)
-    | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c))
-    | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c))
-    | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
-    )
-
-  let rename na na' t c =
-    match (na,na') with
-      | (_,Name id), (_,Name id') ->
-        (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c)
-      | (_,Name id), (_,Anonymous) -> (na,t,c)
-      | _ -> (na',t,c)
-
-  let split_product na' = CAst.with_loc_val (fun ?loc -> function
-    | CProdN ([[na],bk,t],c) -> rename na na' t c
-    | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c))
-    | CProdN ((na::nal,bk,t)::bl,c) ->
-      rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c))
-    | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
-    )
-
-  let rec split_fix n typ def =
-    if Int.equal n 0 then ([],typ,def)
-    else
-      let (na,_,def) = split_lambda def in
-      let (na,t,typ) = split_product na typ in
-      let (bl,typ,def) = split_fix (n-1) typ def in
-      (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def)
-
   let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
@@ -574,8 +512,7 @@ let tag_var = tag Tag.variable
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
           lfix
         )
-      | CProdN _ ->
-        let (bl,a) = extract_prod_binders a in
+      | CProdN (bl,a) ->
         return (
           hov 0 (
             hov 2 (pr_delimited_binders pr_forall spc
@@ -583,8 +520,7 @@ let tag_var = tag Tag.variable
               str "," ++ pr spc ltop a),
           lprod
         )
-      | CLambdaN _ ->
-        let (bl,a) = extract_lam_binders a in
+      | CLambdaN (bl,a) ->
         return (
           hov 0 (
             hov 2 (pr_delimited_binders pr_fun spc
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1320cce9be..158906dd2a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -17,14 +17,6 @@ open Names
 open Misctypes
 open Notation_term
 
-val extract_lam_binders :
-  constr_expr -> local_binder_expr list * constr_expr
-val extract_prod_binders :
-  constr_expr -> local_binder_expr list * constr_expr
-val split_fix :
-  int -> constr_expr -> constr_expr ->
-  local_binder_expr list *  constr_expr * constr_expr
-
 val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
-- 
cgit v1.2.3


From 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Aug 2017 19:24:50 +0200
Subject: Introducing an intermediary type "constr_prod_entry_key" for grammar
 productions.

This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.

The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.

Also exporting less of extend.mli in API.
---
 printing/ppvernac.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 950246c531..a7e73c91f4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -102,7 +102,6 @@ open Decl_kinds
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
-    | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
-- 
cgit v1.2.3


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 ++++++++++++++---------
 printing/ppvernac.ml  |  2 +-
 printing/ppvernac.mli |  2 ++
 3 files changed, 17 insertions(+), 10 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c58d9eb9a6..8735059403 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 ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a7e73c91f4..ae73640525 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -96,7 +96,7 @@ open Decl_kinds
   let pr_set_entry_type = function
     | ETName -> str"ident"
     | ETReference -> str"global"
-    | ETPattern -> str"pattern"
+    | ETPattern _ -> str"pattern"
     | ETConstr _ -> str"constr"
     | ETOther (_,e) -> str e
     | ETBigint -> str "bigint"
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 34b4fb97f6..5e0cc8da5f 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,6 +9,8 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
+val pr_set_entry_type : ('a,'b) Extend.constr_entry_key_gen -> Pp.t
+
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
 
-- 
cgit v1.2.3


From 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 17:09:21 +0100
Subject: Notations: A step in cleaning constr_entry_key.

- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions
---
 printing/ppvernac.ml  | 30 +++++++++++++++++++-----------
 printing/ppvernac.mli |  2 +-
 2 files changed, 20 insertions(+), 12 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ae73640525..42329d03a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -93,16 +93,28 @@ open Decl_kinds
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
-  let pr_set_entry_type = function
+  let pr_at_level = function
+    | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+    | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+
+  let pr_set_entry_type pr = function
     | ETName -> str"ident"
     | ETReference -> str"global"
-    | ETPattern _ -> str"pattern"
-    | ETConstr _ -> str"constr"
+    | ETPattern None -> str"pattern"
+    | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETConstr lev -> str"constr" ++ pr lev
     | ETOther (_,e) -> str e
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
 
+  let pr_at_level_opt = function
+    | None -> mt ()
+    | Some n -> spc () ++ pr_at_level n
+
+  let pr_set_simple_entry_type =
+    pr_set_entry_type pr_at_level_opt
+
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
@@ -359,17 +371,13 @@ open Decl_kinds
   let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
 
   let pr_syntax_modifier = function
-    | SetItemLevel (l,NextLevel) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at next level"
-    | SetItemLevel (l,NumLevel n) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at level" ++ spc() ++ int n
-    | SetLevel n -> keyword "at level" ++ spc() ++ int n
+    | SetItemLevel (l,n) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+    | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
     | SetAssoc NonA -> keyword "no associativity"
-    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
     | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 5e0cc8da5f..603be63083 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,7 +9,7 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
-val pr_set_entry_type : ('a,'b) Extend.constr_entry_key_gen -> Pp.t
+val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
-- 
cgit v1.2.3


From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: Notations: Adding modifiers to tell which kind of binder a constr can
 parse.

Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".

This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.

The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
---
 printing/ppvernac.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 42329d03a7..2fc7843eda 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -97,13 +97,21 @@ open Decl_kinds
     | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
     | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
 
+  let pr_constr_as_binder_kind = function
+    | AsIdent -> keyword "as ident"
+    | AsIdentOrPattern -> keyword "as pattern"
+    | AsStrictPattern -> keyword "as strict pattern"
+
+  let pr_strict b = if b then str "strict " else mt ()
+
   let pr_set_entry_type pr = function
     | ETName -> str"ident"
     | ETReference -> str"global"
-    | ETPattern None -> str"pattern"
-    | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETPattern (b,None) -> pr_strict b ++ str"pattern"
+    | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
     | ETConstr lev -> str"constr" ++ pr lev
     | ETOther (_,e) -> str e
+    | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
@@ -373,6 +381,9 @@ open Decl_kinds
   let pr_syntax_modifier = function
     | SetItemLevel (l,n) ->
       prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+    | SetItemLevelAsBinder (l,bk,n) ->
+      prlist_with_sep sep_v2 str l ++
+      spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk
     | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
-- 
cgit v1.2.3


From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Nov 2017 13:30:36 +0100
Subject: Change default for notations with variables bound to both terms and
 binders.

For compatibility, the default is to parse as ident and not as pattern.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2fc7843eda..31c0d20f32 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -383,7 +383,7 @@ open Decl_kinds
       prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
     | SetItemLevelAsBinder (l,bk,n) ->
       prlist_with_sep sep_v2 str l ++
-      spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk
+      spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
     | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
-- 
cgit v1.2.3