CompilerExample

Compiler Example

This example illustrates the use of path-dependent types of length greater than one which allows us to encode recursion between types in nested modules

Require Import ExampleTactics.
Require Import String.

Section CompilerExample.

Variables DottyCore Tpe Symbol Any : typ_label.
Variables dottyCore types typeRef symbols symbol symb tpe denotation srcPos : trm_label.

Notation TpeImpl := (μ(typ_rcd {denotation Id})).
Notation SymbolImpl := (μ(typ_rcd {srcPos Id})).

Hypothesis AD: Any DottyCore.
Hypothesis TS: types symbols.
Hypothesis ST: symb denotation.
Hypothesis TS': tpe srcPos.

Notation typesType tpe_lower tpe_upper :=
  (typ_rcd {Tpe >: tpe_lower <: tpe_upper}
     typ_rcd {typeRef ∀(supersymbolsSymbol)
                         (superTpe (typ_rcd {symb ssupersymbolsSymbol}))}).
Notation symbolsType symb_lower symb_upper :=
  (typ_rcd {Symbol >: symb_lower <: symb_upper}
   typ_rcd {symbol ∀(supertypesTpe)
                      (superSymbol (typ_rcd {tpe ssupertypesTpe}))}).
Notation DottyCorePackage tpe_lower tpe_upper symb_lower symb_upper :=
  (typ_rcd {types μ(typesType tpe_lower tpe_upper)}
   typ_rcd {symbols μ(symbolsType symb_lower symb_upper)}).

Notation DottyCoreAbstract := (DottyCorePackage ).
Notation DottyCoreTight := (DottyCorePackage TpeImpl TpeImpl SymbolImpl SymbolImpl).

Definition t := (trm_val
(ν[thisAny]
  (typ_rcd {Any >: <: }
   typ_rcd {DottyCore >: μ DottyCoreAbstract <: μ DottyCoreAbstract}
   typ_rcd {dottyCore Lazy (super DottyCore)})
  defs_nil Λ
  {Any ⦂= } Λ
  {DottyCore ⦂= μ DottyCoreAbstract} Λ
  {dottyCore :=
     lazy (let_trm (trm_val (ν[ssuperAny](DottyCoreTight)
                              defs_nil Λ
                              {types :=
                                 defv (ν[sssuperAny](typesType TpeImpl TpeImpl)
                                        defs_nil Λ
                                        {Tpe ⦂= TpeImpl} Λ
                                        {typeRef :=
                                           defv (λ(supersymbolsSymbol)
                                                  (let_trm (trm_val (ν[sssssuperAny](typ_rcd {symb ({{ super }}) }
                                                                       typ_rcd {denotation Id})
                                                                      defs_nil Λ
                                                                      {symb := defp super} Λ
                                                                      {denotation := defv id})))) }) } Λ
                              {symbols :=
                                 defv (ν[sssuperAny](symbolsType SymbolImpl SymbolImpl)
                                        defs_nil Λ
                                        {Symbol ⦂= SymbolImpl} Λ
                                        {symbol :=
                                           defv (λ(supertypesTpe)
                                                  (let_trm (trm_val (ν[sssssuperAny](typ_rcd {tpe {{ super }}}
                                                                       typ_rcd {srcPos Id})
                                                                      defs_nil Λ
                                                                      {tpe := defp super} Λ
                                                                      {srcPos := defv id}))))})})))})).

Notation T :=
  (μ(typ_rcd {Any >: <: }
     typ_rcd {DottyCore >: μ DottyCoreAbstract <: μ DottyCoreAbstract}
     typ_rcd {dottyCore Lazy (super DottyCore)})).

Ltac solve_tag :=
  crush; eapply ty_sub; try solve [apply ty_var; eauto];
  eapply subtyp_trans; try solve [apply subtyp_top];
  apply subtyp_sel2 with (T := );
  eapply ty_sub; try solve [subst; apply ty_var; eauto];
  repeat (eapply subtyp_trans; apply subtyp_and11).

Lemma compiler_typecheck :
  empty t : T.
