From 846b74275511bd89c2f3abe19245133050d2199c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Jan 2017 20:11:01 +0100
Subject: [constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
---
 interp/notation.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f7296..04711808b7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -472,11 +472,11 @@ let interp_prim_token =
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
 let rec rcp_of_glob looked_for = function
-  | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
-  | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+  | GVar (loc,id)     -> Loc.tag ~loc @@ RCPatAtom (Some id)
+  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None)
+  | GRef (loc,g,_)    -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[])
   | GApp (loc,GRef (_,g,_),l) ->
-    looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+    looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
   | _ -> raise Not_found
 
 let interp_prim_token_cases_pattern_expr loc looked_for p =
-- 
cgit v1.2.3


From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Jan 2017 13:02:55 +0100
Subject: [location] Move Glob_term.cases_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 04711808b7..aef0892996 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -273,7 +273,7 @@ let glob_constr_keys = function
   | _ -> [Oth]
 
 let cases_pattern_key = function
-  | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
+  | _, PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-- 
cgit v1.2.3


From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

---
 interp/notation.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index aef0892996..3bcec30012 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -264,12 +264,12 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 let prim_token_key_table = ref KeyMap.empty
 
 let glob_prim_constr_key = function
-  | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref)
+  | _, GApp ((_, GRef (ref,_)),_) | _, GRef (ref,_) -> RefKey (canonical_gr ref)
   | _ -> Oth
 
 let glob_constr_keys = function
-  | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth]
-  | GRef (_,ref,_) -> [RefKey (canonical_gr ref)]
+  | _, GApp ((_, GRef (ref,_)),_) -> [RefKey (canonical_gr ref); Oth]
+  | _, GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | _ -> [Oth]
 
 let cases_pattern_key = function
@@ -471,13 +471,14 @@ let interp_prim_token =
 
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
-let rec rcp_of_glob looked_for = function
-  | GVar (loc,id)     -> Loc.tag ~loc @@ RCPatAtom (Some id)
-  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None)
-  | GRef (loc,g,_)    -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[])
-  | GApp (loc,GRef (_,g,_),l) ->
-    looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
+let rec rcp_of_glob looked_for gt = Loc.map (function
+  | GVar id       -> RCPatAtom (Some id)
+  | GHole (_,_,_) -> RCPatAtom None
+  | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
+  | GApp ((_, GRef (g,_)),l) ->
+    looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
   | _ -> raise Not_found
+  ) gt
 
 let interp_prim_token_cases_pattern_expr loc looked_for p =
   interp_prim_token_gen (rcp_of_glob looked_for) loc p
