diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 7 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 63 | ||||
| -rw-r--r-- | dev/top_printers.ml | 32 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
5 files changed, 86 insertions, 22 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 1dfade261f..a6972c9500 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -13,8 +13,8 @@ ######################################################################## # UniMath ######################################################################## -: ${UniMath_CI_BRANCH:=master} -: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} +: ${UniMath_CI_BRANCH:=coq_makefile2-fix} +: ${UniMath_CI_GITURL:=https://github.com/maximedenes/UniMath.git} ######################################################################## # Unicoq + Metacoq diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index fad6472911..1f7fbcbf68 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,7 +25,8 @@ 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 == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then + mathcomp_CI_BRANCH=options+remove_non_sync + mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git fi + diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8ea1638c99..d52c184623 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,63 @@ 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. + +In GOption: + + Support for non-synchronous options has been removed. Now all + options are handled as a piece of normal document state, and thus + passed to workers, etc... As a consequence, the field + `Goptions.optsync` has been removed. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. @@ -93,6 +150,12 @@ alternative solution would be to fully qualify Ltac modules, e.g. turning any call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not work for EXTEND macros though. +** Additional changes in tactic extensions ** + +Entry "constr_with_bindings" has been renamed into +"open_constr_with_bindings". New entry "constr_with_bindings" now +uses type classes and rejects terms with unresolved holes. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For 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)) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 64431ea161..fa2864cec9 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident}} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} |