From 41a300e4605f2cc9520028199a727cff9bd61415 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 1 Aug 2024 12:03:52 +0200 Subject: [PATCH] Cleaned up the files in except lang --- theories/examples/except_lang/interp.v | 527 +------------------------ theories/examples/except_lang/lang.v | 132 ------- 2 files changed, 2 insertions(+), 657 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 2df5c3b..2584395 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -471,9 +471,6 @@ Module interp (Errors : ExcSig). with interp_val_ren {S S'} env (δ : S [→] S') (e : val S) : interp_val (fmap δ e) env ≡ interp_val e (ren_scope δ env). - (** with interp_cont_ren {S S'} env - (δ : S [→] S') (e : cont S) : - interp_cont (fmap δ e) env ≡ interp_cont e (ren_scope δ env). **) Proof. - destruct e; simpl. + by apply interp_val_ren. @@ -506,40 +503,8 @@ Module interp (Errors : ExcSig). destruct y' as [| [| y]]; simpl; first done. * by iRewrite - "IH". * done. - (* - destruct e; simpl; intros ?; simpl. - + reflexivity. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_expr_ren | by apply interp_expr_ren]. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. - + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. - + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. - + repeat f_equiv. by apply interp_cont_ren. - + repeat f_equiv; last done. - intro. - simpl. - destruct x0. - do 2 rewrite laterO_map_Next. - f_equiv. - simpl. - rewrite interp_expr_ren. - f_equiv. - intro. - destruct x0; done. *) Qed. -(* - Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : cont S): - interp_expr (fill K e) env ≡ (interp_cont K) env ((interp_expr e) env). - Proof. - revert env. - induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). - - repeat f_equiv. - by rewrite IHK. - - repeat f_equiv. - by rewrite IHK. - - repeat f_equiv. - by rewrite IHK. - Qed. -*) + Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') : interp_scope S := λne x, interp_expr (δ x) env. @@ -562,9 +527,6 @@ Module interp (Errors : ExcSig). with interp_val_subst {S S'} (env : interp_scope S') (δ : S [⇒] S') e : interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env). -(* with interp_cont_subst {S S'} (env : interp_scope S') - (δ : S [⇒] S') e : - interp_cont (bind δ e) env ≡ interp_cont e (sub_scope δ env). *) Proof. - destruct e; simpl. + by apply interp_val_subst. @@ -610,26 +572,6 @@ Module interp (Errors : ExcSig). iApply internal_eq_pointwise. iIntros (z). done. - (* - destruct e; simpl; intros ?; simpl. - + reflexivity. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_expr_subst | by apply interp_expr_subst]. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. - + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. - + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. - + repeat f_equiv. - by apply interp_cont_subst. - + repeat f_equiv; last done. - intros []. simpl. - do 2 rewrite laterO_map_Next. - f_equiv. simpl. - rewrite interp_expr_subst. - f_equiv. - intros []; simpl. - * done. - * rewrite interp_expr_ren. - f_equiv. - by intro. *) Qed. Lemma split_cont_decomp {S} K K1 K2 p t p1 t1 env h err f k: @@ -842,8 +784,7 @@ Module interp (Errors : ExcSig). + constructor. * repeat f_equiv. intro. simpl. - f_equiv. - f_equiv. (* Reflexivity doesn't work here, really funny, show Sergei *) + do 2 f_equiv. intro. simpl. done. @@ -971,7 +912,6 @@ Module interp (Errors : ExcSig). intro. simpl. done. } - simpl in HE0, HE1. - (** (interp_expr (subst h (Val v)) env), t) **) 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. @@ -1025,467 +965,4 @@ Module interp (Errors : ExcSig). constructor; done. Qed. - Theorem stuck {S} : ∀ c c' e σr σ n (env : interp_scope S), - interp_config c env = (e, σ) → - (∀ m e' σ', m > 0 → ¬ (ssteps (gReifiers_sReifier rs) - e (gState_recomp σr (sR_state σ)) - e' (gState_recomp σr (sR_state σ')) m)) → - c ===> c' / n → - n = 0. - intros c c' e σr σ n env Hc Hst Hred. - destruct n; first done. - exfalso. - destruct (interp_config c' env) as (e', σ') eqn:Hc'. - eapply (soundness _ _ _ _ σr _ _ _ _ Hc Hc') in Hred. - specialize (Hst (Datatypes.S n) e' σ'). - apply Hst; first lia. - apply Hred. - Qed. - - (** BOOKMARK **) - (** ** Interpretation of evaluation contexts induces homomorphism *) - - -(* - #[local] Instance interp_cont_hom_emp {S} env : - IT_hom (interp_cont (EmptyIK : cont S) env). - Proof. - simple refine (IT_HOM _ _ _ _ _); intros; auto. - simpl. fold (@idfun IT). f_equiv. intro. simpl. - by rewrite laterO_map_id. - Qed. - - #[local] Instance interp_cont_hom_if {S} - (K : cont S) (e1 e2 : expr S) env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (IfIK K e1 e2) env). - Proof. - intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -IF_Tick. do 3 f_equiv. apply hom_tick. - - assert ((interp_cont K env (Vis op i ko)) ≡ - (Vis op i (laterO_map (λne y, interp_cont K env y) ◎ ko))). - { by rewrite hom_vis. } - trans (IF (Vis op i (laterO_map (λne y : IT, interp_cont K env y) ◎ ko)) - (interp_expr e1 env) (interp_expr e2 env)). - { do 3 f_equiv. by rewrite hom_vis. } - rewrite IF_Vis. f_equiv. simpl. - intro. simpl. by rewrite -laterO_map_compose. - - trans (IF (Err e) (interp_expr e1 env) (interp_expr e2 env)). - { repeat f_equiv. apply hom_err. } - apply IF_Err. - Qed. - - #[local] Instance interp_cont_hom_appr {S} (K : cont S) - (e : expr S) env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppRIK e K) env). - Proof. - intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite !hom_tick. - - rewrite !hom_vis. f_equiv. intro x. simpl. - by rewrite laterO_map_compose. - - by rewrite !hom_err. - Qed. - - #[local] Instance interp_cont_hom_appl {S} (K : cont S) - (v : val S) (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppLIK K v) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -APP'_Tick_l. do 2 f_equiv. apply hom_tick. - - trans (APP' (Vis op i (laterO_map (interp_cont K env) ◎ ko)) - (interp_val v env)). - + do 2f_equiv. rewrite hom_vis. do 3 f_equiv. by intro. - + rewrite APP'_Vis_l. f_equiv. intro x. simpl. - by rewrite -laterO_map_compose. - - trans (APP' (Err e) (interp_val v env)). - { do 2f_equiv. apply hom_err. } - apply APP'_Err_l, interp_val_asval. - Qed. - - #[local] Instance interp_cont_hom_natopr {S} (K : cont S) - (e : expr S) op env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (NatOpRIK op e K) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite !hom_tick. - - rewrite !hom_vis. f_equiv. intro x. simpl. - by rewrite laterO_map_compose. - - by rewrite !hom_err. - Qed. - - #[local] Instance interp_cont_hom_natopl {S} (K : cont S) - (v : val S) op (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (NatOpLIK op K v) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -NATOP_ITV_Tick_l. do 2 f_equiv. apply hom_tick. - - trans (NATOP (do_natop op) - (Vis op0 i (laterO_map (interp_cont K env) ◎ ko)) - (interp_val v env)). - { do 2 f_equiv. rewrite hom_vis. f_equiv. by intro. } - rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl. - by rewrite -laterO_map_compose. - - trans (NATOP (do_natop op) (Err e) (interp_val v env)). - + do 2 f_equiv. apply hom_err. - + by apply NATOP_Err_l, interp_val_asval. - Qed. - - #[local] Instance interp_cont_hom_throw {S} (K : cont S) err (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (ThrowIK err K) env). - Proof. - Opaque THROW. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by do 2 rewrite hom_tick. - - do 2 rewrite hom_vis. f_equiv. by intro. - - by do 2 rewrite hom_err. - Qed. - - - #[global] Instance interp_cont_hom {S} (IK : cont S) env : - (∃ K, IK = cont_of_cont K) → - IT_hom (interp_cont IK env). - Proof. - intros [K ->]. - induction K; try apply _. - Qed. - - (** ** Finally, preservation of reductions *) - Lemma interp_expr_head_step {S : Set} (env : interp_scope S) (e : expr S) e' n : - head_step e e' (n, 0) → - interp_expr e env ≡ Tick_n n $ interp_expr e' env. - Proof. - inversion 1; cbn-[IF APP' INPUT Tick get_ret2]. - - (* app lemma *) - subst. - erewrite APP_APP'_ITV; last apply _. - trans (APP (Fun (Next (ir_unf (interp_expr e1) env))) (Next $ interp_val v2 env)). - { repeat f_equiv. apply interp_rec_unfold. } - rewrite APP_Fun. simpl. rewrite Tick_eq. do 2 f_equiv. - simplify_eq. - rewrite !interp_expr_subst. - f_equiv. - intros [| [| x]]; simpl; [| reflexivity | reflexivity]. - rewrite interp_val_ren. - f_equiv. - intros ?; simpl; reflexivity. - - (* the natop stuff *) - simplify_eq. - destruct v1,v2; try naive_solver. simpl in *. - rewrite NATOP_Ret. - destruct op; simplify_eq/=; done. - - rewrite IF_True; last lia. - reflexivity. - - rewrite IF_False; last lia. - reflexivity. - Qed. - - Lemma interp_expr_fill_no_reify {S} K (env : interp_scope S) (e e' : expr S) n : - head_step e e' (n, 0) → - interp_expr (fill (cont_of_cont K) e) env - ≡ - Tick_n n $ interp_expr (fill (cont_of_cont K) e') env. - Proof. - intros He. - rewrite !interp_comp. - erewrite <-hom_tick_n. - - apply (interp_expr_head_step env) in He. - rewrite He. - reflexivity. - - apply interp_cont_hom. exists K. done. - Qed. - - Opaque extend_scope. - Opaque Ret. - (** - Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) - (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : - head_step e e' (n, 1) → - reify (gReifiers_sReifier rs) - (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) - ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). - Proof. - intros Hst. - trans (reify (gReifiers_sReifier rs) (interp_cont K env (interp_expr e env)) - (gState_recomp σr (sR_state σ))). - { f_equiv. by rewrite interp_comp. } - inversion Hst; simplify_eq; cbn-[gState_recomp]. - - trans (reify (gReifiers_sReifier rs) (INPUT (interp_cont K env ◎ Ret)) (gState_recomp σr (sR_state σ))). - { - repeat f_equiv; eauto. - rewrite hom_INPUT. - do 2 f_equiv. by intro. - } - rewrite reify_vis_eq_ctx_indep //; first last. - { - epose proof (@subReifier_reify sz NotCtxDep reify_io rs _ IT _ (inl ()) () _ σ σ' σr) as H. - simpl in H. - simpl. - erewrite <-H; last first. - - rewrite H4. reflexivity. - - f_equiv; - solve_proper. - } - repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. - rewrite interp_comp. - rewrite ofe_iso_21. - simpl. - reflexivity. - - trans (reify (gReifiers_sReifier rs) (interp_cont K env (OUTPUT n0)) (gState_recomp σr (sR_state σ))). - { - do 3 f_equiv; eauto. - rewrite get_ret_ret//. - } - trans (reify (gReifiers_sReifier rs) (OUTPUT_ n0 (interp_cont K env (Ret 0))) (gState_recomp σr (sR_state σ))). - { - do 2 f_equiv; eauto. - by rewrite hom_OUTPUT_. - } - rewrite reify_vis_eq_ctx_indep //; last first. - { - epose proof (@subReifier_reify sz _ reify_io rs _ IT _ (inr (inl ())) n0 _ σ (update_output n0 σ) σr) as H. - simpl in H. - simpl. - erewrite <-H; last reflexivity. - f_equiv. - intros ???. by rewrite /prod_map H0. - } - repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. - rewrite interp_comp. - reflexivity. - Qed. - - Example test1 err : expr ∅ := - (try - (#4) + #5 - catch err => #1 - )%syn. - - Example test2 err : expr ∅ := - (try - #9 - catch err => #1 - )%syn. - - Example uu err σr : ∃ n m σ t, - ssteps (gReifiers_sReifier rs) - (interp_expr (test1 err) (λne (x : leibnizO ∅), match x with end) : IT) - (gState_recomp σr (sR_state σ)) - t - (gState_recomp σr (sR_state σ)) n ∧ - ssteps (gReifiers_sReifier rs) - (interp_expr (test2 err) (λne (x : leibnizO ∅), match x with end) : IT) - (gState_recomp σr (sR_state σ)) - t - (gState_recomp σr (sR_state σ)) m. - Proof. - rewrite /test1 /test2. - simpl. - do 2 eexists. - exists []. - eexists. - split. - - eapply ssteps_many. - + eapply sstep_reify. - { f_equiv. rewrite /ccompose /compose /=. reflexivity. }. - Check reify_vis_eq_ctx_dep. - apply reify_vis_eq_ctx_dep. - - - - Proof. - intros H. - unfold test1 in H. - unfold test2 in H. - simpl in H. - - Compute . - - Lemma soundness {S} (e1 e2 : expr S) (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : - prim_step e1 e2 (n,m) → ∀ σ1, ∃ σ2, - ssteps (gReifiers_sReifier rs) - (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) - (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) n. - Proof. - Opaque gState_decomp gState_recomp. - intros Hstep. - inversion Hstep;simplify_eq/=. - - intros σ1. - eexists. - rewrite !interp_comp. - - - - unshelve eapply (interp_expr_fill_no_reify K) in H2; first apply env. - rewrite H2. - rewrite interp_comp. - eapply ssteps_tick_n. - + inversion H2;subst. - * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. - rewrite interp_comp. - rewrite hom_INPUT. - change 1 with (Nat.add 1 0). econstructor; last first. - { apply ssteps_zero; reflexivity. } - eapply sstep_reify. - { Transparent INPUT. unfold INPUT. simpl. - f_equiv. reflexivity. } - simpl in H2. - rewrite -H2. - repeat f_equiv; eauto. - rewrite interp_comp hom_INPUT. - eauto. - * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. - rewrite interp_comp. simpl. - rewrite get_ret_ret. - rewrite hom_OUTPUT_. - change 1 with (Nat.add 1 0). econstructor; last first. - { apply ssteps_zero; reflexivity. } - eapply sstep_reify. - { Transparent OUTPUT_. unfold OUTPUT_. simpl. - f_equiv. reflexivity. } - simpl in H2. - rewrite -H2. - repeat f_equiv; eauto. - Opaque OUTPUT_. - rewrite interp_comp /= get_ret_ret hom_OUTPUT_. - eauto. - Qed. *) - (** - Section Examples. - Context `{!invGS Σ, !stateG rs R Σ}. - - Opaque CATCH. - - Example prog1 (err : exc) (n : nat) : expr ∅ := - (try - if #n then - throw err #5 - else #4 - catch err => ($0) * $0 - )%syn. - - Example wp_prog1 (err : exc) (n : nat) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ (⌜n = 0⌝ -∗ Φ (RetV 4)) ∗ (⌜n > 0⌝ -∗ Φ (RetV 25))) -∗ - WP@{rs} (interp_expr (prog1 err n) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - iIntros "Hσ H▷". - simpl. - destruct n. - - rewrite IF_False; last lia. - iApply (wp_catch_v _ _ (Ret 4) _ _ _ idfun with "Hσ"). - + by simpl. - + iIntros "!> H£ Hσ". - iPoseProof ("H▷" with "H£ Hσ") as "[HΦ _]". - iApply wp_val. - iModIntro. - by iApply "HΦ". - - rewrite IF_True; last lia. - iApply (wp_catch_throw _ _ (Ret 5) idfun idfun with "Hσ"). - + simpl. - rewrite laterO_map_Next. - simpl. - rewrite NATOP_Ret. - by simpl. - + simpl. - iIntros "!> H£ Hσ". - iPoseProof ("H▷" with "H£ Hσ") as "[_ HΦ]". - iApply wp_val. - iModIntro. - iApply "HΦ". - iPureIntro. - lia. - Qed. - - Example prog2 (err : exc) : expr ∅ := - (if ( - try - throw err #3 - catch err => ($0) * #4 - ) - then #1 - else #0 - )%syn. - - Example wp_prog2 (err : exc) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 1)) -∗ - WP@{rs} (interp_expr (prog2 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - iIntros "Hσ H▷". - simpl. - iApply (wp_catch_throw _ _ (Ret 3) idfun (λne x, IF x (Ret 1) (Ret 0)) with "Hσ"). - - simpl. - rewrite laterO_map_Next /=. - rewrite NATOP_Ret. - by simpl. - - simpl. - iIntros "!>H£ Hσ". - rewrite IF_True; last lia. - iApply wp_val. - iModIntro. - iApply ("H▷" with "H£ Hσ"). - Qed. - - Example prog3 (err : exc) : expr ∅ := - (try - (if ( - throw err #3 - ) - then #1 - else #0) - catch err => ($0) * #4 - )%syn. - - Example wp_prog3 (err : exc) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 12)) -∗ - WP@{rs} (interp_expr (prog3 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - iIntros "Hσ H▷". - simpl. - iApply (wp_catch_throw _ _ (Ret 3) (λne x, IF x (Ret 1) (Ret 0)) idfun with "Hσ"). - - by rewrite laterO_map_Next /= NATOP_Ret /=. - - iIntros "!> H£ Hσ". - iApply wp_val. - by iApply ("H▷" with "H£ Hσ"). - Qed. - - Example prog4 (err1 err2 : exc) : expr ∅ := - (try - try - throw err1 #3 - catch err2 => ($0) + $0 - catch err1 => ($0) * $0 - )%syn. - - Example wp_prog4 (err1 err2 : exc) (Herr : err1 <> err2) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 9)) -∗ - WP@{rs} (interp_expr (prog4 err1 err2) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - Opaque _REG. - iIntros "Hσ H▷". - simpl. - iApply (wp_reg _ _ err1 _ idfun with "Hσ"). - { reflexivity. } - iIntros "!> H£ Hσ". - iApply (wp_reg _ _ _ _ (get_val _) with "Hσ"). - { reflexivity. } - iIntros "!> H£' Hσ". - iApply (wp_throw _ _ _ _ _ _ _ (get_val _) with "Hσ"). - 3: change (?a :: ?b :: σ) with ([a] ++ b::σ); reflexivity. - { constructor; first done. constructor. } - { by rewrite laterO_map_Next /= NATOP_Ret /=. } - iIntros "!> H£'' Hσ". - iApply wp_val. - iModIntro. - iApply ("H▷" with "H£ Hσ"). - Qed. - - End Examples. -**) *) End interp. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index fe0c89f..682bf42 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -638,136 +638,4 @@ Proof. rewrite /Inj; naive_solver. Qed. -(** TODO LATER - -Declare Scope syn_scope. -Delimit Scope syn_scope with syn. - -Coercion Val : val >-> expr. - -Coercion App : expr >-> Funclass. -Coercion AppLK : val >-> Funclass. -Coercion AppRK : expr >-> Funclass. - - -(* XXX: We use these typeclasses to share the notation between the -expressions and the evaluation contexts, for readability. It will be -good to also share the notation between different languages. *) - -Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. - -Arguments __asSynExpr {_} {_} {_}. - -Global Instance AsSynExprValue : AsSynExpr val := { - __asSynExpr _ v := Val v - }. -Global Instance AsSynExprExpr : AsSynExpr expr := { - __asSynExpr _ e := e - }. - -Class OpNotation (A B C D : Type) := { __op : A -> B -> C -> D }. - -Global Instance OpNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : OpNotation (F S) nat_op (G S) (expr S) := { - __op e₁ op e₂ := NatOp op (__asSynExpr e₁) (__asSynExpr e₂) - }. - -Global Instance OpNotationLK {S : Set} : OpNotation (cont S) (nat_op) (val S) (cont S) := { - __op K op v := NatOpRK op K v - }. - -Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : OpNotation (F S) (nat_op) (cont S) (cont S) := { - __op e op K := NatOpLK op (__asSynExpr e) K - }. - -Class IfNotation (A B C D : Type) := { __if : A -> B -> C -> D }. - -Global Instance IfNotationExpr {S : Set} {F G H : Set -> Type} `{AsSynExpr F, AsSynExpr G, AsSynExpr H} : IfNotation (F S) (G S) (H S) (expr S) := { - __if e₁ e₂ e₃ := If (__asSynExpr e₁) (__asSynExpr e₂) (__asSynExpr e₃) - }. - -Global Instance IfNotationK {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : IfNotation (cont S) (F S) (G S) (cont S) := { - __if K e₂ e₃ := IfK K (__asSynExpr e₂) (__asSynExpr e₃) - }. - -Class AppNotation (A B C : Type) := { __app : A -> B -> C }. - -Global Instance AppNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppNotation (F S) (G S) (expr S) := { - __app e₁ e₂ := App (__asSynExpr e₁) (__asSynExpr e₂) - }. - -Global Instance AppNotationLK {S : Set} : AppNotation (cont S) (val S) (cont S) := { - __app K v := AppLK K v - }. - -Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := { - __app e K := AppRK (__asSynExpr e) K - }. - -Class ThrowNotation (A B : Type) := { __throw : exc -> A -> B}. - -Global Instance ThrowNotationExpr {S : Set} {F: Set -> Type} `{AsSynExpr F} : ThrowNotation (F S) (expr S) := - { - __throw e v := Throw e (__asSynExpr v) - }. - -Global Instance ThrowNotationK {S : Set} : ThrowNotation (cont S) (cont S) := - { - __throw e K := ThrowK e K - }. - -Class CatchNotation (A B C : Type) := - { - __catch : exc -> A -> B -> C - }. - -Global Instance CatchNotationExpr {S : Set} (F G : Set -> Type) `{AsSynExpr F} `{AsSynExpr G} : CatchNotation (F S) (G (inc S)) (expr S) := - { - __catch err b h := Catch err (__asSynExpr b) (__asSynExpr h) - }. - -Global Instance CatchNotationK {S : Set} (F : Set -> Type) `{AsSynExpr F} : CatchNotation (cont S) (F (inc S)) (cont S) := - { - __catch err K h := CatchK err K (__asSynExpr h) - }. - - -Notation of_val := Val (only parsing). - -Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope. -Notation "x '+' y" := (__op x%syn Add y%syn) : syn_scope. -Notation "x '-' y" := (__op x%syn Sub y%syn) : syn_scope. -Notation "x '*' y" := (__op x%syn Mult y%syn) : syn_scope. -Notation "'if' x 'then' y 'else' z" := (__if x%syn y%syn z%syn) : syn_scope. -Notation "'#' n" := (LitV n) (at level 60) : syn_scope. -Notation "'rec' e" := (RecV e%syn) (at level 60) : syn_scope. -Notation "'$' fn" := (set_pure_resolver fn) (at level 60) : syn_scope. -Notation "'try' b 'catch' err '=>' h" := - (__catch err b%syn h%syn) (at level 60) : syn_scope. -Notation "'throw' err v" := - (__throw err v%syn) (at level 60) : syn_scope. -Notation "□" := (EmptyK) : syn_scope. -Notation "K '⟪' e '⟫'" := (fill K%syn e%syn) (at level 60) : syn_scope. - -Definition LamV {S : Set} (e : expr (inc S)) : val S := - RecV (shift e). - -Notation "'λ' . e" := (LamV e%syn) (at level 60) : syn_scope. - -Definition LetE {S : Set} (e : expr S) (e' : expr (inc S)) : expr S := - App (LamV e') (e). - -Notation "'let_' e₁ 'in' e₂" := (LetE e₁%syn e₂%syn) (at level 60, right associativity) : syn_scope. - -Definition SeqE {S : Set} (e e' : expr S) : expr S := - App (LamV (shift e)) e'. - -Notation "e₁ ';;' e₂" := (SeqE e₁%syn e₂%syn) : syn_scope. - -Declare Scope typ_scope. -Delimit Scope typ_scope with typ. - -Notation "'ℕ'" := (Tnat) (at level 1) : typ_scope. -Notation "A →ₜ B" := (Tarr A%typ B%typ) - (right associativity, at level 60) : typ_scope. -**) End Lang.