diff options
80 files changed, 1320 insertions, 298 deletions
diff --git a/.gitattributes b/.gitattributes index 00f78b449..f2c096f2d 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,3 +1,36 @@ .gitattributes export-ignore .gitignore export-ignore .mailmap export-ignore + +*.asciidoc whitespace=trailing-space,tab-in-indent +*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent +*.bib whitespace=trailing-space,tab-in-indent +*.c whitespace=trailing-space,tab-in-indent +*.css whitespace=trailing-space,tab-in-indent +*.dtd whitespace=trailing-space,tab-in-indent +*.el whitespace=trailing-space,tab-in-indent +*.h whitespace=trailing-space,tab-in-indent +*.html whitespace=trailing-space,tab-in-indent +*.hva whitespace=trailing-space,tab-in-indent +*.js whitespace=trailing-space,tab-in-indent +*.json whitespace=trailing-space,tab-in-indent +*.lang whitespace=trailing-space,tab-in-indent +*.md whitespace=trailing-space,tab-in-indent +*.merlin whitespace=trailing-space,tab-in-indent +*.ml whitespace=trailing-space,tab-in-indent +*.ml4 whitespace=trailing-space,tab-in-indent +*.mli whitespace=trailing-space,tab-in-indent +*.mll whitespace=trailing-space,tab-in-indent +*.mllib whitespace=trailing-space,tab-in-indent +*.mlp whitespace=trailing-space,tab-in-indent +*.mlpack whitespace=trailing-space,tab-in-indent +*.nsh whitespace=trailing-space,tab-in-indent +*.nsi whitespace=trailing-space,tab-in-indent +*.py whitespace=trailing-space,tab-in-indent +*.sh whitespace=trailing-space,tab-in-indent +*.sty whitespace=trailing-space,tab-in-indent +*.tex whitespace=trailing-space,tab-in-indent +*.txt whitespace=trailing-space,tab-in-indent +*.v whitespace=trailing-space,tab-in-indent +*.xml whitespace=trailing-space,tab-in-indent +*.yml whitespace=trailing-space,tab-in-indent diff --git a/.travis.yml b/.travis.yml index b71f4cc85..3b90f7cf4 100644 --- a/.travis.yml +++ b/.travis.yml @@ -66,6 +66,17 @@ env: matrix: include: + - env: + - TEST_TARGET="lint" + install: [] + before_script: [] + addons: + apt: + sources: [] + packages: [] + script: + - dev/lint-repository.sh + # Full Coq test-suite with two compilers - env: - TEST_TARGET="test-suite" diff --git a/API/API.mli b/API/API.mli index e82297202..ccb71179d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4973,10 +4973,23 @@ end module Genprint : sig + type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + type printer_result = + | PrinterBasic of (unit -> Pp.t) + | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) + | PrinterNeedsContextAndLevel of printer_with_level type 'a printer = 'a -> Pp.t - val generic_top_print : Genarg.tlevel Genarg.generic_argument printer + type 'a top_printer = 'a -> printer_result val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'raw printer -> 'glb printer -> 'top printer -> unit + 'raw printer -> 'glb printer -> 'top top_printer -> unit + val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> + 'raw printer -> unit + val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit + val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer + val generic_val_print : Geninterp.Val.t top_printer end module Pputils : @@ -4997,6 +5010,8 @@ sig val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] + val lsimpleconstr : Notation_term.tolerability + val ltop : Notation_term.tolerability val pr_id : Names.Id.t -> Pp.t val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t @@ -5029,6 +5044,7 @@ sig val pr_constr_pattern : Pattern.constr_pattern -> Pp.t val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t @@ -5041,6 +5057,7 @@ sig val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t diff --git a/dev/base_include b/dev/base_include index 79ecd73e0..f2912e112 100644 --- a/dev/base_include +++ b/dev/base_include @@ -233,8 +233,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; -open Coqloop -let go = loop +let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) let _ = print_string diff --git a/dev/bugzilla2github_stripped.csv b/dev/bugzilla2github_stripped.csv new file mode 100644 index 000000000..3f5cbfd71 --- /dev/null +++ b/dev/bugzilla2github_stripped.csv @@ -0,0 +1,501 @@ +2, 1156 +3, 1157 +4, 1158 +7, 1160 +8, 1161 +10, 1163 +12, 1164 +13, 1165 +14, 1169 +16, 1171 +17, 1184 +18, 1190 +19, 1191 +20, 1193 +21, 1200 +23, 1201 +24, 1203 +25, 1208 +26, 1210 +27, 1212 +28, 1216 +30, 1217 +31, 1223 +34, 1227 +35, 1232 +36, 1235 +38, 1238 +39, 1244 +40, 1245 +41, 1246 +42, 1247 +44, 1248 +45, 1249 +46, 1250 +47, 1252 +48, 1253 +49, 1254 +50, 1256 +52, 1262 +54, 1263 +55, 1264 +56, 1265 +59, 1266 +60, 1267 +61, 1268 +63, 1270 +64, 1272 +65, 1274 +66, 1275 +69, 1276 +70, 1279 +71, 1283 +72, 1284 +73, 1285 +74, 1286 +75, 1287 +78, 1288 +79, 1291 +80, 1292 +82, 1293 +83, 1295 +84, 1296 +85, 1297 +86, 1299 +88, 1301 +89, 1303 +90, 1304 +91, 1305 +92, 1307 +93, 1308 +94, 1310 +95, 1312 +96, 1313 +97, 1314 +98, 1316 +99, 1318 +100, 1319 +101, 1320 +102, 1321 +103, 1323 +105, 1324 +106, 1327 +107, 1328 +108, 1330 +109, 1334 +112, 1335 +115, 1336 +119, 1337 +121, 1341 +123, 1342 +124, 1343 +125, 1344 +126, 1345 +127, 1346 +128, 1348 +129, 1349 +134, 1350 +135, 1351 +136, 1352 +137, 1353 +138, 1354 +139, 1355 +140, 1356 +142, 1357 +143, 1358 +144, 1359 +145, 1360 +147, 1361 +148, 1362 +149, 1363 +150, 1365 +152, 1366 +154, 1368 +155, 1369 +160, 1370 +161, 1371 +162, 1372 +164, 1373 +165, 1374 +166, 1376 +167, 1377 +169, 1378 +170, 1380 +178, 1382 +179, 1383 +180, 1384 +181, 1385 +182, 1386 +183, 1387 +184, 1390 +185, 1391 +186, 1392 +187, 1393 +189, 1394 +190, 1398 +191, 1401 +192, 1402 +194, 1403 +195, 1404 +196, 1405 +197, 1407 +198, 1409 +199, 1410 +202, 1412 +204, 1413 +205, 1421 +207, 1422 +209, 1423 +210, 1426 +212, 1427 +213, 1428 +214, 1429 +215, 1433 +216, 1435 +219, 1436 +220, 1437 +221, 1440 +222, 1444 +224, 1445 +225, 1450 +228, 1452 +229, 1453 +235, 1457 +236, 1458 +238, 1459 +239, 1460 +240, 1462 +242, 1465 +243, 1466 +244, 1470 +245, 1471 +248, 1472 +250, 1473 +253, 1474 +254, 1475 +259, 1476 +261, 1478 +262, 1479 +263, 1480 +264, 1481 +265, 1484 +266, 1485 +267, 1486 +268, 1488 +269, 1489 +270, 1490 +271, 1492 +272, 1493 +273, 1494 +274, 1498 +275, 1500 +277, 1503 +278, 1504 +279, 1505 +282, 1506 +283, 1511 +289, 1513 +290, 1514 +291, 1516 +292, 1517 +294, 1520 +295, 1521 +299, 1523 +301, 1524 +302, 1525 +303, 1527 +305, 1529 +311, 1530 +315, 1531 +316, 1532 +317, 1534 +320, 1535 +322, 1539 +324, 1541 +328, 1542 +329, 1543 +330, 1544 +331, 1545 +333, 1546 +335, 1547 +336, 1548 +338, 1549 +343, 1550 +348, 1551 +350, 1552 +351, 1553 +352, 1554 +353, 1555 +356, 1556 +363, 1557 +368, 1558 +371, 1559 +372, 1560 +413, 1561 +418, 1562 +420, 1563 +426, 1564 +431, 1565 +444, 1566 +447, 1567 +452, 1569 +459, 1570 +462, 1571 +463, 1573 +468, 1574 +472, 1575 +473, 1577 +509, 1578 +519, 1579 +529, 1580 +540, 1581 +541, 1583 +545, 1584 +546, 1585 +547, 1589 +550, 1590 +552, 1591 +553, 1592 +554, 1593 +574, 1594 +592, 1595 +602, 1597 +603, 1598 +606, 1599 +607, 1600 +667, 1601 +668, 1602 +686, 1603 +690, 1605 +699, 1606 +705, 1607 +708, 1609 +711, 1610 +728, 1611 +739, 1612 +742, 1613 +743, 1615 +774, 1617 +775, 1619 +776, 1623 +777, 1624 +778, 1625 +779, 1627 +780, 1628 +781, 1629 +782, 1630 +783, 1631 +784, 1632 +785, 1633 +786, 1636 +787, 1637 +788, 1638 +789, 1639 +790, 1640 +793, 1641 +794, 1642 +795, 1644 +797, 1645 +798, 1646 +803, 1647 +804, 1649 +805, 1650 +808, 1652 +813, 1653 +815, 1655 +816, 1656 +818, 1657 +820, 1658 +821, 1659 +822, 1660 +823, 1661 +826, 1662 +828, 1663 +829, 1664 +830, 1665 +831, 1666 +832, 1667 +834, 1668 +835, 1669 +836, 1670 +837, 5689 +839, 5791 +840, 5792 +841, 5793 +842, 5794 +843, 5795 +844, 5796 +846, 5797 +849, 5798 +850, 5799 +854, 5800 +855, 5801 +856, 5802 +857, 5803 +860, 5804 +861, 5805 +862, 5806 +863, 5807 +864, 5808 +865, 5809 +867, 5810 +868, 5811 +869, 5812 +870, 5813 +871, 5814 +872, 5815 +874, 5816 +875, 5817 +878, 5818 +879, 5819 +881, 5820 +883, 5821 +884, 5822 +885, 5823 +886, 5824 +888, 5825 +889, 5826 +890, 5827 +891, 5828 +892, 5829 +893, 5830 +894, 5831 +896, 5832 +898, 5833 +901, 5834 +903, 5835 +905, 5836 +906, 5837 +909, 5838 +914, 5839 +915, 5840 +922, 5841 +923, 5842 +925, 5843 +927, 5844 +931, 5845 +932, 5846 +934, 5847 +935, 5848 +936, 5849 +937, 5850 +938, 5851 +939, 5852 +940, 5853 +941, 5854 +945, 5855 +946, 5856 +947, 5857 +949, 5858 +950, 5859 +951, 5860 +952, 5861 +953, 5862 +954, 5863 +957, 5864 +960, 5865 +963, 5866 +965, 5867 +967, 5868 +968, 5869 +969, 5870 +972, 5871 +973, 5872 +974, 5873 +975, 5874 +976, 5875 +977, 5876 +979, 5877 +983, 5878 +984, 5879 +985, 5880 +986, 5881 +987, 5882 +988, 5883 +990, 5884 +991, 5885 +993, 5886 +996, 5887 +997, 5888 +1000, 5889 +1001, 5890 +1002, 5891 +1003, 5892 +1004, 5893 +1005, 5894 +1006, 5895 +1007, 5896 +1010, 5897 +1012, 5898 +1013, 5899 +1014, 5900 +1015, 5901 +1016, 5902 +1017, 5903 +1018, 5904 +1025, 5905 +1028, 5906 +1029, 5907 +1030, 5908 +1031, 5909 +1033, 5910 +1035, 5911 +1036, 5912 +1037, 5913 +1039, 5914 +1041, 5915 +1042, 5916 +1044, 5917 +1045, 5918 +1052, 5919 +1053, 5920 +1054, 5921 +1055, 5922 +1056, 5923 +1060, 5924 +1064, 5925 +1067, 5926 +1070, 5927 +1072, 5928 +1075, 5929 +1076, 5930 +1085, 5931 +1086, 5932 +1087, 5933 +1089, 5934 +1091, 5935 +1096, 5936 +1097, 5937 +1098, 5938 +1099, 5939 +1100, 5940 +1101, 5941 +1102, 5942 +1104, 5943 +1107, 5944 +1108, 5945 +1111, 5946 +1113, 5947 +1114, 5948 +1115, 5949 +1116, 5950 +1118, 5951 +1119, 5952 +1120, 5953 +1122, 5954 +1123, 5955 +1124, 5956 +1128, 5957 +1129, 5958 +1132, 5959 +1136, 5960 +1137, 5961 +1138, 5962 +1140, 5963 +1141, 5964 +1142, 5965 +1144, 5966 +1145, 5967 +1149, 5968 +1151, 5969 +1153, 5970 diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat index 7b17e721b..7140a7c61 100644 --- a/dev/build/windows/MakeCoq_regtest_noproxy.bat +++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat @@ -25,5 +25,5 @@ call MakeCoq_MinGW.bat ^ -cygquiet=Y ^
-destcyg %ROOTPATH%\cygwin_coq64_85pl2_abs ^
-destcoq %ROOTPATH%\coq64_85pl2_abs
- -pause
\ No newline at end of file +
+pause
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh index 0b61a31e7..16c972e80 100644 --- a/dev/build/windows/configure_profile.sh +++ b/dev/build/windows/configure_profile.sh @@ -40,4 +40,4 @@ if [ ! -f $donefile ] ; then echo unset OCAMLLIB >> $rcfile touch $donefile -fi
\ No newline at end of file +fi diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c index 5e02c72bb..41f64f98b 100644 --- a/dev/build/windows/patches_coq/ln.c +++ b/dev/build/windows/patches_coq/ln.c @@ -134,4 +134,4 @@ int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLin // Everything is fine return 0; -}
\ No newline at end of file +} diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9be882bb3..5c37b3133 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -28,11 +28,11 @@ ######################################################################## # Mathclasses + Corn ######################################################################## -: ${math_classes_CI_BRANCH:=external-bignums} -: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git} +: ${math_classes_CI_BRANCH:=master} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} -: ${Corn_CI_BRANCH:=external-bignums} -: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git} +: ${Corn_CI_BRANCH:=master} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} ######################################################################## # Iris diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6ade6576f..5be8257e8 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,17 @@ ## Changes between Coq 8.7 and Coq 8.8 +### Bug tracker + +As of 18/10/2017, Coq uses [GitHub issues](https://github.com/coq/coq/issues) +as bug tracker. +Old bug reports were migrated from Bugzilla to GitHub issues using +[this migration script](https://gist.github.com/Zimmi48/d923e52f64fe17c72852d9c148bfcdc6#file-bugzilla2github) +as detailed in [this blog post](https://www.theozimmermann.net/2017/10/bugzilla-to-github/). + +All the bugs with a number below 1154 had to be renumbered, you can find +a correspondence table [here](/dev/bugzilla2github_stripped.csv). +All the other bugs kept their number. + ### Plugin API Coq 8.8 offers a new module overlay containing a proposed plugin API @@ -38,6 +50,13 @@ Some tactics and related functions now support static configurability, e.g.: - if None, tells to behave as told with the flag Keep Proof Equalities - if Some b, tells to keep proof equalities iff b is true +Declaration of printers for arguments used only in vernac command + +- It should now use "declare_extra_vernac_genarg_pprule" rather than + "declare_extra_genarg_pprule", otherwise, a failure at runtime might + happen. An alternative is to register the corresponding argument as + a value, using "Geninterp.register_val0 wit None". + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 492e75a7b..3867d4af9 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -376,9 +376,27 @@ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ +&& \feature{miscellaneous optimizations}\\ Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ +Coq V8.5 & released 22 January 2016 & \\ + +Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\ +&& \feature{Ltac profiling} [14-6-2016]\\ +&& \feature{warning system} [29-6-2016]\\ +&& \feature{miscellaneous optimizations}\\ + +Coq V8.6 & released 14 December 2016 & \\ + +Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\ +&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\ +&& \feature{further optimizations}\\ + +Coq V8.7 beta 2 & released 6 October 2017 & \\ + +Coq V8.7 & released 18 October 2016 & \\ + \end{tabular} \medskip diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh new file mode 100755 index 000000000..eb12bc227 --- /dev/null +++ b/dev/lint-commits.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +# A script to check prettyness for a range of commits + +CALLNAME="$0" + +function usage +{ + >&2 echo "usage: $CALLNAME <commit> <commit>" + >&2 echo "The order of commits is as given to 'git diff'" +} + +if [ "$#" != 2 ]; +then + usage + exit 1 +fi + +BASE_COMMIT="$1" +HEAD_COMMIT="$2" + +# git diff --check +# uses .gitattributes to know what to check +if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT"; +then + : +else + >&2 echo "Whitespace errors!" + >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'." + >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." + exit 1 +fi diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh new file mode 100755 index 000000000..ecf7880e2 --- /dev/null +++ b/dev/lint-repository.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +# A script to check prettyness over the repository. + +# lint-commits.sh seeks to prevent the worsening of already present +# problems, such as tab indentation in ml files. lint-repository.sh +# seeks to prevent the (re-)introduction of solved problems, such as +# newlines at the end of .v files. + +CODE=0 + +if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; +then + # Some problems are too widespread to fix in one commit, but we + # can still check that they don't worsen. + CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} + PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} + MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD) + dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1 +fi + +# Check that the files with 'whitespace' gitattribute end in a newline. +# xargs exit status is 123 if any file failed the test +find . "(" -path ./.git -prune ")" -type f \ +-o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \ +-print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1 + +exit $CODE diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh index b8c1e5ee7..71a9162ef 100644 --- a/dev/nsis/FileAssociation.nsh +++ b/dev/nsis/FileAssociation.nsh @@ -187,4 +187,4 @@ NoOwn: !verbose pop !macroend -!endif # !FileAssociation_INCLUDED
\ No newline at end of file +!endif # !FileAssociation_INCLUDED diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh new file mode 100755 index 000000000..1c578c05c --- /dev/null +++ b/dev/tools/check-eof-newline.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +if [ -z "$(tail -c 1 "$1")" ] +then + exit 0 +else + echo "No newline at end of file $1!" + exit 1 +fi diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh new file mode 100755 index 000000000..8159506b4 --- /dev/null +++ b/dev/tools/should-check-whitespace.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +# determine if a file has whitespace checking enabled in .gitattributes + +git check-attr whitespace -- "$1" | grep -q -v 'unspecified$' diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css index 0b1e640b3..d1b2ce111 100644 --- a/doc/common/styles/html/simple/style.css +++ b/doc/common/styles/html/simple/style.css @@ -10,4 +10,4 @@ margin: 0pt; padding: .5ex 1em; list-style: none -}
\ No newline at end of file +} diff --git a/doc/refman/index.html b/doc/refman/index.html index 9b5250abc..b937350e6 100644 --- a/doc/refman/index.html +++ b/doc/refman/index.html @@ -11,4 +11,4 @@ <FRAME SRC="menu.html"> </FRAMESET> -</HTML>
\ No newline at end of file +</HTML> diff --git a/engine/evd.ml b/engine/evd.ml index 324f883e8..a668826a7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -124,8 +124,7 @@ end (* The type of mappings for existential variables *) -module Dummy = struct end -module Store = Store.Make(Dummy) +module Store = Store.Make () type evar = Term.existential_key diff --git a/engine/geninterp.ml b/engine/geninterp.ml index e79e258fb..768ef3cfd 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -9,11 +9,11 @@ open Names open Genarg -module TacStore = Store.Make(struct end) +module TacStore = Store.Make () (** Dynamic toplevel values *) -module ValT = Dyn.Make(struct end) +module ValT = Dyn.Make () module Val = struct @@ -47,6 +47,8 @@ struct end +module ValTMap = ValT.Map + module ValReprObj = struct type ('raw, 'glb, 'top) obj = 'top Val.tag diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 492e372ad..ae0b26e59 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -39,6 +39,10 @@ sig val inject : 'a tag -> 'a -> t end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the diff --git a/engine/namegen.ml b/engine/namegen.ml index 2e62b8901..a38c73ed0 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -376,15 +376,22 @@ let next_name_for_display sigma flags = | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in sigma flags avoid na c = +let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c = match na with - | Anonymous when noccurn sigma 1 c -> + | Anonymous when noccurn_fun sigma 1 c -> (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in + let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in (idopt, Id.Set.add fresh_id avoid) +let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn + +let compute_displayed_name_in_gen f sigma = + (* only flag which does not need a constr, maybe to be refined *) + let flag = RenamingForGoal in + compute_displayed_name_in_gen_poly f sigma flag + let compute_and_force_displayed_name_in sigma flags avoid na c = match na with | Anonymous when noccurn sigma 1 c -> diff --git a/engine/namegen.mli b/engine/namegen.mli index 6fde90a39..d29b69259 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -106,10 +106,15 @@ val compute_displayed_name_in : val compute_and_force_displayed_name_in : evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_displayed_let_name_in : - evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t val rename_bound_vars_as_displayed : evar_map -> Id.Set.t -> Name.t list -> types -> types +(* Generic function expecting a "not occurn" function *) +val compute_displayed_name_in_gen : + (evar_map -> int -> 'a -> bool) -> + evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t + (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 12b7b171b..9742a002d 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl = value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule $wit$ - $pr_rules$ - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.")) - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) } - >> ] + <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ] open Pcaml diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 536ee7ca5..c2d767396 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -94,10 +94,14 @@ let coincide s pat off = done; !break +let check_separator sep = + if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep." + let rec parse_user_entry s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then let entry = parse_user_entry (String.sub s 3 (l-8)) "" in + check_separator sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then @@ -105,16 +109,20 @@ let rec parse_user_entry s sep = Ulist1sep (entry, sep) else if l > 5 && coincide s "_list" (l-5) then let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + check_separator sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then let entry = parse_user_entry (String.sub s 0 (l-9)) "" in Ulist0sep (entry, sep) else if l > 4 && coincide s "_opt" (l-4) then let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + check_separator sep; Uopt entry else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator sep; Uentryl ("tactic", n) else let s = match s with "hyp" -> "var" | _ -> s in + check_separator sep; Uentry s diff --git a/ide/tags.ml b/ide/tags.ml index 08ca47a84..402027179 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -15,33 +15,22 @@ let make_tag (tt:GText.tag_table) ~name prop = module Script = struct + (* More recently defined tags have highest priority in case of overlapping *) let table = GText.tag_table () - let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] - let incomplete = make_tag table ~name:"incomplete" [ - `BACKGROUND_STIPPLE_SET true; - ] + let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] - let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] - let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) - let ephemere = [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified] - - let all = - comment :: found :: sentence :: ephemere - - let edit_zone = - let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in - t#set_priority (List.length all); - t - let all = edit_zone :: all - + let comment = make_tag table ~name:"comment" [] + let sentence = make_tag table ~name:"sentence" [] + let edit_zone = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] (* for debugging *) + let all = edit_zone :: comment :: sentence :: ephemere end module Proof = struct diff --git a/ide/tags.mli b/ide/tags.mli index 265dfe46e..15a35185d 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -17,7 +17,6 @@ sig val processed : GText.tag val incomplete : GText.tag val unjustified : GText.tag - val found : GText.tag val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f1bee65ef..bb4227b4a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1120,7 +1120,11 @@ let any_any_branch = (* | _ => _ *) Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) -let rec glob_of_pat env sigma pat = DAst.make @@ match pat with +let compute_displayed_name_in_pattern sigma avoid na c = + let open Namegen in + compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c + +let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1130,7 +1134,7 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l) + GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1141,30 +1145,36 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), - [glob_of_pat env sigma c]) + [glob_of_pat avoid env sigma c]) | PApp (f,args) -> - GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) + GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args) | PSoApp (n,args) -> GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), - List.map (glob_of_pat env sigma) args) + List.map (glob_of_pat avoid env sigma) args) | PProd (na,t,c) -> - GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c) | PLetIn (na,b,t,c) -> - GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, - glob_of_pat (na::env) sigma c) + let na',avoid' = Namegen.compute_displayed_let_name_in sigma Namegen.RenamingForGoal avoid na c in + let env' = Termops.add_name na' env in + GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t, + glob_of_pat avoid' env' sigma c) | PLambda (na,t,c) -> - GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c) | PIf (c,b1,b2) -> - GIf (glob_of_pat env sigma c, (Anonymous,None), - glob_of_pat env sigma b1, glob_of_pat env sigma b2) + GIf (glob_of_pat avoid env sigma c, (Anonymous,None), + glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2) | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> - let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in - GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b) + let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in + GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b) | PCase (info,p,tm,bl) -> let mat = match bl, info.cip_ind with | [], _ -> [] | _, Some ind -> - let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in + let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in simple_cases_matrix_of_branches ind bl' | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in @@ -1173,16 +1183,16 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> - return_type_of_predicate ind nargs (glob_of_pat env sigma p) + return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p) | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in - GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) + | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = - extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) + extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in diff --git a/interp/genintern.ml b/interp/genintern.ml index f4996c997..2f2edab30 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -10,7 +10,7 @@ open Names open Mod_subst open Genarg -module Store = Store.Make(struct end) +module Store = Store.Make () type glob_sign = { ltacvars : Id.Set.t; diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 45dec5112..65c55a584 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -28,7 +28,7 @@ let wit_string : string uniform_genarg_type = make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 ~dyn:(val_tag (topwit wit_string)) "preident" + make0 "preident" let loc_of_or_by_notation f = function | AN c -> f c diff --git a/lib/cSig.mli b/lib/cSig.mli index 151cfbdca..6910cbbf0 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -48,8 +48,6 @@ end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) -module type EmptyS = sig end - module type MapS = sig type key diff --git a/lib/dyn.ml b/lib/dyn.ml index 6bd43455f..83e673d2c 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,6 +11,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type PreS = sig type 'a tag @@ -24,24 +44,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list @@ -59,7 +62,7 @@ sig end -module Make(M : CSig.EmptyS) = struct +module Make () = struct module Self : PreS = struct (* Dynamics, programmed with DANGER !!! *) @@ -104,6 +107,8 @@ let dump () = Int.Map.bindings !dyntab module Map(M : TParam) = struct type t = Obj.t M.t Int.Map.t +type 'a obj = 'a M.t +type 'a key = 'a tag let cast : 'a M.t -> 'b M.t = Obj.magic let empty = Int.Map.empty let add tag v m = Int.Map.add tag (cast v) m diff --git a/lib/dyn.mli b/lib/dyn.mli index e43c8a9bc..e0e1a9d14 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -13,6 +13,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type S = sig type 'a tag @@ -26,24 +46,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list @@ -59,5 +62,4 @@ end end -(** FIXME: use OCaml 4.02 generative functors when available *) -module Make(M : CSig.EmptyS) : S +module Make () : S diff --git a/lib/exninfo.ml b/lib/exninfo.ml index d049dc6cf..167d3d6dc 100644 --- a/lib/exninfo.ml +++ b/lib/exninfo.ml @@ -10,7 +10,7 @@ containing a pair composed of the distinguishing [token] and the backtrace information. We discriminate the token by pointer equality. *) -module Store = Store.Make(struct end) +module Store = Store.Make () type 'a t = 'a Store.field diff --git a/lib/genarg.ml b/lib/genarg.ml index b78fe4037..a3bfb405c 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -11,7 +11,7 @@ open Util module ArgT = struct - module DYN = Dyn.Make(struct end) + module DYN = Dyn.Make () module Map = DYN.Map type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag type any = Any : ('a, 'b, 'c) tag -> any diff --git a/lib/spawn.ml b/lib/spawn.ml index 0cf163e73..de31d87d0 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -28,8 +28,6 @@ module type Control = sig end -module type Empty = sig end - module type MainLoopModel = sig type async_chan type condition @@ -216,7 +214,7 @@ let rec wait p = end -module Sync(T : Empty) = struct +module Sync () = struct type process = { cin : in_channel; diff --git a/lib/spawn.mli b/lib/spawn.mli index a131715e9..fd2b92ae3 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -34,8 +34,6 @@ module type Control = sig end (* Abstraction to work with both threads and main loop models *) -module type Empty = sig end - module type MainLoopModel = sig type async_chan type condition @@ -64,7 +62,7 @@ module Async(ML : MainLoopModel) : sig end (* spawn a process and read its output synchronously *) -module Sync(T : Empty) : sig +module Sync () : sig type process val spawn : diff --git a/lib/store.ml b/lib/store.ml index a1788f7da..97a8fea08 100644 --- a/lib/store.ml +++ b/lib/store.ml @@ -14,10 +14,6 @@ stores, we might want something static to avoid troubles with plugins order. *) -module type T = -sig -end - module type S = sig type t @@ -30,7 +26,7 @@ sig val field : unit -> 'a field end -module Make (M : T) : S = +module Make () : S = struct let next = diff --git a/lib/store.mli b/lib/store.mli index 8eab314ed..5cc5bb859 100644 --- a/lib/store.mli +++ b/lib/store.mli @@ -9,11 +9,6 @@ (*** This module implements an "untyped store", in this particular case we see it as an extensible record whose fields are left unspecified. ***) -module type T = -sig -(** FIXME: Waiting for first-class modules... *) -end - module type S = sig type t @@ -42,5 +37,5 @@ sig end -module Make (M : T) : S +module Make () : S (** Create a new store type. *) diff --git a/library/libobject.ml b/library/libobject.ml index 013c6fa0a..0c11be9ab 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -9,7 +9,7 @@ open Libnames open Pp -module Dyn = Dyn.Make(struct end) +module Dyn = Dyn.Make () type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a diff --git a/library/summary.ml b/library/summary.ml index 69eff830d..9f49d1f83 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,7 +10,7 @@ open Pp open CErrors open Util -module Dyn = Dyn.Make(struct end) +module Dyn = Dyn.Make () type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3d00b220b..d34da159e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -543,11 +543,11 @@ let epsilon_value f e = (** Synchronized grammar extensions *) -module GramState = Store.Make(struct end) +module GramState = Store.Make () type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t -module GrammarCommand = Dyn.Make(struct end) +module GrammarCommand = Dyn.Make () module GrammarInterp = struct type 'a t = 'a grammar_extension end module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 62ecaa552..829556a71 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -144,8 +144,7 @@ END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d89586..fea9e837b 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -155,6 +155,4 @@ let () = | None -> mt () | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c22e68323..b148d962e 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in - Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d588c888c..e467d3e2c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -116,7 +116,13 @@ type 'a extra_genarg_printer = | Val.Base t -> begin match Val.eq t tag with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some Refl -> + let open Genprint in + match generic_top_print (in_gen (Topwit wit) x) with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -432,12 +438,13 @@ type 'a extra_genarg_printer = let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) - let pr_clauses default_is_concl pr_id = function + (* Some true = default is concl; Some false = default is all; None = no default *) + let pr_clauses has_default pr_id = function | { onhyps=Some []; concl_occs=occs } - when (match default_is_concl with Some true -> true | _ -> false) -> + when (match has_default with Some true -> true | _ -> false) -> pr_with_occurrences mt (occs,()) | { onhyps=None; concl_occs=AllOccurrences } - when (match default_is_concl with Some false -> true | _ -> false) -> mt () + when (match has_default with Some false -> true | _ -> false) -> mt () | { onhyps=None; concl_occs=NoOccurrences } -> pr_in (str " * |-") | { onhyps=None; concl_occs=occs } -> @@ -1174,83 +1181,122 @@ let declare_extra_genarg_pprule wit g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x in let h x = - let env = Global.env () in - h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + Genprint.PrinterNeedsContext (fun env sigma -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_vernac_genarg_pprule wit f = + let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + Genprint.register_vernac_print0 wit f + (** Registering *) -let run_delayed c = c (Global.env ()) Evd.empty +let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> + let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in + Miscprint.pr_intro_pattern print_constr p) + +let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> + pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, + pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) + +let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + Miscprint.pr_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + pr_with_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, c = match c with + | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) + | clear_flag,ElimOnAnonHyp n as x -> sigma, x + | clear_flag,ElimOnIdent id as x -> sigma, x in + pr_destruction_arg + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) + +let make_constr_printer f c = + Genprint.PrinterNeedsContextAndLevel { + Genprint.default_already_surrounded = Ppconstr.ltop; + Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; + Genprint.printer = (fun env sigma n -> f env sigma n c)} -let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) - | clear_flag,ElimOnAnonHyp n as x -> x - | clear_flag,ElimOnIdent id as x -> x +let lift f a = Genprint.PrinterBasic (fun () -> f a) let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - let pr_string s = str "\"" ++ str s ++ str "\"" in Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) int; + (pr_or_var int) (pr_or_var int) (lift int); Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); Genprint.register_print0 wit_ident - pr_id pr_id pr_id; + pr_id pr_id (lift pr_id); Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) pr_id; + (pr_located pr_id) (pr_located pr_id) (lift pr_id); Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); + pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id))) + (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) - Printer.pr_closed_glob + (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) - (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + pr_red_expr_env + ; + Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); + pr_bindings_env + ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); + pr_with_bindings_env + ; + Genprint.register_print0 wit_open_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + pr_with_bindings_env + ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it)); - Genprint.register_print0 Stdarg.wit_int int int int; - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; - Genprint.register_print0 Stdarg.wit_pre_ident str str str; - Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string + pr_destruction_arg_env + ; + Genprint.register_print0 Stdarg.wit_int int int (lift int); + Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); + Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); + Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); + Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) let () = let printer _ _ prtac = prtac (0, E) in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index d9da954fe..5ecfaf590 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -46,6 +46,10 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_vernac_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> unit + type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { @@ -69,11 +73,16 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t + +val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t + val pr_in_clause : ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t -val pr_clauses : bool option -> +val pr_clauses : (* default: *) bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t + (* Some true = default is concl; Some false = default is all; None = no default *) val pr_raw_generic : env -> rlevel generic_argument -> Pp.t @@ -116,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability + +val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) -> + 'a Genprint.top_printer diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index a79a92a66..4d171ecbc 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -17,15 +17,23 @@ open Geninterp exception CannotCoerceTo of string +let base_val_typ wit = + match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.") + let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_context" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in wit (* includes idents known to be bound and references *) let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_under_binders" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun c -> + Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0bf6e3d15..ee84be541 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -63,28 +63,37 @@ let get_separator = function | None -> user_err Pp.(str "Missing separator.") | Some sep -> sep -let rec parse_user_entry s sep = +let check_separator ?loc = function +| None -> () +| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") + +let rec parse_user_entry ?loc s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + check_separator ?loc sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in Ulist1sep (entry, get_separator sep) else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + check_separator ?loc sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in Ulist0sep (entry, get_separator sep) else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + check_separator ?loc sep; Uopt entry else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator ?loc sep; Uentryl ("tactic", n) else + let _ = check_separator ?loc sep in Uentry s let interp_entry_name interp symb = @@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s | TacNonTerm (loc, ((nt, sep), ido)) -> - let symbol = parse_user_entry nt sep in + let symbol = parse_user_entry ?loc nt sep in let interp s = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 99d7684d3..f171fd07d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let dummy_pat = PRel 0 -let intern_typed_pattern ist p = +let intern_typed_pattern ist ~as_type ~ltacvars p = (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) (* type it, so we remember the pattern as a glob_constr only *) + let metas,pat = + if !strict_check then + let ltacvars = { + Constrintern.ltac_vars = ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in + Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p + else + [], dummy_pat in let (glob,_ as c) = intern_constr_gen true false ist p in let bound_names = Glob_ops.bound_glob_vars glob in - (bound_names,c,dummy_pat) + metas,(bound_names,c,pat) let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = @@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> - Inr (intern_typed_pattern ist c)) + Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -529,7 +539,12 @@ let rec intern_atomic lf ist x = then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) | TacChange (Some p,c,cl) -> - TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, + let { ltacvars } = ist in + let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in + let fold accu x = Id.Set.add x accu in + let ltacvars = List.fold_left fold ltacvars metas in + let ist' = { ist with ltacvars } in + TacChange (Some pat,intern_constr ist' c, clause_app (intern_hyp_location ist) cl) (* Equality and inversion *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 66f124d2d..fd75862c6 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -76,6 +76,9 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) +let base_val_typ wit = + match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") + let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -124,6 +127,8 @@ type tacvalue = let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -231,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = let v = Value.normalize v in - if has_type v (topwit wit_tacvalue) then str "a tactic" - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in + let pr_with_env pr = match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - match env with - | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c - | _ -> str "a term" - else - str "a value of type" ++ spc () ++ pr_argument_type v + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in @@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c = end (** TODO: should use dedicated printers *) -let rec message_of_value v = +let message_of_value v = let v = Value.normalize v in - let open Ftactic in - if has_type v (topwit wit_tacvalue) then - Ftactic.return (str "<tactic>") - else if has_type v (topwit wit_constr) then - let v = out_gen (topwit wit_constr) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end - else if has_type v (topwit wit_unit) then - Ftactic.return (str "()") - else if has_type v (topwit wit_int) then - Ftactic.return (int (out_gen (topwit wit_int) v)) - else if has_type v (topwit wit_intro_pattern) then - let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = - let (sigma, c) = c env sigma in - pr_econstr_env env sigma c - in - Ftactic.enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end - else if has_type v (topwit wit_uconstr) then - let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_closed_glob_env (pf_env gl) - (project gl) c) - end - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end - else match Value.to_list v with - | Some l -> - Ftactic.List.map message_of_value l >>= fun l -> - Ftactic.return (prlist_with_sep spc (fun x -> x) l) - | None -> - let tag = pr_argument_type v in - Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) + let pr_with_env pr = + Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> Ftactic.return (pr ()) + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) @@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in sigma,(interp_hyp ist env sigma id,ipat) -let interp_binding_name ist sigma = function +let interp_binding_name ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function @@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,(interp_binding_name ist sigma b,c)) + sigma, (loc,(interp_binding_name ist env sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -1386,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end >>= fun v -> (* No errors happened, we propagate the trace *) let v = append_trace trace v in - Proofview.tclLIFT begin - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value None v) + let call_debug env = + Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in + begin + let open Genprint in + match generic_val_print v with + | PrinterBasic _ -> call_debug None + | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ad1409f5b..7f81d1aa3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -842,6 +842,15 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false +let find_most_recent_projection evi sols = + let sign = List.map get_id (evar_filtered_context evi) in + match sols with + | y::l -> + List.fold_right (fun (id,p as x) (id',_ as y) -> + if List.index Id.equal id sign < List.index Id.equal id' sign then x else y) + l y + | _ -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -1429,7 +1438,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> + | _ -> + let (id,p) = find_most_recent_projection evi sols in if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3b3ad021e..aaa946706 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -96,6 +96,31 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false +let rec occurn_pattern n = function + | PRel p -> Int.equal n p + | PApp (f,args) -> + (occurn_pattern n f) || (Array.exists (occurn_pattern n) args) + | PProj (_,arg) -> occurn_pattern n arg + | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t || + (occurn_pattern (n+1) c) + | PIf (c,c1,c2) -> + (occurn_pattern n c) || + (occurn_pattern n c1) || (occurn_pattern n c2) + | PCase(_,p,c,br) -> + (occurn_pattern n p) || + (occurn_pattern n c) || + (List.exists (fun (_,_,p) -> occurn_pattern n p) br) + | PMeta _ | PSoApp _ -> true + | PEvar (_,args) -> Array.exists (occurn_pattern n) args + | PVar _ | PRef _ | PSort _ -> false + | PFix fix -> not (noccurn n (mkFix fix)) + | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + +let noccurn_pattern n c = not (occurn_pattern n c) + exception BoundPattern;; let rec head_pattern_bound t = diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index ffe0186af..2d1ce1dbc 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern +val noccurn_pattern : int -> constr_pattern -> bool + exception BoundPattern (** [head_pattern_bound t] extracts the head variable/constant of the diff --git a/printing/genprint.ml b/printing/genprint.ml index 543b05024..776a212b5 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -8,13 +8,100 @@ open Pp open Genarg +open Geninterp + +(* We register printers at two levels: + - generic arguments for general printers + - generic values for printing ltac values *) + +(* Printing generic values *) + +type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + +type printer_result = +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| PrinterNeedsContextAndLevel of printer_with_level type 'a printer = 'a -> Pp.t +type 'a top_printer = 'a -> printer_result + +module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end) + +let print0_val_map = ref ValMap.empty + +let find_print_val_fun tag = + try ValMap.find tag !print0_val_map + with Not_found -> + let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in + CErrors.anomaly (msg (Val.repr tag)) + +let generic_val_print v = + let Val.Dyn (tag,v) = v in + find_print_val_fun tag v + +let register_val_print0 s pr = + print0_val_map := ValMap.add s pr !print0_val_map + +let combine_dont_needs pr_pair pr1 = function + | PrinterBasic pr2 -> + PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) + | PrinterNeedsContext pr2 -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (pr2 env sigma)) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded)) + +let combine_needs pr_pair pr1 = function + | PrinterBasic pr2 -> + PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) + | PrinterNeedsContext pr2 -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (pr2 env sigma)) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded)) + +let combine pr_pair pr1 v2 = + match pr1 with + | PrinterBasic pr1 -> + combine_dont_needs pr_pair pr1 (generic_val_print v2) + | PrinterNeedsContext pr1 -> + combine_needs pr_pair pr1 (generic_val_print v2) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded) + (generic_val_print v2) + +let _ = + let pr_cons a b = Pp.(a ++ spc () ++ b) in + register_val_print0 Val.typ_list + (function + | [] -> PrinterBasic mt + | a::l -> + List.fold_left (combine pr_cons) (generic_val_print a) l) + +let _ = + register_val_print0 Val.typ_opt + (function + | None -> PrinterBasic Pp.mt + | Some v -> generic_val_print v) + +let _ = + let pr_pair a b = Pp.(a ++ spc () ++ b) in + register_val_print0 Val.typ_pair + (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2) + +(* Printing generic arguments *) + type ('raw, 'glb, 'top) genprinter = { raw : 'raw printer; glb : 'glb printer; - top : 'top printer; + top : 'top -> printer_result; } module PrintObj = @@ -27,7 +114,7 @@ struct let printer = { raw = (fun _ -> str "<genarg:" ++ str name ++ str ">"); glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - top = (fun _ -> str "<genarg:" ++ str name ++ str ">"); + top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); } in Some printer | _ -> assert false @@ -37,6 +124,18 @@ module Print = Register (PrintObj) let register_print0 wit raw glb top = let printer = { raw; glb; top; } in + Print.register0 wit printer; + match val_tag (Topwit wit), wit with + | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' -> + register_val_print0 t top + | _ -> + (* An alias, thus no primitive printer attached *) + () + +let register_vernac_print0 wit raw = + let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in + let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in + let printer = { raw; glb; top; } in Print.register0 wit printer let raw_print wit v = (Print.obj wit).raw v diff --git a/printing/genprint.mli b/printing/genprint.mli index 130a89c92..2da9bbc36 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,20 +10,37 @@ open Genarg +type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + +type printer_result = +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| PrinterNeedsContextAndLevel of printer_with_level + type 'a printer = 'a -> Pp.t -val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t +type 'a top_printer = 'a -> printer_result + +val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) -val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer (** Printer for glob level generic arguments. *) -val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) +val register_print0 : ('raw, 'glb, 'top) genarg_type -> + 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit +val register_val_print0 : 'top Geninterp.Val.typ -> + 'top top_printer -> unit +val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> + 'raw printer -> unit + val generic_raw_print : rlevel generic_argument printer val generic_glb_print : glevel generic_argument printer -val generic_top_print : tlevel generic_argument printer - -val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> 'top printer -> unit +val generic_top_print : tlevel generic_argument top_printer +val generic_val_print : Geninterp.Val.t top_printer diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 102c6ef6d..109a40a03 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -738,34 +738,40 @@ let tag_var = tag Tag.variable pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Notation_term.precedence * Notation_term.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt + let pr prec = function + (* A toplevel printer hack mimicking parsing, incidentally meaning + that we cannot use [pr] correctly anymore in a recursive loop + if the current expr is followed by other exprs which would be + interpreted as arguments *) + | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us + | c -> pr prec c + let transf env c = if !Flags.beautify_file then let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr prec c = pr prec (transf (Global.env()) c) + let pr_expr prec c = pr prec (transf (Global.env()) c) - let pr_simpleconstr = function - | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us - | c -> pr lsimpleconstr c + let pr_simpleconstr = pr_expr lsimpleconstr let default_term_pr = { pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr ltop; + pr_lconstr_expr = pr_expr ltop; pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr ltop + pr_lconstr_pattern_expr = pr_expr ltop } let term_pr = ref default_term_pr let set_term_pr = (:=) term_pr + let pr_constr_expr_n n c = pr_expr n c let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c @@ -775,5 +781,5 @@ let tag_var = tag Tag.variable let pr_record_body = pr_record_body_gen pr - let pr_binders = pr_undelimited_binders spc (pr ltop) + let pr_binders = pr_undelimited_binders spc (pr_expr ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 7546c748d..be96cfce5 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t val pr_constr_expr : constr_expr -> Pp.t val pr_lconstr_expr : constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t +val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : constr_expr -> Pp.t; @@ -86,9 +87,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -type precedence -val lsimpleconstr : precedence -val ltop : precedence +val lsimpleconstr : tolerability +val ltop : tolerability val modular_constr_pr : - ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> precedence -> constr_expr -> Pp.t + ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index 28b10c781..c6650ea3b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -79,11 +79,14 @@ let _ = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) +let pr_econstr_n_core goal_concl_style env sigma n t = + pr_constr_expr_n n (extern_constr goal_concl_style env sigma t) let pr_econstr_core goal_concl_style env sigma t = pr_constr_expr (extern_constr goal_concl_style env sigma t) let pr_leconstr_core goal_concl_style env sigma t = pr_lconstr_expr (extern_constr goal_concl_style env sigma t) +let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) let _ = Hook.set Refine.pr_constr pr_constr_env @@ -94,6 +97,7 @@ let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (ECons let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c +let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c let pr_econstr_env env sigma c = pr_econstr_core false env sigma c @@ -166,6 +170,8 @@ let pr_glob_constr c = let (sigma, env) = get_current_context () in pr_glob_constr_env env c +let pr_closed_glob_n_env env sigma n c = + pr_constr_expr_n n (extern_closed_glob false env sigma c) let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) let pr_closed_glob c = diff --git a/printing/printer.mli b/printing/printer.mli index ba849bee6..658ea6060 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -33,6 +33,8 @@ val pr_constr_env : env -> evar_map -> constr -> Pp.t val pr_constr : constr -> Pp.t val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t + (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) @@ -48,6 +50,8 @@ val pr_econstr : EConstr.t -> Pp.t val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t + val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t @@ -70,6 +74,7 @@ val pr_ltype : types -> Pp.t val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 5d9b595d3..a356f32e9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -49,7 +49,7 @@ end type expiration = bool ref -module Make(T : Task) = struct +module Make(T : Task) () = struct exception Die type response = @@ -107,7 +107,7 @@ module Make(T : Task) = struct let open Feedback in feedback ~id:Stateid.initial (WorkerStatus(id, s)) - module Worker = Spawn.Sync(struct end) + module Worker = Spawn.Sync () module Model = struct @@ -354,5 +354,5 @@ module Make(T : Task) = struct end -module MakeQueue(T : Task) = struct include Make(T) end -module MakeWorker(T : Task) = struct include Make(T) end +module MakeQueue(T : Task) () = struct include Make(T) () end +module MakeWorker(T : Task) () = struct include Make(T) () end diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index a80918e93..1044e668b 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -41,7 +41,7 @@ end type expiration = bool ref -module MakeQueue(T : Task) : sig +module MakeQueue(T : Task) () : sig type queue @@ -76,7 +76,7 @@ module MakeQueue(T : Task) : sig end -module MakeWorker(T : Task) : sig +module MakeWorker(T : Task) () : sig val main_loop : unit -> unit val init_stdout : unit -> unit diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index a27c6d6cd..10b42f7e9 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) +module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index ac7a270ac..a1fe50c63 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) +module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout diff --git a/stm/stm.ml b/stm/stm.ml index 84a4c5cc5..3cac3b609 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -179,7 +179,7 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *) let default_info () = { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } -module DynBlockData : Dyn.S = Dyn.Make(struct end) +module DynBlockData : Dyn.S = Dyn.Make () (* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose * no constraint on properties, here we impose boxes to be non overlapping. @@ -1558,7 +1558,7 @@ and Slaves : sig end = struct (* {{{ *) - module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) + module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () let queue = ref None let init () = @@ -1884,7 +1884,7 @@ and Partac : sig end = struct (* {{{ *) - module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) + module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) () let vernac_interp ~solve ~abstract cancel nworkers safe_id id { indentation; verbose; loc; expr = e; strlen } @@ -2014,7 +2014,7 @@ and Query : sig end = struct (* {{{ *) - module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) + module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) () let queue = ref None diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 1716ac0c6..17f90b7b1 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) +module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 9507e90ba..da6a095ab 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -14,7 +14,7 @@ let check_vio (ts,f) = Stm.set_compilation_hints long_f_dot_v; List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts -module Worker = Spawn.Sync(struct end) +module Worker = Spawn.Sync () module IntOT = struct type t = int diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ab643239..f8f9e029b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1743,7 +1743,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma thm_ty - nprod in - if n<0 then error "Applied theorem has not enough premisses."; + if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags with exn when catchable_exception exn -> diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v new file mode 100644 index 000000000..b4f09305b --- /dev/null +++ b/test-suite/bugs/closed/2881.v @@ -0,0 +1,7 @@ +(* About scoping of pattern variables in strict/non-strict mode *) + +Ltac eta_red := change (fun a => ?f0 a) with f0. +Goal forall T1 T2 (f : T1 -> T2), (fun x => f x) = f. +intros. +eta_red. +Abort. diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v index 77bf169e1..e5bca5b5e 100644 --- a/test-suite/bugs/closed/5245.v +++ b/test-suite/bugs/closed/5245.v @@ -15,4 +15,4 @@ Undo. progress hnf; intros; exact eq_refl. Undo. unfold foo_rel. intros x. exact eq_refl. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/5401.v b/test-suite/bugs/closed/5401.v new file mode 100644 index 000000000..95193b993 --- /dev/null +++ b/test-suite/bugs/closed/5401.v @@ -0,0 +1,21 @@ +(* Testing printing of bound unnamed variables in pattern printer *) + +Module A. +Parameter P : nat -> Type. +Parameter v : forall m, P m. +Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. +Class U (R : P 0) (m : forall x, P x) : Prop. +Instance w : U (f _ (fun _ => v _)) v. +Print HintDb typeclass_instances. +End A. + +(* #5731 *) + +Module B. +Axiom rel : Type -> Prop. +Axiom arrow_rel : forall {A1}, A1 -> rel A1. +Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop. +Axiom inl_rel: forall_rel _ (fun _ => arrow_rel). +Hint Resolve inl_rel : foo. +Print HintDb foo. +End B. diff --git a/test-suite/bugs/closed/5786.v b/test-suite/bugs/closed/5786.v new file mode 100644 index 000000000..20301ec4f --- /dev/null +++ b/test-suite/bugs/closed/5786.v @@ -0,0 +1,29 @@ +(* Printing all kinds of Ltac generic arguments *) + +Tactic Notation "myidtac" string(v) := idtac v. +Goal True. +myidtac "foo". +Abort. + +Tactic Notation "myidtac2" ref(c) := idtac c. +Goal True. +myidtac2 True. +Abort. + +Tactic Notation "myidtac3" preident(s) := idtac s. +Goal True. +myidtac3 foo. +Abort. + +Tactic Notation "myidtac4" int_or_var(n) := idtac n. +Goal True. +myidtac4 3. +Abort. + +Tactic Notation "myidtac5" ident(id) := idtac id. +Goal True. +myidtac5 foo. +Abort. + + + diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out new file mode 100644 index 000000000..3855f88a7 --- /dev/null +++ b/test-suite/output/idtac.out @@ -0,0 +1,11 @@ +"foo" +True +foo +3 +foo +2 +< True False Prop > +< True False Prop > +< > +< > +<< 1 2 3 >> diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v new file mode 100644 index 000000000..ac60ea917 --- /dev/null +++ b/test-suite/output/idtac.v @@ -0,0 +1,45 @@ +(* Printing all kinds of Ltac generic arguments *) + +Tactic Notation "myidtac" string(v) := idtac v. +Goal True. +myidtac "foo". +Abort. + +Tactic Notation "myidtac2" ref(c) := idtac c. +Goal True. +myidtac2 True. +Abort. + +Tactic Notation "myidtac3" preident(s) := idtac s. +Goal True. +myidtac3 foo. +Abort. + +Tactic Notation "myidtac4" int_or_var(n) := idtac n. +Goal True. +myidtac4 3. +Abort. + +Tactic Notation "myidtac5" ident(id) := idtac id. +Goal True. +myidtac5 foo. +Abort. + +(* Checking non focussing of idtac for integers *) +Goal True/\True. split. +all:let c:=numgoals in idtac c. +Abort. + +(* Checking printing of lists and its focussing *) +Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">". +Goal True/\True. split. +all:myidtac6 True False Prop. +(* An empty list is focussing because of interp_genarg of a constr *) +(* even if it is not focussing on printing *) +all:myidtac6. +Abort. + +Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>". +Goal True/\True. split. +all:myidtac7 1 2 3. +Abort. diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v index 83d47dc68..3a1c6dabe 100644 --- a/test-suite/success/guard.v +++ b/test-suite/success/guard.v @@ -25,4 +25,4 @@ match f with match e in (_ = B) return (B -> foo A) -> nat with | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O) end g -end e.
\ No newline at end of file +end e. diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 79723431c..b5c5b2b96 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -288,7 +288,7 @@ let usage () = (Filename.basename Sys.argv.(0)) (Parser.print grammar)) -module Coqide = Spawn.Sync(struct end) +module Coqide = Spawn.Sync () let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index c16e2751b..910c81381 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -350,7 +350,7 @@ let rec loop doc = not possible due exceptions. *) in vernac_loop doc (Stm.get_current_state ~doc) with - | CErrors.Drop -> () + | CErrors.Drop -> doc | CErrors.Quit -> exit 0 | any -> Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++ diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 46dabf995..46934f326 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -36,4 +36,4 @@ val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) -val loop : Stm.doc -> unit +val loop : Stm.doc -> Stm.doc diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 19fcd9993..f3d5d9b85 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -79,6 +79,7 @@ let toploop_init = ref begin fun x -> will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed +let drop_last_doc = ref None (* Default toplevel loop *) let console_toploop_run doc = @@ -88,8 +89,9 @@ let console_toploop_run doc = Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - Coqloop.loop doc; + let doc = Coqloop.loop doc in (* Initialise and launch the Ocaml toplevel *) + drop_last_doc := Some doc; Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); (* We let the feeder in place for users of Drop *) @@ -183,9 +185,9 @@ let load_vernacular doc sid = (fun (doc,sid) (f_in, verbosely) -> let s = Loadpath.locate_file f_in in if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in + Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in else - Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s) + Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s) (doc, sid) (List.rev !load_vernacular_list) let load_init_vernaculars doc sid = @@ -726,7 +728,7 @@ let parse_args arglist = |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then - warning "Native compilation was disabled at configure time." + warning "Native compilation was disabled at configure time." else Flags.native_compiler := true |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 1c7c3f944..5b9494eaa 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -15,6 +15,9 @@ val init_toplevel : string list -> (Stm.doc * Stateid.t) option val start : unit -> unit +(* Last document seen after `Drop` *) +val drop_last_doc : Stm.doc option ref + (* For other toploops *) val toploop_init : (string list -> string list) ref val toploop_run : (Stm.doc -> unit) ref |