Merge PR#402: Uniform attribute handling in interfaces

3 files changed, 80 insertions, 19 deletions

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index fad6472911..28808a5814 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,7 +25,18 @@ echo $TRAVIS_PULL_REQUEST
 echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
-if [ $TRAVIS_PULL_REQUEST == "568" ] || [ $TRAVIS_BRANCH == "remove-tactic-compat" ]; then
-    fiat_parsers_CI_BRANCH=fix-ml
-    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat.git
+if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ]; then
+
+    mathcomp_CI_BRANCH=located_switch
+    mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
+
+    fiat_parsers_CI_BRANCH=located_switch
+    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat.git
+
+    bedrock_src_CI_BRANCH=located_switch
+    bedrock_src_CI_GITURL=https://github.com/ejgallego/bedrock.git
+
+    bedrock_facade_CI_BRANCH=located_switch
+    bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git
+
 fi
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8ea1638c99..527721f8a4 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,56 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+Location handling and AST attributes:
+
+  Location handling has been reworked. First, Loc.ghost has been
+  removed in favor of an option type, all objects carrying an optional
+  source code location have been switched to use `Loc.t option`.
+
+  Storage of location information has been also refactored. The main
+  datatypes representing Coq AST (constrexpr, glob_expr) have been
+  switched to a generic "node with attributes" representation `'a
+  CAst.ast`, which is a record of the form:
+
+```ocaml
+type 'a ast = private {
+  v   : 'a;
+  loc : Loc.t option;
+  ...
+}
+```
+  consumers of AST nodes are recommended to use accessor-based pattern
+  matching `{ v; loc }` to destruct `ast` object. Creation is done
+  with `CAst.make ?loc obj`, where the attributes are optional. Some
+  convenient combinators are provided in the module. A typical match:
+```
+| CCase(loc, a1) -> CCase(loc, f a1)
+```
+  is now done as:
+```
+| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
+```
+  or even better, if plan to preserve the attributes you can wrap your
+  top-level function in `CAst.map` to have:
+
+```
+| CCase(a1) -> CCase(f a1)
+```
+
+  This scheme based on records enables easy extensibility of the AST
+  node type without breaking compatibility.
+
+  Not all objects carrying a location have been converted to the
+  generic node representation, some of them may be converted in the
+  future, for some others the abstraction is not just worth it.
+
+  Thus, we still maintain a `'a Loc.located == Loc.t option * a'`,
+  tuple type which should be treated as private datatype (ok to match
+  against, but forbidden to manually build), and it is mandatory to
+  use it for objects that carry a location. This policy has been
+  implemented in the whole code base. Matching a located object hasn't
+  changed, however, `Loc.tag ?loc obj` must be used to build one.
+
 ** Tactic API **
 
 - pf_constr_of_global now returns a tactic instead of taking a continuation.
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ce6d5dff05..07a47c8b7a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -26,7 +26,7 @@ open Clenv
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
+let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
 
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
@@ -510,7 +510,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -526,46 +526,46 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
 open Libnames
 
-let encode_path loc prefix mpdir suffix id =
+let encode_path ?loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (string_of_mp mp))@
 	DirPath.repr dir) in
-  Qualid (loc, make_qualid
+  Qualid (Loc.tag ?loc @@ make_qualid
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
-let raw_string_of_ref loc _ = function
+let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
-      encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id)
+      encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id)
   | IndRef (kn,i) ->
       let (mp,dir,id) = repr_mind kn in
-      encode_path loc "IND" (Some (mp,dir)) [Label.to_id id]
+      encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id]
 	(Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       let (mp,dir,id) = repr_mind kn in
-      encode_path loc "CSTR" (Some (mp,dir))
+      encode_path ?loc "CSTR" (Some (mp,dir))
 	[Label.to_id id;Id.of_string ("_"^string_of_int i)]
 	(Id.of_string ("_"^string_of_int j))
   | VarRef id ->
-      encode_path loc "SECVAR" None [] id
+      encode_path ?loc "SECVAR" None [] id
 
-let short_string_of_ref loc _ = function
-  | VarRef id -> Ident (loc,id)
-  | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst)))
-  | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn)))
+let short_string_of_ref ?loc _ = function
+  | VarRef id -> Ident (Loc.tag ?loc id)
+  | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst)))
+  | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn)))
   | IndRef (kn,i) ->
-      encode_path loc "IND" None [Label.to_id (pi3 (repr_mind kn))]
+      encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))]
         (Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
-      encode_path loc "CSTR" None
+      encode_path ?loc "CSTR" None
         [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)]
         (Id.of_string ("_"^string_of_int j))