Proof.
  fresh_constructor. repeat apply ty_defs_cons; crush.
  - Case "dottyCore"%string.
    constructor. fresh_constructor. crush.
    fresh_constructor.
    + fresh_constructor. crush.
      apply ty_defs_cons; crush.
      × SCase "types"%string.
        apply ty_defs_one. eapply ty_def_new; eauto.
        { econstructor. constructor×. simpl. auto. }
        crush. apply ty_defs_cons; crush.

        constructor. fresh_constructor. crush. fresh_constructor.
        *** remember_ctx G.
            fresh_constructor. crush.
            apply ty_defs_cons; crush.
            **** apply ty_defs_one.
                 econstructor.
                 eapply ty_sub.
                 ***** rewrite HeqG. constructor×.
                 ***** eapply subtyp_sel1. rewrite proj_rewrite.
                 constructor. apply ty_rcd_intro.
                 eapply ty_sub. apply ty_rec_elim. constructor.
                 eapply ty_sub. rewrite HeqG. constructor×. eauto.
                 crush.
            **** constructor. fresh_constructor. crush.
            **** (* object tag *)
              solve_tag.
        *** match goal with
            | H: _ |- _ & ?y0 ¬ ?T0' & ?y1 ¬ ?T1' & ?y2 ¬ ?T2' _ : _
              remember T0' as T0; remember T1' as T1; remember T2' as T2
            end.
            remember_ctx G.
            assert (binds y2 T2 G) as Hb%ty_var by rewrite× HeqG. crush.
            apply ty_and_intro.
            **** rewrite proj_rewrite. eapply ty_sub.
                 2: {
                   eapply subtyp_sel2. eapply ty_sub. apply ty_rec_elim. constructor.
                   assert (binds y0 T0 G) as Hb'%ty_var by rewrite× HeqG.
                   rewrite HeqT0 in Hb'. eapply ty_sub; eauto.
                   unfold open_typ_p. rewrite HeqT1. simpl. eauto.
                 }
                 apply ty_rec_intro. crush.
                 rewrite HeqT2 in Hb. apply ty_rec_elim in Hb.
                 eapply ty_sub. eauto. crush.
            **** assert (binds y0 T0 G) as Hb' by rewrite× HeqG.
                 rewrite HeqT0 in Hb'. apply ty_var in Hb'.
                 match goal with
                 | H: _ tvar y0 : ?T0''' ?T0'' |- _
                   remember T0'' as T0'; remember T0''' as T01
                 end.
                 rewrite HeqT2 in Hb.
                 apply ty_rec_elim in Hb. unfold open_typ_p in Hb.
                 simpl in ×. rewrite HeqT1. rewrite proj_rewrite.
                 apply ty_rcd_intro.
                 eapply ty_sub.
                 2: {
                   eapply subtyp_sel2.
                   assert (G tvar y0 : T0') as Hy0 by eauto.
                   rewrite HeqT0' in Hy0. apply ty_new_elim in Hy0.
                   apply ty_rec_elim in Hy0. unfold open_typ_p in Hy0. simpl in ×.
                   eapply ty_sub. apply Hy0. crush.
                 }
                 eapply ty_sub. eapply ty_sngl. constructor. eapply ty_sub. apply Hb.
                 eauto. rewrite HeqG. constructor×. rewrite HeqT1.
                 eapply subtyp_sel1.
                 assert (G tvar y0 : T0') as Hy0 by eauto.
                 rewrite HeqT0' in Hy0. apply ty_new_elim, ty_rec_elim in Hy0.
                 unfold open_typ_p in Hy0. simpl in ×. eapply ty_sub.
                 apply Hy0. eauto.
        ***
          crush.
          Ltac clean_path_sel :=
            match goal with
            | |- _ trm_path (p_sel (avar_f ?y) (?a :: nil)) : _idtac y; idtac a;
              assert (HES: p_sel (avar_f y) (a :: nil) = (pvar y) a) by trivial;
              rewrite HES; clear HES
            end.
          clean_path_sel.
          eapply ty_sub.
          eapply ty_new_elim.
          Ltac solve_and_typing :=
            (apply subtyp_and12 || apply subtyp_and11).
          Ltac solve_object_typing :=
            crush; eapply ty_sub; try solve [subst; apply ty_var; eauto];
            solve_and_typing.
          solve_object_typing.
          eapply subtyp_trans; try solve [apply subtyp_top].
          apply subtyp_sel2 with (T := ).
          eapply ty_sub; try solve [subst; apply ty_var; eauto].
          repeat (eapply subtyp_trans; apply subtyp_and11).
      × eapply ty_def_new; eauto.
        { repeat econstructor. }
        crush. apply ty_defs_cons; crush.
        constructor. fresh_constructor. crush.
        fresh_constructor.
        *** remember_ctx G.
            fresh_constructor. crush.
            apply ty_defs_cons; crush.
            **** apply ty_defs_one.
                 econstructor.
                 eapply ty_sub.
                 ***** rewrite HeqG. constructor×.
                 ***** eapply subtyp_sel1. rewrite proj_rewrite.
                 constructor. apply ty_rcd_intro.
                 eapply ty_sub. apply ty_rec_elim. constructor.
                 eapply ty_sub. rewrite HeqG. constructor×. eauto. crush.
            **** constructor. fresh_constructor. crush.
            **** solve_tag.
        *** match goal with
            | H: _ |- _ & ?y0 ¬ ?T0' & ?y1 ¬ ?T1' & ?y2 ¬ ?T2' _ : _
              remember T0' as T0; remember T1' as T1; remember T2' as T2
            end.
            remember_ctx G.
            assert (binds y2 T2 G) as Hb%ty_var by rewrite× HeqG. crush.
            apply ty_and_intro.
            **** rewrite proj_rewrite. eapply ty_sub.
                 2: {
                   eapply subtyp_sel2. eapply ty_sub. apply ty_rec_elim. constructor.
                   assert (binds y0 T0 G) as Hb'%ty_var by rewrite× HeqG.
                   rewrite HeqT0 in Hb'. eapply ty_sub; eauto. crush.
                 }
                 apply ty_rec_intro. crush.
                 rewrite HeqT2 in Hb. apply ty_rec_elim in Hb.
                 eapply ty_sub. eauto. crush.
            **** assert (binds y0 T0 G) as Hb' by rewrite× HeqG.
                 rewrite HeqT0 in Hb'. apply ty_var in Hb'.
                 match goal with
                 | H: _ tvar y0 : ?T0''' ?T0'' |- _
                   remember T0'' as T01; remember T0''' as T0'
                 end.
                 rewrite HeqT2 in Hb.
                 apply ty_rec_elim in Hb. unfold open_typ_p in Hb.
                 simpl in ×. rewrite HeqT1. rewrite proj_rewrite.
                 apply ty_rcd_intro.
                 eapply ty_sub.
                 2: {
                   eapply subtyp_sel2.
                   assert (G tvar y0 : T0') as Hy0 by eauto.
                   rewrite HeqT0' in Hy0. apply ty_new_elim in Hy0.
                   apply ty_rec_elim in Hy0. unfold open_typ_p in Hy0. simpl in ×.
                   eapply ty_sub. apply Hy0. case_if. eauto.
                 }
                 eapply ty_sub. eapply ty_sngl. constructor. eapply ty_sub. apply Hb.
                 eauto. rewrite HeqG. constructor×. rewrite HeqT1.
                 eapply subtyp_sel1.
                 assert (G tvar y0 : T0') as Hy0 by eauto.
                 rewrite HeqT0' in Hy0. apply ty_new_elim, ty_rec_elim in Hy0.
                 unfold open_typ_p in Hy0. simpl in ×. eapply ty_sub.
                 apply Hy0. eauto.
        ***
          crush.
          clean_path_sel.
          eapply ty_sub.
          eapply ty_new_elim.
          solve_object_typing.
          eapply subtyp_trans; try solve [apply subtyp_top].
          apply subtyp_sel2 with (T := ).
          eapply ty_sub; try solve [subst; apply ty_var; eauto].
          repeat (eapply subtyp_trans; apply subtyp_and11).
      × solve_tag.
    + unfold open_trm. simpl. case_if.
      match goal with
      | H: _ |- ?G' & _ ¬ ?T0' _ : _
        remember G' as G; remember T0' as T0
      end.
      assert (binds y0 T0 (G & y0 ¬ T0)) as Hb%ty_var by auto.
      rewrite HeqT0 in Hb. apply ty_rec_elim in Hb.
      eapply ty_sub. 2: {
        repeat rewrite <- concat_assoc in HeqG.
        rewrite concat_empty_l in HeqG.
        match goal with
        | H: G = z ¬ ?Tz' & _ |- _
          remember Tz' as Tz
        end.
        assert (binds z Tz (G & y0 ¬ T0)) as Hz%ty_var. {
          rewrite HeqG. repeat eapply binds_concat_left; auto. apply binds_single_eq.
        }
        eapply subtyp_sel2. rewrite HeqTz in Hz.
        eapply ty_sub. apply Hz. eauto.
      }
      apply ty_rec_intro.
      unfold open_typ_p in ×. simpl in ×. repeat case_if.
      match goal with
      | H: _ trm_path (pvar y0) : ?U' ?U'' |- _
        remember U' as S; remember U'' as U
      end.
      apply ty_and_intro.
      × assert (G & y0 ¬ T0 tvar y0 : S) as Ht. {
          rewrite HeqS, HeqT0. eapply ty_sub. apply Hb. rewrite HeqS. eauto.
        }
        rewrite HeqS in Ht. apply ty_rcd_intro.
        apply ty_new_elim in Ht. apply ty_rec_intro. apply ty_rec_elim in Ht.
        unfold open_typ_p in ×. simpl in ×. case_if.
        apply ty_and_intro.
        ** eapply ty_sub.
           2: {
             apply subtyp_typ. apply subtyp_bot. apply subtyp_top.
           }
           eapply ty_sub. apply Ht. eauto.
        ** eapply ty_sub. apply Ht. eauto.
      × assert (G & y0 ¬ T0 tvar y0 : U) as Ht. {
          rewrite HeqU, HeqT0. eapply ty_sub. apply Hb. rewrite HeqU. eauto.
        }
        rewrite HeqU in Ht. apply ty_rcd_intro.
        apply ty_new_elim in Ht. apply ty_rec_intro. apply ty_rec_elim in Ht.
        unfold open_typ_p in ×. simpl in ×. case_if.
        apply ty_and_intro.
        ** eapply ty_sub.
           2: {
             apply subtyp_typ. apply subtyp_bot. apply subtyp_top.
           }
           eapply ty_sub. apply Ht. eauto.
        ** eapply ty_sub. apply Ht. eauto.
  - solve_tag.
  Unshelve. exact . exact \{}.
Qed.

End CompilerExample.