mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-19 16:28:12 +03:00
Pull proof robustness modifications from ICFP21 artefact
This commit is contained in:
Denis Merigoux
parent
a6ba0290ed
commit
faedeaf3ce
@ -499,7 +499,7 @@ and substitution_preserves_typing_list
|
||||
|
||||
(**** Preservation theorem *)
|
||||
|
||||
#push-options "--fuel 3 --ifuel 1 --z3rlimit 20"
|
||||
#push-options "--fuel 4 --ifuel 2 --z3rlimit 100 --quake 10/1"
|
||||
let rec preservation (e: exp) (tau: ty)
|
||||
: Lemma (requires (typing empty e tau /\ Some? (step e)))
|
||||
(ensures (typing empty (Some?.v (step e)) tau))
|
||||
@ -527,10 +527,10 @@ let rec preservation (e: exp) (tau: ty)
|
||||
else preservation e2 tau_arg
|
||||
else preservation e1 (TArrow tau_arg tau)
|
||||
| EDefault exceptions just cons tau' ->
|
||||
if List.Tot.for_all (fun except -> is_value except) exceptions then
|
||||
if List.Tot.for_all is_value exceptions then
|
||||
match empty_count AllEmpty exceptions with
|
||||
| AllEmpty ->
|
||||
begin if not (is_value just) then preservation just TBool else match just with
|
||||
begin if not (is_value just) then begin assert(Some? (step just)); preservation just TBool end else match just with
|
||||
| ELit LTrue -> ()
|
||||
| _ -> ()
|
||||
end
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
[
|
||||
"ÈRZ<\u0003\u001a\u0014]\u001bàós˜<73>\u001a ",
|
||||
"^ÖÒ\u0019æ<39>œ¦R³ïi¨\n\u001c6",
|
||||
[
|
||||
[
|
||||
"Catala.DefaultCalculus.ty",
|
||||
@ -8,7 +8,7 @@
|
||||
1,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"12150cad5f4ddd027a123d3c1158bd22"
|
||||
"f9fc150dd19183938eeb34ba6bdbd657"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__TArrow__item__tin",
|
||||
@ -20,7 +20,7 @@
|
||||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||||
],
|
||||
0,
|
||||
"f5a4a5e56629567a3f3abebc47a175f6"
|
||||
"f3d2b8f547abda0782f87d707c869b8d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__TArrow__item__tout",
|
||||
@ -32,7 +32,7 @@
|
||||
"refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee"
|
||||
],
|
||||
0,
|
||||
"32aa6b12103fab987cab73d2805b8c4c"
|
||||
"ae852addd65be90b335b6bb218cd95e5"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.exp",
|
||||
@ -51,7 +51,7 @@
|
||||
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
|
||||
],
|
||||
0,
|
||||
"5c21ef04a7f1a272f0a758c0f9d4157f"
|
||||
"9d2a37207e7e44a0aa6f895ac36f1711"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EVar__item__v",
|
||||
@ -63,7 +63,7 @@
|
||||
"refinement_interpretation_Tm_refine_f7bcdc7958786fcb60dfc7f410094686"
|
||||
],
|
||||
0,
|
||||
"86d09cadd40705978f79fb65229cc940"
|
||||
"05f351ca93ca78b5c20d9328736cafe5"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EApp__item__fn",
|
||||
@ -75,7 +75,7 @@
|
||||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||||
],
|
||||
0,
|
||||
"f936cabcaa864c9de9ef7060d4beda9e"
|
||||
"78ec509aeb281285063fdd61420f514c"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EApp__item__arg",
|
||||
@ -87,7 +87,7 @@
|
||||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||||
],
|
||||
0,
|
||||
"9a2c69a981e794b9f0b928d48bf90ae3"
|
||||
"32f71b14277a31a4820bb616728f3bd2"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EApp__item__tau_arg",
|
||||
@ -99,7 +99,7 @@
|
||||
"refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d"
|
||||
],
|
||||
0,
|
||||
"ab25b3f78be3cc5aabd9f1fd351a0bc1"
|
||||
"fd0ed4fe677d8fede0d42bcbc67941cd"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EAbs__item__vty",
|
||||
@ -111,7 +111,7 @@
|
||||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||||
],
|
||||
0,
|
||||
"74f08bfcc019ccad07bdf4b110444b3e"
|
||||
"7826102b160ea54aa1f02dd7f88fa29d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EAbs__item__body",
|
||||
@ -123,7 +123,7 @@
|
||||
"refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5"
|
||||
],
|
||||
0,
|
||||
"a8f6ac1b8b1eadf6a785be3fe9fb927a"
|
||||
"7075e86600a1b931d7638df53c3d7644"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__ELit__item__l",
|
||||
@ -135,7 +135,7 @@
|
||||
"refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf"
|
||||
],
|
||||
0,
|
||||
"ff76bf58b2a6d5314cdde4b538aba56c"
|
||||
"1fb7b5d0d6bbc1c9f454281a01f5d2e5"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EIf__item__test",
|
||||
@ -147,7 +147,7 @@
|
||||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||||
],
|
||||
0,
|
||||
"cd48dc9eb173c293455593df0f6845f8"
|
||||
"e0826990f2bf12b896b259ea7a29ef9c"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EIf__item__btrue",
|
||||
@ -159,7 +159,7 @@
|
||||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||||
],
|
||||
0,
|
||||
"64ea55616f7ddf6ca1e471e4aaff7d9b"
|
||||
"3e0b50e34c3d0856d8063655fa3c78b9"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EIf__item__bfalse",
|
||||
@ -171,7 +171,7 @@
|
||||
"refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3"
|
||||
],
|
||||
0,
|
||||
"cd4749573d6077d9736cda47882cdfee"
|
||||
"abe0700812430ee14bee827a916c4c36"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EDefault__item__exceptions",
|
||||
@ -183,7 +183,7 @@
|
||||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||||
],
|
||||
0,
|
||||
"cf49a90661edd3f0858eb2722af413f4"
|
||||
"2c8da04378b45ddc9e70997245b3d392"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EDefault__item__just",
|
||||
@ -195,7 +195,7 @@
|
||||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||||
],
|
||||
0,
|
||||
"c9df05fe32fbcde1f09ce17d029667ea"
|
||||
"71722c3137aef8a070db92954483c125"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EDefault__item__cons",
|
||||
@ -207,7 +207,7 @@
|
||||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||||
],
|
||||
0,
|
||||
"93ff28a22eb5be2147e7adea388d6cfd"
|
||||
"c9b5aa06f3d4f96ce9c2dd3b36b4e95e"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__EDefault__item__tau",
|
||||
@ -219,7 +219,7 @@
|
||||
"refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12"
|
||||
],
|
||||
0,
|
||||
"ae54db2c6ac7a040b9bb50d0307b53ec"
|
||||
"fc5a0984f34fcd69654e5047e1be4a72"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.is_renaming_prop",
|
||||
@ -235,7 +235,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"a5871f23ea914484dbc8d47a28d16241"
|
||||
"47c120cc648999657f8b75f2e0dbf98d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.is_renaming_size",
|
||||
@ -247,7 +247,7 @@
|
||||
"refinement_interpretation_Tm_refine_1c1d1c6e28a4d07ae30d44381ee0d524"
|
||||
],
|
||||
0,
|
||||
"0d5c9fb7f30a119d4b46e222cefd114a"
|
||||
"1646f35ef9996dc3507029920875e4cb"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.increment",
|
||||
@ -261,7 +261,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"4ee76b70ce018b172689339c1f9ba1a7"
|
||||
"58c826601d51afd33df888b64778cf63"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.increment_is_renaming",
|
||||
@ -277,7 +277,7 @@
|
||||
"projection_inverse_Catala.DefaultCalculus.EVar_v"
|
||||
],
|
||||
0,
|
||||
"6e078d9ccf128e72e747d681859fec07"
|
||||
"a33ba95b81f3dfeb49bb013dce518b46"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.subst",
|
||||
@ -344,7 +344,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"2ac81019ed65010c01639cde5ce4bd24"
|
||||
"d204a4c04ff4bc41a8e408f2c793af32"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.subst",
|
||||
@ -365,7 +365,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"0d5ade8a32c11b981665f8671b91057a"
|
||||
"f33db5ddb71da97242c740564a00705e"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.subst",
|
||||
@ -404,7 +404,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"91b895d6b22c636592ada525fa8b6e21"
|
||||
"999f67f38fe11e22b56ff48356f22e05"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.var_to_exp_beta",
|
||||
@ -419,7 +419,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"4919dd145a17c7faf0fa0134990f7e24"
|
||||
"dfbbef2a7fec7f91a01db5caddc3f504"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.empty_count_result",
|
||||
@ -428,7 +428,7 @@
|
||||
1,
|
||||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||||
0,
|
||||
"05a61ea6afa54b936185f89ab9f81057"
|
||||
"454de250dadf437ce9064f8c2faea487"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__OneNonEmpty__item___0",
|
||||
@ -440,7 +440,7 @@
|
||||
"refinement_interpretation_Tm_refine_73db3433a5536656aa27657eb477efcf"
|
||||
],
|
||||
0,
|
||||
"4c9e376e3b1d380a9a228dc4cde9412d"
|
||||
"ae7f3ffcfdaa53938d6fe23884ff4317"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.exceptions_count_result",
|
||||
@ -449,7 +449,7 @@
|
||||
1,
|
||||
[ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ],
|
||||
0,
|
||||
"5b75d806bc2195f123968f463592e8c7"
|
||||
"3bbdf3db8159f245ce2f2b1c10d6f185"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.__proj__SomeStep__item___0",
|
||||
@ -461,7 +461,7 @@
|
||||
"refinement_interpretation_Tm_refine_562b75d472a96c36a24c70375d81f26c"
|
||||
],
|
||||
0,
|
||||
"177794c807654230fd0f2a3c1064cb12"
|
||||
"f118d5761b19e05ce48da02ba76c2f6b"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.empty_count",
|
||||
@ -486,7 +486,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"33fab59152a25fb11ae6416f0c1d7ffa"
|
||||
"f6427a407f48df6b59262b4edde385d8"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -503,7 +503,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"a7c323cfaba27d5e7df545707c3ca4ed"
|
||||
"bc2f87497f995ee90a31614799faef5d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -515,7 +515,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"c09544ba3d4ab4c6a612329534698084"
|
||||
"b11c90217682aba8d32a382aa9725984"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -536,7 +536,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"74d07d02a774893a2736842e43273b3f"
|
||||
"24f79481280d552251146950686604be"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -569,7 +569,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"85964bd5932ba9afbd2878998276dcb3"
|
||||
"0b662622406376d0a2bd18937e18ed5e"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -594,7 +594,7 @@
|
||||
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"6720e36dd54fb92ae3cf738f1b6d99c7"
|
||||
"0d237febd87140396125c39c4ddc415b"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.step_app",
|
||||
@ -616,7 +616,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"48361c5e0ee8cdfa9389b377a1e1034e"
|
||||
"0cd9555520b3ca27b77b9ee22f77a1a3"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.extend",
|
||||
@ -631,7 +631,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"959e0ad7f119bf608ef98c6b407085a9"
|
||||
"b4d7124ea3722a753e1998e8e1c6eb80"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.typing",
|
||||
@ -653,7 +653,7 @@
|
||||
"subterm_ordering_Catala.DefaultCalculus.EIf"
|
||||
],
|
||||
0,
|
||||
"c00bf7a3d4293b2ca0d3f471a94a7443"
|
||||
"0cab940a4adca30ec6c107f4bd65ab7e"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.typing",
|
||||
@ -668,7 +668,7 @@
|
||||
"projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"a912ce2537d5bd5b8efac5742694d5e0"
|
||||
"4e3b314f9599171e039bda02fbe32288"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.is_bool_value_cannot_be_abs",
|
||||
@ -694,7 +694,7 @@
|
||||
"typing_tok_Catala.DefaultCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"fcce91fe26fc2f7278f943781c702e71"
|
||||
"96fcf67d7e9d68c08815d5b863cc5d75"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.typing_conserved_by_list_reduction",
|
||||
@ -711,7 +711,7 @@
|
||||
"projection_inverse_BoxBool_proj_0"
|
||||
],
|
||||
0,
|
||||
"4cb4f790bd65800755bf9b124baf211b"
|
||||
"26ee0e9ab80a19918e4ab06c7aee8d1d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.progress",
|
||||
@ -798,7 +798,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"4dbdda6ef73e359692b6571a7ac927de"
|
||||
"dd491009ff9878ade2d35c8a0b85322d"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.progress",
|
||||
@ -925,7 +925,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"5b33ceef79d8a11910f5923459b91078"
|
||||
"679a7f3e7e17536eec0ea6f54aff9c71"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.progress",
|
||||
@ -996,7 +996,7 @@
|
||||
"typing_FStar.List.Tot.Base.for_all"
|
||||
],
|
||||
0,
|
||||
"49410cf76d076b55772b0c9a4b2de111"
|
||||
"08a419c32cc4a72f098d5ba10436fdfc"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.empty_count_preserves_type",
|
||||
@ -1062,7 +1062,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"c276ecd52a1dcec3934e865400780d2b"
|
||||
"244f9100ad5c28fa85f738e2670fd162"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.substitution_extensionnal",
|
||||
@ -1125,7 +1125,7 @@
|
||||
"true_interp"
|
||||
],
|
||||
0,
|
||||
"f5242e01fdb2ece7a83caa64523ecd2a"
|
||||
"988376e56f3be5f5faa5177a5f4bce4b"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.substitution_extensionnal",
|
||||
@ -1153,7 +1153,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"01210c300d902daad597be384d236e96"
|
||||
"9fccb768658c208db732cb784b5ae99a"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.subst_typing",
|
||||
@ -1165,7 +1165,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"17d57ea9dcdbf3e5529ae5c016b6e267"
|
||||
"a9581b31b098f8c6ed0c28a5af28af64"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.substitution_preserves_typing",
|
||||
@ -1307,7 +1307,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"aa3a6a24f4728c912a06d82c99426292"
|
||||
"17d841d14a1131d163065fbd7aabaaba"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.substitution_preserves_typing",
|
||||
@ -1356,7 +1356,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"c519c453b0f1a9388f56d0535bc50cb3"
|
||||
"b393907a80bc0e092e77f702ffaf264a"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.preservation",
|
||||
@ -1369,7 +1369,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"3bf4fe76ba9dfb3c52e3ed63de7adcae"
|
||||
"2caf5bf722b94a214563c4b58dfd0592"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.preservation",
|
||||
@ -1555,7 +1555,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"1e47a11fea34c5c271443a4b0f90e428"
|
||||
"1f5c06cb5572febc9e2355e796f50834"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.preservation",
|
||||
@ -1568,13 +1568,13 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"0e7a6af020959c58c04caab0a14b1921"
|
||||
"b3bcc3a1d16fea99e6f6a223fe293e0f"
|
||||
],
|
||||
[
|
||||
"Catala.DefaultCalculus.preservation",
|
||||
4,
|
||||
3,
|
||||
1,
|
||||
4,
|
||||
2,
|
||||
[
|
||||
"@MaxFuel_assumption", "@MaxIFuel_assumption",
|
||||
"@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||||
@ -1602,7 +1602,6 @@
|
||||
"data_elim_Catala.DefaultCalculus.EDefault",
|
||||
"data_elim_FStar.Pervasives.Native.Some",
|
||||
"data_typing_intro_Catala.DefaultCalculus.EDefault@tok",
|
||||
"data_typing_intro_Catala.DefaultCalculus.ELit@tok",
|
||||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok",
|
||||
"disc_equation_FStar.Pervasives.Native.None",
|
||||
"disc_equation_FStar.Pervasives.Native.Some",
|
||||
@ -1630,6 +1629,7 @@
|
||||
"projection_inverse_Catala.DefaultCalculus.EDefault_just",
|
||||
"projection_inverse_Catala.DefaultCalculus.EDefault_tau",
|
||||
"projection_inverse_Catala.DefaultCalculus.ELit_l",
|
||||
"projection_inverse_FStar.Pervasives.Native.None_a",
|
||||
"projection_inverse_FStar.Pervasives.Native.Some_v",
|
||||
"projection_inverse_Prims.Cons_a",
|
||||
"projection_inverse_Prims.Cons_hd",
|
||||
@ -1640,7 +1640,6 @@
|
||||
"refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14",
|
||||
"refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1",
|
||||
"subterm_ordering_Prims.Cons",
|
||||
"token_correspondence_Catala.DefaultCalculus.step.fuel_instrumented",
|
||||
"token_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented",
|
||||
"token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented",
|
||||
"token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented",
|
||||
@ -1648,12 +1647,11 @@
|
||||
"typing_Catala.DefaultCalculus.step",
|
||||
"typing_Catala.DefaultCalculus.step_exceptions_left_to_right",
|
||||
"typing_Catala.DefaultCalculus.typing",
|
||||
"typing_tok_Catala.DefaultCalculus.LConflictError@tok",
|
||||
"typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion",
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"8027f16b03d414235a16bb198765a509"
|
||||
"0ffcc137baddae54cd5223d99bb5fffa"
|
||||
]
|
||||
]
|
||||
]
|
||||
@ -8,7 +8,7 @@
|
||||
1,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"8de2ec0ff3dee94558714e126cccaca4"
|
||||
"0e311e55c6adcf97ececac5dd9a61c53"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__TArrow__item__tin",
|
||||
@ -20,7 +20,7 @@
|
||||
"refinement_interpretation_Tm_refine_e0df9c7637802e33e8c31682fffa5ba6"
|
||||
],
|
||||
0,
|
||||
"bbccaed5704979c55a559a1c31a1834c"
|
||||
"87405cb79d852640cd955a508fa53697"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__TArrow__item__tout",
|
||||
@ -32,7 +32,7 @@
|
||||
"refinement_interpretation_Tm_refine_e0df9c7637802e33e8c31682fffa5ba6"
|
||||
],
|
||||
0,
|
||||
"8fab8bc658b169864bda6f068334f6ce"
|
||||
"789de8a72ff29de292515f0c853a91d4"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__TList__item__elts",
|
||||
@ -44,7 +44,7 @@
|
||||
"refinement_interpretation_Tm_refine_d983dccc0214b834973ff1399f92beb8"
|
||||
],
|
||||
0,
|
||||
"76268d2f639e4f5bc0d502f45d867c56"
|
||||
"7f1846b71fe8bcbf2a13fb6ba299a817"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__TOption__item__a",
|
||||
@ -56,7 +56,7 @@
|
||||
"refinement_interpretation_Tm_refine_3d558d916dde713422174b28b39dc533"
|
||||
],
|
||||
0,
|
||||
"a870f36b0cd10999ebf920fdb3271420"
|
||||
"b500e52f927c6fa9f95258a13e2f2bc3"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.lit",
|
||||
@ -65,7 +65,7 @@
|
||||
1,
|
||||
[ "@query", "assumption_Catala.LambdaCalculus.err__uu___haseq" ],
|
||||
0,
|
||||
"2030bcfc0e28da947ac45fe58c6cc1e0"
|
||||
"5e6ce25851abdb93d9e5d78d97a18b59"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__LError__item__err",
|
||||
@ -77,7 +77,7 @@
|
||||
"refinement_interpretation_Tm_refine_03c5f53bf3c3d998eb9852e335e5f83b"
|
||||
],
|
||||
0,
|
||||
"d752ee7fff2be31ce886ccaa29ba767d"
|
||||
"44b3e279e6f9cdeb11b4887c749b66be"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.exp",
|
||||
@ -98,7 +98,7 @@
|
||||
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
|
||||
],
|
||||
0,
|
||||
"cf66495fa49d61cfc6a9e34bd2fc8af5"
|
||||
"2a5e6e9a46fb03e85d5d09bf9b6c7ccb"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EVar__item__v",
|
||||
@ -110,7 +110,7 @@
|
||||
"refinement_interpretation_Tm_refine_ba87924536b02a4efbb171a9a3f24dc1"
|
||||
],
|
||||
0,
|
||||
"807ab3c72e77bd5e5ab1f522508b0a7e"
|
||||
"4e113c94c6ebf7cae84a79d1b6980774"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EApp__item__fn",
|
||||
@ -122,7 +122,7 @@
|
||||
"refinement_interpretation_Tm_refine_a719520990feb006edba4632bf1de67c"
|
||||
],
|
||||
0,
|
||||
"56a9590f38fef0e368dc49671f13e429"
|
||||
"5369de316813ed5967b9b4d207bf1700"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EApp__item__arg",
|
||||
@ -134,7 +134,7 @@
|
||||
"refinement_interpretation_Tm_refine_a719520990feb006edba4632bf1de67c"
|
||||
],
|
||||
0,
|
||||
"0fee0a2cf90edf2e7cbe779d3eea1678"
|
||||
"6620ffb9a81fd6e942e7e9b54ba957cf"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EApp__item__tau_arg",
|
||||
@ -146,7 +146,7 @@
|
||||
"refinement_interpretation_Tm_refine_a719520990feb006edba4632bf1de67c"
|
||||
],
|
||||
0,
|
||||
"ec68032617fc4491889b91e0c2f408e8"
|
||||
"52f10ad5aa895f9deb915f9ee8f669eb"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EAbs__item__vty",
|
||||
@ -158,7 +158,7 @@
|
||||
"refinement_interpretation_Tm_refine_64f2adea38011f2f250c3e2a8698555e"
|
||||
],
|
||||
0,
|
||||
"250cdd4d1befbdb320f34f541a3fad3c"
|
||||
"b35a51a46ee83d7ea300022694a62bca"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EAbs__item__body",
|
||||
@ -170,7 +170,7 @@
|
||||
"refinement_interpretation_Tm_refine_64f2adea38011f2f250c3e2a8698555e"
|
||||
],
|
||||
0,
|
||||
"84a7bff35e43a7943088a46289aa9efd"
|
||||
"eb5dc1df75878e4e70e01cb0a8d74bdf"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EThunk__item__body",
|
||||
@ -182,7 +182,7 @@
|
||||
"refinement_interpretation_Tm_refine_fa1bc5d4438d467178933555e84bfdb0"
|
||||
],
|
||||
0,
|
||||
"e1588468dca9ea1d839943321335c987"
|
||||
"acfa67613af2e2b652f95b3a311e2ab0"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__ELit__item__l",
|
||||
@ -194,7 +194,7 @@
|
||||
"refinement_interpretation_Tm_refine_b8b77a9f0a7ac5cbd4fe272d4407c47b"
|
||||
],
|
||||
0,
|
||||
"800974582885f0c85300d2cc343e0024"
|
||||
"bde3011fa4a1e78ff3e0b9b869fec8fa"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EIf__item__test",
|
||||
@ -206,7 +206,7 @@
|
||||
"refinement_interpretation_Tm_refine_f36dce8ad972049e00d02a4e8af7bfcf"
|
||||
],
|
||||
0,
|
||||
"c10a6ab0e827e474db114afa930cfa82"
|
||||
"d9c5401295c054aeca11b0942773a415"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EIf__item__btrue",
|
||||
@ -218,7 +218,7 @@
|
||||
"refinement_interpretation_Tm_refine_f36dce8ad972049e00d02a4e8af7bfcf"
|
||||
],
|
||||
0,
|
||||
"2b105d57bd4707b3446049bcbbe78f3b"
|
||||
"f3bc0404e7cb9db46a7e45b940ab3ab8"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EIf__item__bfalse",
|
||||
@ -230,7 +230,7 @@
|
||||
"refinement_interpretation_Tm_refine_f36dce8ad972049e00d02a4e8af7bfcf"
|
||||
],
|
||||
0,
|
||||
"d63561aa21b29c97fe7412d848a9aebb"
|
||||
"feba0dcfd4b637e530d3f1df55692b26"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__ESome__item__s",
|
||||
@ -242,7 +242,7 @@
|
||||
"refinement_interpretation_Tm_refine_20fa929526977a65cb1df84b45438b8d"
|
||||
],
|
||||
0,
|
||||
"e1fff2f2dacdee4e4db9ddad56903cf0"
|
||||
"3026bf7c38e36947da44fe3de9d93b13"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EMatchOption__item__arg",
|
||||
@ -254,7 +254,7 @@
|
||||
"refinement_interpretation_Tm_refine_57367977d238cf27e36a3ef56ad291f4"
|
||||
],
|
||||
0,
|
||||
"d5f58d23a25a05fe4fc1ecf70c37416b"
|
||||
"a6cf19275df5278a353cb59137e52bac"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EMatchOption__item__tau_some",
|
||||
@ -266,7 +266,7 @@
|
||||
"refinement_interpretation_Tm_refine_57367977d238cf27e36a3ef56ad291f4"
|
||||
],
|
||||
0,
|
||||
"f8564b4f8e934a645c18d48aedebe858"
|
||||
"57b98f77d487ad63b2027c4eaeeb8674"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EMatchOption__item__none",
|
||||
@ -278,7 +278,7 @@
|
||||
"refinement_interpretation_Tm_refine_57367977d238cf27e36a3ef56ad291f4"
|
||||
],
|
||||
0,
|
||||
"46c3bbed626fb87616e634b004ffdd67"
|
||||
"84986ecb0e5990a650cb69c1bf7b7282"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EMatchOption__item__some",
|
||||
@ -290,7 +290,7 @@
|
||||
"refinement_interpretation_Tm_refine_57367977d238cf27e36a3ef56ad291f4"
|
||||
],
|
||||
0,
|
||||
"b4df29a440b197f8345d040a7d6c05da"
|
||||
"9a416e0463745168114d4004ded3a8c1"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EList__item__l",
|
||||
@ -302,7 +302,7 @@
|
||||
"refinement_interpretation_Tm_refine_01736dfac08f9723e991fedf308a456b"
|
||||
],
|
||||
0,
|
||||
"554be0743f7d47c871372140e4b71a09"
|
||||
"295bb443a75c1bacb1dc3e58f011c90c"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__ECatchEmptyError__item__to_try",
|
||||
@ -314,7 +314,7 @@
|
||||
"refinement_interpretation_Tm_refine_9a40a813c12283df68af10f9acc20e9e"
|
||||
],
|
||||
0,
|
||||
"07b4feecbf6fa06a0d64f3994820b78b"
|
||||
"52b1f8f0f063a04889f7f3e3c8c7501d"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__ECatchEmptyError__item__catch_with",
|
||||
@ -326,7 +326,7 @@
|
||||
"refinement_interpretation_Tm_refine_9a40a813c12283df68af10f9acc20e9e"
|
||||
],
|
||||
0,
|
||||
"ad9284dcc3fff5f6779ee0b78c6ce2fd"
|
||||
"8cc3f0b443adb97e45890741c8c844ce"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EFoldLeft__item__f",
|
||||
@ -338,7 +338,7 @@
|
||||
"refinement_interpretation_Tm_refine_65688a1c5ad79fa9ee8734e7ef72d1b7"
|
||||
],
|
||||
0,
|
||||
"11682f08873245cc93fce0e4ba007c55"
|
||||
"e87d4a16d12dc19fe148715242fdba9d"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EFoldLeft__item__init",
|
||||
@ -350,7 +350,7 @@
|
||||
"refinement_interpretation_Tm_refine_65688a1c5ad79fa9ee8734e7ef72d1b7"
|
||||
],
|
||||
0,
|
||||
"174e572bf31a43995981ae5ac6e6bb36"
|
||||
"c7d869d6294328efe5209691a8111bb2"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EFoldLeft__item__tau_init",
|
||||
@ -362,7 +362,7 @@
|
||||
"refinement_interpretation_Tm_refine_65688a1c5ad79fa9ee8734e7ef72d1b7"
|
||||
],
|
||||
0,
|
||||
"8e2595ca05da87bd542403f5c20633c7"
|
||||
"4ff553418ce428f8ac6a9977798eb1a4"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EFoldLeft__item__l",
|
||||
@ -374,7 +374,7 @@
|
||||
"refinement_interpretation_Tm_refine_65688a1c5ad79fa9ee8734e7ef72d1b7"
|
||||
],
|
||||
0,
|
||||
"f202c595c2392dc47e5cfe10dac07177"
|
||||
"6c77d28a91cafa8e4a8b6da09644f430"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__EFoldLeft__item__tau_elt",
|
||||
@ -386,7 +386,7 @@
|
||||
"refinement_interpretation_Tm_refine_65688a1c5ad79fa9ee8734e7ef72d1b7"
|
||||
],
|
||||
0,
|
||||
"3b3b3b8f5880d96d70b5339425204617"
|
||||
"ea174cb63e7a3ed6fa0d162c27bb721e"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_value",
|
||||
@ -402,7 +402,7 @@
|
||||
"subterm_ordering_Catala.LambdaCalculus.ESome"
|
||||
],
|
||||
0,
|
||||
"59567df5b16387c44cbd971535258c7e"
|
||||
"d5c93964e0fcd7d4a58d041faa44a609"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_value",
|
||||
@ -419,7 +419,7 @@
|
||||
"projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"f6f09e0cad6439bfa25cf2f1f595bea6"
|
||||
"4250df247014a087fdd788c3533f106a"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_renaming_prop",
|
||||
@ -435,7 +435,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"217a0c6ccdce03a3a4273001c6149c43"
|
||||
"a1ec58e609bd64e52bebe12ca171e36e"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_renaming_size",
|
||||
@ -447,7 +447,7 @@
|
||||
"refinement_interpretation_Tm_refine_e7ef4ddcb37f8c967ca2870b656141e3"
|
||||
],
|
||||
0,
|
||||
"beb9c51c18139eeb226255828fbafc87"
|
||||
"f6be76141a7830bfa1599d9faee514f6"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.increment",
|
||||
@ -461,7 +461,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"4f71c622ce69cd8abd4dd84f56b02f65"
|
||||
"826f38c893b00b91d12ab4196fa88ee1"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.increment_is_renaming",
|
||||
@ -477,7 +477,7 @@
|
||||
"projection_inverse_Catala.LambdaCalculus.EVar_v"
|
||||
],
|
||||
0,
|
||||
"d575a68308c59405356b557e01fc2a85"
|
||||
"47bf36691b2a4a823b18e4d352bacff5"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst",
|
||||
@ -572,7 +572,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"8729ef20b50c0be16ced54716c51e6d9"
|
||||
"30e77d01469e0b97a5bb4ec7a83dcdc4"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst",
|
||||
@ -595,7 +595,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"652d96ce304667f0ced54b058ad2f97c"
|
||||
"2deb362b7ec990eb62110370c8d238d8"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst",
|
||||
@ -634,7 +634,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"66365e1fa44a46cad61420cdbcc5e8b4"
|
||||
"320594af148d303e54dc789f4113981e"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.var_to_exp_beta",
|
||||
@ -649,7 +649,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"baf1dc778c2652e71750817e4dfd1ec5"
|
||||
"e245ace6d1b8bf9373b14df4f867d690"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.list_step_result",
|
||||
@ -662,7 +662,7 @@
|
||||
"kinding_Catala.LambdaCalculus.exp@tok"
|
||||
],
|
||||
0,
|
||||
"736d635b5a29da13ac84ed36d58726b2"
|
||||
"3604773b754f8447f78790e4955f636a"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__Good__item___0",
|
||||
@ -674,7 +674,7 @@
|
||||
"refinement_interpretation_Tm_refine_a6e7ab89f661323296c36eb1747076b6"
|
||||
],
|
||||
0,
|
||||
"01e5997352294f98df0ebb15b3314b27"
|
||||
"c52f7d3c9aee3436269c7e10abdf42c3"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.__proj__Error__item___0",
|
||||
@ -686,7 +686,7 @@
|
||||
"refinement_interpretation_Tm_refine_c5b4d354da344d8cd86bdf12541d59c0"
|
||||
],
|
||||
0,
|
||||
"b1ad150bd6ad4bc5d9b136bc69133301"
|
||||
"2a376f52fd138a18a8bb1a4be11990b3"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_not_bad",
|
||||
@ -702,7 +702,7 @@
|
||||
"projection_inverse_BoxBool_proj_0"
|
||||
],
|
||||
0,
|
||||
"add5d7152901a3ec00c8ce034b01989f"
|
||||
"6bb65a2141176c759d3cfe80d1454415"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -719,7 +719,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"749e1da01f4a8659865e5dd66727e18a"
|
||||
"f2a5c1280bd052394d2582552562ea5e"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -731,7 +731,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"75fd805108b24efbcef483629868303b"
|
||||
"181b225b79b7d02249595851c45ed58d"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -743,7 +743,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"5843a642b88bf50fbf77ad85340a1345"
|
||||
"a730f7989e50fe7a82a052d3357d460a"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -770,7 +770,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"f0735b14edde035f7deb94085b9b6bbf"
|
||||
"f4ab78374ab6c164ca022933d9001346"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -782,7 +782,7 @@
|
||||
"lemma_FStar.Pervasives.invertOption"
|
||||
],
|
||||
0,
|
||||
"823c41dd1061aeed0bbb3c58941a11f1"
|
||||
"1481331f0ec24a1739aa3b12fa8b2cef"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -815,7 +815,7 @@
|
||||
"typing_Catala.LambdaCalculus.is_value"
|
||||
],
|
||||
0,
|
||||
"1eed5729dccbbe490fbbbc0f3b165442"
|
||||
"5bcaae97487e368fd2d9fb45ded53799"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.step_app",
|
||||
@ -851,7 +851,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"cae0f4a76913633da31475a5fa514df2"
|
||||
"cfd79511cb01c06fc61027f1af38f141"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.extend",
|
||||
@ -866,7 +866,7 @@
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"8423da4c4c6744d1c9d2663d8b3e45fe"
|
||||
"055548d3ff1af27ae05e1347d43241c1"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.typing",
|
||||
@ -894,7 +894,7 @@
|
||||
"subterm_ordering_Catala.LambdaCalculus.EThunk"
|
||||
],
|
||||
0,
|
||||
"23c50f39f5fe5bb9e66be250d5586cda"
|
||||
"40bf7072490113404bf28f2bdaa7cd15"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.typing",
|
||||
@ -911,7 +911,7 @@
|
||||
"projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"79670879d71b99c8f3fed539711896ab"
|
||||
"c5c4fa980bdb5d2f6c751f27fe4c7b52"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.is_bool_value_cannot_be_abs",
|
||||
@ -939,7 +939,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"1179fb7dd55fa4fa68715269af71445d"
|
||||
"1ecd002c0642e08ee395fe39000c208d"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.typing_conserved_by_list_reduction",
|
||||
@ -956,7 +956,7 @@
|
||||
"projection_inverse_BoxBool_proj_0"
|
||||
],
|
||||
0,
|
||||
"5fc7ec88715d4b68b1c959089dd7b501"
|
||||
"bccaa71046651a63e01c914dc27265b4"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.size_for_progress",
|
||||
@ -998,7 +998,7 @@
|
||||
"subterm_ordering_Catala.LambdaCalculus.EThunk"
|
||||
],
|
||||
0,
|
||||
"0ed20890bdc4d2a427666f2739d89301"
|
||||
"3eff628fe238bbea2021f8d7d5a84235"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.size_for_progress",
|
||||
@ -1020,7 +1020,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"ddb34c1cbff5b588aeea0eea59cf6c53"
|
||||
"090549f4e2ca6594f744032f0e49541c"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.lemma_size_fold_step",
|
||||
@ -1067,7 +1067,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"e8e903157510795394e5958d95d08ada"
|
||||
"2d6a1bcb40667bec4c4e82fa54ee4e7b"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.lemma_size_fold_f",
|
||||
@ -1094,7 +1094,7 @@
|
||||
"typing_Catala.LambdaCalculus.size_for_progress"
|
||||
],
|
||||
0,
|
||||
"a68e8cb24dc6be13d457a909913c6bc7"
|
||||
"c7eb0606a328c8247fa68f56dbeb2dc0"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.lemma_size_fold_init",
|
||||
@ -1120,7 +1120,7 @@
|
||||
"token_correspondence_Catala.LambdaCalculus.size_for_progress.fuel_instrumented"
|
||||
],
|
||||
0,
|
||||
"ff8214e7fa2b4374d3cc0097680bf181"
|
||||
"28cbf400e760cf1343d7298b52383da8"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.lemma_size_fold_l",
|
||||
@ -1147,7 +1147,7 @@
|
||||
"typing_Catala.LambdaCalculus.size_for_progress"
|
||||
],
|
||||
0,
|
||||
"b6438c9acd74b9fc96737f3bf7141be0"
|
||||
"787ccf1eec3cde9722698427cd22c917"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.progress",
|
||||
@ -1156,7 +1156,7 @@
|
||||
2,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"f1dbb5de672c8c0a65ae1ef0914766cf"
|
||||
"fc1c0c4374692ba34e9b35149b4135db"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.progress",
|
||||
@ -1339,7 +1339,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"8e8e471453f35981acc2b77b61e16011"
|
||||
"1a727fc1746265d817a3155e0a5e2cd5"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.progress",
|
||||
@ -1348,7 +1348,7 @@
|
||||
2,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"e3d828df7df188144d2719b9b0247a82"
|
||||
"db945381124fb742158d229c45adc679"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.progress",
|
||||
@ -1427,7 +1427,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"ffa6f467dceade56ba1aa7cbee1777c7"
|
||||
"1e54549db87ae7bee99379999bcea455"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.substitution_extensionnal",
|
||||
@ -1519,7 +1519,7 @@
|
||||
"true_interp", "typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"a767ec62f9b851bfa2114c36b15c04cc"
|
||||
"f54d0a707cef68e009feb483a192f332"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.substitution_extensionnal",
|
||||
@ -1550,7 +1550,7 @@
|
||||
"subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"8fed6da686196f65ad6f9267ec127539"
|
||||
"db8688eee6a0661b7a6d54ffad888cd0"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst_typing",
|
||||
@ -1562,7 +1562,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"45e2a42eeb6ff38d73ac3925fa13a1b5"
|
||||
"85e833e849bccbed2de5eab2884806cc"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.substitution_preserves_typing",
|
||||
@ -1740,7 +1740,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"503e1308cd7f0194f0a88a292ec7c5a4"
|
||||
"4557d2bcd77fb6338b3789bf69c2b5e6"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.substitution_preserves_typing",
|
||||
@ -1792,7 +1792,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"60db2b6decbf8571a30717ad0aa54a6e"
|
||||
"7ad9ca8b2d5c0b0ae8bea3c26e5efd1e"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.preservation",
|
||||
@ -1813,7 +1813,7 @@
|
||||
"typing_Catala.LambdaCalculus.uu___is_Error"
|
||||
],
|
||||
0,
|
||||
"5dbaf0f7d6769730448331e005017428"
|
||||
"b885510315594c78804893f5c418efe0"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.preservation",
|
||||
@ -2004,7 +2004,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"b5d4cbedd5a681dfd5dcbd0be26ca0a0"
|
||||
"e55d162bf2923d776361c9b2d0ae781f"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.preservation",
|
||||
@ -2025,7 +2025,7 @@
|
||||
"typing_Catala.LambdaCalculus.uu___is_Error"
|
||||
],
|
||||
0,
|
||||
"100a2d01a40bb6cf7867b44bf94f1fd0"
|
||||
"39edd1d9172620df4366a04073969284"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.preservation",
|
||||
@ -2109,7 +2109,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"207e9c5fd253624a7049b15163e1d5ae"
|
||||
"376eb0108f4a454de4735876e7bc5672"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst_by_identity_is_identity",
|
||||
@ -2211,7 +2211,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"fc26110757db955805ecd1af420837ec"
|
||||
"3c6bfa9970a7c86fc5a56ccd63301fd9"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.subst_by_identity_is_identity",
|
||||
@ -2240,7 +2240,7 @@
|
||||
"typing_Catala.LambdaCalculus.identity_var_to_exp"
|
||||
],
|
||||
0,
|
||||
"8ef12925c8c020c90f37048bc07abd4b"
|
||||
"c43b3c306ac7eb485636fa0fb73ea36a"
|
||||
],
|
||||
[
|
||||
"Catala.LambdaCalculus.typing_empty_can_be_extended",
|
||||
@ -2269,7 +2269,7 @@
|
||||
"typing_Tm_abs_683fecef0f32ab9df689545bd34ec676"
|
||||
],
|
||||
0,
|
||||
"e2d5abc6fdc10316d10362c338d39919"
|
||||
"32b9533f89a7349a06bce6a7b93e1e0f"
|
||||
]
|
||||
]
|
||||
]
|
||||
@ -804,7 +804,7 @@ let step_exceptions_head_value_error
|
||||
acc, 6
|
||||
#pop-options
|
||||
|
||||
#push-options "--fuel 8 --ifuel 1 --z3rlimit 1500"
|
||||
#push-options "--fuel 8 --ifuel 1 --z3rlimit 1000 --quake 10/1"
|
||||
let step_exceptions_head_value_non_error
|
||||
(tau: ty)
|
||||
(tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
|
||||
@ -889,7 +889,7 @@ let step_exceptions_head_value_non_error
|
||||
let init5 = EApp (EAbs tau (ELit (LError ConflictError))) hd tau in
|
||||
assert(step init4 == Some init5);
|
||||
let c_err = ELit (LError ConflictError) in
|
||||
assert(step init5 == Some c_err);
|
||||
assert_norm(step init5 == Some c_err);
|
||||
preservation init0 (TOption tau); preservation init1 (TOption tau);
|
||||
preservation init2 (TOption tau); preservation init3 (TOption tau);
|
||||
preservation init4 (TOption tau); preservation init5 (TOption tau);
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
[
|
||||
"i*™û!d\u000bÅYö\u0001\u0005\u000f\u0017yi",
|
||||
"¤ïXWç;<3B>$\u0003¦«† ug×",
|
||||
[
|
||||
[
|
||||
"Catala.Translation.Helpers.typ_process_exceptions_f",
|
||||
@ -29,7 +29,7 @@
|
||||
"typing_Tm_abs_683fecef0f32ab9df689545bd34ec676"
|
||||
],
|
||||
0,
|
||||
"f4621b9177ba8510238ce22175c67eb6"
|
||||
"143b9302181ab46ccd0e5d15c2e0941f"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.build_default_translation_typing",
|
||||
@ -85,7 +85,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"7a3913649f012fb3c414cf909eafd41c"
|
||||
"33e0affa7261e9067cdbce3ddcddf4e2"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.process_exceptions_untouched_by_subst",
|
||||
@ -161,7 +161,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"3653a502e2c84a85da3971009003c3e6"
|
||||
"5964f8288c016f27611188cfa97624a6"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.take_l_steps",
|
||||
@ -195,7 +195,7 @@
|
||||
"typing_Catala.LambdaCalculus.step", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"5bcda4dd84f1df6ea161b597dcf9de2b"
|
||||
"0ebf747631c6235c501b01bbd431d70f"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.take_l_steps_transitive",
|
||||
@ -205,11 +205,11 @@
|
||||
[
|
||||
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
|
||||
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
|
||||
"refinement_interpretation_Tm_refine_506891b7f1b4542ed9ee2fd85986009e",
|
||||
"refinement_interpretation_Tm_refine_2d1d82d8e7b45c4b826c650f2ee22c70",
|
||||
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
|
||||
],
|
||||
0,
|
||||
"1cfbbe940ee4c4c17f160e56608752f6"
|
||||
"fb0875233a6681c0bf006b58f08a0338"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.take_l_steps_transitive",
|
||||
@ -256,7 +256,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"a9c81e863bb135dcf216d9c8d5c5530d"
|
||||
"efd12261adda6a797b529668c6c40d06"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_lift_commute_non_value",
|
||||
@ -277,7 +277,7 @@
|
||||
"typing_tok_Prims.T@tok"
|
||||
],
|
||||
0,
|
||||
"f566661da55618dcbe2b2ec400423480"
|
||||
"7ca2a4bf2f69213d17aa0a2471759ad4"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.is_stepping_agnostic_lift",
|
||||
@ -291,7 +291,7 @@
|
||||
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
|
||||
],
|
||||
0,
|
||||
"1b0eee8a73a0f9faa887c4b21d775649"
|
||||
"6eb5f22d8aa332b43c7ca8b6f0bbe7c4"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.l_values_dont_step",
|
||||
@ -305,7 +305,7 @@
|
||||
"kinding_Catala.LambdaCalculus.exp@tok"
|
||||
],
|
||||
0,
|
||||
"907ff2bc00df5eef887aaa695cf54c25"
|
||||
"ae5ed7f5f262164fd7b5647f2113bf69"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.l_values_dont_step",
|
||||
@ -366,7 +366,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"9809adc742f341e861abeee3b4d313ec"
|
||||
"f8e5f4b23fe3908178cc11be93bc8620"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.l_values_dont_step",
|
||||
@ -380,7 +380,7 @@
|
||||
"kinding_Catala.LambdaCalculus.exp@tok"
|
||||
],
|
||||
0,
|
||||
"fc5e06d5b11f113a89f5f1f1693e37f6"
|
||||
"d21803a41f4927e9b583c59e18188f3c"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.l_values_dont_step",
|
||||
@ -420,7 +420,7 @@
|
||||
"typing_Catala.LambdaCalculus.is_value_list"
|
||||
],
|
||||
0,
|
||||
"41a331c575f7077efc0abf1a4a0e95b2"
|
||||
"3e25f8d2e0e087deea78daa3f5e63aaa"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.lift_multiple_l_steps",
|
||||
@ -429,7 +429,7 @@
|
||||
1,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"4fbc059703e5ebe675959304f95bf436"
|
||||
"c802c133f612226c1374acdfa8324bc7"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.lift_multiple_l_steps",
|
||||
@ -487,7 +487,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"676edb28716d4ddaf236fff80c7de179"
|
||||
"b11f10cda30c9c61b3501c24f3b8c310"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.if_cond_lift'",
|
||||
@ -517,7 +517,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"d0702c3be1b49defcc01981a79d1e355"
|
||||
"3076e194fecd0a04ba5711e9d7670385"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.if_cond_lift_is_stepping_agnostic",
|
||||
@ -555,7 +555,7 @@
|
||||
"typing_Catala.Translation.Helpers.if_cond_lift_"
|
||||
],
|
||||
0,
|
||||
"13e37e1bf89473a14dee08ad2d3af5ad"
|
||||
"d00dd8bb9ad0636706d568784576c9cc"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.if_cond_lift",
|
||||
@ -567,7 +567,7 @@
|
||||
"equation_Catala.Translation.Helpers.is_stepping_agnostic_lift"
|
||||
],
|
||||
0,
|
||||
"411cef90d7ae00fc18b7d94ad4c947bf"
|
||||
"86174ad51352d43d77b93c4a1db2dc34"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_f_lift'",
|
||||
@ -593,7 +593,7 @@
|
||||
"typing_Catala.LambdaCalculus.empty"
|
||||
],
|
||||
0,
|
||||
"769f3842b338720df48a3c861c21c62d"
|
||||
"e43d70be6d1d2dcd9ddf562c95c009bd"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_f_lift_is_stepping_agnostic",
|
||||
@ -633,7 +633,7 @@
|
||||
"typing_Catala.Translation.Helpers.app_f_lift_"
|
||||
],
|
||||
0,
|
||||
"4bc94208324dbce77be874e2930d0be4"
|
||||
"3a6b677653f08ceebdd2c993e5751e75"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_f_lift",
|
||||
@ -645,7 +645,7 @@
|
||||
"equation_Catala.Translation.Helpers.is_stepping_agnostic_lift"
|
||||
],
|
||||
0,
|
||||
"649aac82175906a9cdf671184ceadaab"
|
||||
"5b62797a4131996b4b308c346d5017e3"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_arg_lift'",
|
||||
@ -676,7 +676,7 @@
|
||||
"typing_Catala.LambdaCalculus.typing"
|
||||
],
|
||||
0,
|
||||
"d4e9f4c8c23dd689d28644180d524f7b"
|
||||
"1eb479df49f9bd44d04668ead937ea1f"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_arg_lift_is_stepping_agnostic",
|
||||
@ -721,7 +721,7 @@
|
||||
"true_interp", "typing_Tm_abs_e963bfe47364f5aa72ea70ed36eb1677"
|
||||
],
|
||||
0,
|
||||
"45a1006bef4bcc60e5d92678ebd96983"
|
||||
"8cda1d30ae820910243655e6f58eae95"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.app_arg_lift",
|
||||
@ -733,7 +733,7 @@
|
||||
"equation_Catala.Translation.Helpers.is_stepping_agnostic_lift"
|
||||
],
|
||||
0,
|
||||
"41c6a2646b2f71dc22f6c57553606171"
|
||||
"e93629647176b0bfbbea807bd5a2aca6"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_head_lift'",
|
||||
@ -857,7 +857,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"35bda88bfa3fb4a50b7db24ff68df574"
|
||||
"df1298f3aadddbdb4d3bb3e586a360c0"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_head_lift_is_stepping_agnostic",
|
||||
@ -910,7 +910,7 @@
|
||||
"true_interp", "typing_Catala.LambdaCalculus.step"
|
||||
],
|
||||
0,
|
||||
"8fbe8b9d58576e2b35cc1e3dd584ee53"
|
||||
"dfb16d5a0e38d3c28889619783287c64"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_head_lift",
|
||||
@ -922,7 +922,7 @@
|
||||
"equation_Catala.Translation.Helpers.is_stepping_agnostic_lift"
|
||||
],
|
||||
0,
|
||||
"b2ad2061e7913cc685915a5c8c2c27ed"
|
||||
"65358c88d6fc4d6ce800f6db696619ec"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_init_lift'",
|
||||
@ -1019,7 +1019,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"86a935521dec34e9e48d641f00b6eabe"
|
||||
"a4528e796a162796e72facc3a4db8aef"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_init_lift_is_stepping_agnostic",
|
||||
@ -1078,7 +1078,7 @@
|
||||
"typing_Catala.LambdaCalculus.typing"
|
||||
],
|
||||
0,
|
||||
"492599b9aabaa6fbfd51e4af80e70e8d"
|
||||
"12130b4ed57f71ea866b34b6388a2fe7"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_init_lift",
|
||||
@ -1090,7 +1090,7 @@
|
||||
"equation_Catala.Translation.Helpers.is_stepping_agnostic_lift"
|
||||
],
|
||||
0,
|
||||
"b91b94fd1fad3ebbae3b18dd0290fc71"
|
||||
"668a4a3f5d9fe58c7d25849b1c8229c3"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.stepping_lemma",
|
||||
@ -1240,7 +1240,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"2d4523fe4dd3278ce6b10025809816e6"
|
||||
"87f7c608e239ce2ca96d28b468c9495a"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.stepping_lemma",
|
||||
@ -1270,7 +1270,7 @@
|
||||
"typing_Catala.LambdaCalculus.typing"
|
||||
],
|
||||
0,
|
||||
"3ed1297ee869d570f516e7c2b3ad888d"
|
||||
"0f8c86cdaa61e9c3aeca800afa856db1"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.lift_multiple_l_steps_exceptions_head",
|
||||
@ -1458,7 +1458,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"981a7d2637cb254881caed2de02cd2a7"
|
||||
"90375b98f78397c3f602a928ae1297a7"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.process_exceptions_applied",
|
||||
@ -1508,7 +1508,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"3849a64803205c5d1a8e60dafc926b96"
|
||||
"1351745ed59b26a0eb38fdd007f6de23"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.process_exceptions_applied_stepped",
|
||||
@ -1601,7 +1601,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"62020cd2d20cc66d0148059df648558c"
|
||||
"81ec8c9b094595193c0d4fa9c9e0f67e"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.process_exceptions_applied_stepping",
|
||||
@ -1740,7 +1740,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"fa2d818f44d65d7ad08f22e6a677e972"
|
||||
"a998c17c4c0d368c49d68724a81a066d"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_head_lift_steps_to_error",
|
||||
@ -1814,7 +1814,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ConflictError@tok"
|
||||
],
|
||||
0,
|
||||
"3cd481ad9d8981e3d18c835a620846a9"
|
||||
"0b5e2044806ac6b3e9099ca056be806a"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exceptions_head_lift_steps_to_error",
|
||||
@ -1846,7 +1846,7 @@
|
||||
"typing_Catala.LambdaCalculus.is_value_list"
|
||||
],
|
||||
0,
|
||||
"8c30f8c2b95b0bfe3334b181da5b60b8"
|
||||
"bd9092a179ef07e37a2a90cc2ba80e77"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.exception_init_lift_conflict_error",
|
||||
@ -1943,7 +1943,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"6ef9ec9f5de17cb2fbcb9cc7febb8b17"
|
||||
"64ddb595dcc317a512102e50ae2df213"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.is_option_value",
|
||||
@ -1972,7 +1972,7 @@
|
||||
"typing_Catala.LambdaCalculus.typing"
|
||||
],
|
||||
0,
|
||||
"74eab4cade48e13ee20bc17393d4f558"
|
||||
"836f2939f9ea1c7599ba6e3347bfa9b5"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value_error",
|
||||
@ -2152,7 +2152,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"ac20c8e8310d0bbbaaeecf755c7ea3a0"
|
||||
"ab38acf3ac1ed6287a545e9e282f06c6"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value_non_error",
|
||||
@ -2342,7 +2342,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"30b7e2c2a9e22714e15d77296a1b524a"
|
||||
"5053a5ebb4dd3639b539de6e78500118"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value",
|
||||
@ -2367,7 +2367,7 @@
|
||||
"typing_Catala.LambdaCalculus.uu___is_ELit"
|
||||
],
|
||||
0,
|
||||
"f999de9dee37dbccaf3667a1c037299d"
|
||||
"2b5d722d46440cfad7471440df32d11a"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result",
|
||||
@ -2376,7 +2376,7 @@
|
||||
2,
|
||||
[ "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq" ],
|
||||
0,
|
||||
"b423bad682a96e9426b1247ad0b5fbe1"
|
||||
"e05f6308cdce42d7b81337591cb1f396"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result",
|
||||
@ -2392,7 +2392,7 @@
|
||||
"refinement_interpretation_Tm_refine_cdbe32eb48421474d9b70d61150eebfe"
|
||||
],
|
||||
0,
|
||||
"3705c047eb2ca8352d94938e68b9424e"
|
||||
"7ce3f98595d41dc52a0c9aad7b178f72"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_head_value_go_through",
|
||||
@ -2434,7 +2434,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.EmptyError@tok"
|
||||
],
|
||||
0,
|
||||
"17e6b22a20160daf0e9d0208217c1ae4"
|
||||
"fd39ad81dcdf53ccdce3c204c9485e57"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_empty_conflict_error",
|
||||
@ -2475,7 +2475,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"cde6bc6eff2b3d58efe321fc0bccf691"
|
||||
"964a7b7a9f0052d73330917f701ab7a8"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_empty_some_acc",
|
||||
@ -2620,7 +2620,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"5ab7e1ff6226204dffb925a44caf5c9e"
|
||||
"8b7eacb9ede89cadf60542b15ca48913"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_empty_none",
|
||||
@ -2748,7 +2748,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"6965fd115a1073ab65424aa723c9725e"
|
||||
"04a3454dcfd63671c86c799d598c0404"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_cons_conflict_error",
|
||||
@ -2861,7 +2861,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"d3ecb1e3753adefb6cd64231fab0c603"
|
||||
"8193afcb622515601d683c0439d272c6"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.Helpers.step_exceptions_general_conflict_error",
|
||||
@ -2958,7 +2958,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"cf84291cad1827ed516563b11f2acc1d"
|
||||
"ae623444f9eab8e4819f002af7dbe5e6"
|
||||
]
|
||||
]
|
||||
]
|
||||
@ -927,7 +927,7 @@ let translation_correctness_exceptions_step
|
||||
take_l_steps ltau le' n2 == Some target_e
|
||||
))
|
||||
=
|
||||
if List.Tot.for_all (fun except -> D.is_value except) dexceptions then begin
|
||||
if List.Tot.for_all D.is_value dexceptions then begin
|
||||
let n1, target_e = translation_correctness_exceptions_empty_count_exception_triggered
|
||||
de dexceptions djust dcons dtau D.AllEmpty L.ENone rec_lemma
|
||||
in
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
[
|
||||
"\u0007<ùÝF9WLû¢É\u0002{\u001a\u000ež",
|
||||
"ˆS$ˆ\u001aú*—z€÷o\u000e\b\u0018U",
|
||||
[
|
||||
[
|
||||
"Catala.Translation.translate_ty",
|
||||
@ -19,7 +19,7 @@
|
||||
"subterm_ordering_Catala.DefaultCalculus.TArrow"
|
||||
],
|
||||
0,
|
||||
"fe152aee929ab96d1f4e1c0cad36b6d6"
|
||||
"360557d7355569320e61b2adde7605e6"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_lit",
|
||||
@ -37,7 +37,7 @@
|
||||
"projection_inverse_BoxBool_proj_0"
|
||||
],
|
||||
0,
|
||||
"913787c8580b9948aaec41dc79f2e2f0"
|
||||
"0afe7fe2131c90eaa171ebab6655eec5"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_exp",
|
||||
@ -62,7 +62,7 @@
|
||||
"subterm_ordering_Catala.DefaultCalculus.EIf"
|
||||
],
|
||||
0,
|
||||
"2dd183cd8badc0a5cd48b9ff2b0bdc38"
|
||||
"8124114d8f8d9dbd4a56447ea032f355"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_exp",
|
||||
@ -77,7 +77,7 @@
|
||||
"projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
|
||||
],
|
||||
0,
|
||||
"fc2e4840d24815038fb1fad1bfaa324c"
|
||||
"036d56652ce12c9e879af3352c69bf63"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_env",
|
||||
@ -104,7 +104,7 @@
|
||||
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e"
|
||||
],
|
||||
0,
|
||||
"87732d3b7d37685498341d246edc8f25"
|
||||
"ff85ef47d0fc8f072456d5adff68e50d"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.extend_translate_commute",
|
||||
@ -169,7 +169,7 @@
|
||||
"typing_Tm_abs_9b0fb98b88819d883b74246421860dc1"
|
||||
],
|
||||
0,
|
||||
"782e3ade22fa74ef54e66ce0f193b560"
|
||||
"32102b72b7afb44efb6ca8b5105cb9a0"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_empty_is_empty",
|
||||
@ -221,7 +221,7 @@
|
||||
"typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af"
|
||||
],
|
||||
0,
|
||||
"46d1f7dffaf78afd794f093c56caed08"
|
||||
"e332260c0ee4edc5db0d8d12c0288537"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_preserves_typ",
|
||||
@ -370,7 +370,7 @@
|
||||
"unit_typing", "well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"0aba12804e76cefbeae73102e62d9d8a"
|
||||
"2d9370359dfb74d1af8151f7b5500357"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_preserves_typ",
|
||||
@ -463,7 +463,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"5f9f4c6443f931a736e31bf0b5069f12"
|
||||
"4275671a1045677481e20dc09e1950bd"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_preserves_typ",
|
||||
@ -529,7 +529,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"7b45c1574645e452b7aecb4f90a1e346"
|
||||
"addaa04a1080e64077badb6aa10e5828"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_preserves_empty_typ",
|
||||
@ -538,7 +538,7 @@
|
||||
1,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"e981997619f0184f871d24774854f8a3"
|
||||
"dd61e0f87bd617c49b32f730eb742bb3"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.substitution_correctness",
|
||||
@ -695,7 +695,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"13a9185a3da7d38d0ef3957ba0ee406f"
|
||||
"d8f05c31d7658f5f0fda367b59f867b5"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.substitution_correctness",
|
||||
@ -750,7 +750,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"655b17574b541ba203b0d3b93c404656"
|
||||
"a33946920d9d7d27686678c74c580c02"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.substitution_correctness",
|
||||
@ -817,7 +817,7 @@
|
||||
"well-founded-ordering-on-nat"
|
||||
],
|
||||
0,
|
||||
"1e61527e8f7980a688897c5a3095bbcf"
|
||||
"a9302094ac7035cfc959aa6d0e93337c"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.exceptions_smaller'",
|
||||
@ -835,7 +835,7 @@
|
||||
"subterm_ordering_Catala.DefaultCalculus.EDefault"
|
||||
],
|
||||
0,
|
||||
"f6a2887a860733e12bb7112c629536bb"
|
||||
"028a207243177f9a44abd6fcba416770"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.exceptions_smaller",
|
||||
@ -849,7 +849,7 @@
|
||||
"data_typing_intro_Catala.DefaultCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"0fe4ef40800e4b557eb7bda0e63072a6"
|
||||
"50d4650a4543754ea85f89247ea46243"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.build_default_translation_typing_source",
|
||||
@ -865,7 +865,7 @@
|
||||
"typing_tok_Catala.DefaultCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"9bdccba35703c6d63fdcade9e6120c59"
|
||||
"f6ccd8f003fa6e2b535763404f3cd7b9"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translate_list_is_value_list",
|
||||
@ -900,7 +900,7 @@
|
||||
"typing_Catala.Translation.translate_exp_list"
|
||||
],
|
||||
0,
|
||||
"c24012fa7cfb99f2e3941f8ca5b6a6e5"
|
||||
"cf2f8206270415943350cdd3318d5dbe"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_value",
|
||||
@ -931,7 +931,7 @@
|
||||
"typing_Catala.Translation.translate_exp"
|
||||
],
|
||||
0,
|
||||
"352446b295861e1cb404f9e50353c313"
|
||||
"587277000f1336e97f0fe48c34013f3e"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.rec_correctness_step_type",
|
||||
@ -943,7 +943,7 @@
|
||||
"refinement_interpretation_Tm_refine_68c49ed091afe9cc5d8c52c1c0db7cda"
|
||||
],
|
||||
0,
|
||||
"e96d217969e01ba93b9d560876f70066"
|
||||
"18831206892d4b6a16a0020e5d9c6280"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_left_to_right_step_head_not_value",
|
||||
@ -1140,7 +1140,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"60793d5f8f2bc4232ff5ba804bb1b9d5"
|
||||
"96af148581157a4df43eae4b3dc08e6e"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.step_exceptions_left_to_right_result_shape",
|
||||
@ -1189,7 +1189,7 @@
|
||||
"typing_tok_Catala.DefaultCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"08f68eddb5fa71c3a45203101e01141c"
|
||||
"28938058dc54118a49383f9f3e529c37"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_left_to_right_step_error",
|
||||
@ -1338,7 +1338,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ConflictError@tok"
|
||||
],
|
||||
0,
|
||||
"da1795257c139be1714f2522fcde91c1"
|
||||
"3df5a1a2d525627eb8cb35e98ba551fb"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_left_to_right_step",
|
||||
@ -1476,7 +1476,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"771d4e2df3fd7eb0e65e74bf993b1433"
|
||||
"9febd186ba2626ced739934e94bc377d"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_left_to_right_step",
|
||||
@ -1675,7 +1675,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"6cf032651d25f4f6810c71e1f47cdf73"
|
||||
"ea8b56f7aa7c67693514b91cef90d6e2"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.dacc_lacc_sync",
|
||||
@ -1696,7 +1696,7 @@
|
||||
"typing_tok_Prims.T@tok"
|
||||
],
|
||||
0,
|
||||
"5f22e53e7ecbc91012857e35116e1d45"
|
||||
"dda8e973711b6298ee1823f745e4fc6f"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.step_exceptions_head_value_source_acc_synced_dacc",
|
||||
@ -1806,7 +1806,7 @@
|
||||
"typing_tok_Catala.DefaultCalculus.Conflict@tok"
|
||||
],
|
||||
0,
|
||||
"ecc4eaedd065d021ce2d5428bb8d03ac"
|
||||
"99e2d23fb7d007b043bb97e08c047feb"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_empty_count_exception_triggered",
|
||||
@ -1860,7 +1860,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ConflictError@tok"
|
||||
],
|
||||
0,
|
||||
"2190435df0d4da2a645ca91fc7742ed5"
|
||||
"9266465e8bf7e5fd699536e0272741ef"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_empty_count_exception_triggered",
|
||||
@ -2022,7 +2022,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TUnit@tok"
|
||||
],
|
||||
0,
|
||||
"df1522d4706864024a8d00c7eca85ff8"
|
||||
"634e0264559a4ba8330f03c9f4af52d0"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_step",
|
||||
@ -2145,7 +2145,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"2cdd7e047a5e4214a2456fd0440fcb66"
|
||||
"96d2c2387fe97c8a556c115be400ce08"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.final_default_subexp",
|
||||
@ -2182,7 +2182,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"b56114963f8b25ed9971c5773dd5e347"
|
||||
"c4473a7d176efe5087ac3176af08a6d7"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.empty_count_non_all_empty_if_one",
|
||||
@ -2194,7 +2194,7 @@
|
||||
"assumption_Catala.DefaultCalculus.empty_count_result__uu___haseq"
|
||||
],
|
||||
0,
|
||||
"63ad766b3f90e37baa25773b028afa4a"
|
||||
"3f0d3393a6b2369c3b681326cf941e67"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.empty_count_non_all_empty_if_one",
|
||||
@ -2239,7 +2239,7 @@
|
||||
"subterm_ordering_Prims.Cons", "unit_inversion", "unit_typing"
|
||||
],
|
||||
0,
|
||||
"e176bb40b6fb79a2760c66430718e827"
|
||||
"9bf2777e239012f19c3ce5a0c75c7ccc"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_no_exceptions_triggered",
|
||||
@ -2281,7 +2281,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok"
|
||||
],
|
||||
0,
|
||||
"9b86c4b4a45545dab9bed6b362bb07df"
|
||||
"11286a0e3a8139510b9d358235f0c387"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_exceptions_no_exceptions_triggered",
|
||||
@ -2446,7 +2446,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.ENone@tok", "unit_typing"
|
||||
],
|
||||
0,
|
||||
"7a0dcf2a69e10e408b9fa0a53561becc"
|
||||
"bb171606d6fc5a7a0c26c6f532462ccb"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.step_exceptions_left_to_right_does_not_depend_on_condition",
|
||||
@ -2455,7 +2455,7 @@
|
||||
1,
|
||||
[ "@query" ],
|
||||
0,
|
||||
"0d22f6bbe33296881e14c45ad63887c5"
|
||||
"444c928361b6f50a4a024c54b75637c5"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.step_exceptions_left_to_right_does_not_depend_on_condition",
|
||||
@ -2521,7 +2521,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"dca094a79a9e5212a618d94e6fa58fb4"
|
||||
"b0c334633118987c80ca9057fa678ade"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.step_exceptions_does_not_depend_on_condition",
|
||||
@ -2582,7 +2582,7 @@
|
||||
"unit_typing"
|
||||
],
|
||||
0,
|
||||
"48b53d6357e001884bccffe8d3c6fdfd"
|
||||
"6709b068a045b44b25333d58db86287e"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_step",
|
||||
@ -2594,7 +2594,7 @@
|
||||
"refinement_interpretation_Tm_refine_68c49ed091afe9cc5d8c52c1c0db7cda"
|
||||
],
|
||||
0,
|
||||
"ac95eb5140dec130aec03a112e29f1b1"
|
||||
"6ea0807d1310617c7ff21bde609cb082"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness_step",
|
||||
@ -2871,7 +2871,7 @@
|
||||
"typing_tok_Catala.LambdaCalculus.TBool@tok"
|
||||
],
|
||||
0,
|
||||
"c5da85525b1756ec8c83db55660e1da0"
|
||||
"703f6c334dccdcb3a59ec25f0a237bee"
|
||||
],
|
||||
[
|
||||
"Catala.Translation.translation_correctness",
|
||||
@ -2892,7 +2892,7 @@
|
||||
"typing_Catala.DefaultCalculus.typing"
|
||||
],
|
||||
0,
|
||||
"194a5a636327c4847725dc82ae551359"
|
||||
"866338bbbb263aefa4b6725d36748041"
|
||||
]
|
||||
]
|
||||
]
|
||||
Loading…
Reference in New Issue
Block a user