From 1c9d2dc696d41649e07acb3eb8f24c23a94d0594 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Wed, 3 Mar 2021 12:23:16 +0100 Subject: [PATCH] Killed the last suspicious admit --- .../Catala.Translation.Helpers.fst | 137 +++++- .../Catala.Translation.Helpers.fst.hints | 398 +++++++++++++++--- doc/formalization/Catala.Translation.fst | 99 ++++- .../Catala.Translation.fst.hints | 304 +++++++++---- 4 files changed, 788 insertions(+), 150 deletions(-) diff --git a/doc/formalization/Catala.Translation.Helpers.fst b/doc/formalization/Catala.Translation.Helpers.fst index 80e46dc2..33b81a95 100644 --- a/doc/formalization/Catala.Translation.Helpers.fst +++ b/doc/formalization/Catala.Translation.Helpers.fst @@ -389,6 +389,78 @@ let exceptions_init_lift Classical.forall_intro (exceptions_init_lift_is_stepping_agnostic tau tl just cons); exceptions_init_lift' tau tl just cons +#push-options "--fuel 10 --ifuel 2 --z3rlimit 80" +let stepping_lemma + (tau: ty) + (acc: typed_l_exp (TOption tau){is_value acc /\ not (is_error acc)}) + (hd: typed_l_exp tau) + : Lemma ( + typ_process_exceptions_f empty tau; + typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau)); + typing_empty_can_be_extended acc (TOption tau) + (extend (extend empty (TOption tau)) tau); + let e_final = + EApp (EAbs (TOption tau) (EMatchOption acc tau (EVar 0) + (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (ELit (LError ConflictError))))))) + (ECatchEmptyError (ESome (EApp (EThunk hd) (ELit LUnit) TUnit)) ENone) (TOption tau) + in + take_l_steps (TOption tau) (EApp + (EApp (process_exceptions_f tau) acc (TOption tau)) (EThunk hd) (TArrow TUnit tau)) 2 == + Some e_final) + = + typ_process_exceptions_f empty tau; + typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau)); + typing_empty_can_be_extended acc (TOption tau) + (extend (extend empty (TOption tau)) tau); + let e0 = + EApp (EApp (process_exceptions_f tau) acc (TOption tau)) (EThunk hd) (TArrow TUnit tau) + in + let e0' = + (EApp (subst (var_to_exp_beta acc) (EAbs (TArrow (TUnit) tau) (EApp (EAbs (TOption tau) + (EMatchOption (EVar 2) tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau (EVar 3) + (EAbs tau (ELit (LError (ConflictError)))))))) + (ECatchEmptyError (ESome (EApp (EVar 0) (ELit (LUnit)) (TUnit))) (ENone)) + (TOption tau)))) (EThunk hd) (TArrow (TUnit) tau)) + in + let e1 = + EApp ( + EAbs (TArrow TUnit tau) ( + EApp (EAbs (TOption tau) ( + EMatchOption acc tau + (EVar 0) + (EAbs tau ( + EMatchOption (EVar 1) tau + acc + (EAbs tau (ELit (LError ConflictError))) + )) + )) + (ECatchEmptyError (ESome (EApp (EVar 0) (ELit LUnit) TUnit)) ENone) + (TOption tau) + )) (EThunk hd) (TArrow TUnit tau) + in + let e2 = + EApp (EAbs (TOption tau) (EMatchOption acc tau (EVar 0) + (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (ELit (LError ConflictError))))))) + (ECatchEmptyError (ESome (EApp (EThunk hd) (ELit LUnit) TUnit)) ENone) (TOption tau) + in + let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] = + well_typed_terms_invariant_by_subst s acc (TOption tau) + in + assert(step e0 == Some e0') by ( + T.norm [delta_only [ + "Catala.Translation.Helpers.process_exceptions_f"; + "Catala.LambdaCalculus.step"; + "Catala.LambdaCalculus.step_app"; + "Catala.LambdaCalculus.is_value"; + ]; zeta; iota]; + T.smt () + ); + assert(e0' == e1); + assert(step e1 == Some e2); + preservation e0 (TOption tau); + preservation e1 (TOption tau); + take_l_steps_transitive (TOption tau) e0 e1 1 1 +#pop-options #push-options "--fuel 7 --ifuel 2 --z3rlimit 80" let lift_multiple_l_steps_exceptions_head @@ -401,7 +473,7 @@ let lift_multiple_l_steps_exceptions_head (hd: typed_l_exp tau) (final_hd: typed_l_exp tau) : Lemma - (requires (take_l_steps tau hd n_hd == Some final_hd /\ is_value acc)) + (requires (take_l_steps tau hd n_hd == Some final_hd /\ is_value acc /\ not (is_error acc))) (ensures ( build_default_translation_typing ((EThunk hd)::tl) acc just cons tau empty; @@ -433,16 +505,8 @@ let lift_multiple_l_steps_exceptions_head )))) (ECatchEmptyError (ESome hd) ENone) (TOption tau) in - let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] = - well_typed_terms_invariant_by_subst s acc (TOption tau) - in - let hd_invariant (s: var_to_exp) : Lemma (subst s hd == hd) - [SMTPat (subst s hd)] = - well_typed_terms_invariant_by_subst s hd tau - in - assume(take_l_steps (TOption tau) init0 2 == Some init2); - (* F* cannot prove these rather trivial substitutions automatically, might have to do it - manually. This proof should use the acc_invariant and hd_invariant above *) + stepping_lemma tau acc hd; + assert(take_l_steps (TOption tau) init0 2 == Some init2); assert(step init2 == Some init3); preservation init2 (TOption tau); take_l_steps_transitive (TOption tau) init0 init2 2 1; @@ -631,9 +695,9 @@ let step_exceptions_head_value_error (cons: (typed_l_exp tau)) (hd_err: err) : Pure (typed_l_exp (TOption tau) & nat) - (requires (is_value acc)) + (requires (is_value acc /\ acc <> ELit (LError EmptyError))) (ensures (fun (new_acc, n) -> - is_value new_acc /\ + is_value new_acc /\ new_acc <> ELit (LError EmptyError) /\ take_l_steps tau (exceptions_head_lift tau tl acc just cons (ELit (LError hd_err))) n == Some (exceptions_init_lift tau tl just cons new_acc) )) @@ -740,7 +804,7 @@ let step_exceptions_head_value_error acc, 6 #pop-options -#push-options "--fuel 8 --ifuel 1 --z3rlimit 150" +#push-options "--fuel 8 --ifuel 1 --z3rlimit 1500" let step_exceptions_head_value_non_error (tau: ty) (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)}) @@ -749,9 +813,9 @@ let step_exceptions_head_value_non_error (cons: (typed_l_exp tau)) (hd: typed_l_exp tau) : Pure (typed_l_exp (TOption tau) & nat) - (requires (is_value hd /\ not (is_error hd) /\ is_value acc)) + (requires (is_value hd /\ not (is_error hd) /\ is_value acc /\ acc <> ELit (LError EmptyError))) (ensures (fun (new_acc, n) -> - is_value new_acc /\ + is_value new_acc /\ new_acc <> ELit (LError EmptyError) /\ take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) n == Some (exceptions_init_lift tau tl just cons new_acc) )) @@ -847,9 +911,9 @@ let step_exceptions_head_value (cons: (typed_l_exp tau)) (hd: (typed_l_exp tau)) : Pure (typed_l_exp (TOption tau) & nat) - (requires (is_value hd /\ is_value acc)) + (requires (is_value hd /\ is_value acc /\ acc <> ELit (LError EmptyError))) (ensures (fun (new_acc, n) -> - is_value new_acc /\ + is_value new_acc /\ new_acc <> ELit (LError EmptyError) /\ take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) n == Some (exceptions_init_lift tau tl just cons new_acc) )) @@ -862,7 +926,7 @@ let step_exceptions_head_value_same_acc_result (tau: ty) (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)}) (tl': list exp{is_value_list tl' /\ typing_list empty tl' (TArrow TUnit tau)}) - (acc: typed_l_exp (TOption tau){is_value acc}) + (acc: typed_l_exp (TOption tau){is_value acc /\ acc <> ELit (LError EmptyError)}) (just: (typed_l_exp TBool)) (cons: (typed_l_exp tau)) (hd: (typed_l_exp tau){is_value hd}) @@ -1005,3 +1069,38 @@ let step_exceptions_cons_conflict_error one_step 1 1; 2 #pop-options + +#push-options "--fuel 4 --ifuel 1 --z3rlimit 40" +let step_exceptions_general_conflict_error + (tau: ty) + (just: (typed_l_exp TBool)) + (cons: (typed_l_exp tau)) + (exceptions: list exp) + : Pure nat + (requires (is_value_list exceptions /\ typing_list empty exceptions (TArrow TUnit tau))) + (ensures (fun n -> + build_default_translation_typing + exceptions (ELit (LError ConflictError)) just cons tau empty; + take_l_steps tau + (build_default_translation exceptions (ELit (LError ConflictError)) just cons tau) n + == Some (ELit (LError ConflictError)))) + = + let l_err: typed_l_exp (TOption tau) = (ELit (LError ConflictError)) in + build_default_translation_typing + exceptions + (ELit (LError ConflictError)) just cons tau empty; + let one_step : typed_l_exp tau = + EMatchOption l_err tau + (EIf just cons (ELit (LError (EmptyError)))) + (EAbs tau (EVar 0)) + in + assert(take_l_steps tau + (build_default_translation exceptions (ELit (LError ConflictError)) just cons tau) 1 == + Some one_step); + let l_err': typed_l_exp tau = (ELit (LError ConflictError)) in + assert(take_l_steps tau one_step 1 == Some l_err'); + take_l_steps_transitive tau + (build_default_translation exceptions (ELit (LError ConflictError)) just cons tau) + one_step 1 1; + 2 +#pop-options diff --git a/doc/formalization/Catala.Translation.Helpers.fst.hints b/doc/formalization/Catala.Translation.Helpers.fst.hints index 01b50413..8b0e589b 100644 --- a/doc/formalization/Catala.Translation.Helpers.fst.hints +++ b/doc/formalization/Catala.Translation.Helpers.fst.hints @@ -1,5 +1,5 @@ [ - "qº#AÉlïD7õû&Pì\u0001ñ", + "i*™û!d\u000bÅYö\u0001\u0005\u000f\u0017yi", [ [ "Catala.Translation.Helpers.typ_process_exceptions_f", @@ -29,7 +29,7 @@ "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676" ], 0, - "2edf83af09d8dcaa2f5c3391c1f3adbc" + "f4621b9177ba8510238ce22175c67eb6" ], [ "Catala.Translation.Helpers.build_default_translation_typing", @@ -85,7 +85,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "3ea949f9ef394472f74f9c5b107b7d6f" + "7a3913649f012fb3c414cf909eafd41c" ], [ "Catala.Translation.Helpers.process_exceptions_untouched_by_subst", @@ -161,7 +161,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "bf7815f067f902608855453b949b0b44" + "3653a502e2c84a85da3971009003c3e6" ], [ "Catala.Translation.Helpers.take_l_steps", @@ -195,7 +195,7 @@ "typing_Catala.LambdaCalculus.step", "well-founded-ordering-on-nat" ], 0, - "68c107cceb12c57800ad3cb4c196ed6e" + "5bcda4dd84f1df6ea161b597dcf9de2b" ], [ "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_2d1d82d8e7b45c4b826c650f2ee22c70", + "refinement_interpretation_Tm_refine_506891b7f1b4542ed9ee2fd85986009e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "0b3d76ed2a16dd06dabf94238d320c16" + "1cfbbe940ee4c4c17f160e56608752f6" ], [ "Catala.Translation.Helpers.take_l_steps_transitive", @@ -256,7 +256,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "8e96e7b0924e81bbf046eb6bbf941539" + "a9c81e863bb135dcf216d9c8d5c5530d" ], [ "Catala.Translation.Helpers.step_lift_commute_non_value", @@ -277,7 +277,7 @@ "typing_tok_Prims.T@tok" ], 0, - "b235cccadbdad66e4074b17f14697888" + "f566661da55618dcbe2b2ec400423480" ], [ "Catala.Translation.Helpers.is_stepping_agnostic_lift", @@ -291,7 +291,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "ad321fa1494a804d279c773f1a6213ce" + "1b0eee8a73a0f9faa887c4b21d775649" ], [ "Catala.Translation.Helpers.l_values_dont_step", @@ -305,7 +305,7 @@ "kinding_Catala.LambdaCalculus.exp@tok" ], 0, - "e413d2c5c92e95efe10551540a296e75" + "907ff2bc00df5eef887aaa695cf54c25" ], [ "Catala.Translation.Helpers.l_values_dont_step", @@ -366,7 +366,7 @@ "well-founded-ordering-on-nat" ], 0, - "8fb45b08d292e4a8166c68ea06b72eb0" + "9809adc742f341e861abeee3b4d313ec" ], [ "Catala.Translation.Helpers.l_values_dont_step", @@ -380,7 +380,7 @@ "kinding_Catala.LambdaCalculus.exp@tok" ], 0, - "a929282455a2affd79c59167186b5759" + "fc5e06d5b11f113a89f5f1f1693e37f6" ], [ "Catala.Translation.Helpers.l_values_dont_step", @@ -420,7 +420,7 @@ "typing_Catala.LambdaCalculus.is_value_list" ], 0, - "b98cf1de997d744d901aa4f0de3f4c9b" + "41a331c575f7077efc0abf1a4a0e95b2" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps", @@ -429,7 +429,7 @@ 1, [ "@query" ], 0, - "f593ecd59533fa9a1c64a1f3522f44da" + "4fbc059703e5ebe675959304f95bf436" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps", @@ -487,7 +487,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "399d201270c934078d58d947d72362a2" + "676edb28716d4ddaf236fff80c7de179" ], [ "Catala.Translation.Helpers.if_cond_lift'", @@ -517,7 +517,7 @@ "typing_tok_Catala.LambdaCalculus.TBool@tok" ], 0, - "215eb5d188544d37d334642ce0e94f45" + "d0702c3be1b49defcc01981a79d1e355" ], [ "Catala.Translation.Helpers.if_cond_lift_is_stepping_agnostic", @@ -555,7 +555,7 @@ "typing_Catala.Translation.Helpers.if_cond_lift_" ], 0, - "b5ca086aa4a55df624f63e4af5df3827" + "13e37e1bf89473a14dee08ad2d3af5ad" ], [ "Catala.Translation.Helpers.if_cond_lift", @@ -567,7 +567,7 @@ "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, - "45f58d68b0b0e9c165e5709171684918" + "411cef90d7ae00fc18b7d94ad4c947bf" ], [ "Catala.Translation.Helpers.app_f_lift'", @@ -593,7 +593,7 @@ "typing_Catala.LambdaCalculus.empty" ], 0, - "9e8a070ff6e2a2882a6fb1e1b787fd9a" + "769f3842b338720df48a3c861c21c62d" ], [ "Catala.Translation.Helpers.app_f_lift_is_stepping_agnostic", @@ -633,7 +633,7 @@ "typing_Catala.Translation.Helpers.app_f_lift_" ], 0, - "f7800b065d4fd5859f56feb788f3f643" + "4bc94208324dbce77be874e2930d0be4" ], [ "Catala.Translation.Helpers.app_f_lift", @@ -645,7 +645,7 @@ "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, - "d467fb34fec1e775431fa01e920944c2" + "649aac82175906a9cdf671184ceadaab" ], [ "Catala.Translation.Helpers.app_arg_lift'", @@ -676,7 +676,7 @@ "typing_Catala.LambdaCalculus.typing" ], 0, - "9952cf20fc2c9b9f275123f5baf43b8c" + "d4e9f4c8c23dd689d28644180d524f7b" ], [ "Catala.Translation.Helpers.app_arg_lift_is_stepping_agnostic", @@ -721,7 +721,7 @@ "true_interp", "typing_Tm_abs_e963bfe47364f5aa72ea70ed36eb1677" ], 0, - "79ca7a99789aec1167cf8741f04fb3b4" + "45a1006bef4bcc60e5d92678ebd96983" ], [ "Catala.Translation.Helpers.app_arg_lift", @@ -733,7 +733,7 @@ "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, - "3af9d20c50d7036b3678b58bc16ac4ae" + "41c6a2646b2f71dc22f6c57553606171" ], [ "Catala.Translation.Helpers.exceptions_head_lift'", @@ -857,7 +857,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "661cff8766567058f1d1c31a49883376" + "35bda88bfa3fb4a50b7db24ff68df574" ], [ "Catala.Translation.Helpers.exceptions_head_lift_is_stepping_agnostic", @@ -910,7 +910,7 @@ "true_interp", "typing_Catala.LambdaCalculus.step" ], 0, - "c172ea30152a33d31c5c48eecd709d12" + "8fbe8b9d58576e2b35cc1e3dd584ee53" ], [ "Catala.Translation.Helpers.exceptions_head_lift", @@ -922,7 +922,7 @@ "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, - "cc4e02c75b1299b6bfce6cff170613fe" + "b2ad2061e7913cc685915a5c8c2c27ed" ], [ "Catala.Translation.Helpers.exceptions_init_lift'", @@ -1019,7 +1019,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "eeb079d2ee0039f145fe30d198b0410a" + "86a935521dec34e9e48d641f00b6eabe" ], [ "Catala.Translation.Helpers.exceptions_init_lift_is_stepping_agnostic", @@ -1078,7 +1078,7 @@ "typing_Catala.LambdaCalculus.typing" ], 0, - "19cbdab4143b930319528feec50e0b0c" + "492599b9aabaa6fbfd51e4af80e70e8d" ], [ "Catala.Translation.Helpers.exceptions_init_lift", @@ -1090,7 +1090,187 @@ "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, - "e2341b547eb2f60d8b69e2b0f2c62a12" + "b91b94fd1fad3ebbae3b18dd0290fc71" + ], + [ + "Catala.Translation.Helpers.stepping_lemma", + 1, + 10, + 2, + [ + "@MaxFuel_assumption", "@MaxIFuel_assumption", + "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", + "@query", + "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", + "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", + "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", + "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", + "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", + "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", + "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", + "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", + "constructor_distinct_Catala.LambdaCalculus.EAbs", + "constructor_distinct_Catala.LambdaCalculus.EApp", + "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", + "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", + "constructor_distinct_Catala.LambdaCalculus.EIf", + "constructor_distinct_Catala.LambdaCalculus.EList", + "constructor_distinct_Catala.LambdaCalculus.ELit", + "constructor_distinct_Catala.LambdaCalculus.EMatchOption", + "constructor_distinct_Catala.LambdaCalculus.ENone", + "constructor_distinct_Catala.LambdaCalculus.ESome", + "constructor_distinct_Catala.LambdaCalculus.EThunk", + "constructor_distinct_Catala.LambdaCalculus.EVar", + "constructor_distinct_Catala.LambdaCalculus.LError", + "constructor_distinct_Catala.LambdaCalculus.LUnit", + "constructor_distinct_Catala.LambdaCalculus.TArrow", + "constructor_distinct_Catala.LambdaCalculus.TOption", + "constructor_distinct_Catala.LambdaCalculus.TUnit", + "constructor_distinct_FStar.Pervasives.Native.None", + "constructor_distinct_FStar.Pervasives.Native.Some", + "constructor_distinct_Tm_unit", + "data_elim_Catala.LambdaCalculus.EAbs", + "data_elim_Catala.LambdaCalculus.EVar", + "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", + "data_typing_intro_Catala.LambdaCalculus.EApp@tok", + "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", + "data_typing_intro_Catala.LambdaCalculus.ELit@tok", + "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", + "data_typing_intro_Catala.LambdaCalculus.ENone@tok", + "data_typing_intro_Catala.LambdaCalculus.ESome@tok", + "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", + "data_typing_intro_Catala.LambdaCalculus.EVar@tok", + "data_typing_intro_Catala.LambdaCalculus.LError@tok", + "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", + "data_typing_intro_Catala.LambdaCalculus.TOption@tok", + "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", + "disc_equation_Catala.LambdaCalculus.EVar", + "disc_equation_FStar.Pervasives.Native.None", + "equality_tok_Catala.LambdaCalculus.ConflictError@tok", + "equality_tok_Catala.LambdaCalculus.ENone@tok", + "equality_tok_Catala.LambdaCalculus.LUnit@tok", + "equality_tok_Catala.LambdaCalculus.TUnit@tok", + "equation_Catala.LambdaCalculus.empty", + "equation_Catala.LambdaCalculus.extend", + "equation_Catala.LambdaCalculus.increment", + "equation_Catala.LambdaCalculus.is_error", + "equation_Catala.LambdaCalculus.is_renaming_prop", + "equation_Catala.LambdaCalculus.var", + "equation_Catala.LambdaCalculus.var_to_exp", + "equation_Catala.LambdaCalculus.var_to_exp_beta", + "equation_Catala.Translation.Helpers.process_exceptions_f", + "equation_Catala.Translation.Helpers.typed_l_exp", + "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", + "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", + "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", + "function_token_typing_Prims.__cache_version_number__", + "int_inversion", "int_typing", + "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", + "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", + "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", + "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", + "kinding_Catala.LambdaCalculus.exp@tok", + "lemma_FStar.FunctionalExtensionality.feq_on_domain", + "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition", + "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", + "primitive_Prims.op_Subtraction", + "proj_equation_FStar.Pervasives.Native.Some_v", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_BoxInt_proj_0", + "projection_inverse_Catala.LambdaCalculus.EAbs_body", + "projection_inverse_Catala.LambdaCalculus.EAbs_vty", + "projection_inverse_Catala.LambdaCalculus.EApp_arg", + "projection_inverse_Catala.LambdaCalculus.EApp_fn", + "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", + "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", + "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", + "projection_inverse_Catala.LambdaCalculus.ELit_l", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", + "projection_inverse_Catala.LambdaCalculus.ESome_s", + "projection_inverse_Catala.LambdaCalculus.EThunk_body", + "projection_inverse_Catala.LambdaCalculus.EVar_v", + "projection_inverse_Catala.LambdaCalculus.LError_err", + "projection_inverse_Catala.LambdaCalculus.TArrow_tin", + "projection_inverse_Catala.LambdaCalculus.TArrow_tout", + "projection_inverse_Catala.LambdaCalculus.TOption_a", + "projection_inverse_FStar.Pervasives.Native.Some_a", + "projection_inverse_FStar.Pervasives.Native.Some_v", + "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", + "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", + "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", + "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", + "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "refinement_interpretation_Tm_refine_d8dd43e05db2d11a4a14435baf3ab736", + "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "subterm_ordering_Catala.LambdaCalculus.EApp", + "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", + "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", + "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "true_interp", "typing_Catala.LambdaCalculus.empty", + "typing_Catala.LambdaCalculus.extend", + "typing_Catala.LambdaCalculus.increment", + "typing_Catala.LambdaCalculus.is_error", + "typing_Catala.LambdaCalculus.is_value", + "typing_Catala.LambdaCalculus.step", + "typing_Catala.LambdaCalculus.typing", + "typing_Catala.LambdaCalculus.var_to_exp_beta", + "typing_Catala.Translation.Helpers.process_exceptions_f", + "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", + "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", + "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", + "typing_tok_Catala.LambdaCalculus.ConflictError@tok", + "typing_tok_Catala.LambdaCalculus.ENone@tok", + "typing_tok_Catala.LambdaCalculus.LUnit@tok", + "typing_tok_Catala.LambdaCalculus.TUnit@tok" + ], + 0, + "2d4523fe4dd3278ce6b10025809816e6" + ], + [ + "Catala.Translation.Helpers.stepping_lemma", + 2, + 10, + 2, + [ + "@MaxFuel_assumption", "@MaxIFuel_assumption", + "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", + "@query", "bool_inversion", + "constructor_distinct_FStar.Pervasives.Native.Some", + "equation_Catala.LambdaCalculus.empty", + "equation_Catala.LambdaCalculus.is_error", + "equation_Catala.Translation.Helpers.typed_l_exp", + "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", + "projection_inverse_FStar.Pervasives.Native.Some_a", + "projection_inverse_FStar.Pervasives.Native.Some_v", + "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "refinement_interpretation_Tm_refine_d8dd43e05db2d11a4a14435baf3ab736", + "typing_Catala.LambdaCalculus.empty", + "typing_Catala.LambdaCalculus.is_error", + "typing_Catala.LambdaCalculus.is_value", + "typing_Catala.LambdaCalculus.typing" + ], + 0, + "3ed1297ee869d570f516e7c2b3ad888d" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps_exceptions_head", @@ -1278,7 +1458,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "882b4cac9a5f424e2873ba6ae8c84c65" + "981a7d2637cb254881caed2de02cd2a7" ], [ "Catala.Translation.Helpers.process_exceptions_applied", @@ -1328,7 +1508,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "88a65dd59e0cfec5c03ab0cf334aebb5" + "3849a64803205c5d1a8e60dafc926b96" ], [ "Catala.Translation.Helpers.process_exceptions_applied_stepped", @@ -1421,7 +1601,7 @@ "typing_tok_Catala.LambdaCalculus.ENone@tok" ], 0, - "4ec1ab3a48a377b7ff87c4799a9fed73" + "62020cd2d20cc66d0148059df648558c" ], [ "Catala.Translation.Helpers.process_exceptions_applied_stepping", @@ -1560,7 +1740,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "5765d7e37939ef7254346bc87bfdbf42" + "fa2d818f44d65d7ad08f22e6a677e972" ], [ "Catala.Translation.Helpers.exceptions_head_lift_steps_to_error", @@ -1634,7 +1814,7 @@ "typing_tok_Catala.LambdaCalculus.ConflictError@tok" ], 0, - "a551d5f1e445aab12d54e8bd54eaa56a" + "3cd481ad9d8981e3d18c835a620846a9" ], [ "Catala.Translation.Helpers.exceptions_head_lift_steps_to_error", @@ -1666,7 +1846,7 @@ "typing_Catala.LambdaCalculus.is_value_list" ], 0, - "c8a2a0a85550ad76442f841213c540c5" + "8c30f8c2b95b0bfe3334b181da5b60b8" ], [ "Catala.Translation.Helpers.exception_init_lift_conflict_error", @@ -1763,7 +1943,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "60968358f53c4a497e35a04523f5271f" + "6ef9ec9f5de17cb2fbcb9cc7febb8b17" ], [ "Catala.Translation.Helpers.is_option_value", @@ -1792,7 +1972,7 @@ "typing_Catala.LambdaCalculus.typing" ], 0, - "1087c146b298ad597834dce5591f8b6f" + "74eab4cade48e13ee20bc17393d4f558" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_error", @@ -1818,7 +1998,8 @@ "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", - "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", + "Prims_pretyping_ae567c2fb75be05905677af440075565", + "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.ConflictError", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", @@ -1971,7 +2152,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "2eed85a8ad7fc2a3f0d9e47a327312f4" + "ac20c8e8310d0bbbaaeecf755c7ea3a0" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_non_error", @@ -2003,7 +2184,9 @@ "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", - "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", + "Prims_pretyping_ae567c2fb75be05905677af440075565", + "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", + "constructor_distinct_Catala.LambdaCalculus.ConflictError", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", @@ -2015,6 +2198,7 @@ "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", + "constructor_distinct_Catala.LambdaCalculus.EmptyError", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TBool", @@ -2045,6 +2229,7 @@ "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", + "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", @@ -2071,6 +2256,7 @@ "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "fuel_guarded_inversion_Catala.LambdaCalculus.err", "fuel_guarded_inversion_Catala.LambdaCalculus.exp", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", @@ -2156,7 +2342,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "132369e46a5baeb4fd10999b9a765746" + "30b7e2c2a9e22714e15d77296a1b524a" ], [ "Catala.Translation.Helpers.step_exceptions_head_value", @@ -2166,8 +2352,8 @@ [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", - "@query", "bool_inversion", - "disc_equation_Catala.LambdaCalculus.ELit", + "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq", + "bool_inversion", "disc_equation_Catala.LambdaCalculus.ELit", "disc_equation_Catala.LambdaCalculus.LError", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.Translation.Helpers.typed_l_exp", @@ -2181,23 +2367,32 @@ "typing_Catala.LambdaCalculus.uu___is_ELit" ], 0, - "0aa106b2c506e7d36e4992ac9bdf892f" + "f999de9dee37dbccaf3667a1c037299d" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result", 1, 7, 2, + [ "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq" ], + 0, + "b423bad682a96e9426b1247ad0b5fbe1" + ], + [ + "Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result", + 2, + 7, + 2, [ "@MaxIFuel_assumption", "@query", "equation_Catala.Translation.Helpers.step_exceptions_head_value", "equation_Catala.Translation.Helpers.step_exceptions_head_value_error", "equation_Catala.Translation.Helpers.step_exceptions_head_value_non_error", - "refinement_interpretation_Tm_refine_c959619bd6335065d0fb704c226b7c3c", + "refinement_interpretation_Tm_refine_490a77d8724dba478516c70d0d037b5b", "refinement_interpretation_Tm_refine_cdbe32eb48421474d9b70d61150eebfe" ], 0, - "e7fbf44dd176673a65431866bf6a9161" + "3705c047eb2ca8352d94938e68b9424e" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_go_through", @@ -2239,7 +2434,7 @@ "typing_tok_Catala.LambdaCalculus.EmptyError@tok" ], 0, - "d06a0e62b0b32544dac04ba67047e57e" + "17e6b22a20160daf0e9d0208217c1ae4" ], [ "Catala.Translation.Helpers.step_exceptions_empty_conflict_error", @@ -2280,7 +2475,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "a3b5a124983e46ae58828d33a2088da9" + "cde6bc6eff2b3d58efe321fc0bccf691" ], [ "Catala.Translation.Helpers.step_exceptions_empty_some_acc", @@ -2425,7 +2620,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "70046712f89393f0a06b6291b148683f" + "5ab7e1ff6226204dffb925a44caf5c9e" ], [ "Catala.Translation.Helpers.step_exceptions_empty_none", @@ -2553,7 +2748,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "1e3445c421fd52ac45e88862bbe439b4" + "6965fd115a1073ab65424aa723c9725e" ], [ "Catala.Translation.Helpers.step_exceptions_cons_conflict_error", @@ -2666,7 +2861,104 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "679f3bb29dcc4b5e21a86fc780598e7c" + "d3ecb1e3753adefb6cd64231fab0c603" + ], + [ + "Catala.Translation.Helpers.step_exceptions_general_conflict_error", + 1, + 4, + 1, + [ + "@MaxFuel_assumption", "@MaxIFuel_assumption", + "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", + "@query", + "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", + "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", + "Prims_pretyping_ae567c2fb75be05905677af440075565", + "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", + "bool_typing", "constructor_distinct_Catala.LambdaCalculus.EAbs", + "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", + "constructor_distinct_Catala.LambdaCalculus.EList", + "constructor_distinct_Catala.LambdaCalculus.ELit", + "constructor_distinct_Catala.LambdaCalculus.EMatchOption", + "constructor_distinct_Catala.LambdaCalculus.LError", + "constructor_distinct_FStar.Pervasives.Native.Some", + "constructor_distinct_Tm_unit", + "data_elim_Catala.LambdaCalculus.EMatchOption", + "data_typing_intro_Catala.LambdaCalculus.EList@tok", + "data_typing_intro_Catala.LambdaCalculus.ELit@tok", + "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", + "data_typing_intro_Catala.LambdaCalculus.ENone@tok", + "data_typing_intro_Catala.LambdaCalculus.LError@tok", + "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", + "data_typing_intro_Catala.LambdaCalculus.TOption@tok", + "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", + "disc_equation_FStar.Pervasives.Native.None", + "equality_tok_Catala.LambdaCalculus.ConflictError@tok", + "equality_tok_Catala.LambdaCalculus.TBool@tok", + "equality_tok_Catala.LambdaCalculus.TUnit@tok", + "equation_Catala.LambdaCalculus.empty", + "equation_Catala.Translation.Helpers.build_default_translation", + "equation_Catala.Translation.Helpers.process_exceptions_f", + "equation_Catala.Translation.Helpers.typed_l_exp", + "equation_Prims.nat", + "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", + "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "fuel_guarded_inversion_FStar.Pervasives.Native.option", + "function_token_typing_Prims.__cache_version_number__", "int_typing", + "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", + "primitive_Prims.op_Subtraction", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_BoxInt_proj_0", + "projection_inverse_Catala.LambdaCalculus.EAbs_body", + "projection_inverse_Catala.LambdaCalculus.EAbs_vty", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", + "projection_inverse_Catala.LambdaCalculus.EList_l", + "projection_inverse_Catala.LambdaCalculus.ELit_l", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", + "projection_inverse_Catala.LambdaCalculus.LError_err", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", + "projection_inverse_FStar.Pervasives.Native.Some_a", + "projection_inverse_FStar.Pervasives.Native.Some_v", + "refinement_interpretation_Tm_refine_1ce4cf8402ca4362b3cefd5b2138fe7c", + "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", + "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", + "subterm_ordering_Catala.LambdaCalculus.EMatchOption", + "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", + "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "typing_Catala.LambdaCalculus.empty", + "typing_Catala.LambdaCalculus.is_value_list", + "typing_Catala.LambdaCalculus.step", + "typing_Catala.LambdaCalculus.typing", + "typing_Catala.Translation.Helpers.build_default_translation", + "typing_Catala.Translation.Helpers.process_exceptions_f", + "typing_tok_Catala.LambdaCalculus.ConflictError@tok", + "typing_tok_Catala.LambdaCalculus.TBool@tok", + "typing_tok_Catala.LambdaCalculus.TUnit@tok" + ], + 0, + "cf84291cad1827ed516563b11f2acc1d" ] ] ] \ No newline at end of file diff --git a/doc/formalization/Catala.Translation.fst b/doc/formalization/Catala.Translation.fst index 20acc7d4..47afef2a 100644 --- a/doc/formalization/Catala.Translation.fst +++ b/doc/formalization/Catala.Translation.fst @@ -309,7 +309,7 @@ let translation_correctness_exceptions_left_to_right_step_head_not_value D.typing_list D.empty dexceptions dtau /\ D.typing D.empty djust D.TBool /\ D.typing D.empty dcons dtau /\ - L.is_value acc /\ + L.is_value acc /\ not (L.is_error acc) /\ Some? (D.step_exceptions_left_to_right de dexceptions djust dcons dtau) /\ (match dexceptions with hd::tl -> not (D.is_value hd) | _ -> False) )) @@ -449,21 +449,20 @@ let step_exceptions_left_to_right_result_shape () #pop-options -#push-options "--fuel 2 --ifuel 1 --z3rlimit 1500" -let rec translation_correctness_exceptions_left_to_right_step +#push-options "--fuel 2 --ifuel 1 --z3rlimit 150" +let translation_correctness_exceptions_left_to_right_step_error (de: D.exp) (dexceptions: list D.exp {dexceptions << de}) (djust: D.exp{djust << de}) (dcons: D.exp{dcons << de}) (dtau: D.ty) (acc: typed_l_exp (L.TOption (translate_ty dtau))) - (rec_lemma: rec_correctness_step_type de) : Pure (nat & typed_l_exp (translate_ty dtau) & nat) (requires ( D.typing_list D.empty dexceptions dtau /\ D.typing D.empty djust D.TBool /\ D.typing D.empty dcons dtau /\ - L.is_value acc /\ + L.is_value acc /\ L.is_error acc /\ acc <> L.ELit (L.LError L.EmptyError) /\ Some? (D.step_exceptions_left_to_right de dexceptions djust dcons dtau) )) (ensures (fun (n1, target_e, n2) -> @@ -508,7 +507,95 @@ let rec translation_correctness_exceptions_left_to_right_step let ljust = translate_exp djust in let lcons = translate_exp dcons in let lexceptions = translate_exp_list dexceptions in - match dexceptions with + let c_err : typed_l_exp ltau = L.ELit (L.LError L.ConflictError) in + let aux () : Lemma (acc == c_err) = + match acc with + | L.ELit (L.LError _) -> () + | _ -> () + in + aux (); + translate_list_is_value_list dexceptions; + let n1 = step_exceptions_general_conflict_error ltau ljust lcons lexceptions in + build_default_translation_typing lexceptions c_err ljust lcons ltau L.empty; + assert(take_l_steps ltau (build_default_translation lexceptions acc ljust lcons ltau) + n1 == Some c_err); + D.preservation_exceptions_left_to_right de dexceptions djust dcons dtau; + translation_preserves_empty_typ de' dtau; + match de' with + | D.ELit D.LConflictError -> n1, c_err, 0 + | D.EDefault dexceptions' djust' dcons' dtau' -> + let lexceptions' = translate_exp_list dexceptions' in + translate_list_is_value_list dexceptions'; + assert(djust' == djust /\ dcons' == dcons /\ dtau' == dtau); + translation_preserves_typ_exceptions D.empty de' dexceptions' dtau'; + build_default_translation_typing lexceptions' acc ljust lcons ltau L.empty; + let n2 = step_exceptions_general_conflict_error ltau ljust lcons lexceptions' in + n1, c_err, n2 +#pop-options + +#push-options "--fuel 2 --ifuel 1 --z3rlimit 1500" +let rec translation_correctness_exceptions_left_to_right_step + (de: D.exp) + (dexceptions: list D.exp {dexceptions << de}) + (djust: D.exp{djust << de}) + (dcons: D.exp{dcons << de}) + (dtau: D.ty) + (acc: typed_l_exp (L.TOption (translate_ty dtau))) + (rec_lemma: rec_correctness_step_type de) + : Pure (nat & typed_l_exp (translate_ty dtau) & nat) + (requires ( + D.typing_list D.empty dexceptions dtau /\ + D.typing D.empty djust D.TBool /\ + D.typing D.empty dcons dtau /\ + L.is_value acc /\ acc <> L.ELit (L.LError L.EmptyError) /\ + Some? (D.step_exceptions_left_to_right de dexceptions djust dcons dtau) + )) + (ensures (fun (n1, target_e, n2) -> + translate_empty_is_empty (); + translation_preserves_typ_exceptions D.empty de dexceptions dtau; + translation_preserves_empty_typ djust D.TBool; + translation_preserves_empty_typ dcons dtau; + let lexceptions = translate_exp_list dexceptions in + let ljust = translate_exp djust in + let lcons = translate_exp dcons in + let Some de' = D.step_exceptions_left_to_right de dexceptions djust dcons dtau in + let ltau = translate_ty dtau in + translation_preserves_typ_exceptions D.empty de dexceptions dtau; + build_default_translation_typing lexceptions acc ljust lcons ltau L.empty; + take_l_steps ltau (build_default_translation lexceptions acc ljust lcons ltau) + n1 == Some target_e /\ + begin + D.preservation_exceptions_left_to_right de dexceptions djust dcons dtau; + translation_preserves_empty_typ de' dtau; + let le' = translate_exp de' in + match de' with + | D.ELit D.LConflictError -> take_l_steps ltau le' n2 == Some target_e + | D.EDefault dexceptions' djust' dcons' dtau' -> + assert(djust' == djust /\ dcons' == dcons /\ dtau' == dtau); + let lexceptions' = translate_exp_list dexceptions' in + take_l_steps ltau (build_default_translation lexceptions' acc ljust lcons ltau) + n2 == Some target_e + end + )) + (decreases dexceptions) + = + let Some de' = D.step_exceptions_left_to_right de dexceptions djust dcons dtau in + let le = translate_exp de in + D.preservation_exceptions_left_to_right de dexceptions djust dcons dtau; + translate_empty_is_empty (); + translation_preserves_typ_exceptions D.empty de dexceptions dtau; + translation_preserves_empty_typ djust D.TBool; + translation_preserves_empty_typ dcons dtau; + translation_preserves_empty_typ de' dtau; + let ltau = translate_ty dtau in + let le' : typed_l_exp ltau = translate_exp de' in + let ljust = translate_exp djust in + let lcons = translate_exp dcons in + let lexceptions = translate_exp_list dexceptions in + if L.is_error acc then + translation_correctness_exceptions_left_to_right_step_error + de dexceptions djust dcons dtau acc + else match dexceptions with | [] -> 0, le, 0 | dhd::dtl -> let ltl = translate_exp_list dtl in diff --git a/doc/formalization/Catala.Translation.fst.hints b/doc/formalization/Catala.Translation.fst.hints index de27d58b..75beaa6a 100644 --- a/doc/formalization/Catala.Translation.fst.hints +++ b/doc/formalization/Catala.Translation.fst.hints @@ -1,5 +1,5 @@ [ - "i÷æZGú„ÈUZe>·£\")", + "\u0007<ùÝF9WLû¢É\u0002{\u001a\u000ež", [ [ "Catala.Translation.translate_ty", @@ -19,7 +19,7 @@ "subterm_ordering_Catala.DefaultCalculus.TArrow" ], 0, - "ac0200308891036630e1069620f66212" + "fe152aee929ab96d1f4e1c0cad36b6d6" ], [ "Catala.Translation.translate_lit", @@ -37,7 +37,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "92c6ccd9fca376fd93da11dc2e62c940" + "913787c8580b9948aaec41dc79f2e2f0" ], [ "Catala.Translation.translate_exp", @@ -62,7 +62,7 @@ "subterm_ordering_Catala.DefaultCalculus.EIf" ], 0, - "e90da622f829804aa1c371333a01a17d" + "2dd183cd8badc0a5cd48b9ff2b0bdc38" ], [ "Catala.Translation.translate_exp", @@ -77,7 +77,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "bfae68a075a56465c0ce319672a99313" + "fc2e4840d24815038fb1fad1bfaa324c" ], [ "Catala.Translation.translate_env", @@ -104,7 +104,7 @@ "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e" ], 0, - "b589434343ea3a8deb250a7b0a9cd977" + "87732d3b7d37685498341d246edc8f25" ], [ "Catala.Translation.extend_translate_commute", @@ -169,7 +169,7 @@ "typing_Tm_abs_9b0fb98b88819d883b74246421860dc1" ], 0, - "1ea650c8e126164774e7b3f1cd578a48" + "782e3ade22fa74ef54e66ce0f193b560" ], [ "Catala.Translation.translate_empty_is_empty", @@ -221,7 +221,7 @@ "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af" ], 0, - "3bb71423ccb6d1603f73d9fde82491f1" + "46d1f7dffaf78afd794f093c56caed08" ], [ "Catala.Translation.translation_preserves_typ", @@ -370,7 +370,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "d80c636e42d120af2b97f169370d0b7c" + "0aba12804e76cefbeae73102e62d9d8a" ], [ "Catala.Translation.translation_preserves_typ", @@ -463,7 +463,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "341c16a0fa7535487d2bf48391e0d5c2" + "5f9f4c6443f931a736e31bf0b5069f12" ], [ "Catala.Translation.translation_preserves_typ", @@ -529,7 +529,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "e7828e36772f5f4c6892889a1fd620e0" + "7b45c1574645e452b7aecb4f90a1e346" ], [ "Catala.Translation.translation_preserves_empty_typ", @@ -538,7 +538,7 @@ 1, [ "@query" ], 0, - "e451495066b5d06d85742e55cb691ac6" + "e981997619f0184f871d24774854f8a3" ], [ "Catala.Translation.substitution_correctness", @@ -695,7 +695,7 @@ "well-founded-ordering-on-nat" ], 0, - "99552507cff59cb62022fe34bfd41fdb" + "13a9185a3da7d38d0ef3957ba0ee406f" ], [ "Catala.Translation.substitution_correctness", @@ -750,7 +750,7 @@ "well-founded-ordering-on-nat" ], 0, - "fa219dce52bc3fd234c69037eceab2e8" + "655b17574b541ba203b0d3b93c404656" ], [ "Catala.Translation.substitution_correctness", @@ -817,7 +817,7 @@ "well-founded-ordering-on-nat" ], 0, - "7ef48464d9725b027649fa3ff0066b53" + "1e61527e8f7980a688897c5a3095bbcf" ], [ "Catala.Translation.exceptions_smaller'", @@ -835,7 +835,7 @@ "subterm_ordering_Catala.DefaultCalculus.EDefault" ], 0, - "40c2e8e0dcb57ef2b6f8dabdc3e99a8c" + "f6a2887a860733e12bb7112c629536bb" ], [ "Catala.Translation.exceptions_smaller", @@ -849,7 +849,7 @@ "data_typing_intro_Catala.DefaultCalculus.TUnit@tok" ], 0, - "0a738e04797f9b04b4e7f57f7d74fcfe" + "0fe4ef40800e4b557eb7bda0e63072a6" ], [ "Catala.Translation.build_default_translation_typing_source", @@ -865,7 +865,7 @@ "typing_tok_Catala.DefaultCalculus.TBool@tok" ], 0, - "e80add6d7fb7da2a97f21e9057522037" + "9bdccba35703c6d63fdcade9e6120c59" ], [ "Catala.Translation.translate_list_is_value_list", @@ -900,7 +900,7 @@ "typing_Catala.Translation.translate_exp_list" ], 0, - "f1e29db3d163b68119a1fa9d5def84ed" + "c24012fa7cfb99f2e3941f8ca5b6a6e5" ], [ "Catala.Translation.translation_correctness_value", @@ -931,7 +931,7 @@ "typing_Catala.Translation.translate_exp" ], 0, - "35ca013fefe27cba8d9184e156c559f8" + "352446b295861e1cb404f9e50353c313" ], [ "Catala.Translation.rec_correctness_step_type", @@ -943,7 +943,7 @@ "refinement_interpretation_Tm_refine_68c49ed091afe9cc5d8c52c1c0db7cda" ], 0, - "3b5fe18c944ac401f058989b5fb5ec7f" + "e96d217969e01ba93b9d560876f70066" ], [ "Catala.Translation.translation_correctness_exceptions_left_to_right_step_head_not_value", @@ -965,6 +965,9 @@ "@fuel_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", "@fuel_correspondence_Catala.Translation.translate_ty.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented", + "@fuel_irrelevance_Catala.DefaultCalculus.step_app.fuel_instrumented", + "@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented", + "@fuel_irrelevance_Catala.DefaultCalculus.step_if.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", @@ -977,24 +980,30 @@ "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", + "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", + "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", + "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", + "bool_typing", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_Catala.DefaultCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", + "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.EThunk", - "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", + "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", + "constructor_distinct_Tm_unit", "data_elim_Catala.DefaultCalculus.EVar", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.EVar", "data_elim_Prims.Cons", @@ -1008,6 +1017,7 @@ "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", + "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "data_typing_intro_Prims.Cons@tok", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.ELit", @@ -1025,11 +1035,13 @@ "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_Catala.LambdaCalculus.empty", + "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Catala.Translation.translate_lit", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", + "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", @@ -1046,7 +1058,10 @@ "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.__cache_version_number__", + "int_inversion", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", + "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", + "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "kinding_Catala.DefaultCalculus.exp@tok", "kinding_Catala.LambdaCalculus.exp@tok", @@ -1069,43 +1084,43 @@ "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", - "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.EVar_v", - "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", - "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", - "refinement_interpretation_Tm_refine_142c9384348c77c01db3330a7dee6fe0", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "refinement_interpretation_Tm_refine_fc7d42468177a14ffb0ff54c0072580d", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", + "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "token_correspondence_Catala.Translation.translate_exp.fuel_instrumented", "token_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", "typing_Catala.DefaultCalculus.empty", + "typing_Catala.DefaultCalculus.is_value", "typing_Catala.DefaultCalculus.step", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.typing_list", "typing_Catala.LambdaCalculus.empty", + "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value_list", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", @@ -1116,6 +1131,8 @@ "typing_Catala.Translation.translate_exp_list", "typing_Catala.Translation.translate_ty", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", + "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", + "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "typing_tok_Catala.DefaultCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", @@ -1123,7 +1140,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "25ba17c0db49510cc15d0d7a6337a22b" + "60793d5f8f2bc4232ff5ba804bb1b9d5" ], [ "Catala.Translation.step_exceptions_left_to_right_result_shape", @@ -1172,7 +1189,156 @@ "typing_tok_Catala.DefaultCalculus.TUnit@tok" ], 0, - "e2c36d4939b2cf0a9c830e2353939d36" + "08f68eddb5fa71c3a45203101e01141c" + ], + [ + "Catala.Translation.translation_correctness_exceptions_left_to_right_step_error", + 1, + 2, + 1, + [ + "@MaxFuel_assumption", "@MaxIFuel_assumption", + "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", + "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", + "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", + "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.translate_exp.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", + "@fuel_correspondence_Catala.Translation.translate_ty.fuel_instrumented", + "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", + "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", + "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", + "@fuel_irrelevance_Catala.Translation.translate_exp.fuel_instrumented", + "@fuel_irrelevance_Catala.Translation.translate_exp_list.fuel_instrumented", + "@query", + "Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9", + "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", + "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", + "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", + "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", + "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", + "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", + "Prims_pretyping_ae567c2fb75be05905677af440075565", + "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", + "bool_typing", + "constructor_distinct_Catala.DefaultCalculus.EDefault", + "constructor_distinct_Catala.DefaultCalculus.ELit", + "constructor_distinct_Catala.DefaultCalculus.LConflictError", + "constructor_distinct_Catala.DefaultCalculus.TBool", + "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", + "constructor_distinct_Catala.LambdaCalculus.ELit", + "constructor_distinct_Catala.LambdaCalculus.EMatchOption", + "constructor_distinct_Catala.LambdaCalculus.LError", + "constructor_distinct_Catala.LambdaCalculus.TArrow", + "constructor_distinct_FStar.Pervasives.Native.None", + "constructor_distinct_FStar.Pervasives.Native.Some", + "data_elim_Catala.DefaultCalculus.EVar", + "data_elim_Catala.LambdaCalculus.EMatchOption", + "data_elim_Catala.LambdaCalculus.EVar", "data_elim_Prims.Cons", + "data_typing_intro_Catala.DefaultCalculus.EDefault@tok", + "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", + "data_typing_intro_Catala.LambdaCalculus.ELit@tok", + "data_typing_intro_Catala.LambdaCalculus.ENone@tok", + "data_typing_intro_Catala.LambdaCalculus.LError@tok", + "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", + "data_typing_intro_Catala.LambdaCalculus.TOption@tok", + "disc_equation_Catala.DefaultCalculus.EDefault", + "disc_equation_Catala.DefaultCalculus.ELit", + "disc_equation_Catala.DefaultCalculus.LConflictError", + "disc_equation_Catala.LambdaCalculus.ELit", + "disc_equation_Catala.LambdaCalculus.LError", + "disc_equation_FStar.Pervasives.Native.Some", + "disc_equation_Prims.Nil", + "equality_tok_Catala.DefaultCalculus.LConflictError@tok", + "equality_tok_Catala.DefaultCalculus.TBool@tok", + "equality_tok_Catala.LambdaCalculus.ConflictError@tok", + "equality_tok_Catala.LambdaCalculus.ENone@tok", + "equality_tok_Catala.LambdaCalculus.EmptyError@tok", + "equality_tok_Catala.LambdaCalculus.TUnit@tok", + "equation_Catala.DefaultCalculus.c_err", + "equation_Catala.DefaultCalculus.empty", + "equation_Catala.DefaultCalculus.var", + "equation_Catala.LambdaCalculus.empty", + "equation_Catala.LambdaCalculus.is_error", + "equation_Catala.LambdaCalculus.var", + "equation_Catala.Translation.Helpers.build_default_translation", + "equation_Catala.Translation.Helpers.step_exceptions_general_conflict_error", + "equation_Catala.Translation.Helpers.typed_l_exp", + "equation_Catala.Translation.translate_lit", + "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", + "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", + "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", + "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", + "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", + "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", + "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", + "equation_with_fuel_Catala.Translation.translate_exp.fuel_instrumented", + "equation_with_fuel_Catala.Translation.translate_ty.fuel_instrumented", + "fuel_guarded_inversion_Catala.DefaultCalculus.exp", + "fuel_guarded_inversion_Catala.DefaultCalculus.ty", + "fuel_guarded_inversion_Catala.LambdaCalculus.err", + "fuel_guarded_inversion_FStar.Pervasives.Native.option", + "fuel_guarded_inversion_Prims.list", + "function_token_typing_Prims.__cache_version_number__", "int_typing", + "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", + "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", + "lemma_FStar.FunctionalExtensionality.feq_on_domain", + "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", + "proj_equation_Catala.DefaultCalculus.ELit_l", + "proj_equation_Catala.LambdaCalculus.ELit_l", + "proj_equation_FStar.Pervasives.Native.Some_v", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_Catala.DefaultCalculus.EDefault_cons", + "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", + "projection_inverse_Catala.DefaultCalculus.EDefault_just", + "projection_inverse_Catala.DefaultCalculus.EDefault_tau", + "projection_inverse_Catala.DefaultCalculus.ELit_l", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", + "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", + "projection_inverse_Catala.LambdaCalculus.EIf_btrue", + "projection_inverse_Catala.LambdaCalculus.EIf_test", + "projection_inverse_Catala.LambdaCalculus.ELit_l", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", + "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", + "projection_inverse_Catala.LambdaCalculus.LError_err", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", + "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", + "projection_inverse_FStar.Pervasives.Native.Some_a", + "projection_inverse_FStar.Pervasives.Native.Some_v", + "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", + "refinement_interpretation_Tm_refine_4b11b40c88c01ef5c4ed447a3187e07a", + "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", + "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "subterm_ordering_Catala.DefaultCalculus.EDefault", + "token_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", + "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", + "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", + "typing_Catala.DefaultCalculus.empty", + "typing_Catala.DefaultCalculus.typing", + "typing_Catala.DefaultCalculus.typing_list", + "typing_Catala.LambdaCalculus.empty", + "typing_Catala.LambdaCalculus.is_error", + "typing_Catala.LambdaCalculus.typing", + "typing_Catala.Translation.Helpers.build_default_translation", + "typing_Catala.Translation.translate_exp", + "typing_Catala.Translation.translate_exp_list", + "typing_Catala.Translation.translate_ty", + "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", + "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", + "typing_tok_Catala.DefaultCalculus.TBool@tok", + "typing_tok_Catala.LambdaCalculus.ConflictError@tok" + ], + 0, + "da1795257c139be1714f2522fcde91c1" ], [ "Catala.Translation.translation_correctness_exceptions_left_to_right_step", @@ -1184,7 +1350,6 @@ "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", - "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.translate_exp.fuel_instrumented", "@fuel_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", @@ -1205,7 +1370,8 @@ "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", - "bool_inversion", "bool_typing", + "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", + "bool_typing", "constructor_distinct_BoxBool", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_Catala.DefaultCalculus.TBool", @@ -1216,9 +1382,11 @@ "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", + "constructor_distinct_Tm_unit", + "data_elim_Catala.DefaultCalculus.EVar", "data_elim_Catala.LambdaCalculus.EIf", "data_elim_Catala.LambdaCalculus.EMatchOption", - "data_elim_Catala.LambdaCalculus.EVar", "data_elim_Prims.Cons", + "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.DefaultCalculus.EDefault@tok", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "data_typing_intro_Catala.LambdaCalculus.EFoldLeft@tok", @@ -1232,6 +1400,7 @@ "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.LConflictError", + "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Nil", "equality_tok_Catala.DefaultCalculus.LConflictError@tok", "equality_tok_Catala.DefaultCalculus.TBool@tok", @@ -1239,7 +1408,6 @@ "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.DefaultCalculus.c_err", "equation_Catala.DefaultCalculus.empty", - "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.var", @@ -1247,22 +1415,21 @@ "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", - "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", - "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", + "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.translate_exp.fuel_instrumented", "equation_with_fuel_Catala.Translation.translate_exp_list.fuel_instrumented", "equation_with_fuel_Catala.Translation.translate_ty.fuel_instrumented", - "fuel_guarded_inversion_Catala.DefaultCalculus.exp", - "fuel_guarded_inversion_Prims.list", "int_inversion", + "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "int_inversion", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", + "primitive_Prims.op_disEquality", "proj_equation_Catala.DefaultCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", @@ -1284,11 +1451,10 @@ "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "refinement_interpretation_Tm_refine_56428814d986116048cacf72e4a86929", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", + "refinement_interpretation_Tm_refine_de3518bb8bba3d415331ba5c41c6c505", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.Translation.translate_exp.fuel_instrumented", "token_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", @@ -1310,7 +1476,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "2ac53fbcd4c4da8e02aeca86f9b1922b" + "771d4e2df3fd7eb0e65e74bf993b1433" ], [ "Catala.Translation.translation_correctness_exceptions_left_to_right_step", @@ -1344,13 +1510,12 @@ "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", - "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", - "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", + "assumption_Catala.LambdaCalculus.exp__uu___haseq", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "binder_x_6aa41574d40712b03e0367a1a3c256b3_4", @@ -1363,18 +1528,17 @@ "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_Catala.DefaultCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.EAbs", + "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.TArrow", - "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", - "constructor_distinct_Tm_unit", "data_elim_Catala.DefaultCalculus.EVar", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.EVar", "data_elim_Prims.Cons", @@ -1402,6 +1566,7 @@ "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_Catala.LambdaCalculus.empty", + "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.exceptions_init_lift", @@ -1424,14 +1589,12 @@ "equation_with_fuel_Catala.Translation.translate_ty.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_Catala.DefaultCalculus.ty", + "fuel_guarded_inversion_Catala.LambdaCalculus.exp", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3", "fuel_guarded_inversion_Prims.list", - "function_token_typing_Prims.__cache_version_number__", - "int_inversion", "int_typing", + "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", - "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", - "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", @@ -1460,7 +1623,6 @@ "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.EThunk_body", - "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", @@ -1468,6 +1630,7 @@ "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", + "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", @@ -1475,9 +1638,8 @@ "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", - "refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf", - "refinement_interpretation_Tm_refine_84f5ba5657c7ac7ede689388f55f2be6", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", + "refinement_interpretation_Tm_refine_94eb2d27391aa916f8507b1c8533dfcf", "refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", @@ -1492,11 +1654,10 @@ "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "token_correspondence_Catala.Translation.translate_exp.fuel_instrumented", "token_correspondence_Catala.Translation.translate_exp_list.fuel_instrumented", - "typing_Catala.DefaultCalculus.__proj__ELit__item__l", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.typing_list", - "typing_Catala.DefaultCalculus.uu___is_LConflictError", + "typing_Catala.DefaultCalculus.uu___is_EDefault", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.is_value_list", @@ -1508,15 +1669,13 @@ "typing_Catala.Translation.translate_exp_list", "typing_Catala.Translation.translate_ty", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", - "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", - "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "typing_tok_Catala.DefaultCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "9ed0017dd14a9473c48494d34a9ad304" + "6cf032651d25f4f6810c71e1f47cdf73" ], [ "Catala.Translation.dacc_lacc_sync", @@ -1537,7 +1696,7 @@ "typing_tok_Prims.T@tok" ], 0, - "4b516f4e6dfeff9d00619bcaf5a0b369" + "5f22e53e7ecbc91012857e35116e1d45" ], [ "Catala.Translation.step_exceptions_head_value_source_acc_synced_dacc", @@ -1647,7 +1806,7 @@ "typing_tok_Catala.DefaultCalculus.Conflict@tok" ], 0, - "85a0f349526a7aa8e9cfd5ebaf88e511" + "ecc4eaedd065d021ce2d5428bb8d03ac" ], [ "Catala.Translation.translation_correctness_exceptions_empty_count_exception_triggered", @@ -1701,7 +1860,7 @@ "typing_tok_Catala.LambdaCalculus.ConflictError@tok" ], 0, - "913b4d12a10ae9c809fd9e6b080e445a" + "2190435df0d4da2a645ca91fc7742ed5" ], [ "Catala.Translation.translation_correctness_exceptions_empty_count_exception_triggered", @@ -1863,7 +2022,7 @@ "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, - "1040940883460539a6c58ba9b3b55cb7" + "df1522d4706864024a8d00c7eca85ff8" ], [ "Catala.Translation.translation_correctness_exceptions_step", @@ -1986,7 +2145,7 @@ "typing_tok_Catala.LambdaCalculus.ENone@tok" ], 0, - "dc387d506622e614032babe728e29dd4" + "2cdd7e047a5e4214a2456fd0440fcb66" ], [ "Catala.Translation.final_default_subexp", @@ -2023,7 +2182,7 @@ "typing_tok_Catala.LambdaCalculus.TBool@tok" ], 0, - "62b2f487af3e0f51398e5bb0d50ea6e8" + "b56114963f8b25ed9971c5773dd5e347" ], [ "Catala.Translation.empty_count_non_all_empty_if_one", @@ -2035,7 +2194,7 @@ "assumption_Catala.DefaultCalculus.empty_count_result__uu___haseq" ], 0, - "a6e9e751cc403ff636d67d24c0310baf" + "63ad766b3f90e37baa25773b028afa4a" ], [ "Catala.Translation.empty_count_non_all_empty_if_one", @@ -2080,7 +2239,7 @@ "subterm_ordering_Prims.Cons", "unit_inversion", "unit_typing" ], 0, - "76fef207300ab57b3d23eabc5c8491c0" + "e176bb40b6fb79a2760c66430718e827" ], [ "Catala.Translation.translation_correctness_exceptions_no_exceptions_triggered", @@ -2112,7 +2271,7 @@ "projection_inverse_Catala.LambdaCalculus.TOption_a", "refinement_interpretation_Tm_refine_0ec5f1a19bb675f9f135275926f522ff", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", - "refinement_interpretation_Tm_refine_7d1af323afac67d3e895a0aca96813cb", + "refinement_interpretation_Tm_refine_c1d042e5b7e4dd74f0617be8e07a5529", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.typing", "typing_Catala.LambdaCalculus.empty", @@ -2122,7 +2281,7 @@ "typing_tok_Catala.LambdaCalculus.ENone@tok" ], 0, - "605d93be824e27c8d337ba89ada3a8fb" + "9b86c4b4a45545dab9bed6b362bb07df" ], [ "Catala.Translation.translation_correctness_exceptions_no_exceptions_triggered", @@ -2206,6 +2365,7 @@ "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", + "equation_Catala.LambdaCalculus.is_error", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", @@ -2286,7 +2446,7 @@ "typing_tok_Catala.LambdaCalculus.ENone@tok", "unit_typing" ], 0, - "f8bf0ad52e9c5891fa094dfd844e966e" + "7a0dcf2a69e10e408b9fa0a53561becc" ], [ "Catala.Translation.step_exceptions_left_to_right_does_not_depend_on_condition", @@ -2295,7 +2455,7 @@ 1, [ "@query" ], 0, - "c079759ff36cdc42073914f180e04f3e" + "0d22f6bbe33296881e14c45ad63887c5" ], [ "Catala.Translation.step_exceptions_left_to_right_does_not_depend_on_condition", @@ -2361,7 +2521,7 @@ "unit_typing" ], 0, - "ba862f715dd9f5a93cf54b0ee40df804" + "dca094a79a9e5212a618d94e6fa58fb4" ], [ "Catala.Translation.step_exceptions_does_not_depend_on_condition", @@ -2422,7 +2582,7 @@ "unit_typing" ], 0, - "55d5505c6cd41c4f6e2ee330df7e0bf9" + "48b53d6357e001884bccffe8d3c6fdfd" ], [ "Catala.Translation.translation_correctness_step", @@ -2434,7 +2594,7 @@ "refinement_interpretation_Tm_refine_68c49ed091afe9cc5d8c52c1c0db7cda" ], 0, - "9907d4a7255c02f37a10fe3d61f495f9" + "ac95eb5140dec130aec03a112e29f1b1" ], [ "Catala.Translation.translation_correctness_step", @@ -2711,7 +2871,7 @@ "typing_tok_Catala.LambdaCalculus.TBool@tok" ], 0, - "9de9f19d669b69fabd09035940ec770b" + "c5da85525b1756ec8c83db55660e1da0" ], [ "Catala.Translation.translation_correctness", @@ -2732,7 +2892,7 @@ "typing_Catala.DefaultCalculus.typing" ], 0, - "aca71dbc1818f049526555f1274ea450" + "194a5a636327c4847725dc82ae551359" ] ] ] \ No newline at end of file