diff --git a/examples/bts/12475/why3session.xml b/examples/bts/12475/why3session.xml index 37c3d05bc104f46ab3596610cadd7647519473fe..4853b1afc3dd1361f3e516fefc8b086ca014d6fe 100644 --- a/examples/bts/12475/why3session.xml +++ b/examples/bts/12475/why3session.xml @@ -2,28 +2,25 @@ - + - + - - - - + - + - + - + - + diff --git a/examples/bts/12934/why3session.xml b/examples/bts/12934/why3session.xml index 8e9843862f13096f8c3ea3890a5a28c549b84de3..e435ff41bd1c8f4042d24e4b7c09f380e68ec91b 100644 --- a/examples/bts/12934/why3session.xml +++ b/examples/bts/12934/why3session.xml @@ -1,11 +1,17 @@ - + + + + + + + - + - + diff --git a/examples/einstein/why3session.xml b/examples/einstein/why3session.xml index 43807ae9f65421a6b76d8ed87578b03a8137b362..d7ccfd0afcbd2c1314e7b44a47367fee2b0d975b 100644 --- a/examples/einstein/why3session.xml +++ b/examples/einstein/why3session.xml @@ -1,6 +1,12 @@ - + + + + + + + @@ -9,28 +15,28 @@ - + - + - + - + - + - + - + - + - + diff --git a/examples/hello_proof/why3session.xml b/examples/hello_proof/why3session.xml index 047e896f6e3d4686ba54951ec54b2f7bf237e034..eb385af394d8ee351e3ab1fb99fe09503c0f6044 100644 --- a/examples/hello_proof/why3session.xml +++ b/examples/hello_proof/why3session.xml @@ -1,45 +1,42 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/my_cosine/why3session.xml b/examples/my_cosine/why3session.xml index 8d305021525bafb47f34b9ff0898c28d713b0383..2c8cc0f2aa01017353bf6702a4cd7047cd88107a 100644 --- a/examples/my_cosine/why3session.xml +++ b/examples/my_cosine/why3session.xml @@ -2,34 +2,31 @@ - + - + - - - - + - + - + - + - + - + - + - + diff --git a/examples/programs/assigning_meanings_to_programs/why3session.xml b/examples/programs/assigning_meanings_to_programs/why3session.xml index 66188fc1062580cccb821bf7b1758a67f3e95c58..111c7b76b67285c2b0df992e0c22fffd1263b925 100644 --- a/examples/programs/assigning_meanings_to_programs/why3session.xml +++ b/examples/programs/assigning_meanings_to_programs/why3session.xml @@ -2,26 +2,23 @@ - + - + - - - - + - + - + diff --git a/examples/programs/binary_search/why3session.xml b/examples/programs/binary_search/why3session.xml index 44f2aa22e6b554bb61fd2ce58b62918e921ce8d1..26429a652a36de40bd92fa52657d58c4fb11c169 100644 --- a/examples/programs/binary_search/why3session.xml +++ b/examples/programs/binary_search/why3session.xml @@ -2,22 +2,19 @@ - + - + - - - - + - + - + diff --git a/examples/programs/bresenham/why3session.xml b/examples/programs/bresenham/why3session.xml index f8741c47577c24bc8b47417b923d663a4fa021db..85b65d2bfbeefa11b37220b7574b0fe74020a55f 100644 --- a/examples/programs/bresenham/why3session.xml +++ b/examples/programs/bresenham/why3session.xml @@ -2,78 +2,75 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/checking_a_large_routine/why3session.xml b/examples/programs/checking_a_large_routine/why3session.xml index ec3704a696e49ad472cf7d08d433b14a62ec6c45..61ed4f21c30b86bfcda54e977baf03b7f7d4519a 100644 --- a/examples/programs/checking_a_large_routine/why3session.xml +++ b/examples/programs/checking_a_large_routine/why3session.xml @@ -1,6 +1,6 @@ - + @@ -9,65 +9,65 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/decrease1/why3session.xml b/examples/programs/decrease1/why3session.xml index 313cfc842f51df098e88bc8b51575c1458f91abb..4881cf6bb0d0df7f491c64bed93b0e95f08d8688 100644 --- a/examples/programs/decrease1/why3session.xml +++ b/examples/programs/decrease1/why3session.xml @@ -1,223 +1,220 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/edit_distance/why3session.xml b/examples/programs/edit_distance/why3session.xml index 739cdf1dde998e38a8cba020b18c5d1c67609c13..d6215c60e949299e30c95d0bc373a68aca74c3b7 100644 --- a/examples/programs/edit_distance/why3session.xml +++ b/examples/programs/edit_distance/why3session.xml @@ -2,305 +2,302 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/euler001/why3session.xml b/examples/programs/euler001/why3session.xml index f3826a5aae28532739fb7785beb6dd962ee11eba..052c20aa66a320fcc1eaacbf32e1a30fd59b036e 100644 --- a/examples/programs/euler001/why3session.xml +++ b/examples/programs/euler001/why3session.xml @@ -1,80 +1,77 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/fact/why3session.xml b/examples/programs/fact/why3session.xml index 9081349f979e17828c42218ba6310e7e827bc79b..deb13b32251a9a29604ccffe780be96ec33a07d2 100644 --- a/examples/programs/fact/why3session.xml +++ b/examples/programs/fact/why3session.xml @@ -2,26 +2,23 @@ - + - + - - - - + - + - + diff --git a/examples/programs/fib_memo/why3session.xml b/examples/programs/fib_memo/why3session.xml index e3ce33c7a1c389909ee6e8e282ccaefcfa5821ce..1329c28ec5458b1e2128d4b7a01cbde53092ba1f 100644 --- a/examples/programs/fib_memo/why3session.xml +++ b/examples/programs/fib_memo/why3session.xml @@ -9,26 +9,26 @@ - + - + - + - + - + - + - + - + diff --git a/examples/programs/find/why3session.xml b/examples/programs/find/why3session.xml index b5694258e95e49578b351d3721648a2aa231ca2a..10be46f3710c6ab6e837e5db9e0b0c5aec3e146c 100644 --- a/examples/programs/find/why3session.xml +++ b/examples/programs/find/why3session.xml @@ -2,254 +2,251 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/gcd/why3session.xml b/examples/programs/gcd/why3session.xml index abc9e4cb221466bf49ad62801353fec83b3f4a7a..14a62a5b7e00671adf214c5ef481f09cc3d3f7af 100644 --- a/examples/programs/gcd/why3session.xml +++ b/examples/programs/gcd/why3session.xml @@ -2,41 +2,38 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/gcd_bezout/why3session.xml b/examples/programs/gcd_bezout/why3session.xml index 20cf2d1e96521c80c302920d689ee189eff2f70d..4d7f4f7b1079735ee71c38aff38bcfdefee7adab 100644 --- a/examples/programs/gcd_bezout/why3session.xml +++ b/examples/programs/gcd_bezout/why3session.xml @@ -2,76 +2,73 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/insertion_sort/why3session.xml b/examples/programs/insertion_sort/why3session.xml index 2e269739707e818f76a0cf4b8936105623f00f78..01da002b70a876d7eeff87c1ebb10f3eca7d1f6e 100644 --- a/examples/programs/insertion_sort/why3session.xml +++ b/examples/programs/insertion_sort/why3session.xml @@ -2,275 +2,272 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/insertion_sort_list/why3session.xml b/examples/programs/insertion_sort_list/why3session.xml index 4aba0b02db4d8749d149520fb5bd247f8f504cd2..99052393721bd24b58c10bd759ebd85360bda939 100644 --- a/examples/programs/insertion_sort_list/why3session.xml +++ b/examples/programs/insertion_sort_list/why3session.xml @@ -2,69 +2,66 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/isqrt/why3session.xml b/examples/programs/isqrt/why3session.xml index 75a82b41063b952855f369cfe55f2ef0cec9d1ee..c85f0b5072f1be2543dbd917c858d512191aeae1 100644 --- a/examples/programs/isqrt/why3session.xml +++ b/examples/programs/isqrt/why3session.xml @@ -1,176 +1,173 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/kmp/why3session.xml b/examples/programs/kmp/why3session.xml index 691f7dacd0a96772bffc554d4663069d52a7aafa..ca99acdc2ef331c908a1fcd8f223d1666015d79e 100644 --- a/examples/programs/kmp/why3session.xml +++ b/examples/programs/kmp/why3session.xml @@ -2,412 +2,409 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/mccarthy/why3session.xml b/examples/programs/mccarthy/why3session.xml index d8c3389415ca1cd8edb52240e821ae74af9de8e6..d13919f243493c0bd98796cdbb08f86465991d39 100644 --- a/examples/programs/mccarthy/why3session.xml +++ b/examples/programs/mccarthy/why3session.xml @@ -2,96 +2,93 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/mergesort_list/why3session.xml b/examples/programs/mergesort_list/why3session.xml index 30f2ffcdbfd9b39e213e64e326e7404a9fe6c6e7..81190e434bad73279166ae431036ff3094c7c18b 100644 --- a/examples/programs/mergesort_list/why3session.xml +++ b/examples/programs/mergesort_list/why3session.xml @@ -9,34 +9,34 @@ - + - + - + - + - + - + - + - + - + - + - + - + @@ -44,74 +44,74 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/muller/why3session.xml b/examples/programs/muller/why3session.xml index e6734f3583801b8de2dfcf5de7fddab05dc4513e..de5ba401b0153ccb1cb432e16dabeae1a15397aa 100644 --- a/examples/programs/muller/why3session.xml +++ b/examples/programs/muller/why3session.xml @@ -2,101 +2,98 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/my_cosine/why3session.xml b/examples/programs/my_cosine/why3session.xml index 40f7192e6069fde5fa9d34ba57696e28c6ec4366..61be3cbaacdaa67871d9c38e85028c349ed531de 100644 --- a/examples/programs/my_cosine/why3session.xml +++ b/examples/programs/my_cosine/why3session.xml @@ -2,41 +2,38 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/power/why3session.xml b/examples/programs/power/why3session.xml index 2bc4eb764d7d4f6ef5d75874e91e98bc76c03c94..165a62a193b404e6e898b07acfc65289ba7f98c1 100644 --- a/examples/programs/power/why3session.xml +++ b/examples/programs/power/why3session.xml @@ -2,114 +2,111 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/queens/why3session.xml b/examples/programs/queens/why3session.xml index a88e522aaf6a46687d96288071dffbd0e90c63d7..62920e0e11135b83a0e588980b6f72926ae9d83d 100644 --- a/examples/programs/queens/why3session.xml +++ b/examples/programs/queens/why3session.xml @@ -2,330 +2,327 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/quicksort/why3session.xml b/examples/programs/quicksort/why3session.xml index 8faf96bd452f402241830804cba1b5bdfa2433f5..1c666e3514f63376f6767af65c186523f780fed6 100644 --- a/examples/programs/quicksort/why3session.xml +++ b/examples/programs/quicksort/why3session.xml @@ -2,198 +2,195 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/same_fringe/why3session.xml b/examples/programs/same_fringe/why3session.xml index 211f2a31fc5bfd5bfa55aeb5609b5b7c00197acf..2caade1002aede5bc19aa2db64e79d228080cfa6 100644 --- a/examples/programs/same_fringe/why3session.xml +++ b/examples/programs/same_fringe/why3session.xml @@ -9,65 +9,65 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/selection_sort/why3session.xml b/examples/programs/selection_sort/why3session.xml index d4560b398f7b7dcd75dce3ad688f2e402cdc7231..b7ed5766b1c057f813bb2f24175998f9dd021ab0 100644 --- a/examples/programs/selection_sort/why3session.xml +++ b/examples/programs/selection_sort/why3session.xml @@ -2,140 +2,137 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/sf/why3session.xml b/examples/programs/sf/why3session.xml index a1dc4472e76718c54169296012c4067c04c010c7..de7d746a63fb2e6f97d415e4aa15ff0cda13dece 100644 --- a/examples/programs/sf/why3session.xml +++ b/examples/programs/sf/why3session.xml @@ -9,121 +9,121 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/sorted_list/why3session.xml b/examples/programs/sorted_list/why3session.xml index 9bcd428904799776d0c735aa73dcc402b9553e28..48141077fa63cb542d570943114bb588fc3be7e5 100644 --- a/examples/programs/sorted_list/why3session.xml +++ b/examples/programs/sorted_list/why3session.xml @@ -2,24 +2,21 @@ - + - + - - - - + - + - + - + diff --git a/examples/programs/tortoise_and_hare/why3session.xml b/examples/programs/tortoise_and_hare/why3session.xml index 8e67e6ba228f5c0c26389f12e8b37eddfc1514b6..a5fd686a057c916210286a4c837ea4a5e729f393 100644 --- a/examples/programs/tortoise_and_hare/why3session.xml +++ b/examples/programs/tortoise_and_hare/why3session.xml @@ -2,36 +2,33 @@ - + - + - - - - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_aqueue/why3session.xml b/examples/programs/vstte10_aqueue/why3session.xml index fc17d1a3a69c04a9c4686a6785dcfed000d1b4a7..87a00db48e96bbe0e40e7122365b6352d741a7ea 100644 --- a/examples/programs/vstte10_aqueue/why3session.xml +++ b/examples/programs/vstte10_aqueue/why3session.xml @@ -2,53 +2,50 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_inverting/why3session.xml b/examples/programs/vstte10_inverting/why3session.xml index 41e9237227b70c01ec85454e7c533e2b27dc1285..2e619a63155a706cf9b6ccd96cf4ae00fb08446d 100644 --- a/examples/programs/vstte10_inverting/why3session.xml +++ b/examples/programs/vstte10_inverting/why3session.xml @@ -9,81 +9,81 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -92,76 +92,76 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_max_sum/why3session.xml b/examples/programs/vstte10_max_sum/why3session.xml index 91ae0bcfce4f9817d0e8779dc87c6c36ef421931..26f1366af5e4e8ce499f2238f0f290e946d60753 100644 --- a/examples/programs/vstte10_max_sum/why3session.xml +++ b/examples/programs/vstte10_max_sum/why3session.xml @@ -1,412 +1,409 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_queens/why3session.xml b/examples/programs/vstte10_queens/why3session.xml index 53919f66a2937f9f0ea04c30ffa5c59a13d12ceb..2e71fd278dbfdba137e204267c2930e511ace23d 100644 --- a/examples/programs/vstte10_queens/why3session.xml +++ b/examples/programs/vstte10_queens/why3session.xml @@ -2,64 +2,61 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_search_list/why3session.xml b/examples/programs/vstte10_search_list/why3session.xml index f12c00d15043d0668749cf14c2c3229373f7c966..a071e6db8581d6397a33bf9bbb93ccbe23b7a323 100644 --- a/examples/programs/vstte10_search_list/why3session.xml +++ b/examples/programs/vstte10_search_list/why3session.xml @@ -1,191 +1,188 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/zeros/why3session.xml b/examples/programs/zeros/why3session.xml index b34b4523cc7138188850dcb10f71cb1547b60cf6..a8ac047f1769b27cbae880556c6e5bbe7dd7641c 100644 --- a/examples/programs/zeros/why3session.xml +++ b/examples/programs/zeros/why3session.xml @@ -9,48 +9,48 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/regtests.sh b/examples/regtests.sh index 5f2bcbe8c672ba1cc47a098c1c9e780590a6aa41..5cff4d81c1e913d7c3d5f7e7465f9dc4edc24092 100755 --- a/examples/regtests.sh +++ b/examples/regtests.sh @@ -1,6 +1,18 @@ #!/bin/sh # regression tests for why3 +case "$1" in + "-force") + REPLAYOPT="-force" + ;; + "") + REPLAYOPT="" + ;; + *) + echo "$0: Unknown option '$1'" + exit 2 +esac + TMP=$PWD/why3regtests.out TMPERR=$PWD/why3regtests.err @@ -12,7 +24,7 @@ run_dir () { for f in `ls $1/*/why3session.xml`; do d=`dirname $f` echo -n "Replaying $d ... " - ../bin/why3replayer.opt $2 $d 2> $TMPERR > $TMP + ../bin/why3replayer.opt $REPLAYOPT $2 $d 2> $TMPERR > $TMP ret=$? if test "$ret" != "0" ; then echo -n "FAILED (ret code=$ret):" diff --git a/examples/scottish-private-club/why3session.xml b/examples/scottish-private-club/why3session.xml index d6168fcbe43c05f892d683935f8c9ae9a21cba6f..caf4595696560cae608c2d6d621eeda863e36e20 100644 --- a/examples/scottish-private-club/why3session.xml +++ b/examples/scottish-private-club/why3session.xml @@ -1,20 +1,26 @@ - + + + + + + + - + - + - + - + - + diff --git a/src/ide/session.ml b/src/ide/session.ml index 46bd4faaf95a14ee9bc9eb1db27d6b5be9f3b03e..aed14a7f5123fe52f63e3fbf47b251c5cac28215 100644 --- a/src/ide/session.ml +++ b/src/ide/session.ml @@ -285,18 +285,18 @@ let save_status fmt s = | Done r -> save_result fmt r let save_proof_attempt fmt _key a = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" (prover_id a.prover) a.timelimit a.edited_as a.proof_obsolete; save_status fmt a.proof_state; fprintf fmt "@]@\n" let opt lab fmt = function | None -> () - | Some s -> fprintf fmt "%s=\"%s\" " lab s + | Some s -> fprintf fmt "%s=\"%s\"@ " lab s let rec save_goal fmt g = assert (g.goal_shape <> ""); - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" g.goal_name (opt "expl") g.goal_expl g.checksum g.proved g.goal_expanded g.goal_shape; Hashtbl.iter (save_proof_attempt fmt) g.external_proofs; @@ -304,25 +304,25 @@ let rec save_goal fmt g = fprintf fmt "@]@\n" and save_trans fmt _ t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.transf.transformation_name t.transf_proved t.transf_expanded; List.iter (save_goal fmt) t.subgoals; fprintf fmt "@]@\n" let save_theory fmt t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.theory_name t.verified t.theory_expanded; List.iter (save_goal fmt) t.goals; fprintf fmt "@]@\n" let save_file fmt f = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" f.file_name f.file_verified f.file_expanded; List.iter (save_theory fmt) f.theories; fprintf fmt "@]@\n" let save_prover fmt p = - fprintf fmt "@\n@[@]" + fprintf fmt "@\n@[@]" p.prover_id p.prover_name p.prover_version let save fname = @@ -330,7 +330,7 @@ let save fname = let fmt = formatter_of_out_channel ch in fprintf fmt "@\n"; fprintf fmt "@\n"; - fprintf fmt "@[" fname; + fprintf fmt "@[" fname; Util.Mstr.iter (fun _ d -> save_prover fmt d) (get_provers ()); List.iter (save_file fmt) (get_all_files()); fprintf fmt "@]@\n"; @@ -594,6 +594,7 @@ let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal = (* check sum *) (**********************) +(* let task_checksum t = (* TODO: ignore print_locs and print_labels flag *) (* even better: compute check_sum directly, similar to the shape *) @@ -610,6 +611,7 @@ let task_checksum t = eprintf "task %s, sum = %s@." tmp sum; *) sum +*) @@ -646,7 +648,7 @@ let raw_add_goal parent name expl sum shape topt exp = let key = O.create ~parent:parent_key () in let sum,shape = match topt with | None -> sum,shape - | Some t -> (task_checksum t, + | Some t -> (Termcode.task_checksum t, Termcode.t_shape_buf (Task.task_goal_fmla t)) in let goal = { goal_name = name; @@ -836,7 +838,7 @@ let associate_subgoals gname old_goals new_goals = (fun i g -> let id = (Task.task_goal g).Decl.pr_name in let goal_name = gname ^ "." ^ (string_of_int (i+1)) in - let sum = task_checksum g in + let sum = Termcode.task_checksum g in (i,id,goal_name,g,sum)) new_goals in @@ -1152,7 +1154,7 @@ let found_obsolete = ref false let reload_root_goal ~allow_obsolete mth tname old_goals t : goal = let id = (Task.task_goal t).Decl.pr_name in let gname = id.Ident.id_string in - let sum = task_checksum t in + let sum = Termcode.task_checksum t in let old_goal, goal_obsolete = try let old_goal = Util.Mstr.find gname old_goals in diff --git a/src/ide/termcode.ml b/src/ide/termcode.ml index f96c52136d565d3d41e3009aeb7c56260d6225d9..558d21c0f111484a02bc44b85c934d915c2aa307 100644 --- a/src/ide/termcode.ml +++ b/src/ide/termcode.ml @@ -47,6 +47,10 @@ let tag_and = "A" let tag_app = "a" let tag_case = "C" let tag_const = "c" +let tag_Dtype = "Dt" +let ta