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 --- dev/top_printers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 474cc85c17..52cf8cf97d 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 -- 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. --- dev/top_printers.ml | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 52cf8cf97d..96cb9443c5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -521,7 +521,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.internal_ghost, rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] let _ = try @@ -537,46 +537,46 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.internal_ghost,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)) -- cgit v1.2.3 From 9122623f2377bfe6aad0d4ea662481992e768201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 19:40:57 +0200 Subject: [location] Remove `Loc.internal_ghost` `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. --- dev/top_printers.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 96cb9443c5..5fb0aebb52 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -521,7 +521,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.internal_ghost, rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] let _ = try @@ -537,7 +537,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.internal_ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] (* Setting printer of unbound global reference *) open Names -- cgit v1.2.3 From 6eb42e53ffafd9aed3c12805c6a228acccc03827 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 20:08:01 +0200 Subject: [location] Document changes. --- dev/doc/changes.txt | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7f915b7819..10c3f396e4 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,14 @@ 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 has been reworked, Loc.ghost has been removed in +favor of an option type. All objects carrying a source code location +have been switched to `'a Loc.located == Loc.t option * a'`, which +should be treated as private (that is, ok to match against, but +forbidden to manually build), and is mandatory to use for objects with +location. This policy has been implemented in the whole code base, +including all the ASTs for vernacular, gallina, and tactics. + ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other -- cgit v1.2.3 From cd21210dd88732196d97f5b7436946c6b39bbdf3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 19 Apr 2017 01:06:47 +0200 Subject: [travis] mathcomp and fiat overlay for #402 --- dev/ci/ci-user-overlay.sh | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index bb193ebb55..95e47eb988 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,6 +25,14 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT +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 +fi + if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then mathcomp_CI_BRANCH=no_camlp4_compat mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git -- cgit v1.2.3 From a02f76f38592fd84cabd34102d38412f046f0d1b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 25 Apr 2017 15:01:41 +0200 Subject: [located] [doc] Improve docs for `CAst.ast`. --- dev/doc/changes.txt | 56 ++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 49 insertions(+), 7 deletions(-) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 10c3f396e4..57e34f1c93 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,13 +51,55 @@ 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 has been reworked, Loc.ghost has been removed in -favor of an option type. All objects carrying a source code location -have been switched to `'a Loc.located == Loc.t option * a'`, which -should be treated as private (that is, ok to match against, but -forbidden to manually build), and is mandatory to use for objects with -location. This policy has been implemented in the whole code base, -including all the ASTs for vernacular, gallina, and tactics. +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. ** Ltac API ** -- cgit v1.2.3 From 94e783390ef9ad9d26a54add2287e0a3e58d1b70 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 24 May 2017 23:05:21 +0200 Subject: [location] [travis] Add overlays for located_switch --- dev/ci/ci-user-overlay.sh | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 4ad5123170..28808a5814 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -26,9 +26,17 @@ echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT 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 -- cgit v1.2.3