diff --git a/_CoqProject b/_CoqProject index 0359382..943359b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -32,6 +32,7 @@ theories/program_logic.v theories/effects/store.v theories/effects/callcc.v theories/effects/io_tape.v +theories/effects/exceptions.v theories/effects/delim.v theories/lib/pairs.v @@ -57,6 +58,10 @@ theories/examples/input_lang/interp.v theories/examples/input_lang/logpred.v theories/examples/input_lang/logrel.v +theories/examples/except_lang/lang.v +theories/examples/except_lang/interp.v +theories/examples/except_lang/typing.v + theories/examples/affine_lang/lang.v theories/examples/affine_lang/logrel1.v theories/examples/affine_lang/logrel2.v diff --git a/theories/effects/exceptions.v b/theories/effects/exceptions.v new file mode 100644 index 0000000..bcc46b0 --- /dev/null +++ b/theories/effects/exceptions.v @@ -0,0 +1,443 @@ +From gitrees Require Import gitree. +From iris.algebra Require Import list. + +Module Type ExcSig. + Parameter E : Set. + Parameter eq_dec_E : EqDecision E. + Parameter countable_E : @Countable E eq_dec_E. +End ExcSig. + +Module Exc (Errors : ExcSig). + Import Errors. + + Structure exc := Exc { value : E }. + + #[global] Instance eq_dec : EqDecision exc. + intros [x] [y]. + destruct (eq_dec_E x y) as [<-|HDiff]. + - left. reflexivity. + - right. intros Heq. injection Heq as <-. apply HDiff. reflexivity. + Defined. + + #[global] Instance countable_exc : Countable exc. + Proof. + refine (Build_Countable _ _ ?[encode] ?[decode] _). + [encode] : { intros [e]. + exact ((@encode _ _ countable_E) e). + } + [decode] : { intros p. + destruct ((@decode _ _ countable_E) p) as [e|]. + - exact (Some (Exc e)). + - exact None. + } + intros [e]. + simpl. + by rewrite (@decode_encode _ _ countable_E). + Defined. + + Canonical Structure excO := leibnizO exc. + Definition excOF := constOF exc. + + (** State functor, we keep track of the list of error handlers from most recently + registered to least recently registered along with the error they each + handle and the continuation present at the time of registration, this is + so that when raising an error we can erase only the context between the + raising of the error and the registering of the handler **) + Definition stateF : oFunctor := listOF (excOF * (▶ ∙ -n> ▶ ∙ ) * (▶ ∙ -n> ▶ ∙)). + + (** Register an exception handler for an exception type **) + Program Definition regE : opInterp := + {| + Ins := (excOF * (▶ ∙ -n> ▶ ∙ ) * (▶ ∙)); + Outs := (▶ ∙) + |}. + + Program Definition popE : opInterp := + {| + Ins := excOF; + Outs := unitO + |}. + + (** Throw an exception, empty Outs because we don't use the continuation **) + Program Definition throwE : opInterp := + {| + Ins := (excOF * (▶ ∙)); + Outs := Empty_setO; + |}. + + Definition exceptE := @[regE;popE;throwE]. + + (** Register a handler : Push the handler and current context on the stack **) + Definition reify_reg X `{Cofe X} : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ). + + #[export] Instance reify_reg_ne X `{Cofe X}: NonExpansive (reify_reg X : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X)) + ). + Proof. + solve_proper_prepare. + destruct x as [[[[? ?] ?] ?] ?]. + destruct y as [[[[? ?] ?] ?] ?]. + repeat rewrite e pair_dist in H0. + destruct H0 as [[[[? ?] ?] ?] ?]. + repeat f_equiv; done. + Qed. + + (** Unregister a handler : Remove the topmost handler, restore the ambient context from when it was registered **) + Definition reify_pop X `{Cofe X} : excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(err, σ, k), match σ with + | [] => None + | (err', h, k')::σ' => + (if (eq_dec err err') + then Some (k' (k ()), σ') + else None) end. + + #[export] Instance reify_pop_ne X `{Cofe X}: NonExpansive (reify_pop X : + excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X))). + Proof. + intros n [[e σ] k] [[e' σ'] k'] Hequiv. + rewrite pair_dist in Hequiv. + destruct Hequiv as [[He Hσ] Hk]. + simpl in *. + destruct σ' as [|p σ']. + - rewrite nil_dist_eq in Hσ. + rewrite Hσ. done. + - apply cons_dist_eq in Hσ. + destruct Hσ as (x & l' & Hx & Hl' & ->). + destruct x as [[xerr xh] xc]. + destruct p as [[perr ph] pc]. + repeat rewrite pair_dist in Hx. + destruct Hx as [[Herr Hh] Hc]. + rewrite He Herr. + destruct (eq_dec e' perr). + + rewrite Hl'. repeat f_equiv; done. + + reflexivity. + Qed. + + Fixpoint _cut_when {A : ofe} (p : (A -n> boolO)) (l : listO A) : optionO (A * listO A)%type := + match l with + | [] => None + | x::t => if p x then Some (x, t) else _cut_when p t + end. + + Program Definition cut_when {A} : (A -n> boolO) -n> (listO A) -n> optionO (A * listO A)%type + := λne p l, _cut_when p l. + Next Obligation. + Proof. + solve_proper_prepare. + generalize dependent y. + induction x as [|h t IH]. + - intros y Hy. + symmetry in Hy. + apply nil_dist_eq in Hy. + subst. + done. + - intros y Hy. + symmetry in Hy. + apply cons_dist_eq in Hy. + destruct Hy as (h' & t' & Hh & Ht & ->). + destruct (p h) eqn:Hp; + rewrite -Hh in Hp; + rewrite Hp. + + repeat f_equiv; done. + + apply IH. done. + Qed. + + Next Obligation. + Proof. + solve_proper_prepare. + induction x0 as [|h t IH]. + - done. + - simpl. + destruct H with h. + destruct (x h). + + done. + + apply IH. + Qed. + + Lemma cut_when_first_occ {A} : ∀ (p : A -n> bool) (l pre post : list A) (a : A), + l = pre ++ a::post → + p a = true → + Forall (λ x, p x = false) pre → + cut_when p l = Some (a, post). + Proof. + intros p l pre post a Hl Ha Hpre. + generalize dependent l. + induction pre as [|h t]. + - intros l ->. + simpl. + rewrite Ha. + exact eq_refl. + - intros l ->. + inversion Hpre as [|?? Hh Ht]. + simpl. + rewrite Hh. + apply IHt; done. + Qed. + + Program Definition aux {X} (err : exc) : (excO * (laterO X -n> laterO X) * (laterO X -n> laterO X))%type -n> boolO := + λne '(err', _, _), if eq_dec err err' then true else false. + Next Obligation. + Proof. + intros. + simpl. + intros [[e k] p] [[e' k'] p'] Heq. + rewrite pair_dist in Heq. + destruct Heq as [[He Hk] Hp]. + simpl in *. + rewrite He. + reflexivity. + Qed. + + (** Raise an error : Find the most recent handler handling this error and remove all handlers registered after it from the stack then invoke the handler inside the context from when it was registered **) + Definition reify_throw X `{Cofe X} : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(x, σ, _), let (err,v) := x in + match cut_when (aux err) σ with + | None => None + | Some (_, h, k, σ') => Some (k (h v), σ') + end. + + #[export] Instance reify_throw_ne X `{Cofe X} : NonExpansive (reify_throw X : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X))). + Proof. + solve_proper_prepare. + destruct x as [[[e v] σ] k]. + destruct y as [[[e' v'] σ'] k']. + destruct H0 as [[[He Hv] Hσ] Hk]. + simpl in *. + generalize dependent σ'. + induction σ as [|[[err hand] kont] σ]. + - intros. + symmetry in Hσ. + apply nil_dist_eq in Hσ. + rewrite Hσ. + done. + - intros. + symmetry in Hσ. + apply cons_dist_eq in Hσ. + destruct Hσ as ([[err' hand'] kont'] & σ'' & [[Herr Hhand] Hkont] & Hσ'' & ->). + simpl in *. + destruct (eq_dec e err) eqn:HEq. + + rewrite Herr -He. rewrite HEq. repeat f_equiv; done. + + symmetry in Hσ''. + setoid_replace (if eq_dec e' err' then true else false) with (if eq_dec e err then true else false). + * rewrite HEq. + exact (IHσ σ'' Hσ''). + * rewrite Herr -He. reflexivity. + Qed. + + + Canonical Structure reify_exc : sReifier CtxDep. + Proof. + simple refine {| sReifier_ops := exceptE; + sReifier_state := stateF + |}. + intros X HX op. + destruct op as [|[|[|[]]]]. + - simple refine (OfeMor (reify_reg X)). + - simple refine (OfeMor (reify_pop X)). + - simple refine (OfeMor (reify_throw X)). + Defined. + + Section constructors. + Context {Eff : opsInterp} {A} `{!Cofe A}. + Context {subEff0 : subEff exceptE Eff}. + Context {SubOfe0 : SubOfe unitO A}. + Notation IT := (IT Eff A). + Notation ITV := (ITV Eff A). + + + Program Definition _REG : excO -n> (laterO IT -n> laterO IT) -n> laterO IT -n> IT := + λne e h b, Vis (E:=Eff) (subEff_opid (inl ())) (subEff_ins (F:=exceptE) (op:=(inl ())) (e,h,b)) ((λne x, x) ◎ (subEff_outs (F:=exceptE) (op:=(inl ())))^-1). + Solve All Obligations with solve_proper. + + + Program Definition _POP : excO -n> IT := + λne e, Vis (E:=Eff) (subEff_opid (inr (inl ()))) (subEff_ins (F:=exceptE) (op:=(inr(inl ()))) e) ((λne _, Next $ Ret ()) ◎ (subEff_outs (F:=exceptE) (op:=(inr(inl ()))))^-1). + Solve All Obligations with solve_proper. + + Program Definition CATCH : excO -n> (laterO IT -n> laterO IT) -n> IT -n> IT := + λne err h b, + _REG err h (Next $ get_val + (λne res, get_val + (λne _, res) + (_POP err) + ) b + ). + Next Obligation. + Proof. + solve_proper_prepare. + done. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; solve_proper. + Qed. + + Program Definition _THROW : excO -n> laterO IT -n> IT := + λne e v, + Vis (E:=Eff) (subEff_opid (inr (inr (inl ())))) (subEff_ins (F:=exceptE) (op:=(inr(inr(inl ())))) (e,v)) (λne x, Empty_setO_rec _ ((subEff_outs (F:=exceptE) (op:=(inr(inr(inl ())))))^-1 x)). + Next Obligation. + solve_proper_prepare. + destruct ((subEff_outs ^-1) x). + Qed. + Solve All Obligations with solve_proper. + + Program Definition THROW : excO -n> IT -n> IT := + λne e x, get_val (λne res, _THROW e (Next res)) x. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + Proof. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + + End constructors. + + Section weakestpre. + + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {subR : subReifier reify_exc rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context {SubOfe0 : SubOfe unitO R}. + Context {SubOfe1 : SubOfe natO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ, !stateG rs R Σ}. + Notation iProp := (iProp Σ). + + Lemma wp_reg (σ : stateF ♯ IT) (err : excO) (h : laterO IT -n> laterO IT) (k : IT -n> IT) {Hk : IT_hom k} b β s Φ : + b ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate ((err, h, laterO_map k) :: σ) -∗ WP@{rs} β @ s {{ β, Φ β }}) -∗ + WP@{rs} k (_REG err h b) @ s {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + unfold _REG. simpl. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + rewrite /ccompose /compose /=. + repeat f_equiv. + apply cons_equiv; last done. + apply pair_equiv. + split; first done. + trans (laterO_map k : laterO IT -n> laterO IT); last reflexivity. + intro. simpl. f_equiv. apply ofe_iso_21. + - done. + - iAssumption. + Qed. + + Lemma wp_pop (σ σ': stateF ♯ IT) (err : excO) h k (k' : IT -n> IT) {Hk' : IT_hom k'} β Φ : + σ = (err,h,k)::σ' → + k (later_map k' $ Next $ Ret ()) ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} β {{ β, Φ β }}) -∗ + WP@{rs} k' (_POP err) {{ Φ }}. + Proof. + iIntros (-> Hβ) "Hσ Ha". + unfold _POP. + simpl. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + destruct (eq_dec err err); last done. + reflexivity. + - exact Hβ. + - done. + Qed. + + Lemma wp_catch_v σ (v : IT) Φ err h (k : IT -n> IT) {Hk : IT_hom k} `{!AsVal v} β : + k v ≡ β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β {{ Φ }}) -∗ + WP@{rs} k (CATCH err h v) {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + simpl. + iApply (wp_reg _ _ _ k with "Hσ"); first done. + iIntros "!> Hcr Hσ". + simpl. + rewrite get_val_ITV /=. + iApply (wp_pop with "Hσ"). + - reflexivity. + - simpl. unfold later_map. simpl. rewrite get_val_ret. simpl. rewrite Hβ. reflexivity. + - iAssumption. + Qed. + + Global Instance throw_hom {err : exc} : IT_hom (THROW err : IT -n> IT). + Proof. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite hom_tick. + - rewrite hom_vis. do 3 f_equiv. intro. simpl. done. + - by rewrite hom_err. + Qed. + + + Definition wp_throw (σ pre post : stateF ♯ IT) (err : excO) (h k : laterO IT -n> laterO IT) (k' : IT -n> IT) {Hk : IT_hom k'} (v : IT) `{!AsVal v} β Φ : + (Forall (λ '(err',_,_), err <> err') pre) → + k (h (Next v)) ≡ Next β → + σ = pre ++ (err,h,k) :: post → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate post -∗ WP@{rs} β {{ β, Φ β }}) -∗ + WP@{rs} k' (THROW err v) {{ Φ }}. + Proof. + iIntros (Hpre Hβ Hsplit) "Hσ Ha". + simpl. + rewrite get_val_ITV. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + change (_cut_when (aux err) σ) with (cut_when (aux err) σ). + rewrite (cut_when_first_occ _ σ _ _ _ Hsplit). + + reflexivity. + + simpl. destruct (eq_dec err err); done. + + eapply Forall_impl; first by apply Hpre. + intros x Hx. + simpl. + destruct x as [[err' _] _] . simpl in *. + destruct (eq_dec err err'); done. + - exact Hβ. + - iAssumption. + Qed. + + Lemma wp_catch_throw σ (v : IT) `{!AsVal v} (k k': IT -n> IT) {Hk : IT_hom k} {Hk' : IT_hom k'} Φ err (h : laterO IT -n> laterO IT) β : + h (Next v) ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k' β {{ Φ }}) -∗ + WP@{rs} k' (CATCH err h (k (THROW err v))) {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + simpl. + iApply (wp_reg _ _ _ k' with "Hσ"); first done. + iIntros "!> Hcr Hσ". + simpl. + assert (H : ∀ x y, (get_val x (k y)) = ((get_val x) ∘ k) y). + { intros. reflexivity. } + rewrite H. + iApply (wp_throw _ _ _ _ _ _ ((get_val _) ◎ k) with "Hσ"). + - by apply Forall_nil. + - trans (laterO_map k' (h (Next v))); first reflexivity. + rewrite Hβ /= /later_map /=. reflexivity. + - simpl. reflexivity. + - iAssumption. + Qed. + + End weakestpre. + +End Exc. diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v new file mode 100644 index 0000000..2584395 --- /dev/null +++ b/theories/examples/except_lang/interp.v @@ -0,0 +1,968 @@ +From gitrees Require Import gitree lang_generic. +From iris.algebra Require Import list. +From gitrees.effects Require Export exceptions. +From gitrees.examples.except_lang Require Import lang typing. + +Require Import Binding.Lib Binding.Set. + + +Module interp (Errors : ExcSig). + + Module _TYP := Typing Errors. + Import _TYP. + Import _LANG. + Import _Exc. + + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {subE : subReifier reify_exc rs}. + Context {R} `{CR : !Cofe R}. + Context `{!SubOfe natO R}. + Context `{!SubOfe unitO R}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Global Instance denot_cont_ne (κ : IT -n> IT) : + NonExpansive (λ x : IT, Tau (laterO_map κ (Next x))). + Proof. + solve_proper. + Qed. + + (** Interpreting individual operators *) + + Program Definition interp_natop {A} (op : nat_op) (t1 t2 : A -n> IT) : A -n> IT := + λne env, NATOP (do_natop op) (t1 env) (t2 env). + Solve All Obligations with solve_proper_please. + + Global Instance interp_natop_ne A op : NonExpansive2 (@interp_natop A op). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_natop. + + Opaque laterO_map. + Program Definition interp_rec_pre {S : Set} (body : interp_scope (inc (inc S)) -n> IT) + : laterO (interp_scope S -n> IT) -n> interp_scope S -n> IT := + λne self env, Fun $ laterO_map (λne (self : interp_scope S -n> IT) (a : IT), + body (extend_scope (extend_scope env (self env)) a)) self. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + do 3 f_equiv; intros ??; simpl; f_equiv; + intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + by do 2 f_equiv. + Qed. + + Program Definition interp_rec {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) : + interp_scope S -n> IT := + mmuu (interp_rec_pre body). + + Program Definition ir_unf {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) env : IT -n> IT := + λne a, body (extend_scope + (extend_scope env (interp_rec body env)) + a). + Next Obligation. + intros. + solve_proper_prepare. + f_equiv. intros [| [| y']]; simpl; solve_proper. + Qed. + + Lemma interp_rec_unfold {S : Set} (body : interp_scope (inc (inc S)) -n> IT) env : + interp_rec body env ≡ Fun $ Next $ ir_unf body env. + Proof. + trans (interp_rec_pre body (Next (interp_rec body)) env). + { f_equiv. rewrite /interp_rec. apply mmuu_unfold. } + simpl. rewrite laterO_map_Next. repeat f_equiv. + simpl. unfold ir_unf. intro. simpl. reflexivity. + Qed. + + Program Definition interp_app {A} (t1 t2 : A -n> IT) : A -n> IT := + λne env, APP' (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_app_ne A : NonExpansive2 (@interp_app A). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_app. + + Program Definition interp_if {A} (t0 t1 t2 : A -n> IT) : A -n> IT := + λne env, IF (t0 env) (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_if_ne A n : + Proper ((dist n) ==> (dist n) ==> (dist n) ==> (dist n)) (@interp_if A). + Proof. solve_proper. Qed. + + Program Definition interp_nat (n : nat) {A} : A -n> IT := + λne env, Ret n. + + Program Definition interp_throw {A} (err : exc) (e : A -n> IT) : A -n> IT := + λne env, THROW err (e env). + Solve All Obligations with solve_proper. + + Global Instance interp_throw_ne A exc e : NonExpansive (@interp_throw A exc e). + Proof. solve_proper. Qed. + + Program Definition interp_catch {A} (err : exc) (exp : (interp_scope A) -n> IT) (h : (@interp_scope F R _ (inc A)) -n> IT) : interp_scope A -n> IT := + λne env, CATCH err (λne (v : laterO IT), laterO_map (λne x, h (extend_scope env x) ) v) (exp env). + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + intro a. + simpl. + destruct a; done. + Qed. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; last done. + intros a. simpl. + repeat f_equiv. + intros a2. simpl. + repeat f_equiv. + intros a3. simpl. + destruct a3; done. + Qed. + + Program Definition interp_applk {A} + (K : A -n> (IT -n> IT)) + (q : A -n> IT) + : A -n> (IT -n> IT) := + λne env t, interp_app (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_apprk {A} + (q : A -n> IT) + (K : A -n> (IT -n> IT)) + : A -n> (IT -n> IT) := + λne env t, interp_app q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoprk {A} (op : nat_op) + (q : A -n> IT) + (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_natop op q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoplk {A} (op : nat_op) + (K : A -n> (IT -n> IT)) + (q : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_natop op (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_ifk {A} (K : A -n> (IT -n> IT)) (q : A -n> IT) + (p : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_if (λne env, K env t) q p env. + Solve All Obligations with solve_proper. + + Program Definition interp_throwk {A} (err : exc) (K : A -n> (IT -n> IT)) : + A -n> (IT -n> IT) := + λne env t, interp_throw err (λne env, K env t) env. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + Proof. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. Proof. solve_proper. Qed. + + Program Definition interp_catchk {A} (err : exc) (K : interp_scope A -n> (IT -n> IT)) (h : interp_scope (inc A) -n> IT) : + (interp_scope A) -n> (IT -n> IT) := + λne env t, interp_catch err (λne env, K env t) h env. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; last done. + intros a. simpl. + repeat f_equiv. + intros a2. simpl. + repeat f_equiv. + intros a3. simpl. + destruct a3; done. + Qed. + + (** Interpretation for all the syntactic categories: values, expressions, contexts **) + Fixpoint interp_val {S} (v : val S) : interp_scope S -n> IT := + match v with + | LitV n => interp_nat n + | RecV e => interp_rec (interp_expr e) + end + with interp_expr {S} (e : expr S) : interp_scope S -n> IT := + match e with + | Val v => interp_val v + | Var x => interp_var x + | App e1 e2 => interp_app (interp_expr e1) (interp_expr e2) + | NatOp op e1 e2 => interp_natop op (interp_expr e1) (interp_expr e2) + | If e e1 e2 => interp_if (interp_expr e) (interp_expr e1) (interp_expr e2) + | Throw err v => interp_throw err (interp_expr v) + | Catch err b h => interp_catch err (interp_expr b) (interp_expr h) + end. + + Global Instance interp_val_asval {S} {v : val S} {env} : AsVal (interp_val v env). + Proof. + unfold AsVal. + destruct v. + - simpl. exists (RetV n). done. + - simpl. unfold interp_rec. + exists (FunV (Next (ir_unf (interp_expr e) env))). + simpl. + by rewrite interp_rec_unfold. + Qed. + + Program Definition interp_handler {S} (h : expr (inc S)) : interp_scope S -n> laterO IT -n> laterO IT := + λne env, laterO_map (λne x, (interp_expr h) (extend_scope env x)). + Next Obligation. + solve_proper_prepare. + f_equiv. + intros []; simpl; solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + intro. + simpl. + f_equiv. + intros []; + simpl; done. + Qed. + + Program Fixpoint split_cont {S} (K : cont S) : interp_scope S → ((IT -n> IT) * (listO (excO * (laterO IT -n> laterO IT) * (laterO IT -n> laterO IT) )))%type := + λ env, + match K with + | END => (idfun, []) + | IfK e1 e2 K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, IF t + (interp_expr e1 env) + (interp_expr e2 env)), lst) + | AppLK v K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, t ⊙ (interp_val v env)), lst) + | AppRK e K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, (λne v, (interp_expr e env) ⊙ v) t), lst) + | NatOpRK op e K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, NATOP (do_natop op) (interp_expr e env) t), lst) + | NatOpLK op v K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, NATOP (do_natop op) t (interp_val v env)), lst) + + | ThrowK err K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, THROW err t), lst) + | CatchK err h K' => let (f, lst) := split_cont K' env in + (get_val (λne t, get_val (λne _, t) (_POP err)), (err, + interp_handler h env , laterO_map f) + ::lst) + end. + Solve All Obligations with try solve_proper. + Next Obligation. + solve_proper_please. + Qed. + + Global Instance split_cont_ne {S} {K : cont S} : NonExpansive (split_cont K). + Proof. + induction K; try done; intros n x y H; simpl; + assert (Hs : split_cont K x ≡{n}≡ split_cont K y); + try ( f_equiv; done ); + destruct (split_cont K x) as [f t]; + destruct (split_cont K y) as [f' t']; + rewrite pair_dist in Hs; + destruct Hs as [Hf Ht]; f_equiv; try done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; last done. + intro. simpl. repeat f_equiv. done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - repeat f_equiv; try done. + intro x0. simpl. f_equiv. intro x1. simpl. destruct x1; first done. + f_equiv. done. + Qed. + + Theorem split_cont_left_hom {S} {K : cont S} {env : interp_scope S} + : IT_hom (split_cont K env).1 . + Proof. + induction K. + - simple refine (IT_HOM _ _ _ _ _); + intros; + simpl; + repeat f_equiv. + change (λne x : IT, x) with (@idfun IT). + intros x. + rewrite /ccompose /compose /=. + apply laterO_map_id. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + simple refine (IT_HOM _ _ _ _ _). + + intros. simpl. + rewrite IF_Tick. + apply IHK. + + intros. simpl. + rewrite IF_Vis hom_vis. + f_equiv. + rewrite !/ccompose !/compose /=. + intros x. simpl. + rewrite -laterO_map_compose. + repeat f_equiv. + intro. + simpl. + done. + + intros e. simpl. + rewrite IF_Err. + apply IHK. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite APP'_Tick_l. + apply IHK. + + rewrite APP'_Vis_l hom_vis. + f_equiv. + rewrite !/ccompose !/compose /=. + intro. simpl. + rewrite -laterO_map_compose. + f_equiv. + intro. done. + + rewrite APP'_Err_l. apply IHK. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite APP'_Tick_r. apply hom_tick. + + rewrite APP'_Vis_r hom_vis. + f_equiv. + intro. simpl. + rewrite laterO_map_compose. + f_equiv. + intro. done. + + rewrite APP'_Err_r. apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite NATOP_ITV_Tick_l. + apply hom_tick. + + rewrite NATOP_ITV_Vis_l hom_vis. + f_equiv. + intro. simpl. + rewrite -laterO_map_compose. + do 2 f_equiv. intro. simpl. done. + + rewrite NATOP_Err_l. + apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + by rewrite -hom_tick NATOP_Tick_r. + + rewrite NATOP_Vis_r hom_vis. + f_equiv. + intro. simpl. + rewrite laterO_map_compose. + f_equiv. intro. done. + + rewrite NATOP_Err_r. + apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + do 2 rewrite hom_tick. + done. + + do 2 rewrite hom_vis. + f_equiv. + intro. simpl. + rewrite -laterO_map_compose. + f_equiv. + intros []. + done. + + by do 2 rewrite hom_err. + - simpl. + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + by rewrite -hom_tick. + + rewrite hom_vis. + do 3 f_equiv. intro. simpl. done. + + by rewrite hom_err. + Qed. + + Theorem split_cont_left_hom' {S} {K : cont S} {env} f t : split_cont K env = (f,t) → IT_hom f. + Proof. + intros H. + replace f with (split_cont K env).1. + - apply split_cont_left_hom. + - rewrite H. done. + Qed. + + Program Definition interp_config {S} (cfg : @config S) : interp_scope S -n> (IT * stateF ♯ IT)%type := + match cfg with + | Cexpr e => λne env, (interp_expr e env, []) + | Ceval e K => λne env, let (f,t) := split_cont K env in + (f (interp_expr e env), t) + | Ccont K v => λne env, let (f,t) := split_cont K env in + (f (interp_val v env), t) + | Cret v => λne env, (interp_val v env, []) + end. + Solve All Obligations with try solve_proper. + Next Obligation. + Proof. + solve_proper_prepare. + assert (Hs : split_cont K x ≡{n}≡ split_cont K y). { f_equiv. done. } + destruct (split_cont K x) as [f t]. + destruct (split_cont K y) as [f' t']. + rewrite pair_dist in Hs. + destruct Hs as [Hf Ht]. + repeat f_equiv; done. + Qed. + Next Obligation. + Proof. + solve_proper_prepare. + assert (Hs : split_cont K x ≡{n}≡ split_cont K y). { f_equiv. done. } + destruct (split_cont K x) as [f t]. + destruct (split_cont K y) as [f' t']. + rewrite pair_dist in Hs. + destruct Hs as [Hf Ht]. + repeat f_equiv; done. + Qed. + + + Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) := + fun f g => ∀ x, f x = g x. + + Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) := + fun n => fun f g => ∀ x, f x ≡{n}≡ g x. + + Global Instance ren_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@ren_scope F _ CR S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - apply Hs. + - apply HE. + Qed. + + Lemma interp_expr_ren {S S'} env + (δ : S [→] S') (e : expr S) : + interp_expr (fmap δ e) env ≡ interp_expr e (ren_scope δ env) + with interp_val_ren {S S'} env + (δ : S [→] S') (e : val S) : + interp_val (fmap δ e) env ≡ interp_val e (ren_scope δ env). + Proof. + - destruct e; simpl. + + by apply interp_val_ren. + + reflexivity. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv. + * intros []. simpl. do 2 rewrite laterO_map_Next. + f_equiv. simpl. + rewrite interp_expr_ren. + f_equiv. + intros []; by simpl. + * apply interp_expr_ren. + - destruct e; simpl. + + reflexivity. + + clear -interp_expr_ren. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * done. + Qed. + + Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') + : interp_scope S := λne x, interp_expr (δ x) env. + + Global Instance SubEquiv {A B : Set} : Equiv (A [⇒] B) := fun f g => ∀ x, f x = g x. + + Global Instance sub_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@sub_scope S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - f_equiv. + apply HE. + - apply Hs. + Qed. + + Lemma interp_expr_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_expr (bind δ e) env ≡ interp_expr e (sub_scope δ env) + with interp_val_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env). + Proof. + - destruct e; simpl. + + by apply interp_val_subst. + + term_simpl. + reflexivity. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; last done. + intros []. + do 2 rewrite laterO_map_Next. + f_equiv. + simpl. + rewrite interp_expr_subst. + f_equiv. + intros []; simpl. + * done. + * rewrite interp_expr_ren. + f_equiv. + intro. + simpl. + done. + + - destruct e; simpl. + + reflexivity. + + clear -interp_expr_subst. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_subst. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * do 2 rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (z). + done. + Qed. + + Lemma split_cont_decomp {S} K K1 K2 p t p1 t1 env h err f k: + split_cont K env = (p,t) → + split_cont K1 env = (p1,t1) → + K = cont_compose (CatchK err h K1) K2 → + (∀ K4 K3 h', K2 <> @cont_compose S (CatchK err h' K3) K4) → + f = interp_handler h env → + k = laterO_map p1 → + ∃pre, t = pre ++ (err,f,k)::t1 ∧ Forall (λ '(err', _ ,_ ), err <> err' ) pre. + Proof. + generalize dependent K1. + generalize dependent p. + generalize dependent t. + generalize dependent p1. + generalize dependent t1. + generalize dependent K2. + generalize dependent f. + generalize dependent env. + generalize dependent h. + + induction K; intros. + - destruct K2; discriminate. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (IfK e₁ e₂ K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (AppLK v K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (AppRK e K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (NatOpLK op v K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (NatOpRK op e K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (ThrowK err0 K4)). + simpl. + reflexivity. + + - destruct K2; try discriminate. + + injection H1 as <- <- ->. + simpl in H. + rewrite H0 in H. + injection H as <- <-. + eexists []. + rewrite H3 H4. + simpl. + done. + + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h0 K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + epose proof (IHK h0 env _ _ _ _ u g _ Heq H0 _ _ _ _) as (pre & -> & Hfall). + eexists. + split. + { rewrite app_comm_cons. done. } + apply Forall_cons. + split; last done. + intros ->. + by eapply (H2 END). + Unshelve. + 2, 4, 5 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (CatchK err0 h K4) _). + simpl. + done. + Qed. + + Lemma unwind_cut_when {S} : ∀ K K' env f t g t' err h, + split_cont K env = (f,t) → + split_cont K' env = (g,t') → + @unwind S err K = Some (h, K') → + cut_when (aux err) t = Some ((err,interp_handler h env,laterO_map g), t'). + Proof. + intros K K' env f t g t' err h HsplitK HsplitK' Hwind. + apply unwind_decompose in Hwind as (K1 & -> & HK1). + pose proof (split_cont_decomp _ _ _ f t g t' env h err _ _ HsplitK HsplitK' eq_refl HK1 eq_refl eq_refl) as (pre & -> & Hfall). + eapply cut_when_first_occ. + { done. } + { simpl. destruct (eq_dec err err); done. } + eapply Forall_impl. + { exact Hfall. } + intros [[err' ?] ?] ?. + simpl. + destruct (eq_dec err err'); done. + Qed. + + Theorem soundness {S} : ∀ c c' e e' σr σ σ' n (env : interp_scope S), + interp_config c env = (e, σ) → + interp_config c' env = (e', σ') → + c ===> c' / n → + ssteps (gReifiers_sReifier rs) + e (gState_recomp σr (sR_state σ)) + e' (gState_recomp σr (sR_state σ')) n. + Proof. + intros. + revert H H0. + inversion H1; intros HE0 HE1. + - simpl in HE0, HE1. + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + rewrite HE0 in HE1. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t]. + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t]. + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t]. + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + econstructor. + + rewrite hom_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose (@subReifier_reify _ _ _ _ _ _ _ (inl ()) ?[x] (Next _) ?[k] t ?[σ'] σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ ?σ2)) , ?k' ◎ _) ≡ _ => instantiate (x := x'); + instantiate (k := k') + + end. + Unshelve. + 6 : { simpl. done. } + 1 : { simpl in Hry|-*. + erewrite <-Hry. + repeat f_equiv; first by solve_proper. + intro. simpl. done. + } + + constructor. + * repeat f_equiv. + intro. simpl. + do 2 f_equiv. + intro. + simpl. + done. + * simpl. + do 5 f_equiv; + f_equiv; + intro; + simpl; + done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + by constructor. + - simpl in HE0, HE1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + by constructor. + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + econstructor; last (econstructor; reflexivity). + apply sstep_tick; last done. + rewrite -hom_tick. + f_equiv. + pose (interp_rec_unfold (interp_expr f) env) as HEq. + assert (∀ x y z : IT, x ≡ y → x ⊙ z ≡ y ⊙ z) as APP'_equiv. + { intros x y z Hxy. + Transparent APP APP'. + simpl. + Opaque APP APP'. + repeat f_equiv. + intro. simpl. + f_equiv. + done. + } + rewrite (APP'_equiv _ _ _ HEq) APP_APP'_ITV APP_Fun Tick_eq /=. + do 2 rewrite interp_expr_subst. + do 3 f_equiv. + intros []. + + simpl. rewrite -interp_val_subst. + do 2 f_equiv. + pose @subst_shift_id as Hsbs. + unfold subst in Hsbs. + rewrite Hsbs. + done. + + destruct i; simpl. + * done. + * done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; last done. + f_equiv. + destruct n0. + + rewrite IF_False; last lia. + done. + + rewrite IF_True; last lia. + done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; done. + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + constructor; last done. + f_equiv. + destruct v1, v2. + 2, 3, 4 : contradict H; done. + simpl in H. + injection H as <-. + simpl. + apply NATOP_Ret. + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + injection HE0 as <- <-. + injection HE1 as <- <-. + econstructor; last (constructor; done). + rewrite get_val_ITV /= get_val_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inl ())) ?[x] (Next _) ?[k] ?[σ] ?[σ'] σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => + instantiate (x := x'); + instantiate (k := k1 ◎ k2); + instantiate (σ := σ2) + end. + Unshelve. + 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. } + 1 : { simpl in Hry|-*. + match goal with + | [Hry : _ ≡ ?r |- _ ] => transitivity r + end. + 2 : { repeat f_equiv. + Transparent laterO_map. + simpl. + Opaque laterO_map. + f_equiv. + apply get_val_ret. + } + + rewrite -Hry. + + repeat f_equiv; first by solve_proper. + intro. simpl. done. + } + - simpl in HE0, HE1. + destruct (split_cont k env) as [g t] eqn:Heq. + destruct (split_cont k' env) as [g' t'] eqn:Heq'. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection HE0 as <- <-. + injection HE1 as <- <-. + econstructor; last by constructor. + rewrite get_val_ITV hom_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inr (inl ()))) ?[x] (Next _) ?[k] ?[σ] t' σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ _ ?σ2)) , _) ≡ _ => + instantiate (x := x'); + instantiate (σ := σ2) + end. + Unshelve. + 4 : { Opaque cut_when. simpl. + apply (unwind_cut_when _ _ env _ _ _ _ _ _ Heq Heq') in H. + rewrite H. + simpl. + f_equiv. + rewrite laterO_map_Next. + simpl. + rewrite pair_equiv. + split; last done. + f_equiv. + trans (g' (interp_expr (subst h (Val v)) env)); last done. + f_equiv. + rewrite interp_expr_subst. + f_equiv. + intros []; done. + } + 1 : { + simpl in Hry. + simpl. + rewrite -Hry. + repeat f_equiv; first solve_proper. + intro. + simpl. + instantiate (k := (laterO_map (λne y, g y)) ◎ (λne x, Empty_set_rect (λ _ : ∅, laterO IT) x)). + simpl. + done. + Unshelve. + intros n0 []. + } + - simpl in HE0, HE1. + rewrite HE0 in HE1. + injection HE1 as <- <-. + constructor; done. + Qed. + +End interp. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v new file mode 100644 index 0000000..682bf42 --- /dev/null +++ b/theories/examples/except_lang/lang.v @@ -0,0 +1,641 @@ +From gitrees Require Export prelude effects.exceptions. +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. + +Module Lang (Errors : ExcSig). + + Module _Exc := Exc Errors. + + Import _Exc. + + Inductive nat_op := Add | Sub | Mult. + + Inductive expr {X : Set} : Type := + (* Values *) + | Val (v : val) : expr + | Var (x : X) : expr + (* Base lambda calculus *) + | App (e₁ : expr) (e₂ : expr) : expr + (* Base types and their operations *) + | NatOp (op : nat_op) (e₁ : expr) (e₂ : expr) : expr + | If (e₁ : expr) (e₂ : expr) (e₃ : expr) : expr + (* The effects *) + | Throw (err : exc) (e : expr) : expr + | Catch (err : exc) (e₁ : expr) (e₂ : @expr (inc X)) : expr + with val {X : Set} := + | LitV (n : nat) : val + | RecV (e : @expr (inc (inc X))) : val + with cont {X : Set} := + | END : cont + | IfK (e₁ : expr) (e₂ : expr) : cont → cont + | AppLK (v : val) : cont → cont + | AppRK (e : expr) : cont → cont + | NatOpLK (op : nat_op) (v : val) : cont → cont + | NatOpRK (op : nat_op) (e : expr) : cont → cont + | ThrowK (err : exc) : cont → cont + | CatchK (err : exc) (h : @expr (inc X)) : cont → cont. + + Arguments val X%bind : clear implicits. + Arguments expr X%bind : clear implicits. + Arguments cont X%bind : clear implicits. + + + Local Open Scope bind_scope. + + Fixpoint emap {A B : Set} (f : A [→] B) (e : expr A) : expr B := + match e with + | Val v => Val (vmap f v) + | Var x => Var (f x) + | App e₁ e₂ => App (emap f e₁) (emap f e₂) + | NatOp o e₁ e₂ => NatOp o (emap f e₁) (emap f e₂) + | If e₁ e₂ e₃ => If (emap f e₁) (emap f e₂) (emap f e₃) + | Throw err e => Throw err (emap f e) + | Catch err e₁ e₂ => Catch err (emap f e₁) (@emap (inc A) (inc B) (f ↑) e₂) + end + with vmap {A B : Set} (f : A [→] B) (v : val A) : val B := + match v with + | LitV n => LitV n + | RecV e => RecV (emap ((f ↑) ↑) e) + end + with kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B := + match K with + | END => END + | IfK e₁ e₂ K => IfK (emap f e₁) (emap f e₂) (kmap f K) + | AppLK v K => AppLK (vmap f v) (kmap f K) + | AppRK e K => AppRK (emap f e) (kmap f K) + | NatOpLK op v K => NatOpLK op (vmap f v) (kmap f K) + | NatOpRK op e K => NatOpRK op (emap f e) (kmap f K) + | ThrowK err K => ThrowK err (kmap f K) + | CatchK err h K => CatchK err (emap (f ↑) h) (kmap f K) + end. + +#[export] Instance FMap_expr : FunctorCore expr := @emap. +#[export] Instance FMap_val : FunctorCore val := @vmap. +#[export] Instance FMap_cont : FunctorCore cont := @kmap. + +#[export] Instance SPC_expr : SetPureCore expr := @Var. + +Fixpoint ebind {A B : Set} (f : A [⇒] B) (e : expr A) : expr B := + match e with + | Val v => Val (vbind f v) + | Var x => f x + | App e₁ e₂ => App (ebind f e₁) (ebind f e₂) + | NatOp o e₁ e₂ => NatOp o (ebind f e₁) (ebind f e₂) + | If e₁ e₂ e₃ => If (ebind f e₁) (ebind f e₂) (ebind f e₃) + | Throw err e => Throw err (ebind f e) + | Catch err e₁ e₂ => Catch err (ebind f e₁) (ebind (f ↑) e₂) + end +with vbind {A B : Set} (f : A [⇒] B) (v : val A) : val B := + match v with + | LitV n => LitV n + | RecV e => RecV (ebind ((f ↑) ↑) e) + end +. + +Fixpoint kbind {A B : Set} (f : A [⇒] B) (K : cont A) : cont B := + match K with + | END => END + | IfK e₁ e₂ K => IfK (ebind f e₁) (ebind f e₂) (kbind f K) + | AppLK v K => AppLK (vbind f v) (kbind f K) + | AppRK e K => AppRK (ebind f e) (kbind f K) + | NatOpLK op v K => NatOpLK op (vbind f v) (kbind f K) + | NatOpRK op e K => NatOpRK op (ebind f e) (kbind f K) + | ThrowK err K => ThrowK err (kbind f K) + | CatchK err h K => CatchK err (ebind (f ↑) h) (kbind f K) + end. + +#[export] Instance BindCore_expr : BindCore expr := @ebind. +#[export] Instance BindCore_val : BindCore val := @vbind. +#[export] Instance BindCore_cont : BindCore cont := @kbind. + +#[export] Instance IP_typ : SetPure expr. +Proof. + split; intros; reflexivity. +Qed. + +Fixpoint vmap_id X (δ : X [→] X) (v : val X) : δ ≡ ı → fmap δ v = v +with emap_id X (δ : X [→] X) (e : expr X) : δ ≡ ı → fmap δ e = e +with kmap_id X (δ : X [→] X) (e : cont X) : δ ≡ ı → fmap δ e = e. +Proof. + - auto_map_id. + - auto_map_id. + - auto_map_id. +Qed. + +Fixpoint vmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (v : val A) : + f ∘ g ≡ h → fmap f (fmap g v) = fmap h v +with emap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : expr A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e +with kmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : cont A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e. +Proof. + - auto_map_comp. + - auto_map_comp. + - auto_map_comp. +Qed. + +#[export] Instance Functor_val : Functor val. +Proof. + split; [exact vmap_id | exact vmap_comp]. +Qed. +#[export] Instance Functor_expr : Functor expr. +Proof. + split; [exact emap_id | exact emap_comp]. +Qed. +#[export] Instance Functor_cont : Functor cont. +Proof. + split; [exact kmap_id | exact kmap_comp]. +Qed. + +Fixpoint vmap_vbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (v : val A) : + f ̂ ≡ g → fmap f v = bind g v +with emap_ebind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : expr A) : + f ̂ ≡ g → fmap f e = bind g e +with kmap_kbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : cont A) : + f ̂ ≡ g → fmap f e = bind g e. +Proof. + - auto_map_bind_pure. + erewrite emap_ebind_pure; [reflexivity |]. + intros [| [| x]]; term_simpl; [reflexivity | reflexivity |]. + rewrite <-(EQ x). + reflexivity. + - auto_map_bind_pure. + - auto_map_bind_pure. +Qed. + +#[export] Instance BindMapPure_val : BindMapPure val. +Proof. + split; intros; now apply vmap_vbind_pure. +Qed. +#[export] Instance BindMapPure_expr : BindMapPure expr. +Proof. + split; intros; now apply emap_ebind_pure. +Qed. +#[export] Instance BindMapPure_cont : BindMapPure cont. +Proof. + split; intros; now apply kmap_kbind_pure. +Qed. + +Fixpoint vmap_vbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (v : val A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ v) = fmap f₁ (bind g₁ v) +with emap_ebind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : expr A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e) +with kmap_kbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : cont A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e). +Proof. + - auto_map_bind_comm. + erewrite emap_ebind_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity | assumption]. + - auto_map_bind_comm. + - auto_map_bind_comm. +Qed. + +#[export] Instance BindMapComm_val : BindMapComm val. +Proof. + split; intros; now apply vmap_vbind_comm. +Qed. +#[export] Instance BindMapComm_expr : BindMapComm expr. +Proof. + split; intros; now apply emap_ebind_comm. +Qed. +#[export] Instance BindMapComm_cont : BindMapComm cont. +Proof. + split; intros; now apply kmap_kbind_comm. +Qed. + +Fixpoint vbind_id (A : Set) (f : A [⇒] A) (v : val A) : + f ≡ ı → bind f v = v +with ebind_id (A : Set) (f : A [⇒] A) (e : expr A) : + f ≡ ı → bind f e = e +with kbind_id (A : Set) (f : A [⇒] A) (e : cont A) : + f ≡ ı → bind f e = e. +Proof. + - auto_bind_id. + rewrite ebind_id; [reflexivity |]. + apply lift_id, lift_id; assumption. + - auto_bind_id. + - auto_bind_id. +Qed. + +Fixpoint vbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (v : val A) : + f ∘ g ≡ h → bind f (bind g v) = bind h v +with ebind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : expr A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e +with kbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : cont A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e. +Proof. + - auto_bind_comp. + erewrite ebind_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity | assumption]. + - auto_bind_comp. + - auto_bind_comp. +Qed. + +#[export] Instance Bind_val : Bind val. +Proof. + split; intros; [now apply vbind_id | now apply vbind_comp]. +Qed. +#[export] Instance Bind_expr : Bind expr. +Proof. + split; intros; [now apply ebind_id | now apply ebind_comp]. +Qed. +#[export] Instance Bind_cont : Bind cont. +Proof. + split; intros; [now apply kbind_id | now apply kbind_comp]. +Qed. + +Definition to_val {S} (e : expr S) : option (val S) := + match e with + | Val v => Some v + | _ => None + end. + +Definition do_natop (op : nat_op) (x y : nat) : nat := + match op with + | Add => plus x y + | Sub => minus x y + | Mult => mult x y + end. + +Definition nat_op_interp {S} (n : nat_op) (x y : val S) : option (val S) := + match x, y with + | LitV x, LitV y => Some $ LitV $ do_natop n x y + | _,_ => None + end. + +Fixpoint fill {X : Set} (K : cont X) (e : expr X) : expr X := + match K with + | END => e + | IfK e₁ e₂ K => fill K $ If e e₁ e₂ + | AppLK v K => fill K $ App e (Val v) + | AppRK e' K => fill K $ App e' e + | NatOpLK op v K => fill K $ NatOp op e (Val v) + | NatOpRK op e' K => fill K $ NatOp op e' e + | ThrowK err K => fill K $ Throw err e + | CatchK err e' K => fill K $ Catch err e e' + end. + +Lemma fill_emap {X Y : Set} (f : X [→] Y) (K : cont X) (e : expr X) + : fmap f (fill K e) = fill (fmap f K) (fmap f e). +Proof. + revert f. + induction K as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]; + intros f; term_simpl; first done; rewrite IH; reflexivity. +Qed. + +Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S + := match K2 with + | END => K1 + | IfK e₁ e₂ K => IfK e₁ e₂ (cont_compose K1 K) + | AppLK v K => AppLK v (cont_compose K1 K) + | AppRK e K => AppRK e (cont_compose K1 K) + | NatOpLK op v K => NatOpLK op v (cont_compose K1 K) + | NatOpRK op e K => NatOpRK op e (cont_compose K1 K) + | ThrowK err K => ThrowK err (cont_compose K1 K) + | CatchK err h K => CatchK err h (cont_compose K1 K) + end. + + Fixpoint unwind {S : Set} (err : exc) (k : cont S) := + match k with + | END => None + | IfK _ _ K' => unwind err K' + | AppLK _ K' => unwind err K' + | AppRK _ K' => unwind err K' + | NatOpLK _ _ K' => unwind err K' + | NatOpRK _ _ K' => unwind err K' + | ThrowK _ K' => unwind err K' + | CatchK err' h K' => if eq_dec err err' + then Some (h,K') + else unwind err K' + end. + +Theorem unwind_decompose {S : Set} (err : exc) (K : cont S) (h : expr (inc S)) (K2 : cont S) : unwind err K = Some (h, K2) ↔ ∃ (K1 : cont S), (K = cont_compose (CatchK err h K2) K1 + ∧ (∀ K3 K4 h', K1 ≠ cont_compose (CatchK err h' K4) K3 ) + ). +Proof. + induction K. + - split. + + intros. done. + + intros (? & ? & ?). + destruct x; + done. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (IfK e₁ e₂ K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (IfK e₁ e₂ K3) K4 h'). + by apply HNC. + + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (AppLK v K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (AppLK v K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (AppRK e K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (AppRK e K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (NatOpLK op v K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (NatOpLK op v K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (NatOpRK op e K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (NatOpRK op e K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (ThrowK err0 K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (ThrowK err0 K3) K4 h'). + by apply HNC. + + - split. + + intros H. + simpl in H. + destruct (eq_dec err err0) as [-> | Hdiff]. + * injection H as -> ->. + exists END. + split; first done. + intros K3 K4 h'. + destruct K3, K4; done. + * apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (CatchK err0 h0 K1). + simpl. + rewrite HK1. + split; first done. + intros K3 K4 h'. + destruct K3; try done; simpl; intros [=<- <- ->]; first done. + by eapply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + * simpl. + destruct (eq_dec err err0) as [-> | C]. + { simpl in HK1. by injection HK1 as -> ->. } + apply IHK. + injection HK1 as <- <-. + by contradict C. + * injection HK1 as <- <- ->. + simpl. + destruct (eq_dec err err0) as [-> | Herr]. + { + exfalso. + specialize (HNC END K1 h0). + by apply HNC. + } + apply IHK. + exists K1. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (CatchK err0 h0 K3)). + by eapply HNC. +Qed. + +Lemma unwind_decompose_weak {S} : + ∀ (K K1 K2 : cont S) err h, K = cont_compose (CatchK err h K1) K2 → + ∃ h' K3, unwind err K = Some (h', K3). + Proof. + intros K K1 K2. + revert K1. + induction K2; intros K1 err0 h0 ->; try (simpl; by eapply IHK2). + - simpl. destruct (eq_dec err0 err0); last done. + by eexists _,_. + - simpl. destruct (eq_dec err0 err). + + by eexists _,_. + + by eapply IHK2. + Qed. + +Variant config {S : Set} : Type := + | Cexpr : expr S → config + | Ccont : cont S → val S → config + | Ceval : expr S → cont S → config + | Cret : val S → config. + +Reserved Notation "c '===>' c' / n" + (at level 40, c' at level 30). + +Variant Cred {S : Set} : config → config → nat → Prop := + | Cinit e : Cexpr e ===> Ceval e END / 0 + | Cval v k : Ceval (Val v) k ===> Ccont k v / 0 + | Capp e0 e1 k : Ceval (App e0 e1) k ===> Ceval e1 (AppRK e0 k) / 0 + | Cop op e0 e1 k : Ceval (NatOp op e0 e1) k ===> Ceval e1 (NatOpRK op e0 k) / 0 + | Cif cd e1 e2 k : Ceval (If cd e1 e2) k ===> Ceval cd (IfK e1 e2 k) / 0 + | Ccatch err e h k : Ceval (Catch err e h) k ===> Ceval e (CatchK err h k) / 1 + | Cthrow err e k : Ceval (Throw err e) k ===> Ceval e (ThrowK err k) / 0 + | Cappr e v k : Ccont (AppRK e k) v ===> Ceval e (AppLK v k) / 0 + | Cappl f (v : val S) k : Ccont (AppLK v k) (RecV f) ===> Ceval + (subst (Inc := inc) + (subst (F := expr) (Inc := inc) f + (Val (shift (Inc := inc) v))) + (Val (RecV f))) k / 1 + | Cifk n e1 e2 k : Ccont (IfK e1 e2 k) (LitV n) ===> Ceval (if (n =? 0) then e2 else e1) k / 0 + | Coprk op v e k : Ccont (NatOpRK op e k) v ===> Ceval e (NatOpLK op v k) / 0 + | Coplk op v1 v2 v3 k : nat_op_interp op v1 v2 = Some v3 → + Ccont (NatOpLK op v2 k) v1 ===> Ceval (Val v3) k / 0 + | Ccatchk err h v k : Ccont (CatchK err h k) v ===> Ceval (Val v) k / 1 + | Cthrowk err h v k k' : unwind err k = Some (h,k') → + Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' / 1 + | Cend v : Ccont END v ===> Cret v / 0 + +where "c ===> c' / n" := (Cred c c' n). + +Inductive steps {S : Set} : (@config S) → (@config S) → nat → Prop := +| step0 c : steps c c 0 +| step_trans c c' c'' n n' : c ===> c' / n → steps c' c'' n' → steps c c'' (n + n') +. + +(** Carbonara from heap lang *) +Global Instance fill_item_inj {S} (Ki : cont S) : Inj (=) (=) (fill Ki). +Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. + +Lemma fill_item_val {S} K (e : expr S) : + is_Some (to_val (fill K e)) → is_Some (to_val e). +Proof. + intros [v ?]. induction K; simpl in H; try apply IHK in H. + 1 : eauto. + all : contradict H; eauto. +Qed. + +Lemma fill_app {S} (K1 K2 : cont S) e : fill (cont_compose K1 K2) e = fill K1 (fill K2 e). +Proof. + revert K1. + revert e. + induction K2 as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]; + first done; intros e' K1; simpl; rewrite IH; reflexivity. +Qed. + +Lemma fill_val : ∀ {S} K (e : expr S), is_Some (to_val (fill K e)) → is_Some (to_val e). +Proof. + intros S K. + induction K as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]=> e' //=; + inversion 1 as [? HH]; + apply IH in H; + simpl in H; + contradict H; + eauto. +Qed. + +Lemma fill_not_val : ∀ {S} K (e : expr S), to_val e = None → to_val (fill K e) = None. +Proof. + intros S K e. rewrite !eq_None_not_Some. + eauto using fill_val. +Qed. + +Lemma fill_end {S} (e : expr S) : fill END e = e. +Proof. reflexivity. Qed. + +Lemma fill_comp {S} K1 K2 (e : expr S) : fill K2 (fill K1 e) = fill (cont_compose K2 K1) e. +Proof. by rewrite fill_app. Qed. + +Global Instance fill_inj {S} (K : cont S) : Inj (=) (=) (fill K). +Proof. + induction K as [ | | | | | | | ]; + rewrite /Inj; naive_solver. +Qed. + +End Lang. diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v new file mode 100644 index 0000000..df8c504 --- /dev/null +++ b/theories/examples/except_lang/typing.v @@ -0,0 +1,830 @@ +From gitrees.examples.except_lang Require Import lang. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Module Typing (Errors : ExcSig). + Module _LANG := Lang Errors. + Import _LANG. + Import _Exc. + + (** Types indicating possible errors raised **) + Inductive pty : Type := + | Tnat : pty + | Tarr : pty → ty → pty + with ty : Type := + Ty : pty → gmap.gset exc → ty. + + Context (ETy : exc → pty). + Notation "'ℕ'" := Tnat. + Notation "σ '⟶' τ" := (Tarr σ τ) + (at level 20). + Notation "τ ⇑ E" := (Ty τ E) + (at level 20, + E at level 20, + no associativity). + + Reserved Notation "τ '≲' σ" + (at level 20). + + Reserved Notation "τ '⪍' σ" + (at level 20). + + Inductive le_pty : pty → pty → Prop := + | Le_nat : ℕ ≲ ℕ + | Le_arr τ1 τ2 σ1 σ2 : + τ2 ≲ τ1 → + σ1 ⪍ σ2 → + (τ1 ⟶ σ1) ≲ (τ2 ⟶ σ2) + with le_ty : ty → ty → Prop := + Le_Ty τ1 τ2 E1 E2 : + τ1 ≲ τ2 → + E1 ⊆ E2 → + (τ1 ⇑ E1) ⪍ (τ2 ⇑ E2) + where "τ ≲ σ" := (le_pty τ σ) + and "τ ⪍ σ" := (le_ty τ σ). + + Lemma le_pty_trans : ∀ τ1 τ2 τ3, τ1 ≲ τ2 → τ2 ≲ τ3 → τ1 ≲ τ3 + with le_ty_trans : ∀ τ1 τ2 τ3, τ1 ⪍ τ2 → τ2 ⪍ τ3 → τ1 ⪍ τ3. + Proof. + - intros τ1 τ2. + destruct τ2. + + intros τ3 H1 H2. + inversion H1. subst. + inversion H2. subst. + done. + + intros τ3 H1 H2. + inversion H1. subst. + inversion H2. subst. + constructor. + * by eapply le_pty_trans. + * by eapply le_ty_trans. + - intros τ1 τ2 τ3 H1 H2. + destruct τ1, τ2, τ3. + inversion H1. subst. + inversion H2. subst. + constructor. + + by eapply le_pty_trans. + + set_solver. + Qed. + + Lemma le_pty_refl : ∀ τ, τ ≲ τ + with le_ty_refl : ∀ τ, τ ⪍ τ. + Proof. + - intros τ. + destruct τ; constructor. + + apply le_pty_refl. + + apply le_ty_refl. + - intros [τ E]. + constructor. + + apply le_pty_refl. + + reflexivity. + Qed. + + (** Compatibility between types and bare types **) + + Notation "E ⊕ e" := (E ∪ {[e]}) + (at level 20). + Notation "E ⊖ e" := (E ∖ {[e]}) + (at level 20). + + Reserved Notation "Γ '⊢ₑ' e ':' τ" + (at level 70 + , e at level 60 + , τ at level 20 + , no associativity + ). + + Reserved Notation "Γ '⊢ᵥ' v : τ" + (at level 70 + , v at level 60 + , τ at level 20 + , no associativity + ). + Inductive typed {S : Set} : (S → pty) → expr S → ty → Prop := + | typed_Var Γ E x τ : Γ x ≲ τ → + (Γ ⊢ₑ (Var x) : τ ⇑ E) + + | typed_Lit Γ E v : (Γ ⊢ᵥ (LitV v) : ℕ ⇑ E) + + | typed_Rec Γ E f σ τ α : + (σ ⟶ τ) ≲ α → + (Γ ▹ (σ ⟶ τ) ▹ σ ⊢ₑ f : τ) → + (Γ ⊢ᵥ (RecV f) : α ⇑ E) + + | typed_App E E1 E2 E3 Γ f v σ τ : + (E1 ∪ E2 ∪ E3) = E → + (Γ ⊢ₑ f : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → + (Γ ⊢ₑ v : σ ⇑ E3) → + (Γ ⊢ₑ App f v : τ ⇑ E) + + | typed_Op Γ E E1 E2 op l r : + (E1 ∪ E2) = E → + (Γ ⊢ₑ l : ℕ ⇑ E1) → + (Γ ⊢ₑ r : ℕ ⇑ E2) → + (Γ ⊢ₑ NatOp op l r : ℕ ⇑ E) + + | typed_If Γ E E1 E2 E3 c t e τ : + (E1 ∪ E2 ∪ E3) = E→ + (Γ ⊢ₑ c : ℕ ⇑ E1) → + (Γ ⊢ₑ t : τ ⇑ E2) → + (Γ ⊢ₑ e : τ ⇑ E3) → + (Γ ⊢ₑ If c t e : τ ⇑ E) + + | typed_Throw Γ E1 E2 err v σ τ : + σ = ETy err → + (E1 ⊕ err) = E2 → + (Γ ⊢ₑ v : σ ⇑ E1) → + (Γ ⊢ₑ Throw err v : τ ⇑ E2) + + | typed_Catch Γ E E1 E2 err h v σ τ : + ETy err = σ → + (E1 ∪ (E2 ⊖ err)) = E → + (Γ ▹ σ ⊢ₑ h : τ ⇑ E1) → + (Γ ⊢ₑ v : τ ⇑ E2) → + (Γ ⊢ₑ Catch err v h : τ ⇑ E) + + where "Γ ⊢ₑ e : τ" := (typed Γ e τ) + and "Γ ⊢ᵥ v : τ" := (Γ ⊢ₑ (Val v) : τ). + + Reserved Notation "Γ '⊢ₖ' K ':' σ ⇒ τ" + (at level 70 + , K at level 60 + , σ at level 20 + , τ at level 20 + , no associativity + ). + + + Inductive typ_cont {S : Set} : (S → pty) → cont S → ty → ty → Prop := + | typed_END Γ τ1 τ2 : τ1 ⪍ τ2 → + (Γ ⊢ₖ END : τ1 ⇒ τ2) + | typed_IfK Γ e₁ e₂ K E1 E2 E3 E4 τ σ : + (E1 ∪ E2 ∪ E3) = E4 → + (Γ ⊢ₑ e₁ : σ ⇑ E2) → + (Γ ⊢ₑ e₂ : σ ⇑ E3) → + (Γ ⊢ₖ K : σ ⇑ E4 ⇒ τ) → + (Γ ⊢ₖ IfK e₁ e₂ K : ℕ ⇑ E1 ⇒ τ) + | typed_AppLK Γ E1 E2 E3 E4 v K σ τ α : + (E1 ∪ E2 ∪ E3) = E4 → + (Γ ⊢ᵥ v : σ ⇑ E3) → + (Γ ⊢ₖ K : τ ⇑ E4 ⇒ α) → + (Γ ⊢ₖ AppLK v K : ((σ ⟶ (τ ⇑ E1)) ⇑ E2) ⇒ α) + | typed_AppRK Γ E1 E2 E3 E4 e K σ τ α : + (E1 ∪ E2 ∪ E3) = E4 → + (Γ ⊢ₑ e : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → + (Γ ⊢ₖ K : (τ ⇑ E4) ⇒ α) → + (Γ ⊢ₖ AppRK e K : (σ ⇑ E3) ⇒ α) + | typed_NatOpLK Γ E1 E2 E3 op v K τ : + (E1 ∪ E2) = E3 → + (Γ ⊢ᵥ v : ℕ ⇑ E1) → + (Γ ⊢ₖ K : (ℕ ⇑ E3) ⇒ τ) → + (Γ ⊢ₖ NatOpLK op v K : (ℕ ⇑ E2) ⇒ τ) + | typed_NatOpRK Γ E1 E2 E3 op e K τ : + (E1 ∪ E2) = E3 → + (Γ ⊢ₑ e : ℕ ⇑ E1) → + (Γ ⊢ₖ K : ℕ ⇑ E3 ⇒ τ) → + (Γ ⊢ₖ NatOpRK op e K : (ℕ ⇑ E2) ⇒ τ) + | typed_ThrowK Γ E1 E2 err K σ τ α : + σ ≲ ETy err → + (E1 ⊕ err) = E2 → + (Γ ⊢ₖ K : (τ ⇑ E2) ⇒ α) → + (Γ ⊢ₖ ThrowK err K : (σ ⇑ E1) ⇒ α) + | typed_CatchK Γ E1 E2 E3 err h K σ τ τ' α : + ETy err ≲ σ → + τ' ≲ τ → + (E1 ∪ (E2 ⊖ err)) = E3 → + (Γ ▹ σ ⊢ₑ h : (τ ⇑ E1)) → + (Γ ⊢ₖ K : (τ ⇑ E3) ⇒ α) → + (Γ ⊢ₖ CatchK err h K : (τ' ⇑ E2) ⇒ α) + + where "Γ '⊢ₖ' K ':' σ ⇒ τ" := (typ_cont Γ K σ τ). + + + Definition typedConfig {S : Set} (Γ : S → pty) (c : @config S) (τ : ty) : Prop := + match c with + | Cexpr e => (Γ ⊢ₑ e : τ) + | Ceval e K => (Γ ⊢ₑ (fill K e) : τ) + | Ccont K v => (Γ ⊢ₑ (fill K (Val v)) : τ) + | Cret v => (Γ ⊢ᵥ v : τ) + end. + + Notation "Γ ⊢ᵢ c : τ" := (typedConfig Γ c τ) + (at level 70 + , c at level 60 + , τ at level 20 + , no associativity + ). + + Lemma weakening {S T : Set} : + ∀ (Γ : S → pty) (Δ : T → pty) (δ : S [→] T) (e : expr S) τ, + (Γ ⊢ₑ e : τ) → + (Δ • δ ≡ Γ) → + (Δ ⊢ₑ (fmap δ e) : τ). + Proof. + intros Γ Δ δ e τ Hty Hag. + generalize dependent T. + induction Hty; intros. + + constructor. specialize (Hag x). simpl in Hag. rewrite Hag. done. + + by constructor. + + econstructor; first done. + apply IHHty. + intros [|[|]]. + 1, 2 : done. + simpl. + apply Hag. + + eapply typed_App. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + + econstructor. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + + econstructor. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + eapply typed_Throw; try done. + by apply IHHty. + + econstructor; first done. + * eauto. + * apply IHHty1. + intros [|]; first done. + simpl. apply Hag. + * by apply IHHty2. + Qed. + + Lemma weakening_error {S : Set} : + ∀ (Γ : S → pty) (e : expr S) σ τ, + (Γ ⊢ₑ e : σ) → + σ ⪍ τ → + (Γ ⊢ₑ e : τ). + Proof. + intros Γ e [τ Eτ] σ Hty. + generalize dependent σ. + induction Hty; intros [σ' Eσ'] Hsub; inversion Hsub; subst. + + constructor. by eapply le_pty_trans. + + inversion H2. by constructor. + + econstructor; first by eapply le_pty_trans. done. + + econstructor. + * instantiate (3 := E1). + instantiate (2 := E2). + instantiate (1 := Eσ'). + set_solver. + * apply IHHty1. + constructor; last eauto. + constructor; first apply le_pty_refl. + by constructor. + * apply IHHty2. constructor; first apply le_pty_refl. + set_solver. + + inversion H3. subst. + econstructor. + * instantiate (2 := E1). instantiate (1 := Eσ'). set_solver. + * by apply IHHty1. + * apply IHHty2. constructor; first by apply le_pty_refl. set_solver. + + econstructor. + * instantiate (3 := E1). + instantiate (2 := E2). + instantiate (1 := Eσ'). + set_solver. + * apply IHHty1, le_ty_refl. + * apply IHHty2. + by constructor. + * apply IHHty3. constructor; first done. set_solver. + + econstructor. + * done. + * instantiate (1 := Eσ'). set_solver. + * apply IHHty. constructor; first apply le_pty_refl. set_solver. + + econstructor; first done. + * instantiate (1 := E2). instantiate (1 := Eσ'). set_solver. + * apply IHHty1. + constructor; first done. + set_solver. + * apply IHHty2. + by constructor. + Qed. + + Lemma weakening_sub {S: Set} : + ∀ (Γ : S → pty) (Δ : S → pty) (e : expr S) τ, + (Γ ⊢ₑ e : τ) → + (∀ x, Δ x ≲ Γ x) → + (Δ ⊢ₑ e : τ). + Proof. + intros Γ Δ e τ Hty Hag. + induction Hty; intros. + + constructor. eapply le_pty_trans; done. + + by constructor. + + econstructor; first done. + apply IHHty. + intros [|[|]]. + 1, 2 : term_simpl; apply le_pty_refl. + simpl. + apply Hag. + + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + eapply typed_Throw; try done. + by apply IHHty. + + econstructor; try done. + * apply IHHty1. + intros [|]. + { term_simpl. apply le_pty_refl. } + simpl. apply Hag. + * by apply IHHty2. + Qed. + + Lemma weakening_sub_cont {S: Set} : + ∀ (Γ : S → pty) (Δ : S → pty) (K : cont S) σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + (∀ x, Δ x ≲ Γ x) → + (Δ ⊢ₖ K : σ ⇒ τ). + Proof. + intros Γ Δ K σ τ Hty Hag. + induction Hty; intros. + + by constructor. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto. eapply weakening_sub; first done. + intros [|]; term_simpl. + { apply le_pty_refl. } + { apply Hag. } + Qed. + + Lemma substitution_lemma {S : Set}: + ∀ (e : expr S) E T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) + → (∀ (x : S), Δ ⊢ₑ γ x : Γ x ⇑ ∅%stdpp) + → ( Δ ⊢ₑ bind γ e : τ ⇑ E). + Proof. + - revert S. + intros S e E T Γ Δ γ τ Hty. + generalize dependent T. + induction Hty; intros. + + term_simpl. + subst. + eapply weakening_error; first done. + by constructor. + + term_simpl. constructor. + + term_simpl. econstructor; first done. + * apply IHHty. + intros [|[|]]. + { constructor. simpl. apply le_pty_refl. } + { constructor. apply le_pty_refl. } + term_simpl. + eapply (weakening (Δ ▹ σ ⟶ τ0)). + { eapply weakening; done. } + done. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + term_simpl. + econstructor; try done. + by apply IHHty. + + term_simpl. + econstructor; try done. + * apply IHHty1. + intros [|]. + { term_simpl. constructor. apply le_pty_refl. } + { term_simpl. eapply weakening; last done. apply H1. } + * by apply IHHty2. + Qed. + + Lemma weakening_cont {S T : Set} : + ∀ (Γ : S → pty) (Δ : T → pty) (δ : S [→] T) (K : cont S) σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + (Δ • δ ≡ Γ) → + (Δ ⊢ₖ (fmap δ K) : σ ⇒ τ). + Proof. + intros Γ Δ δ e σ τ Hty Hag. + generalize dependent T. + induction Hty; intros. + - term_simpl. by constructor. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + change (Val (fmap δ v)) with (fmap δ (Val v)). + by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + change (Val (fmap δ v)) with (fmap δ (Val v)). + by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : done. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + { done. } + { done. } + eapply weakening; first done. + intros [|]; first done. + apply Hag. + Qed. + + Lemma weakening_error_cont {S : Set} : + ∀ (Γ : S → pty) (K : cont S) σ1 σ2 τ1 τ2, + (Γ ⊢ₖ K : σ1 ⇒ τ1) → + σ2 ⪍ σ1 → + τ1 ⪍ τ2 → + (Γ ⊢ₖ K : σ2 ⇒ τ2). + Proof. + intros Γ K [σ1 Eσ1] σ2 [τ1 Eτ1] τ2 Hty. + revert σ2 τ2. + induction Hty; intros [σ' Eσ'] [ρ Eρ] Hσ Hτ. + - constructor. eapply le_ty_trans; first done. + by eapply le_ty_trans. + - inversion Hσ. subst. inversion H5. subst. + econstructor; last apply IHHty. + { set_solver. } + all : try done. + constructor; first by apply le_pty_refl. + set_solver. + - inversion Hσ. subst. inversion H4. subst. + inversion H5. subst. + econstructor; last apply IHHty. + { set_solver. } + 3 : done. + 1 : by eapply weakening_error. + constructor; first done. + set_solver. + + - inversion Hσ. subst. + econstructor; last eapply IHHty. + { set_solver. } + all : try done. + + eapply weakening_error; first done. + constructor; last done. + constructor; first done. + apply le_ty_refl. + + constructor; last set_solver. + apply le_pty_refl. + - inversion Hσ. subst. + inversion H4. subst. + econstructor; last by apply IHHty. + { instantiate (1 := E1 ∪ E2). set_solver. } + eapply weakening_error; first done. + constructor; first by apply le_pty_refl. + set_solver. + - inversion Hσ. subst. + inversion H4. subst. + econstructor; last by apply IHHty. + { instantiate (1 := E1 ∪ E2). set_solver. } + eapply weakening_error; first done. + constructor; first by apply le_pty_refl. + set_solver. + - inversion Hσ. subst. + econstructor; first by eapply le_pty_trans. + { done. } + apply IHHty. + + constructor; first by apply le_pty_refl. + set_solver. + + done. + - inversion Hσ. subst. + inversion Hτ. subst. + econstructor. + { done. } + { by eapply le_pty_trans. } + { done. } + { done. } + apply IHHty; last done. + constructor; first apply le_pty_refl. + set_solver. + Qed. + + Lemma fill_bind_bind {S T}: ∀ (δ : S [⇒] T) K e, fill (bind δ K) (bind δ e) = bind δ (fill K e). + Proof. + intros δ K. + revert δ. + induction K; first done; + term_simpl; intros; + change (BindCore_expr _ _ δ (fill K ?e) ) with (bind δ (fill K e)); + rewrite -IHK; + done. + Qed. + + Lemma fill_bind_subst {S}: ∀ (K : cont S) e e', fill K (subst e e') = subst (fill (shift K) e) e'. + Proof. + intros K. + induction K; + try done; + term_simpl; intros; + change (BindCore_expr _ _ (mk_subst ?e') (fill (shift K) ?e) ) with (subst (fill (shift K) e) e'); + rewrite -IHK; + term_simpl; try done. + repeat f_equal. + by rewrite subst_shift_id_lifted. + Qed. + + Lemma decomp_types {S} : ∀ (K : cont S) e Γ τ, (Γ ⊢ₑ fill K e : τ) + → ∃ α, (Γ ⊢ₑ e : α) ∧ (Γ ⊢ₖ K : α ⇒ τ). + Proof. + intros K. + induction K; + intros e' Γ τ Hty. + - exists τ. + split; first done. + constructor. + apply le_ty_refl. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + by econstructor. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + by econstructor. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; last done. + set_solver. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split. + + done. + + econstructor. + * apply le_pty_refl. + * reflexivity. + * done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; try done. + all: apply le_pty_refl. + Qed. + + Lemma fill_types {S : Set} : + ∀ (K : cont S) e Γ σ τ, + (Γ ⊢ₖ K : σ ⇒ τ ) → + (Γ ⊢ₑ e : σ) → + (Γ ⊢ₑ fill K e : τ). + Proof. + intros K. + induction K; intros e' Γ σ τ HK He'; inversion HK; subst. + { term_simpl. by eapply weakening_error. } + 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. set_solver. } + all: simpl; + eapply IHK; try done; + try econstructor; try done. + 2 : { eapply weakening_sub; first done. intros [|]; first done. + apply le_pty_refl. + } + all : by eapply weakening_error. + Qed. + + Lemma compose_END_left {S} : ∀ (K : cont S), cont_compose END K = K. + Proof. + intros K. + induction K. + { done. } + all : simpl; by rewrite IHK. + Qed. + + Lemma compose_type {S} : ∀ (K K1 K2 : cont S) Γ σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + K = cont_compose K1 K2 → + ∃ α, (Γ ⊢ₖ K1 : α ⇒ τ) ∧ (Γ ⊢ₖ K2 : σ ⇒ α). + Proof. + intros K K1 K2 Γ σ τ HK. + revert K1 K2. + induction HK; intros K1 K2 Heq. + { destruct K1, K2 ; try discriminate. + eexists. split; econstructor; try done. apply le_ty_refl. } + all: destruct K2; try discriminate; [ + simpl in Heq; subst; + eexists; split; econstructor; try done; apply le_ty_refl + | injection Heq; intros; subst; + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2); + eexists; split; first done; by econstructor]. + Qed. + + Lemma fewer_errors_catch {S} : + ∀ (K : cont S) Γ σ τ E1 E2 err, + (Γ ⊢ₖ K : (σ ⇑ E1) ⇒ (τ ⇑ E2)) → + err ∈ E1 ∧ err ∉ E2 → + ∃ K1 K2 h, K = cont_compose (CatchK err h K1) K2. + Proof. + intros K. + induction K; intros Γ σ τ E1 E2 err0 Hty [HE1 HE2]; inversion Hty; subst; + match goal with + | H : (Γ ⊢ₖ K : _ ⇒ _) |- ∃ _ _ _, (?C _) = _ => + apply (IHK _ _ _ _ _ err0) in H as (K1 & K2 & h & ->); + [by exists K1, (C K2), h | set_solver ] + | _ => idtac + end. + - inversion H. subst. contradict HE2. eauto. + - destruct (eq_dec err err0) as [-> | Hdiff]. + + by exists K, END, h. + + apply (IHK _ _ _ _ _ err0) in H10 as (K1 & K2 & h0 & ->). + * by exists K1, (CatchK err h K2), h0. + * split; last set_solver. + eapply elem_of_weaken; last done. + apply elem_of_union_r. + rewrite elem_of_difference. + split; first done. + by rewrite elem_of_singleton. + Qed. + + Lemma preservation_wk {S} : + ∀ Γ τ1 (c c' : @config S) n, + (Γ ⊢ᵢ c : τ1) → + c ===> c' / n → + ∃ τ2, τ2 ⪍ τ1 ∧ (Γ ⊢ᵢ c' : τ2). + Proof. + intros Γ τ c c' n Hty Hred. + revert Γ τ Hty. + inversion Hred; intros Γ [τ Eτ] Hty; simpl; eexists; try (split; try done; apply le_ty_refl). + - simpl in *. + split; last first. + + do 2 rewrite fill_bind_subst. + apply decomp_types in Hty as (α & Hα & HK). + inversion Hα. subst. + inversion H6. subst. + inversion H3. subst. + eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1))). + * eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1) ▹ σ0)). + -- eapply fill_types. + { eapply (weakening_cont (Γ ▹ (σ0 ⟶ τ1))). + { eapply weakening_cont. + 2 : instantiate (1 := Γ); done. + apply HK. + } + done. + } + eapply weakening_error; first by apply H4. + eapply le_ty_trans; first done. + constructor; first by apply le_pty_refl. + set_solver. + -- intros [|[|]]; term_simpl. + { unfold shift. + change (Val (fmap ?δ ?v)) with (fmap δ (Val v)). + eapply weakening; last by instantiate (1 := Γ). + inversion H8; subst. + + inversion H2. constructor. + + inversion H9. subst. inversion H2. subst. econstructor; last done. + constructor; first by eapply le_pty_trans. + by eapply le_ty_trans. + } + { constructor. apply le_pty_refl. } + { constructor. apply le_pty_refl. } + * intros [|]; term_simpl; first econstructor; try done. + { apply le_pty_refl. } + constructor. apply le_pty_refl. + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + destruct n0; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; set_solver. + + apply le_ty_refl. + - destruct v1, v2; try discriminate. + simpl in H. injection H as <-. + apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + constructor. + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + inversion Hα; subst. + { inversion H6. constructor. } + { econstructor; last done. by eapply le_pty_trans. } + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + apply unwind_decompose in H as (K1 & Hkcomp & HK1). + destruct (compose_type _ _ _ _ _ _ H10 Hkcomp) as (α & HK2 & HK3). + inversion HK2. subst. + split; first last. + + eapply fill_types; first last. + * eapply substitution_lemma; first done. + -- intros [|]; term_simpl. + { inversion Hα; subst. + - inversion H5. rewrite -H in H2. inversion H2. subst. constructor. + - inversion H6. subst. inversion H5. rewrite -H4 in H2. subst. inversion H2. subst. + econstructor; last done. + constructor. + + eapply le_pty_trans; first done. + by eapply le_pty_trans. + + eapply le_ty_trans; first done. + by eapply le_ty_trans. + } + constructor. + apply le_pty_refl. + * eapply weakening_error_cont; first done. + { constructor; first by apply le_pty_refl. set_solver. } + eapply le_ty_refl. + + eapply le_ty_refl. + Qed. + + Lemma preservation {S} : + ∀ Γ τ1 (c c' : @config S) n, + (Γ ⊢ᵢ c : τ1) → + c ===> c' / n → + (Γ ⊢ᵢ c' : τ1). + Proof. + intros. + apply (preservation_wk _ _ _ _ _ H) in H0 as (? & ? & ?). + destruct c'; by eapply weakening_error. + Qed. + + Lemma progress : ∀ (c : config) τ, (□ ⊢ᵢ c : τ ⇑ ∅%stdpp) → (∃ (v : val ∅), c = Cret v) ∨ (∃ c' n, c ===> c' / n). + Proof. + intros c τ Hty. + destruct c. + - right. eexists _, _. constructor. + - right. destruct c, v; try destruct v0; + try (apply decomp_types in Hty as (α & H1 & H2); + inversion H2; subst; + inversion H1; subst). + 1-3, 5-9,13,17,18 : eexists _, _; by constructor. + 6,7 : eapply (fewer_errors_catch _ _ _ _ _ _ err) in H8 as (K1 & K2 & h & HK); try (split; set_solver); + apply unwind_decompose_weak in HK as (? & ? & ?); + eexists _,_; + by constructor. + + inversion H5. + + inversion H8. inversion H5. + + inversion H5. + + inversion H5. + + inversion H5. + - destruct e; right. + 2 : by inversion Hty. + all : eexists _,_ ; try constructor. + - left. eexists. done. + Qed. + +Example confEX (err1 : exc) (err2 : exc) : (@config ∅) := + Ceval (Throw err1 (Throw err2 (Val (LitV 5)))) (CatchK err2 (Val (LitV 8)) END). + +Example typEX (err1 err2 : exc) (Hdiff : err1 <> err2) (Hty : ETy err2 = ℕ) : ∃ τ, (□ ⊢ᵢ (confEX err1 err2) : τ). +Proof. + eexists. + econstructor; first last. + - econstructor; first last. + + econstructor; first last. + * econstructor. + * reflexivity. + * done. + + reflexivity. + + reflexivity. + - econstructor. + - reflexivity. + - reflexivity. + Unshelve. + all : exact (∅%stdpp). +Qed. + +End Typing.