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

Fix list stepping semantics in both default and lambda calculus

Browse Source
This commit is contained in:
Denis Merigoux 2021-02-17 16:24:19 +01:00
parent f5caa5d5fb
commit c2dc8db6ac
3 changed files with 19 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
doc/formalization/Catala.DefaultCalculus.fst
View File

@ -121,12 +121,18 @@ and step_exceptions_left_to_right
: Tot (option exp) (decreases %[ e; 2; exceptions ]) =
match exceptions with
| [] -> None
| [hd] -> begin
match step hd with
| Some (ELit LConflictError) -> Some c_err (* D-ContextConflictError *)
| Some hd' -> Some (EDefault ([hd']) just cons tau) (* D-Context *)
| _ -> None
end
| hd :: tl ->
if is_value hd
then
match step_exceptions_left_to_right e tl just cons tau with
| Some (ELit LConflictError) -> Some c_err (* D-ContextConflictError *)
| Some (EDefault tl' just cons tau) -> Some (EDefault (hd :: tl') just cons tau) (* D-Context *)
| Some (EDefault tl' _ _ _) -> Some (EDefault (hd :: tl') just cons tau) (* D-Context *)
| _ -> None
else
match step hd with

9
doc/formalization/Catala.LambdaCalculus.fst
View File

@ -157,6 +157,13 @@ and step_list
: Tot (list_step_result) (decreases %[ e; 3; l ]) =
match l with
| [] -> Bad
| [hd] -> begin
if is_value hd then Bad else
match step hd with
| None -> Bad
| Some (ELit (LError err)) -> Error (ELit (LError err))
| Some hd' -> Good ([hd'])
end
| hd::tl -> begin
if is_value hd then
match step_list e tl with
@ -747,7 +754,7 @@ and preservation_list
))
(decreases %[ l ]) =
match l with
| [hd] -> if is_value hd then () else preservation hd tau
| [hd] -> begin if is_value hd then () else preservation hd tau end
| hd :: tl ->
if is_value hd then begin
typing_conserved_by_list_reduction empty l tau;

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

@ -787,19 +787,19 @@ let translation_correctness_exceptions_left_to_right_step
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
match dexceptions with
| [] -> 0, le, 0
| dhd::dtl ->
let ljust = translate_exp djust in
let lcons = translate_exp dcons in
let ltl = translate_exp_list dtl in
let lhd = translate_exp dhd in
let lexceptions = translate_exp_list dexceptions in
if D.is_value dhd then begin
match D.step_exceptions_left_to_right de dtl djust dcons dtau with
| Some (D.ELit D.LConflictError) -> admit()
| Some (D.EDefault dtl' djust' dcons' dtau') ->
assume(djust = djust' /\ dcons = dcons' /\ dtau = dtau');
assert(djust' == djust /\ dcons' == dcons /\ dtau' == dtau);
admit()
end else begin
match D.step dhd with