Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

3 files changed, 42 insertions, 11 deletions

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..25817478e7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -19,6 +19,16 @@ 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 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]
@@ -452,6 +462,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
@@ -468,6 +482,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
   )
 
@@ -503,23 +520,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 9dd7068cbc..0d9fb1f453 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,10 @@ 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 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
 
@@ -78,10 +82,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