CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-09 22:16:10 +03:00
Code Issues Projects Releases Wiki Activity

Yet another proof case

Browse Source
This commit is contained in:
Denis Merigoux 2021-02-21 19:17:51 +01:00
parent 038c5b3e07
commit 80f2dffe1d
2 changed files with 53 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
doc/formalization/Catala.Translation.Helpers.fst
View File

@ -675,3 +675,39 @@ let step_exceptions_empty_some_acc
take_l_steps_transitive tau (build_default_translation [] (ESome acc) just cons tau) two_step 2 1;
3
#pop-options
#push-options "--fuel 4 --ifuel 1 --z3rlimit 40"
let step_exceptions_cons_conflict_error
(tau: ty)
(just: (typed_l_exp TBool))
(cons: (typed_l_exp tau))
(hd: typed_l_exp tau)
(tl: list exp)
: Pure nat
(requires (is_value hd /\ is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)))
(ensures (fun n ->
build_default_translation_typing
((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau empty;
take_l_steps tau
(build_default_translation ((EThunk hd)::tl) (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
((EThunk hd)::tl)
(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 ((EThunk hd)::tl) (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 ((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau)
one_step 1 1;
2
#pop-options

19
doc/formalization/Catala.Translation.fst
View File

@ -641,7 +641,7 @@ let dacc_lacc_sync
| D.Conflict, L.ELit (L.LError L.ConflictError) -> True
| _ -> False
#push-options "--fuel 2 --ifuel 1 --z3rlimit 70"
#push-options "--fuel 2 --ifuel 2 --z3rlimit 70"
let rec translation_correctness_exceptions_empty_count_exception_triggered
(de: D.exp)
(dexceptions: list D.exp {dexceptions << de})
@ -707,7 +707,22 @@ let rec translation_correctness_exceptions_empty_count_exception_triggered
let n = step_exceptions_empty_some_acc ltau ljust lcons lacc_inner in
n, lacc_inner
end
| dhd::dtl -> admit()
| dhd::dtl -> begin
FStar.List.Tot.Base.for_all_mem (fun except -> D.is_value except) dexceptions;
translate_empty_is_empty ();
translation_preserves_typ_exceptions D.empty de dexceptions dtau;
translate_list_is_value_list dtl;
assert(D.is_value dhd);
translation_correctness_value dhd;
let ltl = translate_exp_list dtl in
let lhd : typed_l_exp ltau = translate_exp dhd in
match lacc with
| L.ELit (L.LError L.ConflictError) ->
let n_err = step_exceptions_cons_conflict_error ltau ljust lcons lhd ltl in
n_err, l_err
| L.ESome lacc_inner -> admit()
| L.ENone -> admit()
end
#pop-options
#push-options "--fuel 2 --ifuel 1 --z3rlimit 50"