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.
---
 pretyping/cases.ml     | 5 -----
 pretyping/glob_ops.ml  | 5 +++++
 pretyping/glob_ops.mli | 2 ++
 3 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 311c1c09ec..a0434f9279 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -450,11 +450,6 @@ let current_pattern eqn =
     | pat::_ -> pat
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let alias_of_pat = DAst.with_val (function
-  | PatVar name -> name
-  | PatCstr(_,_,name) -> name
-  )
-
 let remove_current_pattern eqn =
   match eqn.patterns with
     | pat::pats ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a21137a05c..eb8a22a881 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -19,6 +19,11 @@ open Ltac_pretype
 
 let cases_pattern_loc c = c.CAst.loc
 
+let alias_of_pat pat = DAst.with_val (function
+  | PatVar name -> name
+  | PatCstr(_,_,name) -> name
+  ) pat
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 9dd7068cbc..c894db18e7 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,8 @@ open Glob_term
 
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
+val alias_of_pat : 'a cases_pattern_g -> Name.t
+
 val cast_type_eq : ('a -> 'a -> bool) ->
   'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
 
-- 
cgit v1.2.3


From ead835b3e8c366800b8c95a28a89062abb62d807 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Aug 2017 13:20:11 +0200
Subject: Canonically add an encoding in glob_constr of "as" operator for
 cases_pattern.

---
 pretyping/glob_ops.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index eb8a22a881..f3573360d4 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -457,6 +457,10 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
 let rec cases_pattern_of_glob_constr na = DAst.map (function
   | GVar id ->
     begin match na with
@@ -473,6 +477,9 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
     | _ -> raise Not_found
     end
+  | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous ->
+     (* A canonical encoding of aliases *)
+     DAst.get (cases_pattern_of_glob_constr na' b)
   | _ -> raise Not_found
   )
 
-- 
cgit v1.2.3


From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 18:32:02 +0200
Subject: Adding patterns in the category of binders for notations.

For instance, the following is now possible:

  Check {(x,y)|x+y=0}.

Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
---
 pretyping/glob_ops.ml  | 21 ++++++++++++++++-----
 pretyping/glob_ops.mli |  6 +++++-
 2 files changed, 21 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f3573360d4..b3e6aa0591 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -515,23 +515,34 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
       drop_local_defs typi l in
   Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
+let add_alias ?loc na c =
+  match na with
+  | Anonymous -> c
+  | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
+
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function
-  | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
-  | PatCstr (cstr,l,Anonymous)  ->
+let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+  | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
+  | PatCstr (cstr,l,na)  ->
       let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
       let l = add_patterns_for_params_remove_local_defs cstr l in
-      GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+  | PatVar (Name id) when not isclosed ->
+      GVar id
+  | PatVar Anonymous when not isclosed ->
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
 let glob_constr_of_closed_cases_pattern p = match DAst.get p with
   | PatCstr (cstr,l,na) ->
       let loc = p.CAst.loc in
-      na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+      na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
+let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+
 (**********************************************************************)
 (* Interpreting ltac variables *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c894db18e7..7a6d501145 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -80,10 +80,14 @@ val map_pattern : (glob_constr -> glob_constr) ->
 
     Take the current alias as parameter,
     @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
+val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
 
 val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
+(** A canonical encoding of cases pattern into constr such that
+    composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
+val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
+
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
-- 
cgit v1.2.3


From 50970e4043d73d9a4fbd17ffe765745f6d726317 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Aug 2017 23:01:04 +0200
Subject: Using an "as" clause when needed for printing irrefutable patterns.

Example which is now reprinted as parsed:

  fun '((x,y) as z) => (y,x)=z
---
 pretyping/glob_ops.ml  | 5 +++++
 pretyping/glob_ops.mli | 2 ++
 2 files changed, 7 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index b3e6aa0591..25817478e7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -24,6 +24,11 @@ let alias_of_pat pat = DAst.with_val (function
   | PatCstr(_,_,name) -> name
   ) pat
 
+let set_pat_alias id = DAst.map (function
+  | PatVar Anonymous -> PatVar (Name id)
+  | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id)
+  | pat -> assert false)
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 7a6d501145..0d9fb1f453 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,6 +15,8 @@ val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val alias_of_pat : 'a cases_pattern_g -> Name.t
 
+val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
+
 val cast_type_eq : ('a -> 'a -> bool) ->
   'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
 
-- 
cgit v1.2.3