mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-09 22:16:10 +03:00
Restored the proof somewhat
This commit is contained in:
Denis Merigoux
parent
b3fd1c030a
commit
2efdd71866
@ -21,22 +21,17 @@ let translate_lit (l: D.lit) : Tot L.lit = match l with
|
||||
| D.LConflictError -> L.LError L.ConflictError
|
||||
|
||||
let process_exceptions_f (tau: L.ty) : Tot L.exp =
|
||||
let a = 0 in
|
||||
let e = 1 in
|
||||
let e' = 2 in
|
||||
let a' = 3 in
|
||||
let e'' = 4 in
|
||||
L.EAbs (L.Named a) (L.TOption tau) (L.EAbs (L.Named e) (L.TArrow L.TUnit tau) (
|
||||
L.EApp (L.EAbs (L.Named e') (L.TOption tau) (
|
||||
L.EMatchOption (L.EVar a) tau
|
||||
(L.EVar e')
|
||||
(L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau
|
||||
(L.EVar a)
|
||||
(L.EAbs (L.Named e'') tau (L.ELit (L.LError L.ConflictError)))
|
||||
L.EAbs (L.TOption tau) (L.EAbs (L.TArrow L.TUnit tau) (
|
||||
L.EApp (L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption (L.EVar 2) tau
|
||||
(L.EVar 0)
|
||||
(L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau
|
||||
(L.EVar 3)
|
||||
(L.EAbs tau (L.ELit (L.LError L.ConflictError)))
|
||||
))
|
||||
))
|
||||
(L.ECatchEmptyError (L.ESome (L.EApp (L.EVar e) (L.ELit L.LUnit) L.TUnit)) L.ENone)
|
||||
(L.ECatchEmptyError (L.ESome (L.EApp (L.EVar 0) (L.ELit L.LUnit) L.TUnit)) L.ENone)
|
||||
(L.TOption tau)
|
||||
))
|
||||
|
||||
@ -65,13 +60,13 @@ let build_default_translation
|
||||
(L.EIf
|
||||
just cons
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau (L.EVar 0))
|
||||
(L.EAbs tau (L.EVar 0))
|
||||
|
||||
let rec translate_exp (e: D.exp) : Tot L.exp = match e with
|
||||
| D.EVar x -> L.EVar x
|
||||
| D.EApp e1 e2 tau_arg ->
|
||||
L.EApp (translate_exp e1) (translate_exp e2) (translate_ty tau_arg)
|
||||
| D.EAbs x ty body -> L.EAbs (L.Named x) (translate_ty ty) (translate_exp body)
|
||||
| D.EAbs ty body -> L.EAbs (translate_ty ty) (translate_exp body)
|
||||
| D.ELit l -> L.ELit (translate_lit l)
|
||||
| D.EIf e1 e2 e3 -> L.EIf
|
||||
(translate_exp e1)
|
||||
@ -87,25 +82,25 @@ let rec translate_exp (e: D.exp) : Tot L.exp = match e with
|
||||
and translate_exp_list (l: list D.exp) : Tot (list L.exp) =
|
||||
match l with
|
||||
| [] -> []
|
||||
| hd::tl -> (L.EAbs L.Silent L.TUnit (translate_exp hd))::(translate_exp_list tl)
|
||||
| hd::tl -> (L.EAbs L.TUnit (L.subst L.increment (translate_exp hd)))::(translate_exp_list tl)
|
||||
|
||||
let translate_env (g: D.env) : Tot L.env =
|
||||
FunctionalExtensionality.on_dom L.var_name
|
||||
FunctionalExtensionality.on_dom L.var
|
||||
(fun v -> match g v with None -> None | Some t -> Some (translate_ty t))
|
||||
|
||||
(*** Typing preservation *)
|
||||
|
||||
(**** Helpers and lemmas *)
|
||||
|
||||
let extend_translate_commute (g: D.env) (x: D.var) (tau: D.ty)
|
||||
: Lemma (L.extend (translate_env g) x (translate_ty tau) == translate_env (D.extend g x tau))
|
||||
let extend_translate_commute (g: D.env) (tau: D.ty)
|
||||
: Lemma (L.extend (translate_env g) (translate_ty tau) == translate_env (D.extend g tau))
|
||||
=
|
||||
FunctionalExtensionality.extensionality L.var_name (fun _ -> option L.ty)
|
||||
(L.extend (translate_env g) x (translate_ty tau))
|
||||
(translate_env (D.extend g x tau))
|
||||
FunctionalExtensionality.extensionality L.var (fun _ -> option L.ty)
|
||||
(L.extend (translate_env g) (translate_ty tau))
|
||||
(translate_env (D.extend g tau))
|
||||
|
||||
let translate_empty_is_empty () : Lemma (translate_env D.empty == L.empty) =
|
||||
FunctionalExtensionality.extensionality L.var_name (fun _ -> option L.ty)
|
||||
FunctionalExtensionality.extensionality L.var (fun _ -> option L.ty)
|
||||
(translate_env D.empty)
|
||||
L.empty
|
||||
|
||||
@ -142,12 +137,12 @@ let rec translation_preserves_typ (g: D.env) (e: D.exp) (tau: D.ty) : Lemma
|
||||
| D.EApp e1 e2 tau_arg ->
|
||||
translation_preserves_typ g e1 (D.TArrow tau_arg tau);
|
||||
translation_preserves_typ g e2 tau_arg
|
||||
| D.EAbs x tau_arg body -> begin
|
||||
| D.EAbs tau_arg body -> begin
|
||||
match tau with
|
||||
| D.TArrow tau_in tau_out ->
|
||||
if tau_in = tau_arg then begin
|
||||
translation_preserves_typ (D.extend g x tau_in) body tau_out;
|
||||
extend_translate_commute g x tau_in
|
||||
translation_preserves_typ (D.extend g tau_in) body tau_out;
|
||||
extend_translate_commute g tau_in
|
||||
end else ()
|
||||
| _ -> ()
|
||||
end
|
||||
@ -173,7 +168,7 @@ let rec translation_preserves_typ (g: D.env) (e: D.exp) (tau: D.ty) : Lemma
|
||||
(translate_exp just)
|
||||
(translate_exp cons)
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau' (L.EVar 0))
|
||||
(L.EAbs tau' (L.EVar 0))
|
||||
in
|
||||
let open FStar.Tactics in
|
||||
assert(L.typing (translate_env g) result_exp tau') by begin
|
||||
@ -206,7 +201,9 @@ and translation_preserves_typ_exceptions
|
||||
let thunked_tau' = L.TArrow L.TUnit tau' in
|
||||
assert(L.typing_list g' tl' thunked_tau');
|
||||
assert(L.typing g' hd' tau');
|
||||
assert(L.typing g' (L.EAbs L.Silent L.TUnit hd') thunked_tau')
|
||||
assert(L.typing g' hd' tau');
|
||||
L.substitution_preserves_typing g' hd' tau' L.increment (L.extend g' L.TUnit) (fun x -> ());
|
||||
assert(L.typing g' (L.EAbs L.TUnit (L.subst L.increment hd')) thunked_tau')
|
||||
#pop-options
|
||||
|
||||
let translation_preserves_empty_typ (e: D.exp) (tau: D.ty) : Lemma
|
||||
@ -283,7 +280,7 @@ let rec l_values_dont_step (e: L.exp) : Lemma
|
||||
(decreases %[e; 1])
|
||||
=
|
||||
match e with
|
||||
| L.EAbs _ _ _ -> ()
|
||||
| L.EAbs _ _ -> ()
|
||||
| L.ELit _ -> ()
|
||||
| L.ENone -> ()
|
||||
| L.EList [] -> ()
|
||||
@ -329,48 +326,162 @@ let rec lift_multiple_l_steps
|
||||
|
||||
|
||||
#push-options "--fuel 9 --ifuel 0"
|
||||
let process_exceptions_untouched_by_subst (x: L.var_name) (e: L.exp) (tau: L.ty) : Lemma
|
||||
(L.subst x e (process_exceptions_f tau) == process_exceptions_f tau)
|
||||
let process_exceptions_untouched_by_subst (s: L.var_to_exp) (tau: L.ty) : Lemma
|
||||
(L.subst s (process_exceptions_f tau) == process_exceptions_f tau)
|
||||
=
|
||||
()
|
||||
#pop-options
|
||||
|
||||
let translate_var_to_exp (s: D.var_to_exp) : Tot L.var_to_exp = fun x -> translate_exp (s x)
|
||||
|
||||
let double_increment : L.var_to_exp = fun y -> L.EVar (y + 2)
|
||||
|
||||
let subst_abs_increment (x: L.var) =
|
||||
if x = 0 then L.EVar 0 else L.EVar (x + 1)
|
||||
|
||||
let dual_substitution_commutation_weakened
|
||||
(s : L.var_to_exp{s 0 == L.EVar 0})
|
||||
(e: L.exp)
|
||||
: Lemma (L.subst subst_abs_increment (L.subst s e) ==
|
||||
L.subst (L.subst_abs s) (L.subst subst_abs_increment e))
|
||||
=
|
||||
admit() // TODO
|
||||
|
||||
let substitution_commutation_bonanza
|
||||
(s: L.var_to_exp)
|
||||
(e: L.exp)
|
||||
: Lemma (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) e) ==
|
||||
L.subst (L.subst_abs (L.subst_abs s)) (L.subst (L.subst_abs L.increment) e))
|
||||
=
|
||||
let aux (x: L.var) : Lemma ((L.subst_abs L.increment) x == subst_abs_increment x) = () in
|
||||
Classical.forall_intro aux;
|
||||
dual_substitution_commutation_weakened (L.subst_abs s) e
|
||||
|
||||
#push-options "--fuel 3 --ifuel 1 --z3rlimit 40"
|
||||
let rec substitution_correctness_for_exception_thunking
|
||||
(s: L.var_to_exp)
|
||||
(e: L.exp)
|
||||
: Lemma (
|
||||
(L.EAbs L.TUnit (L.subst L.increment (L.subst s e))) ==
|
||||
(L.subst s (L.EAbs L.TUnit (L.subst L.increment e)))
|
||||
)
|
||||
=
|
||||
match e with
|
||||
| L.EVar _ -> ()
|
||||
| L.EAbs t body ->
|
||||
// Top to down
|
||||
assert(L.subst s e == L.EAbs t (L.subst (L.subst_abs s) body));
|
||||
assert(L.subst L.increment (L.subst s e) ==
|
||||
L.EAbs t (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) body)));
|
||||
assert(L.EAbs L.TUnit (L.subst L.increment (L.subst s e)) ==
|
||||
L.EAbs L.TUnit
|
||||
(L.EAbs t (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) body))));
|
||||
// Down to top
|
||||
assert(L.subst L.increment e == L.EAbs t (L.subst (L.subst_abs L.increment) body));
|
||||
assert(L.EAbs L.TUnit (L.subst L.increment e) ==
|
||||
L.EAbs L.TUnit (L.EAbs t (L.subst (L.subst_abs L.increment) body)));
|
||||
assert(L.subst s (L.EAbs L.TUnit (L.subst L.increment e)) ==
|
||||
L.EAbs L.TUnit
|
||||
(L.subst (L.subst_abs s) (L.EAbs t (L.subst (L.subst_abs L.increment) body))));
|
||||
assert(L.subst s (L.EAbs L.TUnit (L.subst L.increment e)) ==
|
||||
L.EAbs L.TUnit
|
||||
(L.EAbs t
|
||||
(L.subst (L.subst_abs (L.subst_abs s)) (L.subst (L.subst_abs L.increment) body))));
|
||||
substitution_commutation_bonanza s body
|
||||
| L.EApp e1 e2 _ ->
|
||||
substitution_correctness_for_exception_thunking s e1;
|
||||
substitution_correctness_for_exception_thunking s e2
|
||||
| L.ELit _ -> ()
|
||||
| L.EIf e1 e2 e3 ->
|
||||
substitution_correctness_for_exception_thunking s e1;
|
||||
substitution_correctness_for_exception_thunking s e2;
|
||||
substitution_correctness_for_exception_thunking s e3
|
||||
| L.ESome e1 -> substitution_correctness_for_exception_thunking s e1
|
||||
| L.ENone -> ()
|
||||
| L.EMatchOption e1 _ e2 e3 ->
|
||||
substitution_correctness_for_exception_thunking s e1;
|
||||
substitution_correctness_for_exception_thunking s e2;
|
||||
substitution_correctness_for_exception_thunking s e3
|
||||
| L.ECatchEmptyError e1 e2 ->
|
||||
substitution_correctness_for_exception_thunking s e1;
|
||||
substitution_correctness_for_exception_thunking s e2
|
||||
| L.EFoldLeft e1 e2 _ e3 _ ->
|
||||
substitution_correctness_for_exception_thunking s e1;
|
||||
substitution_correctness_for_exception_thunking s e2;
|
||||
substitution_correctness_for_exception_thunking s e3
|
||||
| L.EList l ->
|
||||
substitution_correctness_for_exception_thunking_list s l
|
||||
and substitution_correctness_for_exception_thunking_list
|
||||
(s: L.var_to_exp)
|
||||
(l: list L.exp)
|
||||
: Lemma (
|
||||
(L.EAbs L.TUnit (L.subst L.increment (L.subst s (L.EList l)))) ==
|
||||
(L.subst s (L.EAbs L.TUnit (L.subst L.increment (L.EList l))))
|
||||
)
|
||||
=
|
||||
match l with
|
||||
| [] -> ()
|
||||
| hd::tl ->
|
||||
substitution_correctness_for_exception_thunking s hd;
|
||||
substitution_correctness_for_exception_thunking_list s tl
|
||||
#pop-options
|
||||
|
||||
#push-options "--fuel 3 --ifuel 1 --z3rlimit 50"
|
||||
let rec substitution_correctness (x: D.var) (e_x e: D.exp)
|
||||
let rec substitution_correctness (s: D.var_to_exp) (e: D.exp)
|
||||
: Lemma (ensures (
|
||||
translate_exp (D.subst x e_x e) == L.subst x (translate_exp e_x) (translate_exp e)))
|
||||
(decreases %[e; 1])
|
||||
translate_exp (D.subst s e) ==
|
||||
L.subst (translate_var_to_exp s) (translate_exp e)))
|
||||
(decreases %[D.is_var_size e; D.is_renaming_size s; 1; e])
|
||||
=
|
||||
match e with
|
||||
| D.EVar y -> ()
|
||||
| D.ELit _ -> ()
|
||||
| D.EIf e1 e2 e3 ->
|
||||
substitution_correctness x e_x e1;
|
||||
substitution_correctness x e_x e2;
|
||||
substitution_correctness x e_x e3
|
||||
| D.EAbs _ _ body ->
|
||||
substitution_correctness x e_x body
|
||||
substitution_correctness s e1;
|
||||
substitution_correctness s e2;
|
||||
substitution_correctness s e3
|
||||
| D.EAbs _ body ->
|
||||
substitution_correctness (D.subst_abs s) body;
|
||||
translate_var_to_exp_abs_commute s
|
||||
| D.EApp e1 e2 _ ->
|
||||
substitution_correctness x e_x e1;
|
||||
substitution_correctness x e_x e2
|
||||
substitution_correctness s e1;
|
||||
substitution_correctness s e2
|
||||
| D.EDefault exceptions just cons tau ->
|
||||
substitution_correctness x e_x just;
|
||||
substitution_correctness x e_x cons;
|
||||
substitution_correctness_list x e_x e exceptions;
|
||||
process_exceptions_untouched_by_subst x (translate_exp e_x) (translate_ty tau)
|
||||
and substitution_correctness_list (x: D.var) (e_x: D.exp) (e: D.exp) (l: list D.exp{l << e})
|
||||
substitution_correctness s just;
|
||||
substitution_correctness s cons;
|
||||
substitution_correctness_list s exceptions;
|
||||
process_exceptions_untouched_by_subst (translate_var_to_exp s) (translate_ty tau)
|
||||
and substitution_correctness_list (s: D.var_to_exp) (l: list D.exp)
|
||||
: Lemma (ensures (
|
||||
translate_exp_list (D.subst_list x e_x l) ==
|
||||
L.subst_list x (translate_exp e_x) (translate_exp_list l)))
|
||||
(decreases %[e; 0; l])
|
||||
translate_exp_list (D.subst_list s l) ==
|
||||
L.subst_list (translate_var_to_exp s) (translate_exp_list l)))
|
||||
(decreases %[1; D.is_renaming_size s; 1; l])
|
||||
=
|
||||
match l with
|
||||
| [] -> ()
|
||||
| hd::tl ->
|
||||
substitution_correctness x e_x hd;
|
||||
substitution_correctness_list x e_x e tl
|
||||
let s' = translate_var_to_exp s in
|
||||
substitution_correctness_list s tl;
|
||||
substitution_correctness s hd;
|
||||
substitution_correctness_for_exception_thunking s' (translate_exp hd)
|
||||
and translate_var_to_exp_abs_commute (s: D.var_to_exp)
|
||||
: Lemma
|
||||
(ensures (
|
||||
FunctionalExtensionality.feq
|
||||
(translate_var_to_exp (D.subst_abs s))
|
||||
(L.subst_abs (translate_var_to_exp s))))
|
||||
(decreases %[1; D.is_renaming_size s; 0])
|
||||
=
|
||||
let s1 = translate_var_to_exp (D.subst_abs s) in
|
||||
let s2 = L.subst_abs (translate_var_to_exp s) in
|
||||
let aux (x: L.var) : Lemma (s1 x == s2 x) =
|
||||
if x = 0 then () else
|
||||
substitution_correctness D.increment (s (x - 1))
|
||||
in
|
||||
Classical.forall_intro aux
|
||||
#pop-options
|
||||
|
||||
|
||||
let exceptions_smaller'
|
||||
(e: D.exp{match e with D.EDefault _ _ _ _ -> True | _ -> False})
|
||||
: Lemma(let D.EDefault exc just cons tau = e in
|
||||
@ -529,23 +640,20 @@ let exceptions_head_lift'
|
||||
(cons: (typed_l_exp tau))
|
||||
: stepping_context tau tau
|
||||
=
|
||||
let e' = 2 in
|
||||
let a' = 3 in
|
||||
let e'' = 4 in
|
||||
fun (hd: typed_l_exp tau) ->
|
||||
typ_process_exceptions_f L.empty tau;
|
||||
L.typing_empty_can_be_extended acc (L.TOption tau) e' (L.TOption tau);
|
||||
L.typing_empty_can_be_extended acc (L.TOption tau) (L.TOption tau);
|
||||
L.EMatchOption
|
||||
(L.EFoldLeft
|
||||
(process_exceptions_f tau)
|
||||
(L.EApp
|
||||
(L.EAbs (L.Named e') (L.TOption tau) (
|
||||
(L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption acc tau
|
||||
(L.EVar e')
|
||||
(L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau
|
||||
(L.EVar 0)
|
||||
(L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau
|
||||
L.ENone
|
||||
(L.EAbs (L.Named e'') tau (L.ELit (L.LError L.ConflictError)))
|
||||
(L.EAbs tau (L.ELit (L.LError L.ConflictError)))
|
||||
))
|
||||
))
|
||||
(L.ECatchEmptyError
|
||||
@ -558,7 +666,7 @@ let exceptions_head_lift'
|
||||
(L.EIf
|
||||
just cons
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau (L.EVar 0))
|
||||
(L.EAbs tau (L.EVar 0))
|
||||
#pop-options
|
||||
|
||||
let exceptions_head_lift_is_stepping_agnostic
|
||||
@ -608,7 +716,7 @@ let exceptions_init_lift'
|
||||
(L.EIf
|
||||
just cons
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau (L.EVar 0))
|
||||
(L.EAbs tau (L.EVar 0))
|
||||
#pop-options
|
||||
|
||||
let exceptions_init_lift_is_stepping_agnostic
|
||||
@ -647,9 +755,11 @@ let process_exceptions_applied
|
||||
: Tot (typed_l_exp (L.TOption tau))
|
||||
=
|
||||
typ_process_exceptions_f L.empty tau;
|
||||
L.typing_empty_can_be_extended hd tau L.TUnit;
|
||||
L.EApp
|
||||
(L.EApp (process_exceptions_f tau) acc (L.TOption tau))
|
||||
(L.EAbs L.Silent L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
(L.EApp (process_exceptions_f tau) acc (L.TOption tau))
|
||||
(L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
|
||||
|
||||
#push-options "--fuel 7 --ifuel 2"
|
||||
let process_exceptions_applied_stepped
|
||||
@ -661,10 +771,10 @@ let process_exceptions_applied_stepped
|
||||
let e' = 2 in
|
||||
let a' = 3 in
|
||||
let e'' = 4 in
|
||||
L.typing_empty_can_be_extended acc (L.TOption tau) e' (L.TOption tau);
|
||||
L.EApp (L.EAbs (L.Named e') (L.TOption tau) (
|
||||
L.EMatchOption acc tau (L.EVar e') (L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau L.ENone (L.EAbs (L.Named e'') tau
|
||||
L.typing_empty_can_be_extended acc (L.TOption tau) (L.TOption tau);
|
||||
L.EApp (L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption acc tau (L.EVar 0) (L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau L.ENone (L.EAbs tau
|
||||
(L.ELit (L.LError L.ConflictError))
|
||||
)
|
||||
))))
|
||||
@ -685,39 +795,40 @@ let process_exceptions_applied_stepping
|
||||
let e'' = 4 in
|
||||
let e1 : L.exp =
|
||||
L.EApp
|
||||
(L.EAbs (L.Named e) (L.TArrow L.TUnit tau) (
|
||||
L.EApp (L.EAbs (L.Named e') (L.TOption tau) (
|
||||
(L.EAbs (L.TArrow L.TUnit tau) (
|
||||
L.EApp (L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption acc tau
|
||||
(L.EVar e')
|
||||
(L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau
|
||||
(L.EVar 0)
|
||||
(L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau
|
||||
acc
|
||||
(L.EAbs (L.Named e'') tau (L.ELit (L.LError L.ConflictError)))
|
||||
(L.EAbs tau (L.ELit (L.LError L.ConflictError)))
|
||||
))
|
||||
))
|
||||
(L.ECatchEmptyError (L.ESome (L.EApp (L.EVar e) (L.ELit L.LUnit) L.TUnit)) L.ENone)
|
||||
(L.TOption tau)
|
||||
)
|
||||
)
|
||||
(L.EAbs L.Silent L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
(L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
in
|
||||
let e2 =
|
||||
L.EApp (L.EAbs (L.Named e') (L.TOption tau) (
|
||||
L.EApp (L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption acc tau
|
||||
(L.EVar e')
|
||||
(L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau
|
||||
(L.EVar 0)
|
||||
(L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau
|
||||
acc
|
||||
(L.EAbs (L.Named e'') tau (L.ELit (L.LError L.ConflictError)))
|
||||
(L.EAbs tau (L.ELit (L.LError L.ConflictError)))
|
||||
))
|
||||
))
|
||||
(L.ECatchEmptyError (L.ESome (L.EApp (L.EAbs L.Silent L.TUnit hd) (L.ELit L.LUnit) L.TUnit)) L.ENone)
|
||||
(L.ECatchEmptyError (L.ESome (L.EApp (L.EAbs L.TUnit hd) (L.ELit L.LUnit) L.TUnit)) L.ENone)
|
||||
(L.TOption tau)
|
||||
|
||||
in
|
||||
assert(L.step (process_exceptions_applied tau acc hd) == Some e1);
|
||||
assume(L.step (process_exceptions_applied tau acc hd) == Some e1);
|
||||
assume(L.step e1 == Some e2);
|
||||
admit()
|
||||
#pop-options
|
||||
|
||||
#push-options "--fuel 7 --ifuel 2 --z3rlimit 50"
|
||||
let lift_multiple_l_steps_exceptions_head
|
||||
@ -732,20 +843,22 @@ let lift_multiple_l_steps_exceptions_head
|
||||
: Lemma
|
||||
(requires (take_l_steps tau hd n_hd == Some final_hd /\ L.is_value acc))
|
||||
(ensures (
|
||||
L.typing_empty_can_be_extended hd tau L.TUnit;
|
||||
build_default_translation_typing
|
||||
((L.EAbs L.Silent L.TUnit hd)::tl) acc just cons tau L.empty;
|
||||
((L.EAbs L.TUnit hd)::tl) acc just cons tau L.empty;
|
||||
take_l_steps tau
|
||||
(build_default_translation ((L.EAbs L.Silent L.TUnit hd)::tl) acc just cons tau)
|
||||
(build_default_translation ((L.EAbs L.TUnit hd)::tl) acc just cons tau)
|
||||
(n_hd + 4) ==
|
||||
Some (exceptions_head_lift tau tl acc just cons final_hd)))
|
||||
=
|
||||
build_default_translation_typing ((L.EAbs L.Silent L.TUnit hd)::tl) acc just cons tau L.empty;
|
||||
L.typing_empty_can_be_extended hd tau L.TUnit;
|
||||
build_default_translation_typing ((L.EAbs L.TUnit hd)::tl) acc just cons tau L.empty;
|
||||
let e' = 2 in
|
||||
let a' = 3 in
|
||||
let e'' = 4 in
|
||||
let init_stepped = L.EApp (L.EAbs (L.Named e') (L.TOption tau) (
|
||||
L.EMatchOption acc tau (L.EVar e') (L.EAbs (L.Named a') tau (
|
||||
L.EMatchOption (L.EVar e') tau L.ENone (L.EAbs (L.Named e'') tau
|
||||
let init_stepped = L.EApp (L.EAbs (L.TOption tau) (
|
||||
L.EMatchOption acc tau (L.EVar 0) (L.EAbs tau (
|
||||
L.EMatchOption (L.EVar 1) tau L.ENone (L.EAbs tau
|
||||
(L.ELit (L.LError L.ConflictError))
|
||||
)
|
||||
))))
|
||||
@ -753,15 +866,16 @@ let lift_multiple_l_steps_exceptions_head
|
||||
in
|
||||
let init = L.EApp
|
||||
(L.EApp (process_exceptions_f tau) acc (L.TOption tau))
|
||||
(L.EAbs L.Silent L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
(L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)
|
||||
in
|
||||
let open FStar.Tactics in
|
||||
admit();
|
||||
assert(take_l_steps (L.TOption tau) init 3 == Some init_stepped) by begin
|
||||
compute ()
|
||||
end;
|
||||
admit();
|
||||
let default_translation: typed_l_exp tau =
|
||||
build_default_translation ((L.EAbs L.Silent L.TUnit hd)::tl) acc just cons tau
|
||||
build_default_translation ((L.EAbs L.TUnit hd)::tl) acc just cons tau
|
||||
in
|
||||
let default_translation_stepped = L.EMatchOption
|
||||
(L.EFoldLeft
|
||||
@ -772,12 +886,12 @@ let lift_multiple_l_steps_exceptions_head
|
||||
(L.EIf
|
||||
just cons
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau (L.EVar 0))
|
||||
(L.EAbs tau (L.EVar 0))
|
||||
in
|
||||
assert(take_l_steps tau default_translation 1 == Some default_translation_stepped);
|
||||
assert(default_translation_stepped == exceptions_init_lift tau tl just cons
|
||||
(L.EApp (L.EApp (process_exceptions_f tau) L.ENone (L.TOption tau))
|
||||
(L.EAbs L.Silent L.TUnit hd) (L.TArrow L.TUnit tau)));
|
||||
(L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)));
|
||||
lift_multiple_l_steps (L.TOption tau) tau init init_stepped 3
|
||||
(exceptions_init_lift tau tl just cons);
|
||||
assert(take_l_steps tau default_translation_stepped 3 ==
|
||||
@ -799,10 +913,10 @@ let exceptions_head_lift_steps_to_error
|
||||
(just: (typed_l_exp L.TBool))
|
||||
(cons: (typed_l_exp tau))
|
||||
: Lemma (take_l_steps tau
|
||||
(exceptions_head_lift tau tl just cons (L.ELit (L.LError L.ConflictError))) 5 ==
|
||||
(exceptions_head_lift tau tl L.ENone just cons (L.ELit (L.LError L.ConflictError))) 5 ==
|
||||
Some (L.ELit (L.LError L.ConflictError)))
|
||||
=
|
||||
let e = exceptions_head_lift tau tl just cons (L.ELit (L.LError L.ConflictError)) in
|
||||
let e = exceptions_head_lift tau tl L.ENone just cons (L.ELit (L.LError L.ConflictError)) in
|
||||
let e_plus_3 : typed_l_exp tau =
|
||||
exceptions_init_lift tau tl just cons (L.ELit (L.LError L.ConflictError))
|
||||
in
|
||||
@ -817,7 +931,7 @@ let exceptions_head_lift_steps_to_error
|
||||
(L.EIf
|
||||
just cons
|
||||
(L.ELit (L.LError L.EmptyError)))
|
||||
(L.EAbs (L.Named 0) tau (L.EVar 0))
|
||||
(L.EAbs tau (L.EVar 0))
|
||||
in
|
||||
assert(L.step e_plus_3 == Some e_plus_4) by begin
|
||||
compute ();
|
||||
@ -840,13 +954,12 @@ let step_exceptions_head_value
|
||||
: Pure (typed_l_exp (L.TOption tau) & nat)
|
||||
(requires (True))
|
||||
(ensures (fun (new_acc, n) ->
|
||||
take_l_steps tau (exceptions_head_lift tau tl just cons hd) n ==
|
||||
take_l_steps tau (exceptions_head_lift tau tl L.ENone just cons hd) n ==
|
||||
Some (exceptions_init_lift tau tl just cons new_acc)
|
||||
))
|
||||
=
|
||||
admit()
|
||||
|
||||
|
||||
(**** Main theorems *)
|
||||
|
||||
let translation_correctness_value (e: D.exp) : Lemma
|
||||
@ -902,7 +1015,8 @@ let rec translation_correctness_exceptions_left_to_right_step
|
||||
D.preservation de dtau;
|
||||
let ltau = translate_ty dtau in
|
||||
translation_preserves_empty_typ de' dtau;
|
||||
take_l_steps ltau (build_default_translation lexceptions ljust lcons ltau)
|
||||
admit();
|
||||
take_l_steps ltau (build_default_translation lcurrent L.ENone ljust lcons ltau)
|
||||
n1 == Some target_e /\
|
||||
take_l_steps ltau le' n2 == Some target_e
|
||||
))
|
||||
@ -1052,7 +1166,7 @@ let translation_correctness_exceptions_step
|
||||
D.preservation de dtau;
|
||||
let ltau = translate_ty dtau in
|
||||
translation_preserves_empty_typ de' dtau;
|
||||
take_l_steps ltau (build_default_translation lexceptions ljust lcons ltau) n1
|
||||
take_l_steps ltau (build_default_translation lexceptions L.ENone ljust lcons ltau) n1
|
||||
== Some target_e /\
|
||||
take_l_steps ltau le' n2 == Some target_e
|
||||
))
|
||||
@ -1061,7 +1175,7 @@ let translation_correctness_exceptions_step
|
||||
admit()
|
||||
else
|
||||
translation_correctness_exceptions_left_to_right_step
|
||||
de dexceptions djust dcons dtau rec_lemma
|
||||
de dexceptions dexceptions djust dcons dtau rec_lemma
|
||||
|
||||
#pop-options
|
||||
|
||||
@ -1089,7 +1203,7 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty)
|
||||
match de with
|
||||
| D.EVar _ -> 0, le, 0
|
||||
| D.ELit _ -> 0, le, 0
|
||||
| D.EAbs _ _ _ -> 0, le, 0
|
||||
| D.EAbs _ _ -> 0, le, 0
|
||||
| D.EIf de1 de2 de3 ->
|
||||
let le1 = translate_exp de1 in
|
||||
let le2 = translate_exp de2 in
|
||||
@ -1143,8 +1257,8 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty)
|
||||
match de1, de2 with
|
||||
| _, D.ELit D.LConflictError -> 1, le', 0
|
||||
| _, D.ELit D.LEmptyError -> 1, le', 0
|
||||
| D.EAbs dx1 dt1 dbody, _ ->
|
||||
substitution_correctness dx1 de2 dbody;
|
||||
| D.EAbs dt1 dbody, _ ->
|
||||
substitution_correctness (D.var_to_exp_beta de2) dbody;
|
||||
1, le', 0
|
||||
end
|
||||
end
|
||||
|
||||
Loading…
Reference in New Issue
Block a user