@@ -521,8 +522,8 @@ let uninterp_prim_token_ind_pattern ind args =
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = GRef (Loc.ghost,ref,None) in
-    match numpr (GApp (Loc.ghost,ref,args')) with
+    let ref = Loc.tag @@ GRef (ref,None) in
+    match numpr (Loc.tag @@ GApp (ref,args')) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
-- 
cgit v1.2.3


From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 interp/notation.ml | 64 +++++++++++++++++++++++++++---------------------------
 1 file changed, 32 insertions(+), 32 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 3bcec30012..150be040f3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -220,10 +220,10 @@ let remove_delimiters scope =
        with Not_found ->
          assert false (* A delimiter for scope [scope] should exist *)
 
-let find_delimiters_scope loc key =
+let find_delimiters_scope ?loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
-    user_err ~loc ~hdr:"find_delimiters"
+    user_err ?loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
@@ -291,7 +291,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 type required_module = full_path * string list
 
 type 'a prim_token_interpreter =
-    Loc.t -> 'a -> glob_constr
+    ?loc:Loc.t -> 'a -> glob_constr
 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
@@ -299,7 +299,7 @@ type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
-    Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+    ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
 
 let prim_token_interpreter_tab =
   (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -309,7 +309,7 @@ let add_prim_token_interpreter sc interp =
     let cont = Hashtbl.find prim_token_interpreter_tab sc in
     Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
   with Not_found ->
-    let cont = (fun _loc _p -> raise Not_found) in
+    let cont = (fun ?loc _p -> raise Not_found) in
     Hashtbl.add prim_token_interpreter_tab sc (interp cont)
 
 let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
@@ -325,22 +325,22 @@ let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let delay dir int loc x = (dir, (fun () -> int loc x))
+let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+    (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+    (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
     (patl, (fun r -> mkString (uninterp r)), inpat)
 
-let check_required_module loc sc (sp,d) =
+let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ~loc ~hdr:"prim_token_interpreter"
+    user_err ?loc ~hdr:"prim_token_interpreter"
     (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
@@ -445,23 +445,23 @@ let notation_of_prim_token = function
   | Numeral n -> "- "^(to_string (neg n))
   | String _ -> raise Not_found
 
-let find_prim_token g loc p sc =
+let find_prim_token ?loc g p sc =
   (* Try for a user-defined numerical notation *)
   try
     let (_,c),df = find_notation (notation_of_prim_token p) sc in
-    g (Notation_ops.glob_constr_of_notation_constr loc c),df
+    g (Notation_ops.glob_constr_of_notation_constr ?loc c),df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
-  check_required_module loc sc spdir;
+  let (spdir,interp) = (Hashtbl.find prim_token_interpreter_tab sc) ?loc p in
+  check_required_module ?loc sc spdir;
   g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
 
-let interp_prim_token_gen g loc p local_scopes =
+let interp_prim_token_gen g ?loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
-  try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
+  try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
   with Not_found ->
-    user_err ~loc ~hdr:"interp_prim_token"
+    user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
@@ -480,14 +480,14 @@ let rec rcp_of_glob looked_for gt = Loc.map (function
   | _ -> raise Not_found
   ) gt
 
-let interp_prim_token_cases_pattern_expr loc looked_for p =
-  interp_prim_token_gen (rcp_of_glob looked_for) loc p
+let interp_prim_token_cases_pattern_expr ?loc looked_for p =
+  interp_prim_token_gen (rcp_of_glob looked_for) ?loc p
 
-let interp_notation loc ntn local_scopes =
+let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
-    user_err ~loc 
+    user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
@@ -541,7 +541,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true
+    try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
     with Not_found -> false in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -823,7 +823,7 @@ let pr_scope_classes sc =
 
 let pr_notation_info prglob ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++
-  prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
+  prglob (Notation_ops.glob_constr_of_notation_constr c)
 
 let pr_named_scope prglob scope sc =
  (if String.equal scope default_scope then
@@ -891,25 +891,25 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
       Some (ntn,sc,ref)
   | _ -> None
 
-let error_ambiguous_notation loc _ntn =
-  user_err ~loc  (str "Ambiguous notation.")
+let error_ambiguous_notation ?loc _ntn =
+  user_err ?loc (str "Ambiguous notation.")
 
-let error_notation_not_reference loc ntn =
-  user_err ~loc 
+let error_notation_not_reference ?loc ntn =
+  user_err ?loc 
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference loc test ntn sc =
+let interp_notation_as_global_reference ?loc test ntn sc =
   let scopes = match sc with
   | Some sc ->
-      let scope = find_scope (find_delimiters_scope Loc.ghost sc) in
+      let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
-  | [] -> error_notation_not_reference loc ntn
+  | [] -> error_notation_not_reference ?loc ntn
   | refs ->
       let f (ntn,sc,ref) =
         let def = find_default ntn !scope_stack in
@@ -919,8 +919,8 @@ let interp_notation_as_global_reference loc test ntn sc =
       in
       match List.filter f refs with
       | [_,_,ref] -> ref
-      | [] -> error_notation_not_reference loc ntn
-      | _ -> error_ambiguous_notation loc ntn
+      | [] -> error_notation_not_reference ?loc ntn
+      | _ -> error_ambiguous_notation ?loc ntn
 
 let locate_notation prglob ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in
-- 
cgit v1.2.3


From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 8 Apr 2017 23:19:35 +0200
Subject: [location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 150be040f3..03dffa6eef 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -471,7 +471,7 @@ let interp_prim_token =
 
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
-let rec rcp_of_glob looked_for gt = Loc.map (function
+let rec rcp_of_glob looked_for gt = CAst.map_from_loc (fun ?loc -> function
   | GVar id       -> RCPatAtom (Some id)
   | GHole (_,_,_) -> RCPatAtom None
   | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
-- 
cgit v1.2.3


From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Apr 2017 03:35:20 +0200
Subject: [location] [ast] Port module AST to CAst

---
 interp/notation.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 03dffa6eef..6b963b8c8d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -264,16 +264,16 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 let prim_token_key_table = ref KeyMap.empty
 
 let glob_prim_constr_key = function
-  | _, GApp ((_, GRef (ref,_)),_) | _, GRef (ref,_) -> RefKey (canonical_gr ref)
+  | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref)
   | _ -> Oth
 
 let glob_constr_keys = function
-  | _, GApp ((_, GRef (ref,_)),_) -> [RefKey (canonical_gr ref); Oth]
-  | _, GRef (ref,_) -> [RefKey (canonical_gr ref)]
+  | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth]
+  | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)]
   | _ -> [Oth]
 
 let cases_pattern_key = function
-  | _, PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
+  | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -471,14 +471,14 @@ let interp_prim_token =
 
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
-let rec rcp_of_glob looked_for gt = CAst.map_from_loc (fun ?loc -> function
+let rec rcp_of_glob looked_for = CAst.map (function
   | GVar id       -> RCPatAtom (Some id)
   | GHole (_,_,_) -> RCPatAtom None
   | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
-  | GApp ((_, GRef (g,_)),l) ->
+  | GApp ({ CAst.v = GRef (g,_)},l) ->
     looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
   | _ -> raise Not_found
-  ) gt
+  )
 
 let interp_prim_token_cases_pattern_expr ?loc looked_for p =
   interp_prim_token_gen (rcp_of_glob looked_for) ?loc p
@@ -522,8 +522,8 @@ let uninterp_prim_token_ind_pattern ind args =
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = Loc.tag @@ GRef (ref,None) in
-    match numpr (Loc.tag @@ GApp (ref,args')) with
+    let ref = CAst.make @@ GRef (ref,None) in
+    match numpr (CAst.make @@ GApp (ref,args')) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
-- 
cgit v1.2.3