diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1 --- a/Admin/components/components.sha1 +++ b/Admin/components/components.sha1 @@ -1,589 +1,590 @@ 59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz 23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz ed740867925dcf58692c8d3e350c28e3b4d4a60f Isabelle_app-20210126.tar.gz 8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz 8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz 51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz 8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz ce750fb7f26f6f51c03c6e78096a57b8eaf11d21 apache-commons-20211211.tar.gz fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz 81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz 97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz 5c5b7c18cc1dc2a4d22b997dac196da09eaca868 bash_process-1.2.3-1.tar.gz 48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz 11815d5f3af0de9022e903ed8702c136591f06fe bash_process-1.2.4-1.tar.gz 729486311833e4eff0fbf2d8041dddad520ca88c bash_process-1.2.4-2.tar.gz 7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee bash_process-1.2.4.tar.gz 9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz 351d1ec27061479595abdd52c28ff4c88c87746e bash_process-1.3.1.tar.gz 84246b9b6460296a6f8e8d661643b36719f7834a bash_process-1.3.tar.gz 7a92beb20d92cc71cabc8585d445f390b0749313 bash_process-20240326.tar.gz a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz 4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz dd6abfacab3f675ddc09376c6b66ce21448b1116 cakeml-2.0-1-test-nopie.tar.gz f92cff635dfba5d4d77f469307369226c868542c cakeml-2.0.tar.gz e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz 81ff56cd379744d1965425c7624feefffdf381eb ci-extras-2.tar.gz e880f31f59bd403fb72fcd3b5afb413c3831a21c csdp-6.1-1.tar.gz 2659100ba8e28e7cb0ecb554178ee5315d4a87f5 csdp-6.1.1.tar.gz a2bd94f4f9281dc70dfda66cf28016c2ffef7ed7 csdp-6.1.tar.gz ec17080269737e4a97b4424a379924c09b338ca2 csdp-6.2.0.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz 541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz 1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.tar.gz 3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz 76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz 03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.tar.gz 9e0d91f9f3bc0b69e60e50ca683cfcdcbfee6d62 cvc5-1.0.2.tar.gz fb4dce7e622c5e3daf56e7db190e05c34985c9f6 cvc5-1.1.1.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz 3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz 1fde9ddf0fa4f398965113d0c0c4f0e97c78d008 cygwin-20130716.tar.gz a03735a53c2963eb0b453f6a7282d3419f28bf38 cygwin-20130916.tar.gz 7470125fc46e24ee188bdaacc6d560e01b6fa839 cygwin-20140520.tar.gz db4dedae026981c5f001be283180abc1962b79ad cygwin-20140521.tar.gz acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz 3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz 8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz 238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz 629b8fbe35952d1551cd2a7ff08db697f6dff870 cygwin-20141024.tar.gz ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c cygwin-20150410.tar.gz fa712dd5ec66ad16add1779d68aa171ff5694064 cygwin-20151210.tar.gz 056b843d5a3b69ecf8a52c06f2ce6e696dd275f9 cygwin-20151221.tar.gz 44f3a530f727e43a9413226c2423c9ca3e4c0cf5 cygwin-20161002.tar.gz dd56dd16d861fc6e1a008bf5e9da6f33ed6eb820 cygwin-20161022.tar.gz d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz f8eb6a0f722e3cfe3775d1204c5c7063ee1f008e cygwin-20170828.tar.gz c22048912b010a5a0b4f2a3eb4d318d6953761e4 cygwin-20170930.tar.gz 5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz 2aa049170e8088de59bd70eed8220f552093932d cygwin-20190320.tar.gz fb898e263fcf6f847d97f564fe49ea0760bb453f cygwin-20190322.tar.gz cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz caa616fbab14c1fce790a87db5c4758c1322cf28 cygwin-20200116.tar.gz f053a9ab01f0be9cb456560f7eff66a8e7ba2fd2 cygwin-20200323.tar.gz 0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz a3d481401b633c0ee6abf1da07d75da94076574c cygwin-20201130.tar.gz 5b1820b87b25d8f2d237515d9854e3ce54ee331b cygwin-20211002.tar.gz 5dff30be394d88dd83ea584fa6f8063bdcdc21fd cygwin-20211004.tar.gz fffaae24da4d274d34b8dc79a76b478b87ec31dd cygwin-20211007.tar.gz 66e16dccd7b177c086ab53013c1b74d09c1893ad cygwin-20220831.tar.gz 6cd34e30e2e650f239d19725c3d15c206fb3a7cf cygwin-20221002.tar.gz fe8c541722f2fd6940f9e9948928b55fbc32d14b cygwin-20230711-1.tar.gz bc634cae08dea80238a830955894919af995cf06 cygwin-20230711.tar.gz ea23f766909632d8a6c0fefafbde467d1d289383 cygwin-20240305.tar.gz 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz 2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz a895a96ec7e6fcc275114bb9b4c92b20fac73dba e-2.0-1.tar.gz 2ebd7e3067a2cdae3cb8b073345827013978d74b e-2.0-2.tar.gz fac44556dd16f666a2c186be30aa6d8c67228bb9 e-2.0-3.tar.gz 5d36fb62912cfcff7f3b99a6266c578aafc288b7 e-2.0-4.tar.gz 3223c51c0b16fe00ced4ae903041fff858e61742 e-2.0-5.tar.gz 6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz 66449a7b68b7d85a7189e10735a81069356123b6 e-2.5-1.tar.gz 813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz 6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz 230d01c2c7274a17b6410535eb41665b16b41ae6 e-3.0.03.tar.gz 239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz 4a3b4b4e0441c4498a0c71dc348f3538be589a15 eptcs-1.7.0.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz 7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz 7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz 9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz 9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz 212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz 6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz 31d6abd58a4c2f7522f14283dfe04e2801a6e828 flatlaf-2.6.tar.gz b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz c947c751810777a4a7668d1b1b92942f178bb7b5 hugo-0.119.0.tar.gz 511fa8df8be88eb0500032bbd17742d33bdd4636 hugo-0.88.1.tar.gz 989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz 9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz f5c63689a394b974ac0d365debda577c6fa31c07 isabelle_fonts-20151107.tar.gz 812101680b75f7fa9ee8e138ea6314fa4824ea2d isabelle_fonts-20151229.tar.gz 2730e1475c7d655655882e75743e0b451725a274 isabelle_fonts-20151231.tar.gz 1f004a6bf20088a7e8f1b3d4153aa85de6fc1091 isabelle_fonts-20160101.tar.gz 379d51ef3b71452dac34ba905def3daa8b590f2e isabelle_fonts-20160102.tar.gz 878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz 8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz 9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz 620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz 3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz 928b5320073d04d93bcc5bc4347b6d01632b9d45 isabelle_fonts-20190210.tar.gz dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz 95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz dabcf5085d67c99159007007ff0e9bf775e423d1 isabelle_fonts-20190409.tar.gz 76827987c70051719e117138858930d42041f57d isabelle_fonts-20190717.tar.gz abc8aea3ae471f9313917008ac90e5c1c99e17da isabelle_fonts-20210317.tar.gz 3ff9195aab574fc75ca3b77af0adb33f9b6d7b74 isabelle_fonts-20210318.tar.gz b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz 9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz 1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz 667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz 916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz e413706694b0968245ee15183af2d464814ce0a4 isabelle_setup-20210711.tar.gz d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5 isabelle_setup-20210716-1.tar.gz 79fad009cb22aa5e7cb4aed3c810ad5f61790293 isabelle_setup-20210716.tar.gz 692a39f716998e556ec9559c9ca362fc8fc9d5b6 isabelle_setup-20210717-1.tar.gz 7322d6d84d75c486a58ed36630431db4499e3232 isabelle_setup-20210717-2.tar.gz 14f8508bcae9140815bb23e430e26d2cbc504b81 isabelle_setup-20210717.tar.gz ca801d5c380ea896ee32b309ff19ae5f34538963 isabelle_setup-20210718.tar.gz ac9739e38e4fbbfce1a71a0987a57b22f83922d3 isabelle_setup-20210724-1.tar.gz 4554679cc8ea31e539655810a14d14216b383d0e isabelle_setup-20210724-2.tar.gz 127a75ae33e97480d352087fcb9b47a632d77169 isabelle_setup-20210724.tar.gz 309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz 91c5d29e9fa40aee015e8e65ffea043e218c2fc5 isabelle_setup-20220323.tar.gz 056979bd1c08eb9d0d12cc1118b4ff70bfe2d594 isabelle_setup-20220701.tar.gz be91402b3e5ef5bc6d4802a45175ee238cd9653e isabelle_setup-20220808.tar.gz 171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz 7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz cb9f061ccd7c6f90d00c8aa115aeea8679f3f996 isabelle_setup-20221028.tar.gz f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz d30109fe63cec35c31cee9ffd17ae3a13c1e6a33 isabelle_setup-20230922.tar.gz cd92c141883f0f6a18adceb885316c8b6119e648 isabelle_setup-20240327.tar.gz f23037b322b968c61350f9ec9995a4f397e6c71c javamail-1.4.7.tar.gz 18e6b60ceb98e327fbf14e52f4613dd5b0483d2f javamail-20240109.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz 06ac8993b5bebd02c70f1bd18ce13075f01115f3 jdk-11.0.3+7.tar.gz e7e3cc9b0550c1e5d71197ad8c30f92b622d7183 jdk-11.0.4+11.tar.gz 49007a84a2643a204ce4406770dfd574b97880d9 jdk-11.0.5+10.tar.gz 3c250e98eb82f98afc6744ddc9170d293f0677e1 jdk-11.0.6+10.tar.gz 76cf7a141e15db30bd975089c65c833b58092aa7 jdk-11.0.9+11.tar.gz 71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz 72455a2fdb6cced9cd563f4d5d6134f7a6c34913 jdk-15.0.1+9.tar.gz e8ae300e61b0b121018456d50010b555bc96ce10 jdk-15.0.2+7.tar.gz a426a32ad34014953c0f7d4cc6f44199572e1c38 jdk-17+35.tar.gz 85707cfe369d0d32accbe3d96a0730c87e8639b5 jdk-17.0.1+12.tar.gz 699ab2d723b2f1df151a7dbcbdf33ddad36c7978 jdk-17.0.2+8.tar.gz 260f5e03e8fc7185f7987a6d2961a23abdce6a0b jdk-17.0.4.1+1.tar.gz 8f417fcbe5d0fef3a958aeb9740499230aa00046 jdk-17.0.5.tar.gz e904e85d0b5f6552344aa385c90f3ca528dc3514 jdk-17.0.6.tar.gz ee31c8ac65d5828d8c426fa3eedeb467cfa497ab jdk-17.0.7.tar.gz d4b43d1be10c9cffb406faeb36e9d46027834980 jdk-21.0.1.tar.gz 94f27b086cf6a2fb305cc961fe2932d8ea3634af jdk-21.0.2.tar.gz 8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz 38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz 13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz 5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz 71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz b66039bc6dc2bdb2992133743005e1e4fc58ae24 jdk-7u72.tar.gz d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz 7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz 5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz 741de6a4a805a0f9fb917d1845409e99346c2747 jdk-8u112.tar.gz ae7df8bd0c18eb40237cf54cc28933f4893b9c92 jdk-8u121.tar.gz 51531a3a0c16e180ed95cb7d2bd680c2ec0aa553 jdk-8u131.tar.gz e45edcf184f608d6f4a7b966d65a5d3289462693 jdk-8u144.tar.gz 264e806b9300a4fb3b6e15ba0e2c664d4ea698c8 jdk-8u152.tar.gz 84b04d877a2ea3a4e2082297b540e14f76722bc5 jdk-8u162.tar.gz 87303a0de3fd595aa3857c8f7cececa036d6ed18 jdk-8u172.tar.gz 9ae0338a5277d8749b4b4c7e65fc627319d98b27 jdk-8u181.tar.gz cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz 44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz 4132cf52d5025bf330d53b96a5c6466fef432377 jdk-8u51.tar.gz 74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz 2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz 778fd85c827ec49d2d658a832d20e63916186b0d jedit-20210715.tar.gz beb99f2cb0bd4e595c5c597d3970c46aa21616e4 jedit-20210717.tar.gz 33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz 0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz 258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz 7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz 9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz 6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz 7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz 8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz 8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz 06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz 5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz 87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz 65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz 30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz 054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz 4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz 14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz 8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz 7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz 23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz 9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.tar.gz cfa65bf8720b9b798ffa0986bafbc8437f44f758 jedit_build-20181026.tar.gz 847492b75b38468268f9ea424d27d53f2d95cef4 jedit_build-20181203.tar.gz 536a38ed527115b4bf2545a2137ec57b6ffad718 jedit_build-20190120.tar.gz 58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz 1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz 1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz 533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz 0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz a0744f1948abdde4bfb51dd4769b619e7444baf1 jedit_build-20210510-1.tar.gz 837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz 7bdae3d24b10261f6cb277446cf9ecab6062bd6f jedit_build-20210708.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz d84b7d8ef273afec55284327fca7dd20f5ecb77a jfreechart-1.5.1.tar.gz 6fa0c221ef55919b684449f0111a8112358e94ff jfreechart-1.5.3.tar.gz c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz 2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz df8bb213d39a7eecae97e6af3b11752d6c704c90 jsoup-1.15.4.tar.gz b1c8e2a289e40cbc139a3c371348cef3b537b1c7 jsoup-1.17.2.tar.gz 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz 0634a946b216f7f07f1a0f7e28cf345daa28828f kodkodi-1.5.3.tar.gz 52e95b3493d71902f9df89d0bb59d0046a5f0c63 kodkodi-1.5.4-1.tar.gz 267189c637de26cf304d699cfa95389da002b250 kodkodi-1.5.4.tar.gz 3ecdade953bb455ed2907952be287d7e5cf6533b kodkodi-1.5.5.tar.gz 8aa939f5127290eb9a99952d375be9ffbf90c43b kodkodi-1.5.6-1.tar.gz 6b12bf3f40b16fae8ff22aa39171fa018d107cb3 kodkodi-1.5.6.tar.gz c8b2e632f3ab959a4e037833a45e6360c8b72a99 kodkodi-1.5.7.tar.gz 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz 759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz 1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz 5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz 881741f6e7192fd03835b542b1db820daf0ae79c lipics-3.1.3.tar.gz 71b6a272d10c53bb54cba23102e15334ec39bfce llncs-2.22.tar.gz 29aa7179fbd02c528ac61df6e2e8512175093e35 llncs-2.23.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz 3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz 5fb1a2d21b220d0e588790c0203ac87c10ed0870 minisat-2.2.1-1.tar.gz ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz 59aa13f48685326995714cc6028aebb789e445e3 mlton-20210117-1.tar.gz 7624509ba58b9b8231626a66eda571fba69f7cd3 mlton-20210117-2.tar.gz 2d8c08fc623e7643a10ee031c7e9e7cb7c01d53a mlton-20210117-3.tar.gz 5d48b7163a68c18b691bedc1511364b0b103baeb mlton-20210117.tar.gz eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz 810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz 37bb6d934cfaf157efcadb349a0244d145ce15b0 naproche-20211211.tar.gz 5a8a59132476ae75cfddefc98781db55f18ed82c naproche-20220808.tar.gz 516b3714e56b708bc291bb0a592ea89de39ac894 naproche-20220910.tar.gz c695a038197477b69180917ee17ec2d92142e8f2 naproche-20220917.tar.gz 0b5a3161a18045540ab618249ba85a464c1fce66 naproche-20221002.tar.gz 48e9d4cbf95626c8e3013bee86ff82e67df6cefd naproche-20221018.tar.gz c66f5ce13d429ea9c8dcc0d33d34b7abf178da5d naproche-20221024.tar.gz 8e6cb32312336abcfe488b718bdc621461a7f132 naproche-20230711.tar.gz 3a310253f003f1759b575823f2a2e116ff6edeac naproche-20230902.tar.gz d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz 4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz 77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz 9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz 3d7b7690dfd09e25ad56e64b519f61f06e3ab706 old_vampire-4.2.2.tar.gz fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz 002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz 108e947d17e9aa6170872614492d8f647802f483 opam-2.1.0.tar.gz f8d0218371457eabe2b4214427d9570de92ed861 pdfjs-2.12.313.tar.gz aa7fc4a3d2cbd6c8744ddfeefd863828ea602bcd pdfjs-2.14.305.tar.gz 1b01278595b6dbd5c867dc55407b1ac705bc43b8 polyml-219e0a248f70.tar.gz 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz 7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz 1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz 36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz 36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz a588640dbf5da9ae15455b02ef709764a48637dc polyml-5.5.2-1.tar.gz 4b690390946f7bfb777b89eb16d6f08987cca12f polyml-5.5.2-2.tar.gz 5b31ad8556e41dfd6d5e85f407818be399aa3d2a polyml-5.5.2-3.tar.gz 532f6e8814752aeb406c62fabcfd2cc05f8a7ca8 polyml-5.5.2.tar.gz 1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5 polyml-5.5.3-20150820.tar.gz b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz 1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz 21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz 03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz 822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz 5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz 5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz 80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz 381a70cecf0fdee47f6842e2bdb5107ed52adab6 polyml-5.7.1-1.tar.gz 39dac33b569ac66f76126b8f4edc6d9227bd8a63 polyml-5.7.1-2.tar.gz 0b896ccc35bd3f2541cd55e6f0ed14637ed9fc68 polyml-5.7.1-4.tar.gz 262450ac9966abebae2e1d4f9ae703cfe0f5d8d9 polyml-5.7.1-5.tar.gz 1aeb57877d694db7fe4d4395287cddf3bc77710b polyml-5.7.1-6.tar.gz e3e7e20b1e0e5d5d68df4cd4caa1e1a7410d46b6 polyml-5.7.1-7.tar.gz 1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz 171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz 5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz 51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz 20a83fa58d497b533150defe39bcd4540529b25f polyml-5.8-20190306.tar.gz 9f0e9cd10df4c3383b063eb076e8b698ca50c3d0 polyml-5.8.1-20191101.tar.gz f46deb909d645ac8c140968e4d32b5763beb9add polyml-5.8.1-20191113.tar.gz 36a40a981b57daae0463d14940a8edf6fa1af179 polyml-5.8.1-20191114.tar.gz 525b05536b08c11a1eae943fe6818a8622326084 polyml-5.8.1-20191124.tar.gz 9043828803483ca14df64488dff014ad050a6d34 polyml-5.8.1-20200228.tar.gz 1186607e2c43b77db86731f12fbedb531ca50a21 polyml-5.8.1-20200708.tar.gz 22ae16bf7850e73b903d2ca8eb506da05b441cf3 polyml-5.8.1.tar.gz cb8e85387315f62dcfc6b21ec378186e58068f76 polyml-5.8.2.tar.gz d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz fb40145228f84513a9b083b54678a7d61b9c34c4 polyml-5.9-5d4caa8f7148.tar.gz 0f1c903b043acf7b221821d8b6374b3f943a122b polyml-5.9-610a153b941d.tar.gz 5f00a47b8f5180b33e68fcc6c343b061957a0a98 polyml-5.9-960de0cd0795.tar.gz 7056b285af67902b32f5049349a064f073f05860 polyml-5.9-cc80e2b43c38.tar.gz d0327534d5f3014f3faa2a40830a9ce1db953fef polyml-5.9.1.tar.gz 0c396bd6b46ff11a2432b91aab2be0248bd9b0a4 polyml-5.9.tar.gz f399ab9ee4a586fddeb6e73ca3605af65a89f969 polyml-5e9c8155ea96.tar.gz 2cea4dd48bb8b171bc04c9793a55c7fa4c2d96f1 polyml-a5d5fba90286.tar.gz 49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz 2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz 8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz b80c17398293d0c8f8d9923427176efb33cf2d89 polyml-test-15c840d48c9a.tar.gz a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz 4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz 85bfda83d138e936fdafd68ed3627b1058e5c2c3 polyml-test-7e49fce62e3d.tar.gz c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz 7df4857d73dbc9edda25a6ad329e47639e70fadf polyml-test-8fda4fd22441.tar.gz 2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz 3dfdc58e5d9b28f038a725e05c9c2f2ce0bb2632 polyml-test-a3cfdf648da-1.tar.gz e2f075b0cc709f4f7f6492b725362f9010b2c6d1 polyml-test-a3cfdf648da-2.tar.gz 33568f69ce813b7405386ddbefa14ad0342bb8f0 polyml-test-a3cfdf648da.tar.gz 4bedaac4f1fb9a9199aa63695735063c47059003 polyml-test-a444f281ccec.tar.gz f3031692edcc5d8028a42861e4e40779f0f9d3e1 polyml-test-b68438d33c69.tar.gz b2901b604124cfe46a6c28041f47c5a3bd3673f0 polyml-test-bafe319bc3a6-1.tar.gz 3ac7e916832c07accebeada9a81b301c299e1930 polyml-test-bafe319bc3a6.tar.gz cb2318cff6ea9293cd16a4435a4fe28ad9dbe0b8 polyml-test-cf46747fee61.tar.gz 67ffed2f98864721bdb1e87f0ef250e4c69e6160 polyml-test-d68c6736402e.tar.gz b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz 609c7d09d3ed01156ff91261e801e2403ff93729 polyml-test-e8d82343b692.tar.gz b6d87466e9b44e8ef4a2fac74c96b139080a506a polyml-test-f54aa41240d0.tar.gz d365f3fc11c2427cafc62b3c79951880a1476ebb polyml-test-f86ae3dc1686.tar.gz a619177143fea42a464f49bb864665407c07a16c polyml-test-fb4f42af00fa.tar.gz 53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz 3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz 7d6ef4320d5163ceb052eb83c1cb3968f099a422 postgresql-42.2.18.tar.gz e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz 1aaa38429dc9aa7b1095394d9a7ba3465f8d6e04 postgresql-42.2.24.tar.gz 231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz 6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.tar.gz f84c7ecafb07a0d763f1d70edc54f7c43c2e8c63 postgresql-42.4.0.tar.gz 143d0d32a13d7d8e15b9bab866e14ad4308a6246 postgresql-42.5.0.tar.gz 36a6e17794a93070278ac590650870ab73e6a7fb postgresql-42.6.0.tar.gz 65bf0d99f4e80f5802c573106327c337fe608fe7 postgresql-42.7.1.tar.gz 459c2b8da13910ba6c89ad91b9d26f4a63615117 postgresql-42.7.3.tar.gz f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz 3fc5e7f759e7220b9e3fc5bac296e312e34a60ad prismjs-1.29.0.tar.gz f042bba5fb82c7eb8aee99f92eb6ec38c8a067f7 python-3.10.4.tar.gz 31d84d632faa216b8f9abf8e8591695e467fbb24 rsync-3.2.7-1.tar.gz d144120b7cf2d2b3106632af0b98c78278c467d7 rsync-3.2.7.tar.gz 0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz 207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz 21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz 44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz 14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz 4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz 27a296495b2167148de06314ed9a942f2dbe23fe scala-2.11.4.tar.gz 4b24326541161ce65424293ca9da3e7c2c6ab452 scala-2.11.5.tar.gz e7cf20e3b27c894c6127c7a37042c1667f57385e scala-2.11.6.tar.gz 4810c1b00719115df235be1c5991aa6ea7186134 scala-2.11.7.tar.gz 3eca4b80710996fff87ed1340dcea2c5f6ebf4f7 scala-2.11.8.tar.gz 0004e53f885fb165b50c95686dec40d99ab0bdbd scala-2.12.0.tar.gz 059cbdc58d36e3ac1fffcccd9139ecd34f271882 scala-2.12.10.tar.gz 82056106aa6fd37c159ea76d16096c20a749cccd scala-2.12.11.tar.gz fe7ff585acffaad7f0dd4a1d079134d15c26ed0d scala-2.12.12.tar.gz 74a8c3dab3a25a87357996ab3e95d825dc820fd0 scala-2.12.2.tar.gz d66796a68ec3254b46b17b1f8ee5bcc56a93aacf scala-2.12.3.tar.gz 1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz 8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz 54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz 02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz 201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz caedd48ae65db9d116a0e1712eec3a66fe95c712 scala-2.13.5-1.tar.gz f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz 0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz 1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz 97c5b73011f4d6438b616e5940e6d759034f5414 scala-3.1.3.tar.gz 87c8e53100df4bc85cd8d4f55028088646d70fb4 scala-3.2.0-1.tar.gz c58db22b9e1e90f5b7a3f5edd8bdb4ddab4947fd scala-3.2.0-2.tar.gz 7677b02fe06c992ca6cf82bf68adb16287294256 scala-3.2.0.tar.gz bee1c9416a086e553057171e5cb571271ed02c60 scala-3.2.1.tar.gz 989736bb2693fa2c484f45841364a0bcb642acc1 scala-3.3.0.tar.gz 347437eb000f93bc751cbe6eccd31e7e798e10e5 scala-3.3.3.tar.gz bdc7406747790b590518182d8b4131b4a0e90c07 scala-3.4.1.tar.gz abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz 43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz 24a1397d06c79361d7507d59cbfe39962ce25148 sqlite-3.45.2.0.tar.gz b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz 27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz 4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz 806be457eb79408fcc5a72aeca3f64b2d89a6b63 sqlite-jdbc-3.30.1.tar.gz cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz 29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz 8a2ca4d02cfedbfe4dad4490f1ed3ddba33a009a sqlite-jdbc-3.36.0.3.tar.gz d2c707638b08ad56469b92dc2941d403efbb3394 sqlite-jdbc-3.39.4.1.tar.gz 12cb90b265bc2308858c63f00d5ecbfb80603dbd sqlite-jdbc-3.41.0.0.tar.gz 68b1b61cffb1e6d4f5821cd6c3bebf2a74af6a97 sqlite-jdbc-3.42.0.0-1.tar.gz 3535a04b8612cb1d98f0f7e41a0668e41667ec8b sqlite-jdbc-3.42.0.0.tar.gz 9b223d9453d654500616922231a7850fc927dcb7 sqlite-jdbc-3.45.0.0.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz fdc415284e031ee3eb2f65828cbc6945736fe995 stack-1.9.1.tar.gz 6e19948ff4a821e2052fc9b3ddd9ae343f4fcdbb stack-1.9.3.tar.gz f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz 423df2c437f7cceac1d269da8e379507feb246ef stack-2.13.1.tar.gz fdfea3b1c6b02612b1d50decb20b1a27ae741629 stack-2.15.1.tar.gz 6fd65aac9147ba93fa3356fa629f6911d82d767b stack-2.15.3.tar.gz +937a061f638823805ebc561b22465198f0ff1670 stack-2.15.5.tar.gz ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz fa2d882ec45cbc8c7d2f3838b705a8316696dc66 stack-2.7.3.tar.gz 18437bc9abd5b95be31a96f7c15a85a3ebf466cf stack-2.9.3.tar.gz 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz 601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz 14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz 44d67b6742919ce59a42368fc60e2afa210a3e42 sumatra_pdf-2.5.2.tar.gz 89719a13bc92810730a430973684629426ed1b2a sumatra_pdf-3.0.tar.gz f5afcc82f8e734665d38867e99475d3ad0d5ed15 sumatra_pdf-3.1.1.tar.gz a45eca5c1277f42f87bb8dc12a3074ccf5488221 sumatra_pdf-3.1.2-1.tar.gz 3b3239b2e6f8062b90d819f3703e30a50f4fa1e7 sumatra_pdf-3.1.2-2.tar.gz 8486387f61557147ec06b1f637117c017c8f0528 sumatra_pdf-3.1.2.tar.gz e8648878f908e93d64a393231ab21fdac976a9c2 sumatra_pdf-3.3.3.tar.gz 25d2004325585fceb0a951181716f77fc4d9d0d4 sumatra_pdf-3.4.6.tar.gz 20b43515c05ebd8d3ec090a119eff3acf2d912a5 sumatra_pdf-3.5.2.tar.gz 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz 399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz 0402978ca952f08eea73e483b694928ac402a304 vampire-4.5.1-1.tar.gz 26d9d171e169c6420a08aa99eda03ef5abb9c545 vampire-4.5.1.tar.gz 4571c042efd6fc3097e105a528826959acd888a3 vampire-4.6.tar.gz 150e2744c11582f681433a493aa2a7ab17cd511b vampire-4.8.tar.gz 98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz 52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-rmx.tar.gz d33e1e36139e86b9e9a48d8b46a6f90d7863a51c verit-2021.06-rmx-1.tar.gz c11d1120fcefaec79f099fe2be05b03cd2aed8b9 verit-2021.06-rmx.tar.gz b576fd5d89767c1067541d4839fb749c6a68d22c verit-2021.06.1-rmx.tar.gz ddfac93c72f79f712a42eb2638b2693d6f9f4692 verit-2021.06.2-rmx-1.tar.gz 19c6e5677b0a26cbc5805da79d00d06a66b7a671 verit-2021.06.2-rmx.tar.gz c4666a6d8080b5e376b50471fd2d9edeb1f9c988 vscode_extension-20220324.tar.gz 86c952d739d1eb868be88898982d4870a3d8c2dc vscode_extension-20220325.tar.gz 5293b9e77e5c887d449b671828b133fad4f18632 vscode_extension-20220829.tar.gz 0d9551ffeb968813b6017278fa7ab9bd6062883f vscode_extension-20230206.tar.gz 67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz c439ab741e0cc49354cc03aa9af501202a5a38e3 vscodium-1.70.1.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz 8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz 14807afcf69e50d49663d5b48f4b103f30ae842b windows_app-20150821.tar.gz ed106181510e825bf959025d8e0a2fc3f78e7a3f windows_app-20180417.tar.gz e809e4ab0d33cb413a7c47dd947e7dbdfcca1c24 windows_app-20181002.tar.gz 9e96ba128a0617a9020a178781df49d48c997e19 windows_app-20181006.tar.gz 4883f93efb27ae51fb2cc0e1f52309728f2dc407 windows_app-20240202.tar.gz 5269b9e38fe58be10272d6817dbfd08b67b312e7 windows_app-20240204.tar.gz 94fecdab25ddc52b5afde4ab3f017a3c14c656c8 windows_app-20240205.tar.gz 1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz 2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz c22196148fcace5443a933238216cff5112948df xz-java-1.5.tar.gz 4368ee09154dff42666a8c87e072261745619e51 xz-java-1.6.tar.gz 63f5fa09e92a895cb9aea27d7142abc86c487d25 xz-java-1.8.tar.gz a06875bdadd653627a68d2083c5178c1264d8fc6 xz-java-1.9.tar.gz 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz 3a8f77822278fe9250890e357248bc678d8fac95 z3-3.2-1.tar.gz 12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz d94a716502c8503d63952bcb4d4176fac8b28704 z3-4.0.tar.gz 86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz 06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz ed37c451b9b748901295898bf713b24d22cc8c17 z3-4.4.0_4.4.1.tar.gz 93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz 4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz d735a4450c6c2ead107179e785942aa6d4cc40c4 z3-4.4.0pre-4.tar.gz 517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz 6e5d7a65757cac970eb5ad28cd62130c99f42c23 z3-4.4.1.tar.gz aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz 9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz b129ec4f8a4474953ec107536298ee08a01fbebc zipperposition-2.1-1.tar.gz 5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz c101182780aeafbc2e0ea7e8b10b91c6f7483af2 zstd-jni-1.5.2-5.tar.gz d787fd0d0ee1827b6fc4d6288363f922770490e0 zstd-jni-1.5.5-4.tar.gz diff --git a/Admin/components/main b/Admin/components/main --- a/Admin/components/main +++ b/Admin/components/main @@ -1,45 +1,45 @@ #main components for repository clones or release bundles gnu-utils-20211030 bash_process-20240326 bib2xhtml-20190409 csdp-6.1.1 cvc4-1.8 e-3.0.03 easychair-3.5 eptcs-1.7.0 flatlaf-2.6 foiltex-2.1.4b idea-icons-20210508 isabelle_fonts-20211004 isabelle_setup-20240327 javamail-20240109 jdk-21.0.2 jedit-20231120 jfreechart-1.5.3 jortho-1.0-2 jsoup-1.17.2 kodkodi-1.5.7 lipics-3.1.3 llncs-2.23 minisat-2.2.1-1 mlton-20210117-3 nunchaku-0.5 opam-2.0.7 pdfjs-2.14.305 polyml-5.9.1 postgresql-42.7.3 prismjs-1.29.0 rsync-3.2.7-1 scala-3.3.3 smbc-0.4.1 spass-3.8ds-2 sqlite-3.45.2.0 -stack-2.15.3 +stack-2.15.5 vampire-4.8 verit-2021.06.2-rmx-1 vscode_extension-20230206 vscodium-1.70.1 xz-java-1.9 z3-4.4.0pre-4 zipperposition-2.1-1 zstd-jni-1.5.5-4 diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,203 +1,203 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 17 -target 17" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -java-output-version 17 -source 3.3 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m" ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex) ### case "$ISABELLE_PLATFORM_FAMILY" in windows*) ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors" ;; *) ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error" ;; esac ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex -c -q" ISABELLE_EPSTOPDF="epstopdf" ### ### Misc path settings ### isabelle_directory '~' isabelle_directory '$ISABELLE_HOME_USER' isabelle_directory '~~' isabelle_directory '$ISABELLE_COMPONENTS_BASE' ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). case "$ISABELLE_PLATFORM_FAMILY" in windows*) ISABELLE_TMP_PREFIX="$TMPDIR/isabelle" ;; *) ISABELLE_TMP_PREFIX="/tmp/isabelle-${USER:-$LOGNAME}" ;; esac # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs and external files ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" ISABELLE_DOCS_EXAMPLES="~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux*) ISABELLE_OPEN="xdg-open" ;; macos*) ISABELLE_OPEN="open" ;; windows*) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp" ### ### Registry ### isabelle_registry "$ISABELLE_HOME/etc/registry.toml?" isabelle_registry "$ISABELLE_HOME_USER/etc/registry.toml?" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols?" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" -ISABELLE_STACK_RESOLVER="lts-22.13" +ISABELLE_STACK_RESOLVER="lts-22.15" ISABELLE_GHC_VERSION="ghc-9.6.4" ### ### .Net / Fsharp ### ISABELLE_DOTNET_VERSION="8.0.203" ### ### Go ### ISABELLE_GO_VERSION="1.22.1" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/Pure/Admin/component_stack.scala b/src/Pure/Admin/component_stack.scala --- a/src/Pure/Admin/component_stack.scala +++ b/src/Pure/Admin/component_stack.scala @@ -1,131 +1,131 @@ /* Title: Pure/Admin/component_stack.scala Author: Makarius Build Isabelle component for GHC stack. See also: - https://www.haskellstack.org - https://github.com/commercialhaskell */ package isabelle object Component_Stack { /* platform information */ sealed case class Download_Platform(platform_name: String, download_name: String) { def is_windows: Boolean = platform_name.endsWith("-windows") } val platforms: List[Download_Platform] = List( Download_Platform("arm64-darwin", "osx-aarch64"), Download_Platform("arm64-linux", "linux-aarch64"), Download_Platform("x86_64-darwin", "osx-x86_64"), Download_Platform("x86_64-linux", "linux-x86_64"), Download_Platform("x86_64-windows", "windows-x86_64")) /* build stack */ val default_url = "https://github.com/commercialhaskell/stack/releases/download" - val default_version = "2.15.3" + val default_version = "2.15.5" def build_stack( base_url: String = default_url, version: String = default_version, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { /* component name */ val component = "stack-" + version val component_dir = Components.Directory(target_dir + Path.basic(component)).create(progress = progress) /* download executables */ for (platform <- platforms) { val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.explode(platform.platform_name)) val url = Url.append_path(base_url, "v" + version + "/stack-" + version + "-" + platform.download_name + ".tar.gz") val exe = Path.explode("stack").exe_if(platform.is_windows) Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_file => Isabelle_System.with_tmp_dir("tmp") { tmp_dir => Isabelle_System.download_file(url, archive_file, progress = progress) Isabelle_System.extract(archive_file, tmp_dir, strip = true) Isabelle_System.move_file(tmp_dir + exe, platform_dir) File.set_executable(platform_dir + exe) } } } /* settings */ component_dir.write_settings(""" ISABELLE_STACK="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}/stack" """) /* README */ File.write(component_dir.README, """This is stack """ + version + """ -- the Haskell Tool Stack. See also https://www.haskellstack.org and executables from """ + base_url + """ The downloaded files were renamed and made executable. Makarius """ + Date.Format.date(Date.now()) + "\n") /* AUTHORS and COPYING */ // download "latest" versions as reasonable approximation Isabelle_System.download_file("https://raw.githubusercontent.com/commercialhaskell/stack/master/LICENSE", component_dir.LICENSE) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("component_stack", "build component for GHC stack", Scala_Project.here, { args => var target_dir = Path.current var base_url = default_url var version = default_version val getopts = Getopts(""" Usage: isabelle component_stack [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") -V VERSION version (default: """" + default_version + """") Build component for GHC stack. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), "V:" -> (arg => version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_stack(base_url = base_url, version = version, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Build/export_theory.ML b/src/Pure/Build/export_theory.ML --- a/src/Pure/Build/export_theory.ML +++ b/src/Pure/Build/export_theory.ML @@ -1,479 +1,479 @@ (* Title: Pure/Build/export_theory.ML Author: Makarius Export foundational theory content and locale/class structure. *) signature EXPORT_THEORY = sig val other_name_space: (theory -> Name_Space.T) -> theory -> theory val export_enabled: Thy_Info.presentation_context -> bool val export_body: theory -> string -> XML.body -> unit end; structure Export_Theory: EXPORT_THEORY = struct (* other name spaces *) fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind); structure Data = Theory_Data ( type T = (theory -> Name_Space.T) Inttab.table; val empty = Inttab.empty; val merge = Inttab.merge (K true); ); val other_name_spaces = map #2 o Inttab.dest o Data.get; fun other_name_space get_space thy = Data.map (Inttab.update (serial (), get_space)) thy; val _ = Theory.setup (other_name_space Thm.oracle_space #> other_name_space Global_Theory.fact_space #> other_name_space (Bundle.bundle_space o Context.Theory) #> other_name_space (Attrib.attribute_space o Context.Theory) #> other_name_space (Method.method_space o Context.Theory)); (* approximative syntax *) -val get_syntax = Syntax.get_approx o Proof_Context.syn_of; +val get_syntax = Syntax.get_approx o Proof_Context.syntax_of; fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; fun get_syntax_param ctxt loc x = let val thy = Proof_Context.theory_of ctxt in if Class.is_class thy loc then (case AList.lookup (op =) (Class.these_params thy [loc]) x of NONE => NONE | SOME (_, (c, _)) => get_syntax_const ctxt c) else get_syntax_fixed ctxt x end; val encode_syntax = XML.Encode.variant [fn NONE => ([], []), fn SOME (Syntax.Prefix delim) => ([delim], []), fn SOME (Syntax.Infix {assoc, delim, pri}) => let val ass = (case assoc of Printer.No_Assoc => 0 | Printer.Left_Assoc => 1 | Printer.Right_Assoc => 2); open XML.Encode Term_XML.Encode; in ([], triple int string int (ass, delim, pri)) end]; (* free variables: not declared in the context *) val is_free = not oo Name.is_declared; fun add_frees used = fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I); fun add_tfrees used = (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); (* locales *) fun locale_content thy loc = let val ctxt = Locale.init loc thy; val args = Locale.params_of thy loc |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x)); val axioms = let val (asm, defs) = Locale.specification_of thy loc; val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs); val (intro1, intro2) = Locale.intros_of thy loc; val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) []; val res = Goal.init (Conjunction.mk_conjunction_balanced cprops) |> (ALLGOALS Goal.conjunction_tac THEN intros_tac) |> try Seq.hd; in (case res of SOME goal => Thm.prems_of goal | NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) end; val typargs = build_rev (fold Term.add_tfrees (map (Free o #1) args @ axioms)); in {typargs = typargs, args = args, axioms = axioms} end; fun get_locales thy = Locale.get_locales thy |> map_filter (fn loc => if Experiment.is_experiment thy loc then NONE else SOME (loc, ())); fun get_dependencies prev_thys thy = Locale.dest_dependencies prev_thys thy |> map_filter (fn dep => if Experiment.is_experiment thy (#source dep) orelse Experiment.is_experiment thy (#target dep) then NONE else let val (type_params, params) = Locale.parameters_of thy (#source dep); val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params; val substT = typargs |> map_filter (fn v => let val T = TFree v; val T' = Morphism.typ (#morphism dep) T; in if T = T' then NONE else SOME (v, T') end); val subst = params |> map_filter (fn (v, _) => let val t = Free v; val t' = Morphism.term (#morphism dep) t; in if t aconv t' then NONE else SOME (v, t') end); in SOME (dep, (substT, subst)) end); (* presentation *) fun export_enabled (context: Thy_Info.presentation_context) = Options.bool (#options context) "export_theory"; fun export_body thy name body = if XML.is_empty_body body then () else Export.export thy (Path.binding0 (Path.make ("theory" :: space_explode "/" name))) body; val _ = (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy => let val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); val consts = Sign.consts_of thy; val thy_ctxt = Proof_Context.init_global thy; val pos_properties = Thy_Info.adjust_pos_properties context; val enabled = export_enabled context; (* strict parents *) val parents = Theory.parents_of thy; val _ = Export.export thy \<^path_binding>\theory/parents\ (XML.Encode.string (cat_lines (map Context.theory_long_name parents) ^ "\n")); (* spec rules *) fun spec_rule_content {pos, name, rough_classification, terms, rules} = let val spec = terms @ map Thm.plain_prop_of rules |> Term_Subst.zero_var_indexes_list |> map Logic.unvarify_global; in {props = pos_properties pos, name = name, rough_classification = rough_classification, typargs = build_rev (fold Term.add_tfrees spec), args = build_rev (fold Term.add_frees spec), terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec), rules = drop (length terms) spec} end; (* entities *) fun make_entity_markup name xname pos serial = let val props = pos_properties pos @ Markup.serial_properties serial; in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end; fun entity_markup space name = let val xname = Name_Space.extern_shortest thy_ctxt space name; val {serial, pos, ...} = Name_Space.the_entry space name; in make_entity_markup name xname pos serial end; fun export_entities export_name get_space decls export = let val parent_spaces = map get_space parents; val space = get_space thy; in build (decls |> fold (fn (name, decl) => if exists (fn space => Name_Space.declared space name) parent_spaces then I else (case export name decl of NONE => I | SOME make_body => let val i = #serial (Name_Space.the_entry space name); val body = if enabled then make_body () else []; in cons (i, XML.Elem (entity_markup space name, body)) end))) |> sort (int_ord o apply2 #1) |> map #2 |> export_body thy export_name end; (* types *) val encode_type = let open XML.Encode Term_XML.Encode in triple encode_syntax (list string) (option typ) end; val _ = export_entities "types" Sign.type_space (Name_Space.dest_table (#types rep_tsig)) (fn c => (fn Type.Logical_Type n => SOME (fn () => encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) | Type.Abbreviation (args, U, false) => SOME (fn () => encode_type (get_syntax_type thy_ctxt c, args, SOME U)) | _ => NONE)); (* consts *) val encode_term = Term_XML.Encode.term consts; val encode_const = let open XML.Encode Term_XML.Encode in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end; val _ = export_entities "consts" Sign.const_space (#constants (Consts.dest consts)) (fn c => fn (T, abbrev) => SOME (fn () => let val syntax = get_syntax_const thy_ctxt c; val U = Logic.unvarifyT_global T; val U0 = Term.strip_sortsT U; val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts; val abbrev' = Option.map trim_abbrev abbrev; val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end)); (* axioms *) fun standard_prop used extra_shyps raw_prop raw_proof = let val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof); val args = rev (add_frees used prop []); val typargs = rev (add_tfrees used prop []); val used_typargs = fold (Name.declare o #1) typargs used; val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; in ((sorts @ typargs, args, prop), proof) end; fun standard_prop_of thm = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm); val encode_prop = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) encode_term end; fun encode_axiom used prop = encode_prop (#1 (standard_prop used [] prop NONE)); val _ = export_entities "axioms" Theory.axiom_space (Theory.all_axioms_of thy) (fn _ => fn prop => SOME (fn () => encode_axiom Name.context prop)); (* theorems and proof terms *) val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val prep_thm = clean_thm #> Thm.unconstrainT #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" else (case lookup_thm_id (Proofterm.thm_header_id header) of NONE => "" | SOME thm_name => Thm_Name.print thm_name); fun entity_markup_thm (serial, (name, i)) = let val space = Global_Theory.fact_space thy; val xname = Name_Space.extern_shortest thy_ctxt space name; val {pos, ...} = Name_Space.the_entry space name; in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; fun encode_thm thm_id raw_thm = let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = prep_thm raw_thm; val proof0 = if Proofterm.export_standard_enabled () then Proof_Syntax.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = standard_prop_of thm (SOME proof0); val _ = Thm.expose_proofs thy [thm]; in (prop, deps, proof) |> let open XML.Encode Term_XML.Encode; val encode_proof = Proofterm.encode_standard_proof consts; in triple encode_prop (list string) encode_proof end end; fun export_thm (thm_id, thm_name) = let val markup = entity_markup_thm (#serial thm_id, thm_name); val body = if enabled then Global_Theory.get_thm_name thy (thm_name, Position.none) |> encode_thm thm_id else []; in XML.Elem (markup, body) end; val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy)); (* type classes *) val encode_class = let open XML.Encode Term_XML.Encode in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; val _ = export_entities "classes" Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))) (fn name => fn () => SOME (fn () => (case try (Axclass.get_info thy) name of NONE => ([], []) | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |> encode_class)); (* sort algebra *) val _ = if enabled then let val prop = encode_axiom Name.context o Logic.varify_global; val encode_classrel = let open XML.Encode in list (pair prop (pair string string)) end; val encode_arities = let open XML.Encode Term_XML.Encode in list (pair prop (triple string (list sort) string)) end; val export_classrel = maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; val export_arities = map (`Logic.mk_arity) #> encode_arities; val {classrel, arities} = Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) (#2 (#classes rep_tsig)); in if null classrel then () else export_body thy "classrel" (export_classrel classrel); if null arities then () else export_body thy "arities" (export_arities arities) end else (); (* locales *) fun encode_locale used = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) (list (encode_axiom used)) end; val _ = export_entities "locales" Locale.locale_space (get_locales thy) (fn loc => fn () => SOME (fn () => let val {typargs, args, axioms} = locale_content thy loc; val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; in encode_locale used (typargs, args, axioms) end handle ERROR msg => cat_error msg ("The error(s) above occurred in locale " ^ quote (Locale.markup_name thy_ctxt loc)))); (* locale dependencies *) fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = (#source dep, (#target dep, (#prefix dep, subst))) |> let open XML.Encode Term_XML.Encode; val encode_subst = pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; val _ = if enabled then get_dependencies parents thy |> map_index (fn (i, dep) => let val xname = string_of_int (i + 1); val name = Long_Name.implode [Context.theory_base_name thy, xname]; val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); val body = encode_locale_dependency dep; in XML.Elem (markup, body) end) |> export_body thy "locale_dependencies" else (); (* constdefs *) val _ = if enabled then let val constdefs = Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |> sort_by #1; val encode = let open XML.Encode in list (pair string string) end; in if null constdefs then () else export_body thy "constdefs" (encode constdefs) end else (); (* spec rules *) val encode_specs = let open XML.Encode Term_XML.Encode in list (fn {props, name, rough_classification, typargs, args, terms, rules} => pair properties (pair string (pair Spec_Rules.encode_rough_classification (pair (list (pair string sort)) (pair (list (pair string typ)) (pair (list (pair encode_term typ)) (list encode_term)))))) (props, (name, (rough_classification, (typargs, (args, (terms, rules))))))) end; val _ = if enabled then (case Spec_Rules.dest_theory thy of [] => () | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules))) else (); (* other entities *) fun export_other get_space = let val space = get_space thy; val export_name = "other/" ^ Name_Space.kind_of space; val decls = Name_Space.get_names space |> map (rpair ()); in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end; val other_spaces = other_name_spaces thy; val other_kinds = map (fn get_space => Name_Space.kind_of (get_space thy)) other_spaces; val _ = if null other_kinds then () else Export.export thy \<^path_binding>\theory/other_kinds\ (XML.Encode.string (cat_lines other_kinds)); val _ = List.app export_other other_spaces; in () end); end; diff --git a/src/Pure/Concurrent/synchronized.ML b/src/Pure/Concurrent/synchronized.ML --- a/src/Pure/Concurrent/synchronized.ML +++ b/src/Pure/Concurrent/synchronized.ML @@ -1,122 +1,144 @@ (* Title: Pure/Concurrent/synchronized.ML Author: Fabian Immler and Makarius Synchronized variables. *) signature SYNCHRONIZED = sig type 'a var val var: string -> 'a -> 'a var val value: 'a var -> 'a val assign: 'a var -> 'a -> unit val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b val change_result: 'a var -> ('a -> 'b * 'a) -> 'b val change: 'a var -> ('a -> 'a) -> unit type 'a cache val cache: (unit -> 'a) -> 'a cache val cache_peek: 'a cache -> 'a option - val cache_eval: 'a cache -> 'a + val cache_eval: {persistent: bool} -> 'a cache -> 'a end; structure Synchronized: SYNCHRONIZED = struct (* state variable *) datatype 'a state = Immutable of 'a | Mutable of {lock: Thread.Mutex.mutex, cond: Thread.ConditionVar.conditionVar, content: 'a}; fun init_state x = Mutable {lock = Thread.Mutex.mutex (), cond = Thread.ConditionVar.conditionVar (), content = x}; fun immutable_fail name = raise Fail ("Illegal access to immutable value " ^ name); abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref} with fun var name x = Var {name = name, state = Unsynchronized.ref (init_state x)}; fun value (Var {name, state}) = (case ! state of Immutable x => x | Mutable {lock, ...} => Multithreading.synchronized name lock (fn () => (case ! state of Immutable x => x | Mutable {content, ...} => content))); fun assign (Var {name, state}) x = (case ! state of Immutable _ => immutable_fail name | Mutable {lock, cond, ...} => Multithreading.synchronized name lock (fn () => (case ! state of Immutable _ => immutable_fail name | Mutable _ => Thread_Attributes.uninterruptible_body (fn _ => (state := Immutable x; RunCall.clearMutableBit state; Thread.ConditionVar.broadcast cond))))); (* synchronized access *) fun timed_access (Var {name, state}) time_limit f = (case ! state of Immutable _ => immutable_fail name | Mutable {lock, cond, ...} => Multithreading.synchronized name lock (fn () => let fun try_change () = (case ! state of Immutable _ => immutable_fail name | Mutable {content = x, ...} => (case f x of NONE => (case Multithreading.sync_wait (time_limit x) cond lock of Exn.Res true => try_change () | Exn.Res false => NONE | Exn.Exn exn => Exn.reraise exn) | SOME (y, x') => Thread_Attributes.uninterruptible_body (fn _ => (state := Mutable {lock = lock, cond = cond, content = x'}; Thread.ConditionVar.broadcast cond; SOME y)))); in try_change () end)); fun guarded_access var f = the (timed_access var (fn _ => NONE) f); (* unconditional change *) fun change_result var f = guarded_access var (SOME o f); fun change var f = change_result var (fn x => ((), f x)); end; (* cached evaluation via weak_ref *) +local + +datatype 'a cache_state = + Undef + | Value of 'a + | Weak_Ref of 'a Unsynchronized.weak_ref; + +fun peek Undef = NONE + | peek (Value x) = SOME x + | peek (Weak_Ref r) = Unsynchronized.weak_peek r; + +fun weak_active (Weak_Ref r) = Unsynchronized.weak_active r + | weak_active _ = false; + +in + abstype 'a cache = - Cache of {expr: unit -> 'a, var: 'a Unsynchronized.weak_ref option var} + Cache of {expr: unit -> 'a, var: 'a cache_state var} with fun cache expr = - Cache {expr = expr, var = var "Synchronized.cache" NONE}; - -fun cache_peek (Cache {var, ...}) = - Option.mapPartial Unsynchronized.weak_peek (value var); + Cache {expr = expr, var = var "Synchronized.cache" Undef}; -fun cache_eval (Cache {expr, var}) = +fun cache_peek (Cache {var, ...}) = peek (value var); + +fun cache_eval {persistent} (Cache {expr, var}) = change_result var (fn state => - (case Option.mapPartial Unsynchronized.weak_peek state of - SOME result => (result, state) - | NONE => - let val result = expr () - in (result, SOME (Unsynchronized.weak_ref result)) end)); + let + val result = + (case peek state of + SOME result => result + | NONE => expr ()); + val state' = + if persistent then Value result + else if weak_active state then state + else Weak_Ref (Unsynchronized.weak_ref result); + in (result, state') end); end; end; + +end; diff --git a/src/Pure/Isar/proof_context.ML b/src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML +++ b/src/Pure/Isar/proof_context.ML @@ -1,1669 +1,1668 @@ (* Title: Pure/Isar/proof_context.ML Author: Markus Wenzel, TU Muenchen The key concept of Isar proof contexts: elevates primitive local reasoning Gamma |- phi to a structured concept, with generic context elements. See also structure Variable and Assumption. *) signature PROOF_CONTEXT = sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: {long: bool} -> theory -> string -> Proof.context type mode val mode_default: mode val mode_pattern: mode val mode_schematic: mode val mode_abbrev: mode val set_mode: mode -> Proof.context -> Proof.context val get_mode: Proof.context -> mode val restore_mode: Proof.context -> Proof.context -> Proof.context val abbrev_mode: Proof.context -> bool - val syn_of: Proof.context -> Syntax.syntax + val syntax_of: Proof.context -> Syntax.syntax val tsig_of: Proof.context -> Type.tsig val set_defsort: sort -> Proof.context -> Proof.context val default_sort: Proof.context -> indexname -> sort val arity_sorts: Proof.context -> string -> sort -> sort list val consts_of: Proof.context -> Consts.T val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context val naming_of: Proof.context -> Name_Space.naming val restore_naming: Proof.context -> Proof.context -> Proof.context val full_name: Proof.context -> binding -> string val get_scope: Proof.context -> Binding.scope option val new_scope: Proof.context -> Binding.scope * Proof.context val private_scope: Binding.scope -> Proof.context -> Proof.context val private: Position.T -> Proof.context -> Proof.context val qualified_scope: Binding.scope -> Proof.context -> Proof.context val qualified: Position.T -> Proof.context -> Proof.context val concealed: Proof.context -> Proof.context val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string val extern_class: Proof.context -> string -> xstring val markup_class: Proof.context -> string -> string val pretty_class: Proof.context -> string -> Pretty.T val extern_type: Proof.context -> string -> xstring val markup_type: Proof.context -> string -> string val pretty_type: Proof.context -> string -> Pretty.T val extern_const: Proof.context -> string -> xstring val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T val transfer: theory -> Proof.context -> Proof.context val transfer_facts: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val facts_of: Proof.context -> Facts.T val facts_of_fact: Proof.context -> string -> Facts.T val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring val augment: term -> Proof.context -> Proof.context val print_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val check_class: Proof.context -> xstring * Position.T -> class * Position.report list val read_class: Proof.context -> string -> class val read_typ: Proof.context -> string -> typ val read_typ_syntax: Proof.context -> string -> typ val read_typ_abbrev: Proof.context -> string -> typ val cert_typ: Proof.context -> typ -> typ val cert_typ_syntax: Proof.context -> typ -> typ val cert_typ_abbrev: Proof.context -> typ -> typ val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> (string * typ) * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context val check_type_name: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T -> typ * Position.report list val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ val consts_completion_message: Proof.context -> xstring * Position.T list -> string val check_const: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T list -> term * Position.report list val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term val read_arity: Proof.context -> xstring * string list * string -> arity val cert_arity: Proof.context -> arity -> arity val allow_dummies: Proof.context -> Proof.context val prepare_sortsT: Proof.context -> typ list -> string list * typ list val prepare_sorts: Proof.context -> term list -> string list * term list val check_tfree: Proof.context -> string * sort -> string * sort val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term val show_abbrevs: bool Config.T val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term val def_type: Proof.context -> indexname -> typ option val standard_typ_check: Proof.context -> typ list -> typ list val standard_term_check_finish: Proof.context -> term list -> term list val standard_term_uncheck: Proof.context -> term list -> term list val export_: {goal: bool} -> Proof.context -> Proof.context -> thm list -> thm list val export: Proof.context -> Proof.context -> thm list -> thm list val export_goal: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context val simult_matches: Proof.context -> term * term list -> (indexname * term) list val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val bind_term: indexname * term -> Proof.context -> Proof.context val cert_propp: Proof.context -> (term * term list) list list -> (term list list * (indexname * term) list) val read_propp: Proof.context -> (string * string list) list list -> (term list list * (indexname * term) list) val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option val dynamic_facts_dummy: bool Config.T val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list val get_fact: Proof.context -> Facts.ref -> thm list val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list val get_thm: Proof.context -> xstring -> thm val is_stmt: Proof.context -> bool val set_stmt: bool -> Proof.context -> Proof.context val restore_stmt: Proof.context -> Proof.context -> Proof.context val add_thms_dynamic: binding * (Context.generic -> thm list) -> Proof.context -> string * Proof.context val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context val note_thms: string -> Thm.binding * (thm list * attribute list) list -> Proof.context -> (string * thm list) * Proof.context val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context val alias_fact: binding -> string -> Proof.context -> Proof.context val read_var: binding * string option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val cert_var: binding * typ option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context -> string list * Proof.context val add_assms: Assumption.export -> (Thm.binding * (term * term list) list) list -> Proof.context -> (string * thm list) list * Proof.context val add_assms_cmd: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context val check_case: Proof.context -> bool -> string * Position.T -> binding option list -> Rule_Cases.T val check_syntax_const: Proof.context -> string * Position.T -> string val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Proof.context -> Proof.context val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Context.generic -> Context.generic val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> Context.generic -> Context.generic val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> Context.generic -> Context.generic val type_alias: binding -> string -> Proof.context -> Proof.context val const_alias: binding -> string -> Proof.context -> Proof.context val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val generic_add_abbrev: string -> binding * term -> Context.generic -> (term * term) * Context.generic val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list} val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context -> stmt * Proof.context val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context -> stmt * Proof.context type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term} val cert_statement: (binding * typ option * mixfix) list -> (term * term list) list list -> (term * term list) list list -> Proof.context -> statement * Proof.context val read_statement: (binding * string option * mixfix) list -> (string * string list) list list -> (string * string list) list list -> Proof.context -> statement * Proof.context val print_syntax: Proof.context -> unit val print_abbrevs: bool -> Proof.context -> unit val pretty_term_bindings: Proof.context -> Pretty.T list val pretty_local_facts: bool -> Proof.context -> Pretty.T list val print_local_facts: bool -> Proof.context -> unit val pretty_cases: Proof.context -> Pretty.T list val print_cases_proof: Proof.context -> Proof.context -> string val debug: bool Config.T val verbose: bool Config.T val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list end; structure Proof_Context: PROOF_CONTEXT = struct val theory_of = Proof_Context.theory_of; val init_global = Proof_Context.init_global; val get_global = Proof_Context.get_global; (** inner syntax mode **) datatype mode = Mode of {pattern: bool, (*pattern binding schematic variables*) schematic: bool, (*term referencing loose schematic variables*) abbrev: bool}; (*abbrev mode -- no normalization*) fun make_mode (pattern, schematic, abbrev) = Mode {pattern = pattern, schematic = schematic, abbrev = abbrev}; val mode_default = make_mode (false, false, false); val mode_pattern = make_mode (true, false, false); val mode_schematic = make_mode (false, true, false); val mode_abbrev = make_mode (false, false, true); (** Isar proof context information **) type cases = Rule_Cases.T Name_Space.table; val empty_cases: cases = Name_Space.empty_table Markup.caseN; datatype data = Data of {mode: mode, (*inner syntax mode*) syntax: Local_Syntax.T, (*local syntax*) tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) facts: Facts.T, (*local facts, based on initial global facts*) cases: cases}; (*named case contexts*) fun make_data (mode, syntax, tsig, consts, facts, cases) = Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; structure Data = Proof_Data ( type T = data; fun init thy = make_data (mode_default, Local_Syntax.init thy, (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), Global_Theory.facts_of thy, empty_cases); ); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); fun map_data_result f ctxt = let val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt; val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data; in (res, Data.put data' ctxt) end; fun map_data f = snd o map_data_result (pair () o f); fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, cases)); fun map_syntax f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, f syntax, tsig, consts, facts, cases)); fun map_syntax_idents f ctxt = let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in ctxt |> map_syntax (K syntax') |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents') end; fun map_tsig f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, f tsig, consts, facts, cases)); fun map_consts f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, f consts, facts, cases)); fun map_facts_result f = map_data_result (fn (mode, syntax, tsig, consts, facts, cases) => let val (res, facts') = f facts in (res, (mode, syntax, tsig, consts, facts', cases)) end); fun map_facts f = snd o map_facts_result (pair () o f); fun map_cases f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, f cases)); val get_mode = #mode o rep_data; val restore_mode = set_mode o get_mode; val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); -val syntax_of = #syntax o rep_data; -val syn_of = Local_Syntax.syn_of o syntax_of; +val syntax_of = Local_Syntax.syntax_of o #syntax o rep_data; val set_syntax_mode = map_syntax o Local_Syntax.set_mode; -val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; +val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o #syntax o rep_data; val tsig_of = #1 o #tsig o rep_data; val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt); val consts_of = #1 o #consts o rep_data; val cases_of = #cases o rep_data; (* naming *) val naming_of = Name_Space.naming_of o Context.Proof; val map_naming = Context.proof_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; val full_name = Name_Space.full_name o naming_of; val get_scope = Name_Space.get_scope o naming_of; fun new_scope ctxt = let val (scope, naming') = Name_Space.new_scope (naming_of ctxt); val ctxt' = map_naming (K naming') ctxt; in (scope, ctxt') end; val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* name spaces *) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt)); val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup; fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup; fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup; fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str; fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str; fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str; (* theory transfer *) fun transfer_syntax thy ctxt = ctxt |> map_syntax (Local_Syntax.rebuild thy) |> map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in if Type.eq_tsig (thy_tsig, global_tsig) then tsig else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in if Consts.eq_consts (thy_consts, global_consts) then consts else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) end); fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; fun transfer_facts thy = map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts)); fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; fun background_theory_result f ctxt = let val (res, thy') = f (theory_of ctxt) in (res, ctxt |> transfer thy') end; (* hybrid facts *) val facts_of = #facts o rep_data; fun facts_of_fact ctxt name = let val local_facts = facts_of ctxt; val global_facts = Global_Theory.facts_of (theory_of ctxt); in if Facts.defined local_facts name then local_facts else global_facts end; fun markup_extern_fact ctxt name = let val facts = facts_of_fact ctxt name; val (markup, xname) = Facts.markup_extern ctxt facts name; val markups = if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] else [markup]; in (markups, xname) end; (* augment context by implicit term declarations *) fun augment t ctxt = ctxt |> Variable.add_fixes_implicit t |> Variable.declare_term t |> Soft_Type_System.augment t; (** pretty printing **) val print_name = Token.print_name o Thy_Header.get_keywords'; val pretty_name = Pretty.str oo print_name; fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_fact_name ctxt a = Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"]; fun pretty_fact ctxt = let val pretty_thm = Thm.pretty_thm ctxt; val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th] | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths)) end; (** prepare types **) (* classes *) fun check_class ctxt (xname, pos) = let val tsig = tsig_of ctxt; val class_space = Type.class_space tsig; val name = Type.cert_class tsig (Name_Space.intern class_space xname) handle TYPE (msg, _, _) => error (msg ^ Position.here pos ^ Completion.markup_report [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]); val reports = if Context_Position.is_reported ctxt pos then [(pos, Name_Space.markup class_space name)] else []; in (name, reports) end; fun read_class ctxt text = let val source = Syntax.read_input text; val (c, reports) = check_class ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in c end; (* types *) fun read_typ_mode mode ctxt s = Syntax.read_typ (Type.set_mode mode ctxt) s; val read_typ = read_typ_mode Type.mode_default; val read_typ_syntax = read_typ_mode Type.mode_syntax; val read_typ_abbrev = read_typ_mode Type.mode_abbrev; fun cert_typ_mode mode ctxt T = Type.certify_typ mode (tsig_of ctxt) T handle TYPE (msg, _, _) => error msg; val cert_typ = cert_typ_mode Type.mode_default; val cert_typ_syntax = cert_typ_mode Type.mode_syntax; val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev; (** prepare terms and propositions **) (* inferred types of parameters *) fun infer_type ctxt x = Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); fun inferred_param x ctxt = let val p = (x, infer_type ctxt (x, dummyT)) in (p, ctxt |> Variable.declare_term (Free p)) end; fun inferred_fixes ctxt = fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt; (* type names *) fun check_type_name {proper, strict} ctxt (c, pos) = if Lexicon.is_tid c then if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos) else let val reports = if Context_Position.is_reported ctxt pos then [(pos, Markup.tfree)] else []; in (TFree (c, default_sort ctxt (c, ~1)), reports) end else let val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos); val _ = if strict andalso not (Type.decl_logical decl) then error ("Bad type name: " ^ quote d ^ Position.here pos) else (); in (Type (d, replicate (Type.decl_args decl) dummyT), reports) end; fun read_type_name flags ctxt text = let val source = Syntax.read_input text; val (T, reports) = check_type_name flags ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in T end; (* constant names *) fun consts_completion_message ctxt (c, ps) = ps |> map (fn pos => Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)) |> Completion.markup_report; fun check_const {proper, strict} ctxt (c, ps) = let val _ = Name.reject_internal (c, ps) handle ERROR msg => error (msg ^ consts_completion_message ctxt (c, ps)); fun err msg = error (msg ^ Position.here_list ps); val consts = consts_of ctxt; val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; val (t, reports) = (case (fixed, Variable.lookup_const ctxt c) of (SOME x, NONE) => let val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); in (Free (x, infer_type ctxt (x, dummyT)), reports) end | (_, SOME d) => let val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); in (Const (d, T), reports) end | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); val _ = (case (strict, t) of (true, Const (d, _)) => (ignore (Consts.the_const_type consts d) handle TYPE (msg, _, _) => err msg) | _ => ()); in (t, reports) end; fun read_const flags ctxt text = let val source = Syntax.read_input text; val (c, pos) = Input.source_content source; val (t, reports) = check_const flags ctxt (c, [pos]); val _ = Context_Position.reports ctxt reports; in t end; (* type arities *) local fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end; in val read_arity = prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); end; (* read_term *) fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); val read_term_pattern = read_term_mode mode_pattern; val read_term_schematic = read_term_mode mode_schematic; val read_term_abbrev = read_term_mode mode_abbrev; (* local abbreviations *) local fun certify_consts ctxt = Consts.certify {normalize = not (abbrev_mode ctxt)} (Context.Proof ctxt) (tsig_of ctxt) (consts_of ctxt); fun expand_binds ctxt = let val Mode {pattern, schematic, ...} = get_mode ctxt; fun reject_schematic (t as Var _) = error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t) | reject_schematic (Abs (_, _, t)) = reject_schematic t | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u) | reject_schematic _ = (); in if pattern then I else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) end; in fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; end; val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true); fun contract_abbrevs ctxt t = let val thy = theory_of ctxt; val consts = consts_of ctxt; val Mode {abbrev, ...} = get_mode ctxt; val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t else Pattern.rewrite_term_top thy [] [match_abbrev] t end; (* patterns *) fun prepare_patternT ctxt T = let val Mode {pattern, schematic, ...} = get_mode ctxt; val _ = pattern orelse schematic orelse T |> Term.exists_subtype (fn T as TVar (xi, _) => not (Type_Infer.is_param xi) andalso error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T) | _ => false) in T end; local val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false); fun check_dummies ctxt t = if Config.get ctxt dummies then t else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term"; fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); in val allow_dummies = Config.put dummies true; fun prepare_patterns ctxt = let val Mode {pattern, ...} = get_mode ctxt in Type_Infer.fixate ctxt pattern #> pattern ? Variable.polymorphic ctxt #> (Same.commit o Same.map o Term.map_types_same) (Same.function_eq (op =) (prepare_patternT ctxt)) #> (if pattern then prepare_dummies else map (check_dummies ctxt)) end; end; (* sort constraints *) local fun prepare_sorts_env ctxt tys = let val tsig = tsig_of ctxt; val defaultS = Type.defaultS tsig; val dummy_var = ("'_dummy_", ~1); fun constraint (xi, raw_S) env = let val (ps, S) = Term_Position.decode_positionS raw_S in if xi = dummy_var orelse S = dummyS then env else Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env handle Vartab.DUP _ => error ("Inconsistent sort constraints for type variable " ^ quote (Term.string_of_vname' xi) ^ Position.here_list ps) end; val env = Vartab.build (tys |> (fold o fold_atyps) (fn TFree (x, S) => constraint ((x, ~1), S) | TVar v => constraint v | _ => I)); fun get_sort xi raw_S = if xi = dummy_var then Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S)) else (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of (NONE, NONE) => defaultS | (NONE, SOME S) => S | (SOME S, NONE) => S | (SOME S, SOME S') => if Type.eq_sort tsig (S, S') then S' else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ " for type variable " ^ quote (Term.string_of_vname' xi))); fun add_report S pos reports = if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports else reports; fun get_sort_reports xi raw_S = let val ps = #1 (Term_Position.decode_positionS raw_S); val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); in fold (add_report S) ps end; val reports = (fold o fold_atyps) (fn T => if Term_Position.is_positionT T then I else (case T of TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S | TVar (xi, raw_S) => get_sort_reports xi raw_S | _ => I)) tys []; in (map #2 reports, get_sort) end; fun replace_sortsT_same get_sort = Term.map_atyps_same (fn T => if Term_Position.is_positionT T then raise Same.SAME else (case T of TFree (x, raw_S) => TFree (x, Same.function_eq (op =) (get_sort (x, ~1)) raw_S) | TVar (xi, raw_S) => TVar (xi, Same.function_eq (op =) (get_sort xi) raw_S) | _ => raise Same.SAME)); in fun prepare_sortsT ctxt tys = let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys in (sorting_report, (Same.commit o Same.map) (replace_sortsT_same get_sort) tys) end; fun prepare_sorts ctxt tms = let val tys = rev ((fold o fold_types) cons tms []); val (sorting_report, get_sort) = prepare_sorts_env ctxt tys; val tms' = (Same.commit o Same.map o Term.map_types_same) (replace_sortsT_same get_sort) tms; in (sorting_report, tms') end; fun check_tfree ctxt v = let val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else (); in a end; end; (* certify terms *) local fun cert_flags flags ctxt t = let val t' = expand_abbrevs ctxt t in #1 (Sign.certify_flags flags (Context.Proof ctxt) (consts_of ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg end; in val cert_term = cert_flags {prop = false, normalize = false}; val cert_prop = cert_flags {prop = true, normalize = false}; end; (* check/uncheck *) fun def_type ctxt = let val Mode {pattern, ...} = get_mode ctxt in Variable.def_type ctxt pattern end; fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt); val standard_term_check_finish = prepare_patterns; fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); (** export results **) fun export_ goal inner outer = map (Assumption.export_ goal inner outer) #> Variable.export inner outer; val export = export_{goal = false}; val export_goal = export_{goal = true}; fun export_morphism inner outer = Assumption.export_morphism inner outer $> Variable.export_morphism inner outer; (** term bindings **) (* auto bindings *) fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt; val auto_bind_goal = auto_bind Auto_Bind.goal; val auto_bind_facts = auto_bind Auto_Bind.facts; (* match bindings *) fun simult_matches ctxt (t, pats) = (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of NONE => error "Pattern match failed!" | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); fun maybe_bind_term (xi, t) ctxt = ctxt |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t); val bind_term = maybe_bind_term o apsnd SOME; (* propositions with patterns *) local fun prep_propp prep_props ctxt raw_args = let val props = prep_props ctxt (maps (map fst) raw_args); val props_ctxt = fold Variable.declare_term props ctxt; val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args; val propps = unflat raw_args (props ~~ patss); val binds = (maps o maps) (simult_matches props_ctxt) propps; in (map (map fst) propps, binds) end; in val cert_propp = prep_propp (map o cert_prop); val read_propp = prep_propp Syntax.read_props; end; (** theorems **) (* fact_tac *) local fun comp_hhf_tac ctxt th i st = PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st; fun comp_incr_tac _ [] _ = no_tac | comp_incr_tac ctxt (th :: ths) i = (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ctxt ths i; val vacuous_facts = [Drule.termI]; in fun potential_facts ctxt prop = let val body = Term.strip_all_body prop; val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts |> map (rpair Position.none); in Facts.could_unify (facts_of ctxt) body @ vacuous end; fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i); end; (* lookup facts *) fun lookup_fact ctxt name = let val context = Context.Proof ctxt; val thy = Proof_Context.theory_of ctxt; in (case Facts.lookup context (facts_of ctxt) name of NONE => Facts.lookup context (Global_Theory.facts_of thy) name | some => some) end; (* retrieve facts *) val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false); local fun retrieve_global context = Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context)); fun retrieve_generic (context as Context.Proof ctxt) arg = (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg => (retrieve_global context arg handle ERROR _ => error local_msg)) | retrieve_generic context arg = retrieve_global context arg; fun retrieve pick context (Facts.Fact s) = let val ctxt = Context.the_proof context; val pos = Syntax.read_input_pos s; val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s |> singleton (Variable.polymorphic ctxt); fun err ps msg = error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop); val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); val results = map_filter (try (apfst prove)) (potential_facts ctxt prop'); val (thm, thm_pos) = (case distinct (eq_fst Thm.eq_thm_prop) results of [res] => res | [] => err [] "Failed to retrieve literal fact" | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact"); val markup = Position.entity_markup Markup.literal_factN ("", thm_pos); val _ = Context_Position.report_generic context pos markup; in pick true ("", thm_pos) [thm] end | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms}; val {name, dynamic, thms} = (case xname of "" => immediate [Drule.dummy_thm] | "_" => immediate [Drule.asm_rl] | "nothing" => immediate [] | _ => retrieve_generic context (xname, pos)); val thms' = if dynamic andalso Config.get_generic context dynamic_facts_dummy then [Drule.free_dummy_thm] else Facts.select (Facts.Named ((name, pos), sel)) thms; in pick (dynamic andalso is_none sel) (name, pos) thms' end; in val get_fact_generic = retrieve (fn dynamic => fn (name, _) => fn thms => (if dynamic then SOME name else NONE, thms)); val get_fact = retrieve (K (K I)) o Context.Proof; val get_fact_single = retrieve (K Facts.the_single) o Context.Proof; fun get_thms ctxt = get_fact ctxt o Facts.named; fun get_thm ctxt = get_fact_single ctxt o Facts.named; end; (* inner statement mode *) val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false); fun is_stmt ctxt = Config.get ctxt inner_stmt; val set_stmt = Config.put inner_stmt; val restore_stmt = set_stmt o is_stmt; (* facts *) fun add_thms_dynamic arg ctxt = ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg); local fun add_facts {index} arg ctxt = ctxt |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg); fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2 | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)); fun full_name_pos ctxt b = (full_name ctxt b, Binding.default_pos_of b); in fun add_thms_lazy kind (b, ths) ctxt = let val name_pos = full_name_pos ctxt b; val ths' = Global_Theory.check_thms_lazy ths |> Lazy.map_finished (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind)); val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt; in ctxt' end; fun note_thms kind ((b, more_atts), facts) ctxt = let val name_pos = full_name_pos ctxt b; fun app_fact (thms, atts) = fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) thms; val (thms', ctxt') = fold_maps app_fact (Global_Theory.name_facts Global_Theory.unofficial1 name_pos facts) ctxt; val thms'' = Global_Theory.name_thms Global_Theory.unofficial2 name_pos thms'; val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms''); in ((#1 name_pos, thms''), ctxt'') end; val note_thmss = fold_map o note_thms; fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming) |> Context_Position.set_visible false |> update_facts {index = index} (apfst Binding.name thms) |> Context_Position.restore_visible ctxt |> restore_naming ctxt; end; fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt; (** basic logical entities **) (* variables *) fun declare_var (x, opt_T, mx) ctxt = let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx) in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end; fun add_syntax vars ctxt = map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt; fun check_var internal b = let val x = Variable.check_name b; val check = if internal then Name.reject_skolem else Name.reject_internal; val _ = if can check (x, []) andalso Symbol_Pos.is_identifier x then () else error ("Bad name: " ^ Binding.print b); in x end; local fun check_mixfix ctxt (b, T, mx) = let val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt; val mx' = Mixfix.reset_pos mx; val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt'; in mx' end; fun prep_var prep_typ internal (b, raw_T, mx) ctxt = let val x = check_var internal b; fun cond_tvars T = if internal then T else Type.no_tvars T handle TYPE (msg, _, _) => error msg; val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx); val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx); in ((b, SOME T, mx'), ctxt') end; in val read_var = prep_var Syntax.read_typ false; val cert_var = prep_var cert_typ true; end; (* syntax *) fun check_syntax_const ctxt (c, pos) = - if is_some (Syntax.lookup_const (syn_of ctxt) c) then c + if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c else error ("Unknown syntax const: " ^ quote c ^ Position.here pos); fun syntax add mode args ctxt = let val args' = map (pair Local_Syntax.Const) args in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end; fun generic_syntax add mode args = Context.mapping (Sign.syntax add mode args) (syntax add mode args); (* notation *) local fun type_syntax (Type (c, args), mx) = SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx)) | type_syntax _ = NONE; fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of ctxt)) c of SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) | NONE => NONE) | const_syntax _ _ = NONE; fun gen_notation make_syntax add mode args ctxt = ctxt |> map_syntax_idents (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args)); in val type_notation = gen_notation (K type_syntax); val notation = gen_notation const_syntax; fun generic_type_notation add mode args phi = let val args' = args |> map_filter (fn (T, mx) => let val T' = Morphism.typ phi T; val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false); in if similar then SOME (T', mx) else NONE end); in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; fun generic_notation add mode args phi = let val args' = args |> map_filter (fn (t, mx) => let val t' = Morphism.term phi t in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end); in Context.mapping (Sign.notation add mode args') (notation add mode args') end; end; (* aliases *) fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; (* local constants *) fun add_const_constraint (c, opt_T) ctxt = let fun prepT raw_T = let val T = cert_typ ctxt raw_T in cert_term ctxt (Const (c, T)); T end; in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; fun add_abbrev mode (b, raw_t) ctxt = let val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; val ((lhs, rhs), consts') = consts_of ctxt |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); in ctxt |> (map_consts o apfst) (K consts') |> Variable.declare_term rhs |> pair (lhs, rhs) end; fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); fun generic_add_abbrev mode arg = Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); fun generic_revert_abbrev mode arg = Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); (* fixes *) local fun gen_fixes prep_var raw_vars ctxt = let val (vars, _) = fold_map prep_var raw_vars ctxt; val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt; val _ = Context_Position.reports ctxt' (flat (map2 (fn x => fn pos => [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)]) xs (map (Binding.pos_of o #1) vars))); val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars; val (Ts, ctxt'') = fold_map declare_var vars' ctxt'; val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars'; in (xs, add_syntax vars'' ctxt'') end; in val add_fixes = gen_fixes cert_var; val add_fixes_cmd = gen_fixes read_var; end; (** assumptions **) local fun gen_assms prep_propp exp args ctxt = let val (propss, binds) = prep_propp ctxt (map snd args); val props = flat propss; in ctxt |> fold Variable.declare_term props |> tap (Variable.warn_extra_tfrees ctxt) |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss |-> (fn premss => auto_bind_facts props #> fold Variable.bind_term binds #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)) end; in val add_assms = gen_assms cert_propp; val add_assms_cmd = gen_assms read_propp; end; (** cases **) fun dest_cases prev_ctxt ctxt = let val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table); val ignored = (case prev_ctxt of NONE => Intset.empty | SOME ctxt0 => let val cases0 = cases_of ctxt0 in Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) => Intset.insert (serial_of cases0 a))) end); val cases = cases_of ctxt; in Name_Space.fold_table (fn (a, c) => let val i = serial_of cases a in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases [] |> sort (int_ord o apply2 #1) |> map #2 end; local fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b | drop_schematic b = b; fun update_case _ ("", _) cases = cases | update_case _ (name, NONE) cases = Name_Space.del_table name cases | update_case context (name, SOME c) cases = #2 (Name_Space.define context false (Binding.name name, c) cases); fun fix (b, T) ctxt = let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt in (Free (x, T), ctxt') end; in fun update_cases args ctxt = let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming); in map_cases (fold (update_case context) args) ctxt end; fun case_result c ctxt = let val Rule_Cases.Case {fixes, ...} = c; val (ts, ctxt') = ctxt |> fold_map fix fixes; val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; in ctxt' |> fold (maybe_bind_term o drop_schematic) binds |> update_cases (map (apsnd SOME) cases) |> pair (assumes, (binds, cases)) end; val apply_case = apfst fst oo case_result; fun check_case ctxt internal (name, pos) param_specs = let val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) = Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos); val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs; fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys | replace [] ys = ys | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name ^ Position.here pos); val fixes' = replace param_specs fixes; val binds' = map drop_schematic binds; in if null (fold (Term.add_tvarsT o snd) fixes []) andalso null (fold (fold Term.add_vars o snd) assumes []) then Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos) end; end; (* structured statements *) type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list}; type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term}; local fun export_binds ctxt' ctxt params binds = let val rhss = map (the_list o Option.map (Logic.close_term params) o snd) binds |> burrow (Variable.export_terms ctxt' ctxt) |> map (try the_single); in map fst binds ~~ rhss end; fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt = let val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt; val xs = map (Variable.check_name o #1) vars; val (xs', fixes_ctxt) = add_fixes vars vars_ctxt; val (propss, binds) = prep_propp fixes_ctxt raw_propps; val (ps, params_ctxt) = fixes_ctxt |> (fold o fold) Variable.declare_term propss |> fold_map inferred_param xs'; val params = xs ~~ map Free ps; val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps; val binds' = binds |> map (apsnd SOME) |> export_binds params_ctxt ctxt params |> map (apsnd the); val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt; val result : stmt = {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'}; in (result, params_ctxt) end; fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt = let val ((fixes, (assumes, shows), binds), ctxt') = ctxt |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows) |-> (fn {vars, propss, binds, ...} => fold Variable.bind_term binds #> pair (map #2 vars, chop (length raw_assumes) propss, binds)); val binds' = (Auto_Bind.facts ctxt' (flat shows) @ (case try List.last (flat shows) of NONE => [] | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds)) |> export_binds ctxt' ctxt fixes; val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows)); val text' = singleton (Variable.export_terms ctxt' ctxt) text; val result : statement = {fixes = fixes, assumes = assumes, shows = shows, result_binds = binds', text = text, result_text = text'}; in (result, ctxt') end; in val cert_stmt = prep_stmt cert_var cert_propp; val read_stmt = prep_stmt read_var read_propp; val cert_statement = prep_statement cert_var cert_propp; val read_statement = prep_statement read_var read_propp; end; (** print context information **) (* local syntax *) -val print_syntax = Syntax.print_syntax o syn_of; +val print_syntax = Syntax.print_syntax o syntax_of; (* abbreviations *) fun pretty_abbrevs verbose show_globals ctxt = let val space = const_space ctxt; val (constants, global_constants) = apply2 (#constants o Consts.dest) (#consts (rep_data ctxt)); val globals = Symtab.make global_constants; fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []); in if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] end; fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true; (* term bindings *) fun pretty_term_bindings ctxt = let val binds = Variable.binds_of ctxt; fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t)); in if Vartab.is_empty binds then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] end; (* local facts *) fun pretty_local_facts verbose ctxt = let val facts = facts_of ctxt; val props = map #1 (Facts.props facts); val local_facts = (if null props then [] else [("", props)]) @ Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts; in if null local_facts then [] else [Pretty.big_list "local facts:" (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))] end; fun print_local_facts verbose ctxt = Pretty.writeln_chunks (pretty_local_facts verbose ctxt); (* named local contexts *) local fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) = let val prt_name = pretty_name ctxt; val prt_term = Syntax.pretty_term ctxt; fun prt_let (xi, t) = Pretty.block [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, Pretty.quote (prt_term t)]; fun prt_asm (a, ts) = Pretty.block (Pretty.breaks ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); fun prt_sect _ _ _ [] = [] | prt_sect head sep prt xs = [Pretty.block (Pretty.breaks (head :: flat (separate sep (map (single o prt) xs))))]; in Pretty.block (prt_name name :: Pretty.str ":" :: Pretty.fbrk :: Pretty.fbreaks (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @ prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @ prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs)) end; in fun pretty_cases ctxt = let val cases = dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) => (name, (fixes, case_result c ctxt))); in if null cases then [] else [Pretty.big_list "cases:" (map pretty_case cases)] end; end; fun print_cases_proof ctxt0 ctxt = let fun trim_name x = if Name.is_internal x then Name.clean x else "_"; val trim_names = map trim_name #> drop_suffix (equal "_"); fun print_case name xs = (case trim_names xs of [] => print_name ctxt name | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs')))); fun is_case x t = x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t); fun indentation depth = prefix (Symbol.spaces (2 * depth)); fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) = let val indent = indentation depth; val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes)); val tail = if null cases then let val concl = if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds then Rule_Cases.case_conclN else Auto_Bind.thesisN in indent ("then show ?" ^ concl ^ " sorry") end else print_proofs depth cases; in head ^ "\n" ^ tail end and print_proofs 0 [] = "" | print_proofs depth cases = let val indent = indentation depth; val body = map (print_proof (depth + 1)) cases |> separate (indent "next") in if depth = 0 then body @ [indent "qed"] else if length cases = 1 then body else indent "{" :: body @ [indent "}"] end |> cat_lines; in (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of "" => "" | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s) end; (* core context *) val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false); val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false); fun pretty_ctxt ctxt = if not (Config.get ctxt debug) then [] else let val prt_term = Syntax.pretty_term ctxt; (*structures*) val {structs, ...} = Syntax_Trans.get_idents ctxt; val prt_structs = if null structs then [] else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: Pretty.commas (map Pretty.str structs))]; (*fixes*) fun prt_fix (x, x') = if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; val fixes = filter_out ((Name.is_internal orf member (op =) structs) o #1) (Variable.dest_fixes ctxt); val prt_fixes = if null fixes then [] else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: Pretty.commas (map prt_fix fixes))]; (*assumptions*) val prt_assms = (case Assumption.all_prems_of ctxt of [] => [] | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]); in prt_structs @ prt_fixes @ prt_assms end; (* main context *) fun pretty_context ctxt = let val verbose = Config.get ctxt verbose; fun verb f x = if verbose then f (x ()) else []; val prt_term = Syntax.pretty_term ctxt; val prt_typ = Syntax.pretty_typ ctxt; val prt_sort = Syntax.pretty_sort ctxt; (*theory*) val pretty_thy = Pretty.block [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)]; (*defaults*) fun prt_atom prt prtT (x, X) = Pretty.block [prt x, Pretty.str " ::", Pretty.brk 1, prtT X]; fun prt_var (x, ~1) = prt_term (Syntax.free x) | prt_var xi = prt_term (Syntax.var xi); fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) | prt_varT xi = prt_typ (TVar (xi, [])); val prt_defT = prt_atom prt_var prt_typ; val prt_defS = prt_atom prt_varT prt_sort; val (types, sorts) = Variable.constraints_of ctxt; in verb single (K pretty_thy) @ pretty_ctxt ctxt @ verb (pretty_abbrevs true false) (K ctxt) @ verb pretty_term_bindings (K ctxt) @ verb (pretty_local_facts true) (K ctxt) @ verb pretty_cases (K ctxt) @ verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) end; end; val show_abbrevs = Proof_Context.show_abbrevs; diff --git a/src/Pure/Syntax/local_syntax.ML b/src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML +++ b/src/Pure/Syntax/local_syntax.ML @@ -1,125 +1,125 @@ (* Title: Pure/Syntax/local_syntax.ML Author: Makarius Local syntax depending on theory syntax, with special support for implicit structure references. *) signature LOCAL_SYNTAX = sig type T - val syn_of: T -> Syntax.syntax + val syntax_of: T -> Syntax.syntax val init: theory -> T val rebuild: theory -> T -> T datatype kind = Type | Const | Fixed val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list -> T -> {structs: string list, fixes: string list} option * T val set_mode: Syntax.mode -> T -> T val restore_mode: T -> T -> T val update_modesyntax: Proof.context -> bool -> Syntax.mode -> (kind * (string * typ * mixfix)) list -> T -> {structs: string list, fixes: string list} option * T end; structure Local_Syntax: LOCAL_SYNTAX = struct (* datatype T *) type local_mixfix = (string * bool) * (*name, fixed?*) ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*) datatype T = Syntax of {thy_syntax: Syntax.syntax, local_syntax: Syntax.syntax, mode: Syntax.mode, mixfixes: local_mixfix list}; fun make_syntax (thy_syntax, local_syntax, mode, mixfixes) = Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, mixfixes = mixfixes}; fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) = make_syntax (f (thy_syntax, local_syntax, mode, mixfixes)); fun is_consistent thy (Syntax {thy_syntax, ...}) = - Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); + Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax); -fun syn_of (Syntax {local_syntax, ...}) = local_syntax; +fun syntax_of (Syntax {local_syntax, ...}) = local_syntax; (* build syntax *) fun build_syntax thy mode mixfixes = let - val thy_syntax = Sign.syn_of thy; + val thy_syntax = Sign.syntax_of thy; fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls | update_gram ((false, add, m), decls) = Syntax.update_const_gram add (Sign.logical_types thy) m decls; val local_syntax = thy_syntax |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end; fun init thy = - let val thy_syntax = Sign.syn_of thy + let val thy_syntax = Sign.syntax_of thy in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end; fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) = if is_consistent thy syntax then syntax else build_syntax thy mode mixfixes; (* mixfix declarations *) datatype kind = Type | Const | Fixed; local fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) | prep_mixfix add mode (Fixed, (x, T, mx)) = SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); fun prep_struct (Fixed, (c, _, Structure _)) = SOME c | prep_struct (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c) | prep_struct _ = NONE; in fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) = (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of [] => (NONE, syntax) | decls => let val new_mixfixes = map_filter (prep_mixfix add mode) decls; val new_structs = map_filter prep_struct decls; val mixfixes' = rev new_mixfixes @ mixfixes; val idents = Syntax_Trans.get_idents ctxt; val idents' = {structs = if add then #structs idents @ new_structs else subtract (op =) new_structs (#structs idents), fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []}; val syntax' = build_syntax (Proof_Context.theory_of ctxt) mode mixfixes'; in (if idents = idents' then NONE else SOME idents', syntax') end); fun add_syntax ctxt = update_syntax ctxt true; end; (* syntax mode *) fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes) => (thy_syntax, local_syntax, mode, mixfixes)); fun restore_mode (Syntax {mode, ...}) = set_mode mode; fun update_modesyntax ctxt add mode args syntax = syntax |> set_mode mode |> update_syntax ctxt add args ||> restore_mode syntax; end; diff --git a/src/Pure/Syntax/syntax.ML b/src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML +++ b/src/Pure/Syntax/syntax.ML @@ -1,692 +1,701 @@ (* Title: Pure/Syntax/syntax.ML Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Standard Isabelle syntax, based on arbitrary context-free grammars (specified by mixfix declarations). *) signature SYNTAX = sig type operations val install_operations: operations -> theory -> theory val root: string Config.T val ambiguity_warning: bool Config.T val ambiguity_limit: int Config.T val encode_input: Input.source -> XML.tree val implode_input: Input.source -> string val read_input_pos: string -> Position.T val read_input: string -> Input.source val parse_input: Proof.context -> (XML.tree list -> 'a) -> (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ val parse_term: Proof.context -> string -> term val parse_prop: Proof.context -> string -> term val unparse_sort: Proof.context -> sort -> Pretty.T val unparse_classrel: Proof.context -> class list -> Pretty.T val unparse_arity: Proof.context -> arity -> Pretty.T val unparse_typ: Proof.context -> typ -> Pretty.T val unparse_term: Proof.context -> term -> Pretty.T val check_sort: Proof.context -> sort -> sort val check_typ: Proof.context -> typ -> typ val check_term: Proof.context -> term -> term val check_prop: Proof.context -> term -> term val check_typs: Proof.context -> typ list -> typ list val check_terms: Proof.context -> term list -> term list val check_props: Proof.context -> term list -> term list val uncheck_sort: Proof.context -> sort -> sort val uncheck_arity: Proof.context -> arity -> arity val uncheck_classrel: Proof.context -> class list -> class list val uncheck_typs: Proof.context -> typ list -> typ list val uncheck_terms: Proof.context -> term list -> term list val read_sort: Proof.context -> string -> sort val read_typ: Proof.context -> string -> typ val read_term: Proof.context -> string -> term val read_prop: Proof.context -> string -> term val read_typs: Proof.context -> string list -> typ list val read_terms: Proof.context -> string list -> term list val read_props: Proof.context -> string list -> term list val read_sort_global: theory -> string -> sort val read_typ_global: theory -> string -> typ val read_term_global: theory -> string -> term val read_prop_global: theory -> string -> term val pretty_term: Proof.context -> term -> Pretty.T val pretty_typ: Proof.context -> typ -> Pretty.T val pretty_sort: Proof.context -> sort -> Pretty.T val pretty_classrel: Proof.context -> class list -> Pretty.T val pretty_arity: Proof.context -> arity -> Pretty.T val string_of_term: Proof.context -> term -> string val string_of_typ: Proof.context -> typ -> string val string_of_sort: Proof.context -> sort -> string val string_of_classrel: Proof.context -> class list -> string val string_of_arity: Proof.context -> arity -> string val is_pretty_global: Proof.context -> bool val set_pretty_global: bool -> Proof.context -> Proof.context val init_pretty_global: theory -> Proof.context val init_pretty: Context.generic -> Proof.context val pretty_term_global: theory -> term -> Pretty.T val pretty_typ_global: theory -> typ -> Pretty.T val pretty_sort_global: theory -> sort -> Pretty.T val string_of_term_global: theory -> term -> string val string_of_typ_global: theory -> typ -> string val string_of_sort_global: theory -> sort -> string val pretty_flexpair: Proof.context -> term * term -> Pretty.T list type syntax + val cache_persistent: bool Unsynchronized.ref + val cache_syntax: syntax -> unit val eq_syntax: syntax * syntax -> bool datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int} val get_approx: syntax -> string -> approx option val lookup_const: syntax -> string -> string option val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option val print_translation: syntax -> string -> Proof.context -> typ -> term list -> term (*exception Match*) val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list val print_ast_translation: syntax -> string -> Proof.context -> Ast.ast list -> Ast.ast (*exception Match*) val prtabs: syntax -> Printer.prtabs type mode val mode_default: mode val mode_input: mode val empty_syntax: syntax val merge_syntax: syntax * syntax -> syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule val update_trfuns: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_const_gram: bool -> string list -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_trrules: Ast.ast trrule list -> syntax -> syntax val remove_trrules: Ast.ast trrule list -> syntax -> syntax val const: string -> term val free: string -> term val var: indexname -> term end; structure Syntax: SYNTAX = struct (** inner syntax operations **) (* operations *) type operations = {parse_sort: Proof.context -> string -> sort, parse_typ: Proof.context -> string -> typ, parse_term: Proof.context -> string -> term, parse_prop: Proof.context -> string -> term, unparse_sort: Proof.context -> sort -> Pretty.T, unparse_typ: Proof.context -> typ -> Pretty.T, unparse_term: Proof.context -> term -> Pretty.T, check_typs: Proof.context -> typ list -> typ list, check_terms: Proof.context -> term list -> term list, check_props: Proof.context -> term list -> term list, uncheck_typs: Proof.context -> typ list -> typ list, uncheck_terms: Proof.context -> term list -> term list}; structure Operations = Theory_Data ( type T = operations option; val empty = NONE; val merge = merge_options; ); fun install_operations ops = Operations.map (fn NONE => SOME ops | SOME _ => raise Fail "Inner syntax operations already installed"); fun operation which ctxt x = (case Operations.get (Proof_Context.theory_of ctxt) of NONE => raise Fail "Inner syntax operations not installed" | SOME ops => which ops ctxt x); (* configuration options *) val root = Config.declare_string ("syntax_root", \<^here>) (K "any"); val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true); val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10); (* formal input *) fun encode_input source = let val delimited = Input.is_delimited source; val pos = Input.pos_of source; val text = Input.text_of source; in XML.Elem (Markup.input delimited (Position.properties_of pos), [XML.Text text]) end; val implode_input = encode_input #> YXML.string_of; local fun input_range (XML.Elem ((name, props), _)) = if name = Markup.inputN then (Markup.is_delimited props, Position.range_of_properties props) else (false, Position.no_range) | input_range (XML.Text _) = (false, Position.no_range); fun input_source tree = let val text = XML.content_of [tree]; val (delimited, range) = input_range tree; in Input.source delimited text range end; in fun read_input_pos str = #1 (#2 (input_range (YXML.parse str handle Fail msg => error msg))); fun read_input str = input_source (YXML.parse str handle Fail msg => error msg); fun parse_input ctxt decode markup parse str = let fun parse_tree tree = let val source = input_source tree; val syms = Input.source_explode source; val pos = Input.pos_of source; val _ = Context_Position.reports ctxt [(pos, Markup.cartouche), (pos, markup (Input.is_delimited source))]; val _ = if Options.default_bool "update_inner_syntax_cartouches" then Context_Position.report_text ctxt pos Markup.update (cartouche (Symbol_Pos.content syms)) else (); in parse (syms, pos) end; in (case YXML.parse_body str handle Fail msg => error msg of body as [tree as XML.Elem ((name, _), _)] => if name = Markup.inputN then parse_tree tree else decode body | [tree as XML.Text _] => parse_tree tree | body => decode body) end; end; (* (un)parsing *) val parse_sort = operation #parse_sort; val parse_typ = operation #parse_typ; val parse_term = operation #parse_term; val parse_prop = operation #parse_prop; val unparse_sort = operation #unparse_sort; val unparse_typ = operation #unparse_typ; val unparse_term = operation #unparse_term; (* (un)checking *) val check_typs = operation #check_typs; val check_terms = operation #check_terms; val check_props = operation #check_props; val check_typ = singleton o check_typs; val check_term = singleton o check_terms; val check_prop = singleton o check_props; val uncheck_typs = operation #uncheck_typs; val uncheck_terms = operation #uncheck_terms; (* derived operations for algebra of sorts *) local fun map_sort f S = (case f (TFree ("", S)) of TFree ("", S') => S' | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); in val check_sort = map_sort o check_typ; val uncheck_sort = map_sort o singleton o uncheck_typs; end; val uncheck_classrel = map o singleton o uncheck_sort; fun unparse_classrel ctxt cs = Pretty.block (flat (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs))); fun uncheck_arity ctxt (a, Ss, S) = let val T = Type (a, replicate (length Ss) dummyT); val a' = (case singleton (uncheck_typs ctxt) T of Type (a', _) => a' | T => raise TYPE ("uncheck_arity", [T], [])); val Ss' = map (uncheck_sort ctxt) Ss; val S' = uncheck_sort ctxt S; in (a', Ss', S') end; fun unparse_arity ctxt (a, Ss, S) = let val prtT = unparse_typ ctxt (Type (a, [])); val dom = if null Ss then [] else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1]; in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end; (* read = parse + check *) fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; fun read_typs ctxt = grouped 10 Par_List.map_independent (parse_typ ctxt) #> check_typs ctxt; fun read_terms ctxt = grouped 10 Par_List.map_independent (parse_term ctxt) #> check_terms ctxt; fun read_props ctxt = grouped 10 Par_List.map_independent (parse_prop ctxt) #> check_props ctxt; val read_typ = singleton o read_typs; val read_term = singleton o read_terms; val read_prop = singleton o read_props; val read_sort_global = read_sort o Proof_Context.init_global; val read_typ_global = read_typ o Proof_Context.init_global; val read_term_global = read_term o Proof_Context.init_global; val read_prop_global = read_prop o Proof_Context.init_global; (* pretty = uncheck + unparse *) fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt; fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt; fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt; fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt; val string_of_term = Pretty.string_of oo pretty_term; val string_of_typ = Pretty.string_of oo pretty_typ; val string_of_sort = Pretty.string_of oo pretty_sort; val string_of_classrel = Pretty.string_of oo pretty_classrel; val string_of_arity = Pretty.string_of oo pretty_arity; (* global pretty printing *) val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false); val is_pretty_global = Config.apply pretty_global; val set_pretty_global = Config.put pretty_global; val init_pretty_global = set_pretty_global true o Proof_Context.init_global; val init_pretty = Context.cases init_pretty_global I; val pretty_term_global = pretty_term o init_pretty_global; val pretty_typ_global = pretty_typ o init_pretty_global; val pretty_sort_global = pretty_sort o init_pretty_global; val string_of_term_global = string_of_term o init_pretty_global; val string_of_typ_global = string_of_typ o init_pretty_global; val string_of_sort_global = string_of_sort o init_pretty_global; (* derived operations *) fun pretty_flexpair ctxt (t, u) = [pretty_term ctxt t, Pretty.str " \\<^sup>?", Pretty.brk 1, pretty_term ctxt u]; (** tables of translation functions **) (* parse (ast) translations *) fun err_dup_trfun name c = error ("More than one " ^ name ^ " for " ^ quote c); fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); fun remove_trtab trfuns = fold (Symtab.remove Syntax_Ext.eq_trfun) trfuns; fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab) handle Symtab.DUP c => err_dup_trfun name c; fun merge_trtabs name tab1 tab2 = Symtab.merge Syntax_Ext.eq_trfun (tab1, tab2) handle Symtab.DUP c => err_dup_trfun name c; (* print (ast) translations *) fun apply_tr' tab c ctxt T args = let val fns = map fst (Symtab.lookup_list tab c); fun app_first [] = raise Match | app_first (f :: fs) = f ctxt T args handle Match => app_first fs; in app_first fns end; fun apply_ast_tr' tab c ctxt args = let val fns = map fst (Symtab.lookup_list tab c); fun app_first [] = raise Match | app_first (f :: fs) = f ctxt args handle Match => app_first fs; in app_first fns end; fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syntax_Ext.eq_trfun) trfuns; fun remove_tr'tab trfuns = fold (Symtab.remove_list Syntax_Ext.eq_trfun) trfuns; fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syntax_Ext.eq_trfun (tab1, tab2); (** tables of translation rules **) type ruletab = (Ast.ast * Ast.ast) list Symtab.table; fun dest_ruletab tab = maps snd (Symtab.dest tab); val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r)); val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); (** datatype syntax **) datatype syntax = Syntax of { input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, gram: Parser.gram Synchronized.cache, consts: string Symtab.table, prmodes: string list, parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, parse_ruletab: ruletab, parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table, print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table, print_ruletab: ruletab, print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, prtabs: Printer.prtabs} * stamp; +val cache_persistent = Unsynchronized.ref false; + +fun cache_eval (gram: Parser.gram Synchronized.cache) = + Synchronized.cache_eval {persistent = ! cache_persistent} gram; + +fun cache_syntax (Syntax ({gram, ...}, _)) = ignore (cache_eval gram); + fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}; fun get_approx (Syntax ({prtabs, ...}, _)) c = (case Printer.get_infix prtabs c of SOME infx => SOME (Infix infx) | NONE => (case Printer.get_prefix prtabs c of SOME prfx => SOME prfx | NONE => Printer.get_binder prtabs c) |> Option.map Prefix); fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; -fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Synchronized.cache_eval gram); +fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram); fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; fun parse_rules (Syntax ({parse_ruletab, ...}, _)) = Symtab.lookup_list parse_ruletab; fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab; fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab; fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab; fun prtabs (Syntax ({prtabs, ...}, _)) = prtabs; type mode = string * bool; val mode_default = ("", true); val mode_input = (Print_Mode.input, true); fun extend_gram new_xprods old_xprods gram = Synchronized.cache (fn () => Parser.make_gram new_xprods old_xprods (Synchronized.cache_peek gram)); fun new_gram new_xprods = Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE); (* empty_syntax *) val empty_syntax = Syntax ({input = [], lexicon = Scan.empty_lexicon, gram = Synchronized.cache (fn () => Parser.empty_gram), consts = Symtab.empty, prmodes = [], parse_ast_trtab = Symtab.empty, parse_ruletab = Symtab.empty, parse_trtab = Symtab.empty, print_trtab = Symtab.empty, print_ruletab = Symtab.empty, print_ast_trtab = Symtab.empty, prtabs = Printer.empty_prtabs}, stamp ()); (* update_syntax *) fun update_const (c, b) tab = if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c)) then tab else Symtab.update (c, b) tab; fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val Syntax_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val new_xprods = if inout then distinct (op =) (filter_out (member (op =) input) xprods) else []; fun if_inout xs = if inout then xs else []; in Syntax ({input = new_xprods @ input, lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, gram = if null new_xprods then gram else extend_gram new_xprods input gram, consts = fold update_const consts2 consts1, prmodes = insert (op =) mode prmodes, parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab, parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab, print_trtab = update_tr'tab print_translation print_trtab, print_ruletab = update_ruletab print_rules print_ruletab, print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab, prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ()) end; (* remove_syntax *) fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let val Syntax_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val input' = if inout then subtract (op =) xprods input else input; val changed = length input <> length input'; fun if_inout xs = if inout then xs else []; in Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon, gram = if changed then new_gram input' else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab, parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab, parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab, print_trtab = remove_tr'tab print_translation print_trtab, print_ruletab = remove_ruletab print_rules print_ruletab, print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab, prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ()) end; (* merge_syntax *) fun merge_syntax (Syntax (tabs1, _), Syntax (tabs2, _)) = let val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1, prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1, prtabs = prtabs1} = tabs1; val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2, prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2; val (input', gram') = if pointer_eq (input1, input2) then (input1, gram1) else (case subtract (op =) input1 input2 of [] => (input1, gram1) | new_xprods2 => if subset (op =) (input1, input2) then (input2, gram2) else let val input' = new_xprods2 @ input1; val gram' = new_gram input'; in (input', gram') end); in Syntax ({input = input', lexicon = Scan.merge_lexicons (lexicon1, lexicon2), gram = gram', consts = Symtab.merge (K true) (consts1, consts2), prmodes = Library.merge (op =) (prmodes1, prmodes2), parse_ast_trtab = merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2, parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2, parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2, print_trtab = merge_tr'tabs print_trtab1 print_trtab2, print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2, print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2, prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ()) end; (** print syntax **) local fun pretty_strs_qs name strs = Pretty.strs (name :: map quote (sort_strings strs)); fun pretty_gram (Syntax (tabs, _)) = let val {lexicon, prmodes, gram, ...} = tabs; val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes); in [Pretty.block (Pretty.breaks (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))), - Pretty.big_list "productions:" (Parser.pretty_gram (Synchronized.cache_eval gram)), + Pretty.big_list "productions:" (Parser.pretty_gram (cache_eval gram)), pretty_strs_qs "print modes:" prmodes'] end; fun pretty_trans (Syntax (tabs, _)) = let fun pretty_tab name tab = pretty_strs_qs name (sort_strings (Symtab.keys tab)); fun pretty_ruletab name tab = Pretty.big_list name (map (Pretty.item o single o Ast.pretty_rule) (dest_ruletab tab)); val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, ...} = tabs; in [pretty_tab "consts:" consts, pretty_tab "parse_ast_translation:" parse_ast_trtab, pretty_ruletab "parse_rules:" parse_ruletab, pretty_tab "parse_translation:" parse_trtab, pretty_tab "print_translation:" print_trtab, pretty_ruletab "print_rules:" print_ruletab, pretty_tab "print_ast_translation:" print_ast_trtab] end; in fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn); fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn); fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn); end; (** prepare translation rules **) (* rules *) datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a; fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y) | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y) | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y); fun parse_rule (Parse_Rule pats) = SOME pats | parse_rule (Print_Rule _) = NONE | parse_rule (Parse_Print_Rule pats) = SOME pats; fun print_rule (Parse_Rule _) = NONE | print_rule (Print_Rule pats) = SOME (swap pats) | print_rule (Parse_Print_Rule pats) = SOME (swap pats); (* check_rules *) local fun check_rule rule = (case Ast.rule_error rule of SOME msg => error ("Error in syntax translation rule: " ^ msg ^ "\n" ^ Pretty.string_of (Ast.pretty_rule rule)) | NONE => rule); in fun check_rules rules = (map check_rule (map_filter parse_rule rules), map check_rule (map_filter print_rule rules)); end; (** modify syntax **) val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns; fun update_type_gram add prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls); fun update_const_gram add logical_types prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls); val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; open Lexicon.Syntax; end; diff --git a/src/Pure/Syntax/syntax_phases.ML b/src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML +++ b/src/Pure/Syntax/syntax_phases.ML @@ -1,1017 +1,1017 @@ (* Title: Pure/Syntax/syntax_phases.ML Author: Makarius Main phases of inner syntax processing, with standard implementations of parse/unparse operations. *) signature SYNTAX_PHASES = sig val markup_free: Proof.context -> string -> Markup.T list val reports_of_scope: Position.T list -> Position.report list val decode_sort: term -> sort val decode_typ: term -> typ val decode_term: Proof.context -> Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result val parse_ast_pattern: Proof.context -> string * string -> Ast.ast val term_of_typ: Proof.context -> typ -> term val print_checks: Proof.context -> unit val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> Context.generic -> Context.generic val term_check: int -> string -> (Proof.context -> term list -> term list) -> Context.generic -> Context.generic val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> Context.generic -> Context.generic val term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> Context.generic -> Context.generic val typ_check': int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic val term_check': int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic val typ_uncheck': int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic val term_uncheck': int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic end structure Syntax_Phases: SYNTAX_PHASES = struct (** markup logical entities **) fun markup_class ctxt c = [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c]; fun markup_type ctxt c = [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c]; fun markup_const ctxt c = [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; fun markup_free ctxt x = Variable.markup ctxt x :: (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x then [Variable.markup_fixed ctxt x] else []); fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; fun markup_bound def ps (name, id) = Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; fun markup_entity ctxt c = - (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of + (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of SOME "" => [] | SOME b => markup_entity ctxt b | NONE => c |> Lexicon.unmark {case_class = markup_class ctxt, case_type = markup_type ctxt, case_const = markup_const ctxt, case_fixed = markup_free ctxt, case_default = K []}); (** reports of implicit variable scope **) fun reports_of_scope [] = [] | reports_of_scope (def_pos :: ps) = let val id = serial (); fun entity def = Position.make_entity_markup def id "" ("", def_pos); in map (rpair Markup.bound) (def_pos :: ps) @ ((def_pos, entity {def = true}) :: map (rpair (entity {def = false})) ps) end; (** decode parse trees **) (* decode_sort *) fun decode_sort tm = let fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]); fun class s = Lexicon.unmark_class s handle Fail _ => err (); fun classes (Const (s, _)) = [class s] | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs | classes _ = err (); fun sort (Const ("_dummy_sort", _)) = dummyS | sort (Const ("_topsort", _)) = [] | sort (Const ("_sort", _) $ cs) = classes cs | sort (Const (s, _)) = [class s] | sort _ = err (); in sort tm end; (* decode_typ *) fun decode_pos (Free (s, _)) = if is_some (Term_Position.decode s) then SOME s else NONE | decode_pos _ = NONE; fun decode_typ tm = let fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]); fun typ ps sort tm = (case tm of Const ("_tfree", _) $ t => typ ps sort t | Const ("_tvar", _) $ t => typ ps sort t | Const ("_ofsort", _) $ t $ s => (case decode_pos s of SOME p => typ (p :: ps) sort t | NONE => if is_none sort then typ ps (SOME (decode_sort s)) t else err ()) | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s) | Free (x, _) => TFree (x, ps @ the_default dummyS sort) | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort) | _ => if null ps andalso is_none sort then let val (head, args) = Term.strip_comb tm; val a = (case head of Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) | _ => err ()); in Type (a, map (typ [] NONE) args) end else err ()); in typ [] NONE tm end; (* parsetree_to_ast *) fun parsetree_to_ast ctxt trf parsetree = let val reports = Unsynchronized.ref ([]: Position.report_text list); fun report pos = Position.store_reports reports [pos]; val append_reports = Position.append_reports reports; fun report_pos tok = if Lexicon.suppress_markup tok then Position.none else Lexicon.pos_of_token tok; fun trans a args = (case trf a of NONE => Ast.mk_appl (Ast.Constant a) args | SOME f => f ctxt args); fun asts_of_token tok = if Lexicon.valued_token tok then [Ast.Variable (Lexicon.str_of_token tok)] else []; fun ast_of_position tok = Ast.Variable (Term_Position.encode (report_pos tok)); fun ast_of_dummy a tok = Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]; fun asts_of_position c tok = [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]] and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = let val pos = report_pos tok; val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos); val _ = append_reports rs; in [Ast.Constant (Lexicon.mark_class c)] end | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = let val pos = report_pos tok; val (Type (c, _), rs) = Proof_Context.check_type_name {proper = true, strict = false} ctxt (Lexicon.str_of_token tok, pos); val _ = append_reports rs; in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) = [ast_of_dummy a tok] | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) = [ast_of_dummy a tok] | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) = [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)] | asts_of (Parser.Node (a, pts)) = let val _ = pts |> List.app (fn Parser.Node _ => () | Parser.Tip tok => if Lexicon.valued_token tok then () else report (report_pos tok) (markup_entity ctxt) a); in [trans a (maps asts_of pts)] end | asts_of (Parser.Tip tok) = asts_of_token tok and ast_of pt = (case asts_of pt of [ast] => ast | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts)); val ast = Exn.result ast_of parsetree; in (! reports, ast) end; (* ast_to_term *) fun ast_to_term ctxt trf = let fun trans a args = (case trf a of NONE => Term.list_comb (Syntax.const a, args) | SOME f => f ctxt args); fun term_of (Ast.Constant a) = trans a [] | term_of (Ast.Variable x) = Lexicon.read_var x | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) = trans a (map term_of asts) | term_of (Ast.Appl (ast :: (asts as _ :: _))) = Term.list_comb (term_of ast, map term_of asts) | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); in term_of end; (* decode_term -- transform parse tree into raw term *) fun decode_const ctxt (c, ps) = let val (Const (c', _), reports) = Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps); in (c', reports) end; local fun get_free ctxt x = let val fixed = Variable.lookup_fixed ctxt x; val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x; val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); in if Variable.is_const ctxt x then NONE else if is_some fixed then fixed else if not is_const orelse is_declared then SOME x else NONE end; in fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result | decode_term ctxt (reports0, Exn.Res tm) = let val reports = Unsynchronized.ref reports0; fun report ps = Position.store_reports reports ps; val append_reports = Position.append_reports reports; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = (case Term_Position.decode_position typ of SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t) | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = (case Term_Position.decode_position typ of SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t) | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) | decode _ qs bs (Abs (x, T, t)) = let val id = serial (); val _ = report qs (markup_bound {def = true} qs) (x, id); in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u | decode ps _ _ (Const (a, T)) = (case try Lexicon.unmark_fixed a of SOME x => (report ps (markup_free ctxt) x; Free (x, T)) | NONE => let val c = (case try Lexicon.unmark_const a of SOME c => c | NONE => #1 (decode_const ctxt (a, []))); val _ = report ps (markup_const ctxt) c; in Const (c, T) end) | decode ps _ _ (Free (a, T)) = ((Name.reject_internal (a, ps) handle ERROR msg => error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); (case get_free ctxt a of SOME x => (report ps (markup_free ctxt) x; Free (x, T)) | NONE => let val (c, rs) = decode_const ctxt (a, ps); val _ = append_reports rs; in Const (c, T) end)) | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) | decode ps _ bs (t as Bound i) = (case try (nth bs) i of SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t) | NONE => t); val tm' = Exn.result (fn () => decode [] [] [] tm) (); in (! reports, tm') end; end; (** parse **) (* results *) fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results; fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results; fun report_result ctxt pos ambig_msgs results = (case (proper_results results, failed_results results) of ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn) | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x) | _ => if null ambig_msgs then error ("Parse error: ambiguous syntax" ^ Position.here pos) else error (cat_lines ambig_msgs)); (* parse raw asts *) fun parse_asts ctxt raw root (syms, pos) = let - val syn = Proof_Context.syn_of ctxt; + val syn = Proof_Context.syntax_of ctxt; val ast_tr = Syntax.parse_ast_translation syn; val toks = Syntax.tokenize syn raw syms; val _ = Context_Position.reports ctxt (maps Lexicon.reports_of_token toks); val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) handle ERROR msg => error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks))); val len = length pts; val limit = Config.get ctxt Syntax.ambiguity_limit; val ambig_msgs = if len <= 1 then [] else [cat_lines (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^ " produces " ^ string_of_int len ^ " parse trees" ^ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree) (take limit pts))]; in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end; fun parse_tree ctxt root input = let - val syn = Proof_Context.syn_of ctxt; + val syn = Proof_Context.syntax_of ctxt; val tr = Syntax.parse_translation syn; val parse_rules = Syntax.parse_rules syn; val (ambig_msgs, asts) = parse_asts ctxt false root input; val results = (map o apsnd o Exn.maps_res) (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts; in (ambig_msgs, results) end; (* parse logical entities *) fun parse_failed ctxt pos msg kind = cat_error msg ("Failed to parse " ^ kind ^ Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) "")); fun parse_sort ctxt = Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort (fn (syms, pos) => parse_tree ctxt "sort" (syms, pos) |> uncurry (report_result ctxt pos) |> decode_sort |> Type.minimize_sort (Proof_Context.tsig_of ctxt) handle ERROR msg => parse_failed ctxt pos msg "sort"); fun parse_typ ctxt = Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type (fn (syms, pos) => parse_tree ctxt "type" (syms, pos) |> uncurry (report_result ctxt pos) |> decode_typ handle ERROR msg => parse_failed ctxt pos msg "type"); fun parse_term is_prop ctxt = let val (markup, kind, root, constrain) = if is_prop then (Markup.language_prop, "prop", "prop", Type.constraint propT) else (Markup.language_term, "term", Config.get ctxt Syntax.root, I); val decode = constrain o Term_XML.Decode.term (Proof_Context.consts_of ctxt); in Syntax.parse_input ctxt decode markup (fn (syms, pos) => let val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt); val parsed_len = length (proper_results results); val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning; val limit = Config.get ctxt Syntax.ambiguity_limit; (*brute-force disambiguation via type-inference*) fun check t = (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t) handle exn as ERROR _ => Exn.Exn exn; fun par_map xs = Par_List.map' {name = "Syntax_Phases.parse_term", sequential = false} xs; val results' = if parsed_len > 1 then (grouped 10 par_map o apsnd o Exn.maps_res) check results else results; val reports' = fst (hd results'); val errs = map snd (failed_results results'); val checked = map snd (proper_results results'); val checked_len = length checked; val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt); in if checked_len = 0 then report_result ctxt pos [] [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))] else if checked_len = 1 then (if not (null ambig_msgs) andalso ambiguity_warning andalso Context_Position.is_visible ctxt then warning (cat_lines (ambig_msgs @ ["Fortunately, only one parse tree is well-formed and type-correct,\n\ \but you may still want to disambiguate your grammar or your input."])) else (); report_result ctxt pos [] results') else report_result ctxt pos [] [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @ (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^ (if checked_len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Pretty.item o single o pretty_term) (take limit checked))))))] end handle ERROR msg => parse_failed ctxt pos msg kind) end; (* parse_ast_pattern *) fun parse_ast_pattern ctxt (root, str) = let - val syn = Proof_Context.syn_of ctxt; + val syn = Proof_Context.syntax_of ctxt; val reports = Unsynchronized.ref ([]: Position.report_text list); fun report ps = Position.store_reports reports ps; fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c); fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x); fun decode_appl ps asts = Ast.Appl (map (decode ps) asts) and decode ps (Ast.Constant c) = decode_const ps c | decode ps (Ast.Variable x) = if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x then decode_const ps x else decode_var ps x | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) = if member (op =) Term_Position.markers c then (case Term_Position.decode x of SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args) | NONE => decode_appl ps asts) else decode_appl ps asts | decode ps (Ast.Appl asts) = decode_appl ps asts; val source = Syntax.read_input str; val pos = Input.pos_of source; val syms = Input.source_explode source; val ast = parse_asts ctxt true root (syms, pos) |> uncurry (report_result ctxt pos) |> decode []; val _ = Context_Position.reports_text ctxt (! reports); in ast end; (** encode parse trees **) (* term_of_sort *) fun term_of_sort S = let val class = Syntax.const o Lexicon.mark_class; fun classes [c] = class c | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs; in if S = dummyS then Syntax.const "_dummy_sort" else (case S of [] => Syntax.const "_topsort" | [c] => class c | cs => Syntax.const "_sort" $ classes cs) end; (* term_of_typ *) fun term_of_typ ctxt ty = let val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup; fun ofsort t raw_S = if show_sorts then let val S = #2 (Term_Position.decode_positionS raw_S) in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end else t; fun term_of (Type (a, Ts)) = Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts) | term_of (TFree (x, S)) = if is_some (Term_Position.decode x) then Syntax.free x else ofsort (Syntax.const "_tfree" $ Syntax.free x) S | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S; in term_of ty end; (* simple_ast_of *) fun simple_ast_of ctxt = let val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?"; fun ast_of (Const (c, _)) = Ast.Constant c | ast_of (Free (x, _)) = Ast.Variable x | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi)) | ast_of (t as _ $ _) = let val (f, args) = strip_comb t in Ast.mk_appl (ast_of f) (map ast_of args) end | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)] | ast_of (Abs _) = raise Fail "simple_ast_of: Abs"; in ast_of end; (* sort_to_ast and typ_to_ast *) fun ast_of_termT ctxt trf tm = let val ctxt' = Config.put show_sorts false ctxt; fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t | ast_of (Const (a, _)) = trans a [] | ast_of (t as _ $ _) = (case strip_comb t of (Const (a, _), args) => trans a args | (f, args) => Ast.Appl (map ast_of (f :: args))) | ast_of t = simple_ast_of ctxt t and trans a args = ast_of (trf a ctxt' dummyT args) handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); in ast_of tm end; fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S); fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T); (* term_to_ast *) local fun mark_aprop tm = let fun aprop t = Syntax.const "_aprop" $ t; fun is_prop Ts t = Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT handle TERM _ => false; fun is_term (Const ("Pure.term", _) $ _) = true | is_term _ = false; fun mark _ (t as Const _) = t | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t) | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) = if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1 else mark Ts t1 $ mark Ts t2 | mark Ts (t as t1 $ t2) = (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop) (mark Ts t1 $ mark Ts t2); in mark [] tm end; fun prune_types tm = let fun regard t t' seen = if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen) else if member (op aconv) seen t then (t', seen) else (t, t :: seen); fun prune (t as Const _, seen) = (t, seen) | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen | prune (t as Bound _, seen) = (t, seen) | prune (Abs (x, T, t), seen) = let val (t', seen') = prune (t, seen); in (Abs (x, T, t'), seen') end | prune (t1 $ t2, seen) = let val (t1', seen') = prune (t1, seen); val (t2', seen'') = prune (t2, seen'); in (t1' $ t2', seen'') end; in #1 (prune (tm, [])) end; fun mark_atoms is_syntax_const ctxt tm = let val {structs, fixes} = Syntax_Trans.get_idents ctxt; val show_structs = Config.get ctxt show_structs; fun mark ((t as Const (c, _)) $ u) = if member (op =) Pure_Thy.token_markers c then t $ u else mark t $ mark u | mark (t $ u) = mark t $ mark u | mark (Abs (x, T, t)) = Abs (x, T, mark t) | mark (t as Const (c, T)) = if is_syntax_const c then t else Const (Lexicon.mark_const c, T) | mark (t as Free (x, T)) = let val i = find_index (fn s => s = x) structs + 1 in if i = 0 andalso member (op =) fixes x then Const (Lexicon.mark_fixed x, T) else if i = 1 andalso not show_structs then Syntax.const "_struct" $ Syntax.const "_indexdefault" else Syntax.const "_free" $ t end | mark (t as Var (xi, T)) = if xi = Auto_Bind.dddot then Const ("_DDDOT", T) else Syntax.const "_var" $ t | mark a = a; in mark tm end; in fun term_to_ast is_syntax_const ctxt trf tm = let val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; val show_markup = Config.get ctxt show_markup; fun ast_of tm = (case strip_comb tm of (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts) | ((c as Const ("_free", _)), Free (x, T) :: ts) => Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) | ((c as Const ("_var", _)), Var (xi, T) :: ts) => Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts) | ((c as Const ("_bound", B)), Free (x, T) :: ts) => let val X = if show_markup andalso not show_types orelse B <> dummyT then T else dummyT; in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end | (Const ("_idtdummy", T), ts) => Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts) | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) and trans a T args = ast_of (trf a ctxt T args) handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) and constrain t T0 = let val T = if show_markup andalso not show_types then Type_Annotation.clean T0 else Type_Annotation.smash T0; in if (show_types orelse show_markup) andalso T <> dummyT then Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t, ast_of_termT ctxt trf (term_of_typ ctxt T)] else simple_ast_of ctxt t end; in tm |> mark_aprop |> show_types ? prune_types |> Variable.revert_bounds ctxt |> mark_atoms is_syntax_const ctxt |> ast_of end; end; (** unparse **) local fun free_or_skolem ctxt x = let val m = if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x else Markup.intensify; in if Name.is_skolem x then ([m, Markup.skolem], Variable.revert_fixed ctxt x) else ([m, Markup.free], x) end; fun var_or_skolem s = (case Lexicon.read_variable s of SOME (x, i) => (case try Name.dest_skolem x of NONE => (Markup.var, s) | SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) | NONE => (Markup.var, s)); val typing_elem = YXML.output_markup_elem Markup.typing; val sorting_elem = YXML.output_markup_elem Markup.sorting; fun unparse_t t_to_ast prt_t markup ctxt t = let val show_markup = Config.get ctxt show_markup; val show_sorts = Config.get ctxt show_sorts; val show_types = Config.get ctxt show_types orelse show_sorts; - val syn = Proof_Context.syn_of ctxt; + val syn = Proof_Context.syntax_of ctxt; val prtabs = Syntax.prtabs syn; val trf = Syntax.print_ast_translation syn; fun markup_extern c = (case Syntax.lookup_const syn c of SOME "" => ([], c) | SOME b => markup_extern b | NONE => c |> Lexicon.unmark {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x), case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x), case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x), case_fixed = fn x => free_or_skolem ctxt x, case_default = fn x => ([], x)}); fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x)) | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) | token_trans _ _ = NONE; fun markup_trans a [Ast.Variable x] = token_trans a x | markup_trans "_constrain" [t, ty] = constrain_trans t ty | markup_trans "_idtyp" [t, ty] = constrain_trans t ty | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s | markup_trans _ _ = NONE and constrain_trans t ty = if show_markup andalso not show_types then let val ((bg1, bg2), en) = typing_elem; val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2; val info = {markup = (bg, en), consistent = false, indent = 0}; in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end else NONE and ofsort_trans ty s = if show_markup andalso not show_sorts then let val ((bg1, bg2), en) = sorting_elem; val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2; val info = {markup = (bg, en), consistent = false, indent = 0}; in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end else NONE and pretty_typ_ast m ast = ast |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern |> Pretty.markup m and pretty_ast m ast = ast |> prt_t ctxt prtabs trf markup_trans markup_extern |> Pretty.markup m; in t_to_ast ctxt (Syntax.print_translation syn) t |> Ast.normalize ctxt (Syntax.print_rules syn) |> pretty_ast markup end; in val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false); val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false); fun unparse_term ctxt = let val thy = Proof_Context.theory_of ctxt; - val syn = Proof_Context.syn_of ctxt; + val syn = Proof_Context.syntax_of ctxt; in unparse_t (term_to_ast (is_some o Syntax.lookup_const syn)) (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) (Markup.language_term false) ctxt end; end; (** translations **) (* type propositions *) fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] = Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T | type_prop_tr' ctxt T [t] = Syntax.const "_ofclass" $ term_of_typ ctxt T $ t | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts); (* type reflection *) fun type_tr' ctxt (Type ("itself", [T])) ts = Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts) | type_tr' _ _ _ = raise Match; (* type constraints *) fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) = Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts) | type_constraint_tr' _ _ _ = raise Match; (* authentic syntax *) fun const_ast_tr intern ctxt asts = (case asts of [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] => let val pos = the_default Position.none (Term_Position.decode p); val (c', _) = decode_const ctxt (c, [pos]); val d = if intern then Lexicon.mark_const c' else c; in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end | _ => raise Ast.AST ("const_ast_tr", asts)); (* setup translations *) val _ = Theory.setup (Sign.parse_ast_translation [("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)] #> Sign.typed_print_translation [("_type_prop", type_prop_tr'), ("\<^const>Pure.type", type_tr'), ("_type_constraint_", type_constraint_tr')]); (** check/uncheck **) (* context-sensitive (un)checking *) type key = int * bool; structure Checks = Generic_Data ( type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; type T = ((key * ((string * typ check) * stamp) list) list * (key * ((string * term check) * stamp) list) list); val empty = ([], []); fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T = (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2), AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); ); fun print_checks ctxt = let fun split_checks checks = List.partition (fn ((_, un), _) => not un) checks |> apply2 (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) #> sort (int_ord o apply2 fst)); fun pretty_checks kind checks = checks |> map (fn (i, names) => Pretty.block [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), Pretty.brk 1, Pretty.strs names]); val (typs, terms) = Checks.get (Context.Proof ctxt); val (typ_checks, typ_unchecks) = split_checks typs; val (term_checks, term_unchecks) = split_checks terms; in pretty_checks "typ_checks" typ_checks @ pretty_checks "term_checks" term_checks @ pretty_checks "typ_unchecks" typ_unchecks @ pretty_checks "term_unchecks" term_unchecks end |> Pretty.writeln_chunks; local fun context_check which (key: key) name f = Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); fun simple_check eq f xs ctxt = let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; in fun typ_check' stage = context_check apfst (stage, false); fun term_check' stage = context_check apsnd (stage, false); fun typ_uncheck' stage = context_check apfst (stage, true); fun term_uncheck' stage = context_check apsnd (stage, true); fun typ_check key name f = typ_check' key name (simple_check (op =) f); fun term_check key name f = term_check' key name (simple_check (op aconv) f); fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f); fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f); end; local fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); fun check_all fs = perhaps_apply (map check_stage fs); fun check which uncheck ctxt0 xs0 = let val funs = which (Checks.get (Context.Proof ctxt0)) |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) |> Library.sort (int_ord o apply2 fst) |> map snd |> not uncheck ? map rev; in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; val apply_typ_check = check fst false; val apply_term_check = check snd false; val apply_typ_uncheck = check fst true; val apply_term_uncheck = check snd true; in fun check_typs ctxt raw_tys = let val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys; val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else (); in tys |> apply_typ_check ctxt |> Term_Sharing.typs (Proof_Context.theory_of ctxt) end; fun check_terms ctxt raw_ts = let val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts; val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts'; val tys = map (Logic.mk_type o snd) ps; val (ts', tys') = ts @ tys |> apply_term_check ctxt |> chop (length ts); val typing_report = fold2 (fn (pos, _) => fn ty => if Position.is_reported pos then cons (Position.reported_text pos Markup.typing (Syntax.string_of_typ ctxt (Logic.dest_type ty))) else I) ps tys' []; val _ = if Context_Position.reports_enabled ctxt then Output.report (sorting_report @ typing_report) else (); in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; val uncheck_typs = apply_typ_uncheck; val uncheck_terms = apply_term_uncheck; end; (* install operations *) val _ = Theory.setup (Syntax.install_operations {parse_sort = parse_sort, parse_typ = parse_typ, parse_term = parse_term false, parse_prop = parse_term true, unparse_sort = unparse_sort, unparse_typ = unparse_typ, unparse_term = unparse_term, check_typs = check_typs, check_terms = check_terms, check_props = check_props, uncheck_typs = uncheck_typs, uncheck_terms = uncheck_terms}); end; (* standard phases *) val _ = Context.>> (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #> Syntax_Phases.term_check 0 "standard" (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #> Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #> Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck); diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,236 +1,238 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit val init_build: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; val protocol_modes2 = [isabelle_processN, Pretty.symbolicN]; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* init protocol -- uninterruptible *) val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); fun ml_statistics () = Output.protocol_message (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) []; in fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => let val _ = SHA1.test_samples () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); val _ = Output.physical_stderr Symbol.STX; (* streams *) val (in_stream, out_stream) = Socket_IO.open_streams address; val _ = Byte_Message.write_line out_stream (Bytes.string password); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); (* messages *) val message_channel = Message_Channel.make out_stream; val message = Message_Channel.message message_channel; fun standard_message props name ss = if forall (fn s => s = "") ss then () else let val pos_props = if exists Markup.position_property props then props else props @ Position.properties_of (Position.thread_data ()); in message name pos_props [XML.blob ss] end; fun report_message ss = if Context_Position.reports_enabled0 () then standard_message [] Markup.reportN ss else (); val serial_props = Markup.serial_properties o serial; val message_context = Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #> Unsynchronized.setmp Private_Output.report_fn report_message #> Unsynchronized.setmp Private_Output.result_fn (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #> Unsynchronized.setmp Private_Output.writeln_fn (fn s => standard_message (serial_props ()) Markup.writelnN s) #> Unsynchronized.setmp Private_Output.state_fn (fn s => standard_message (serial_props ()) Markup.stateN s) #> Unsynchronized.setmp Private_Output.information_fn (fn s => standard_message (serial_props ()) Markup.informationN s) #> Unsynchronized.setmp Private_Output.tracing_fn (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #> Unsynchronized.setmp Private_Output.warning_fn (fn s => standard_message (serial_props ()) Markup.warningN s) #> Unsynchronized.setmp Private_Output.legacy_fn (fn s => standard_message (serial_props ()) Markup.legacyN s) #> Unsynchronized.setmp Private_Output.error_message_fn (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #> Unsynchronized.setmp Private_Output.system_message_fn (fn ss => message Markup.systemN [] [XML.blob ss]) #> Unsynchronized.setmp Private_Output.protocol_message_fn (fn props => fn chunks => message Markup.protocolN props chunks) #> Unsynchronized.setmp print_mode ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes)); (* protocol *) fun protocol_loop () = let fun main () = (case Byte_Message.read_message in_stream of NONE => raise Protocol_Command.STOP 0 | SOME [] => Output.system_message "Isabelle process: no input" | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args); val _ = (case Exn.capture_body main of Exn.Res () => () | Exn.Exn exn => if Protocol_Command.is_protocol_exn exn then Exn.reraise exn else (case Exn.capture Runtime.exn_system_message exn of Exn.Res () => () | Exn.Exn crash => recover crash)); in protocol_loop () end; fun protocol () = (message Markup.initN [] [[XML.Text (Session.welcome ())]]; ml_statistics (); protocol_loop ()); val result = Exn.capture_body (message_context protocol); (* shutdown *) val _ = Future.shutdown (); val _ = Execution.reset (); val _ = Message_Channel.shutdown message_channel; val _ = BinIO.closeIn in_stream; val _ = BinIO.closeOut out_stream; val _ = Options.reset_default (); in (case result of Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc | _ => Exn.release result) end); end; (* init options *) fun init_options () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false; Context.theory_tracing := Options.default_bool "context_theory_tracing"; Context.proof_tracing := Options.default_bool "context_proof_tracing"; - Context.data_timing := Options.default_bool "context_data_timing"); + Context.data_timing := Options.default_bool "context_data_timing"; + Syntax.cache_persistent := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); - Printer.show_markup_default := true); + Printer.show_markup_default := true; + Syntax.cache_persistent := true); (* generic init *) fun init_modes modes = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol modes (address, password) else init_options () end; fun init () = init_modes (protocol_modes1, protocol_modes2); fun init_build () = init_modes ([], protocol_modes2); end; diff --git a/src/Pure/sign.ML b/src/Pure/sign.ML --- a/src/Pure/sign.ML +++ b/src/Pure/sign.ML @@ -1,554 +1,554 @@ (* Title: Pure/sign.ML Author: Lawrence C Paulson and Markus Wenzel Logical signature content: naming conventions, concrete syntax, type signature, polymorphic constants. *) signature SIGN = sig val change_begin: theory -> theory val change_end: theory -> theory val change_end_local: Proof.context -> Proof.context val change_check: theory -> theory - val syn_of: theory -> Syntax.syntax + val syntax_of: theory -> Syntax.syntax val tsig_of: theory -> Type.tsig val classes_of: theory -> Sorts.algebra val all_classes: theory -> class list val super_classes: theory -> class -> class list val minimize_sort: theory -> sort -> sort val complete_sort: theory -> sort -> sort val set_defsort: sort -> theory -> theory val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool val inter_sort: theory -> sort * sort -> sort val witness_sorts: theory -> (typ * sort) list -> sort Ord_List.T -> (typ * sort) list * sort Ord_List.T val logical_types: theory -> string list val typ_instance: theory -> typ * typ -> bool val typ_equiv: theory -> typ * typ -> bool val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int val consts_of: theory -> Consts.T val the_const_constraint: theory -> string -> typ val const_type: theory -> string -> typ option val the_const_type: theory -> string -> typ val declared_tyname: theory -> string -> bool val declared_const: theory -> string -> bool val naming_of: theory -> Name_Space.naming val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory val restore_naming: theory -> theory -> theory val inherit_naming: theory -> Proof.context -> Context.generic val full_name: theory -> binding -> string val full_name_path: theory -> string -> binding -> string val full_bname: theory -> bstring -> string val full_bname_path: theory -> string -> bstring -> string val full_name_pos: theory -> binding -> string * Position.T val const_monomorphic: theory -> string -> bool val const_typargs: theory -> string * typ -> typ list val const_instance: theory -> string * typ list -> typ val mk_const: theory -> string * typ list -> term val class_space: theory -> Name_Space.T val type_space: theory -> Name_Space.T val const_space: theory -> Name_Space.T val intern_class: theory -> xstring -> string val intern_type: theory -> xstring -> string val intern_const: theory -> xstring -> string val type_alias: binding -> string -> theory -> theory val const_alias: binding -> string -> theory -> theory val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class val certify_sort: theory -> sort -> sort val certify_typ: theory -> typ -> typ val certify_typ_mode: Type.mode -> theory -> typ -> typ val certify_flags: {prop: bool, normalize: bool} -> Context.generic -> Consts.T -> theory -> term -> term * typ val certify_term: theory -> term -> term * typ val cert_term: theory -> term -> term val cert_prop: theory -> term -> term val no_frees: Proof.context -> term -> term val no_vars: Proof.context -> term -> term val add_type: Proof.context -> binding * int * mixfix -> theory -> theory val add_types_global: (binding * int * mixfix) list -> theory -> theory val add_nonterminals: Proof.context -> binding list -> theory -> theory val add_nonterminals_global: binding list -> theory -> theory val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory val add_abbrev: string -> binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory val primitive_class: binding * class list -> theory -> theory val primitive_classrel: class * class -> theory -> theory val primitive_arity: arity -> theory -> theory val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val parse_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val print_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory val get_scope: theory -> Binding.scope option val new_scope: theory -> Binding.scope * theory val new_group: theory -> theory val reset_group: theory -> theory val add_path: string -> theory -> theory val root_path: theory -> theory val parent_path: theory -> theory val mandatory_path: string -> theory -> theory val qualified_path: bool -> binding -> theory -> theory val local_path: theory -> theory val init_naming: theory -> theory val private_scope: Binding.scope -> theory -> theory val private: Position.T -> theory -> theory val qualified_scope: Binding.scope -> theory -> theory val qualified: Position.T -> theory -> theory val concealed: theory -> theory val hide_class: bool -> string -> theory -> theory val hide_type: bool -> string -> theory -> theory val hide_const: bool -> string -> theory -> theory end structure Sign: SIGN = struct (** datatype sign **) datatype sign = Sign of {syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*) tsig: Type.tsig, (*order-sorted signature of types*) consts: Consts.T}; (*polymorphic constants*) fun rep_sign (Sign args) = args; fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts}; structure Data = Theory_Data' ( type T = sign; val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty); fun merge args = let val context0 = Context.Theory (#1 (hd args)); val syn' = Library.foldl1 Syntax.merge_syntax (map (#syn o rep_sign o #2) args); val tsig' = Library.foldl1 (Type.merge_tsig context0) (map (#tsig o rep_sign o #2) args); val consts' = Library.foldl1 Consts.merge (map (#consts o rep_sign o #2) args); in make_sign (syn', tsig', consts') end; ); val rep_sg = rep_sign o Data.get; fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts))); fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts)); fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts)); fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts)); (* linear change discipline *) fun change_base begin = map_sign (fn (syn, tsig, consts) => (syn, Type.change_base begin tsig, Consts.change_base begin consts)); val change_begin = change_base true; val change_end = change_base false; fun change_end_local ctxt = Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt; fun change_check thy = if can change_end thy then raise Fail "Unfinished linear change of theory content" else thy; (* syntax *) -val syn_of = #syn o rep_sg; +val syntax_of = #syn o rep_sg; (* type signature *) val tsig_of = #tsig o rep_sg; val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; val all_classes = Sorts.all_classes o classes_of; val super_classes = Sorts.super_classes o classes_of; val minimize_sort = Sorts.minimize_sort o classes_of; val complete_sort = Sorts.complete_sort o classes_of; val set_defsort = map_tsig o Type.set_defsort; val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; val of_sort = Type.of_sort o tsig_of; val inter_sort = Type.inter_sort o tsig_of; val witness_sorts = Type.witness_sorts o tsig_of; val logical_types = Type.logical_types o tsig_of; val typ_instance = Type.typ_instance o tsig_of; fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); val typ_match = Type.typ_match o tsig_of; val typ_unify = Type.unify o tsig_of; (* polymorphic constants *) val consts_of = #consts o rep_sg; val the_const_constraint = Consts.the_constraint o consts_of; val the_const_type = Consts.the_const_type o consts_of; val const_type = try o the_const_type; val const_monomorphic = Consts.is_monomorphic o consts_of; val const_typargs = Consts.typargs o consts_of; val const_instance = Consts.instance o consts_of; fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts)); fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none); val declared_const = can o the_const_constraint; (* naming *) val naming_of = Name_Space.naming_of o Context.Theory; val map_naming = Context.theory_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; fun inherit_naming thy = Name_Space.map_naming (K (naming_of thy)) o Context.Proof; val full_name = Name_Space.full_name o naming_of; fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy)); fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name; fun full_bname_path thy path = full_name_path thy path o Binding.name; fun full_name_pos thy b = (full_name thy b, Binding.default_pos_of b); (** name spaces **) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; (** certify entities **) (*exception TYPE*) (* certify wrt. type signature *) val arity_number = Type.arity_number o tsig_of; fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy); val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; fun certify_typ_mode mode = Type.certify_typ mode o tsig_of; val certify_typ = certify_typ_mode Type.mode_default; (* certify term/prop *) local fun type_check context tm = let fun err_appl bs t T u U = let val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U; in raise TYPE (msg, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T | typ_of (_, Free (_, T)) = T | typ_of (_, Var (_, T)) = T | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript => raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i])) | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body) | typ_of (bs, t $ u) = let val T = typ_of (bs, t) and U = typ_of (bs, u) in (case T of Type ("fun", [T1, T2]) => if T1 = U then T2 else err_appl bs t T u U | _ => err_appl bs t T u U) end; in typ_of ([], tm) end; fun err msg = raise TYPE (msg, [], []); fun check_vars (t $ u) = (check_vars t; check_vars u) | check_vars (Abs (_, _, t)) = check_vars t | check_vars (Free (x, _)) = if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else () | check_vars (Var (xi as (_, i), _)) = if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else () | check_vars _ = (); in fun certify_flags {prop, normalize} context consts thy tm = let val tsig = tsig_of thy; fun check_term t = let val _ = check_vars t; val t' = Type.certify_types Type.mode_default tsig t; val T = type_check context t'; val t'' = Consts.certify {normalize = normalize} context tsig consts t'; in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end; val (tm1, ty1) = check_term tm; val tm' = Soft_Type_System.global_purge thy tm1; val (tm2, ty2) = if tm1 = tm' then (tm1, ty1) else check_term tm'; in if tm = tm2 then (tm, ty2) else (tm2, ty2) end; fun certify_term thy = certify_flags {prop = false, normalize = true} (Context.Theory thy) (consts_of thy) thy; fun cert_term_abbrev thy = #1 o certify_flags {prop = false, normalize = false} (Context.Theory thy) (consts_of thy) thy; val cert_term = #1 oo certify_term; fun cert_prop thy = #1 o certify_flags {prop = true, normalize = true} (Context.Theory thy) (consts_of thy) thy; end; (* specifications *) fun no_variables kind add addT mk mkT ctxt tm = (case (add tm [], addT tm []) of ([], []) => tm | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees))))); val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree; val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar; (** signature extension functions **) (*exception ERROR/TYPE*) (* add type constructors *) fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) => let val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx); val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn; val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig; in (syn', tsig', consts) end); fun add_types_global types thy = fold (add_type (Syntax.init_pretty_global thy)) types thy; (* add nonterminals *) fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts)); fun add_nonterminals_global ns thy = add_nonterminals (Syntax.init_pretty_global thy) ns thy; (* add type abbreviations *) fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts)); (* modify syntax *) fun gen_syntax parse_typ add mode args thy = let val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy); fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c); in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end; val syntax = gen_syntax (K I); val syntax_cmd = gen_syntax Syntax.read_typ; fun type_notation add mode args = let fun type_syntax (Type (c, args), mx) = SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end; fun notation add mode args thy = let fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; in syntax add mode (map_filter const_syntax args) thy end; (* add constants *) local fun gen_add_consts prep_typ ctxt raw_args thy = let val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt; fun prep (b, raw_T, mx) = let val c = full_name thy b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ Binding.print b); val T' = Logic.varifyT_global T; in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) |> syntax true Syntax.mode_default (map #2 args) |> pair (map #3 args) end; in fun add_consts args thy = #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy); fun add_consts_cmd args thy = #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx); fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy; end; (* abbreviations *) fun add_abbrev mode (b, raw_t) thy = (* FIXME proper ctxt (?) *) let val ctxt = Syntax.init_pretty_global thy; val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy; val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg) handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val (res, consts') = consts_of thy |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t); in (res, thy |> map_consts (K consts')) end; fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c); (* add constraints *) fun add_const_constraint (c, opt_T) thy = let fun prepT raw_T = let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T))) in cert_term thy (Const (c, T)); T end handle TYPE (msg, _, _) => error msg; in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; (* primitive classes and arities *) fun primitive_class (bclass, classes) thy = thy |> map_sign (fn (syn, tsig, consts) => let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig; in (syn, tsig', consts) end) |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg); fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.Theory thy) arg); (* add translation functions *) local fun mk trs = map Syntax_Ext.mk_trfun trs; in fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], [])); fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], [])); fun print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), [])); fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, [])); fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's)); end; (* translation rules *) val add_trrules = map_syn o Syntax.update_trrules; val del_trrules = map_syn o Syntax.remove_trrules; (* naming *) val get_scope = Name_Space.get_scope o naming_of; fun new_scope thy = let val (scope, naming') = Name_Space.new_scope (naming_of thy); val thy' = map_naming (K naming') thy; in (scope, thy') end; val new_group = map_naming Name_Space.new_group; val reset_group = map_naming Name_Space.reset_group; val add_path = map_naming o Name_Space.add_path; val root_path = map_naming Name_Space.root_path; val parent_path = map_naming Name_Space.parent_path; val mandatory_path = map_naming o Name_Space.mandatory_path; val qualified_path = map_naming oo Name_Space.qualified_path; fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy); fun init_naming thy = let val theory_naming = Name_Space.global_naming |> Name_Space.set_theory_long_name (Context.theory_long_name thy); in map_naming (K theory_naming) thy end; val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* hide names *) val hide_class = map_tsig oo Type.hide_class; val hide_type = map_tsig oo Type.hide_type; val hide_const = map_consts oo Consts.hide; end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,396 +1,397 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val setup_result: (theory -> 'a * theory) -> 'a val local_setup: (Proof.context -> Proof.context) -> unit val local_setup_result: (Proof.context -> 'a * Proof.context) -> 'a val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check_theory: {get: string -> theory, all: unit -> string list} -> Proof.context -> string * Position.T -> theory val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_const: string -> theory -> theory val add_deps_type: string -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit val equality_axioms: (binding * term) list end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun setup_result f = Context.>>> (Context.map_theory_result f); fun local_setup f = Context.>> (Context.map_proof f); fun local_setup_result f = Context.>>> (Context.map_proof_result f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; fun rep_thy (Thy args) = args; fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], [])); fun merge args = let val thy0 = #1 (hd args); val {pos, id, ...} = rep_thy (#2 (hd args)); val merge_defs = Defs.merge (Defs.global_context thy0); val merge_wrappers = Library.merge (eq_snd op =); val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args); val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args); val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args); val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args); in make_thy (pos, id, axioms', defs', (bgs', ens')) end; ); val rep_theory = rep_thy o Thy.get; fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Position.make_entity_markup def id Markup.theoryN (name, pos); fun init_markup (name, pos) thy = let val id = serial (); val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)]; in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup {def = false} (Context.theory_long_name thy) id pos end; fun check_theory {get, all} ctxt (name, pos) = let val thy = get name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => all () |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy); in thy end; fun check long ctxt arg = let val thy = Proof_Context.theory_of ctxt; val get = Context.get_theory long thy; fun all () = map (Context.theory_name long) (ancestors_of thy); in check_theory {get = get, all = all} ctxt arg end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.init_naming |> Sign.local_path |> apply_wrappers wrappers + |> tap (Syntax.cache_syntax o Sign.syntax_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs)); val rhs_extras = TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd)) |> TFrees.keys; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun add_deps_const c thy = let val T = Logic.unvarifyT_global (Sign.the_const_type thy c); in thy |> add_deps_global "" (const_dep thy (c, T)) [] end; fun add_deps_type c thy = let val n = Sign.arity_number thy c; val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); in thy |> add_deps_global "" (type_dep (c, args)) [] end fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; (** axioms for equality **) local val aT = TFree ("'a", []); val bT = TFree ("'b", []); val x = Free ("x", aT); val y = Free ("y", aT); val z = Free ("z", aT); val A = Free ("A", propT); val B = Free ("B", propT); val f = Free ("f", aT --> bT); val g = Free ("g", aT --> bT); in val equality_axioms = [(Binding.make ("reflexive", \<^here>), Logic.mk_equals (x, x)), (Binding.make ("symmetric", \<^here>), Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), (Binding.make ("transitive", \<^here>), Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))), (Binding.make ("equal_intr", \<^here>), Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))), (Binding.make ("equal_elim", \<^here>), Logic.list_implies ([Logic.mk_equals (A, B), A], B)), (Binding.make ("abstract_rule", \<^here>), Logic.mk_implies (Logic.all x (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), (Binding.make ("combination", \<^here>), Logic.list_implies ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))]; end; end;