src/HaskFlattener.v

   1 (*********************************************************************************************************************************)
   2 (* HaskFlattener:                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*    The Flattening Functor.                                                                                                    *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskLiteralsAndTyCons.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskProof.
  20 Require Import NaturalDeduction.
  21 Require Import NaturalDeductionCategory.
  22
  23 Require Import Algebras_ch4.
  24 Require Import Categories_ch1_3.
  25 Require Import Functors_ch1_4.
  26 Require Import Isomorphisms_ch1_5.
  27 Require Import ProductCategories_ch1_6_1.
  28 Require Import OppositeCategories_ch1_6_2.
  29 Require Import Enrichment_ch2_8.
  30 Require Import Subcategories_ch7_1.
  31 Require Import NaturalTransformations_ch7_4.
  32 Require Import NaturalIsomorphisms_ch7_5.
  33 Require Import BinoidalCategories.
  34 Require Import PreMonoidalCategories.
  35 Require Import MonoidalCategories_ch7_8.
  36 Require Import Coherence_ch7_8.
  37
  38 Require Import HaskStrongTypes.
  39 Require Import HaskStrong.
  40 Require Import HaskProof.
  41 Require Import HaskStrongToProof.
  42 Require Import HaskProofToStrong.
  43 Require Import ProgrammingLanguage.
  44 Require Import HaskProgrammingLanguage.
  45 Require Import PCF.
  46
  47 Open Scope nd_scope.
  48
  49 (*
  50  *  The flattening transformation.  Currently only TWO-level languages are
  51  *  supported, and the level-1 sublanguage is rather limited.
  52  *
  53  *  This file abuses terminology pretty badly.  For purposes of this file,
  54  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  55  *  the whole language (level-0 language including bracketed level-1 terms)
  56  *)
  57 Section HaskFlattener.
  58
  59   Context {Γ:TypeEnv}.
  60   Context {Δ:CoercionEnv Γ}.
  61   Context {ec:HaskTyVar Γ ★}.
  62
  63   Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev).
  64     intros.
  65     rewrite <- mapOptionTree_compose.
  66     simpl.
  67     induction x.
  68     destruct a; simpl; auto.
  69     simpl.
  70     rewrite IHx1 at 1.
  71     rewrite IHx2 at 1.
  72     reflexivity.
  73     Qed.
  74
  75   Context (ga_rep      : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ).
  76   Context (ga_type     : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★).
  77
  78   (*Notation "a ~~~~> b" := (ND Rule [] [ Γ > Δ > a |- b ]) (at level 20).*)
  79   Notation "a ~~~~> b" := (ND (OrgR Γ Δ) [] [ (a , b) ]) (at level 20).
  80
  81   Lemma magic : forall a b c,
  82     ([]                   ~~~~> [ga_type a b @@ nil]) ->
  83     ([ga_type b c @@ nil] ~~~~> [ga_type a c @@ nil]).
  84     admit.
  85     Qed.
  86
  87   Context (ga_lit      : ∀ lit, [] ~~~~> [ga_type (ga_rep   []   )      (ga_rep [literalType lit])@@ nil]).
  88   Context (ga_id       : ∀ σ,   [] ~~~~> [ga_type (ga_rep   σ    )      (ga_rep σ                )@@ nil]).
  89   Context (ga_cancell  : ∀ c  , [] ~~~~> [ga_type (ga_rep ([],,c))      (ga_rep c                )@@ nil]).
  90   Context (ga_cancelr  : ∀ c  , [] ~~~~> [ga_type (ga_rep (c,,[]))      (ga_rep c                )@@ nil]).
  91   Context (ga_uncancell: ∀ c  , [] ~~~~> [ga_type (ga_rep  c     )      (ga_rep ([],,c)          )@@ nil]).
  92   Context (ga_uncancelr: ∀ c  , [] ~~~~> [ga_type (ga_rep  c     )      (ga_rep (c,,[])          )@@ nil]).
  93   Context (ga_assoc    : ∀ a b c,[] ~~~~> [ga_type (ga_rep ((a,,b),,c))  (ga_rep (a,,(b,,c))      )@@ nil]).
  94   Context (ga_unassoc  : ∀ a b c,[] ~~~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c))      @@ nil]).
  95   Context (ga_swap     : ∀ a b, [] ~~~~> [ga_type (ga_rep (a,,b) )      (ga_rep (b,,a)           )@@ nil]).
  96   Context (ga_copy     : ∀ a  , [] ~~~~> [ga_type (ga_rep  a     )      (ga_rep (a,,a)           )@@ nil]).
  97   Context (ga_drop     : ∀ a  , [] ~~~~> [ga_type (ga_rep  a     )      (ga_rep []               )@@ nil]).
  98   Context (ga_first    : ∀ a b c,
  99     [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]).
 100   Context (ga_second   : ∀ a b c,
 101     [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]).
 102   Context (ga_comp     : ∀ a b c,
 103     ([ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil])
 104     ~~~~>
 105     [ga_type (ga_rep a) (ga_rep c) @@nil]).
 106
 107   Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ :=
 108     match lt with
 109       (x,y) => (ga_type (ga_rep x) (ga_rep y))
 110     end.
 111
 112   Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) :=
 113     mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
 114
 115   Hint Constructors Rule_Flat.
 116   Context {ndr:@ND_Relation _ Rule}.
 117
 118   (*
 119    * Here it is, what you've all been waiting for!  When reading this,
 120    * it might help to have the definition for "Inductive ND" (see
 121    * NaturalDeduction.v) handy as a cross-reference.
 122    *)
 123   Hint Constructors Rule_Flat.
 124   Definition FlatteningFunctor_fmor
 125     : forall h c,
 126       (ND (PCFRule Γ Δ ec) h c) ->
 127       ((obact h)~~~~>(obact c)).
 128
 129     set (@nil (HaskTyVar Γ ★)) as lev.
 130
 131     unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
 132
 133     induction X; simpl.
 134
 135     (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
 136     apply nd_rule; apply (org_fc Γ Δ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
 137
 138     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 139     apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
 140
 141     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
 142     eapply nd_comp;
 143       [ idtac
 144       | eapply nd_rule
 145       ; eapply (org_fc  _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
 146       ; auto ].
 147       eapply nd_rule.
 148       eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
 149       apply Flat_RArrange.
 150
 151     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
 152     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
 153       eapply nd_comp; [ apply nd_llecnac | idtac ].
 154       set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
 155         (mapOptionTree (guestJudgmentAsGArrowType) h @@@ lev)) as q.
 156       eapply nd_comp.
 157       eapply nd_prod.
 158       apply q.
 159       apply q.
 160       apply nd_rule.
 161       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 162       destruct h; simpl.
 163       destruct o.
 164       simpl.
 165       apply Flat_RJoin.
 166       apply Flat_RJoin.
 167       apply Flat_RJoin.
 168       apply Flat_RArrange.
 169
 170     (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
 171     eapply nd_comp.
 172       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 173       apply nd_rule.
 174       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 175       apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
 176        (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
 177        (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
 178        (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
 179
 180     (* nd_comp becomes pl_subst (aka nd_cut) *)
 181     eapply nd_comp.
 182       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 183       clear IHX1 IHX2 X1 X2.
 184       apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
 185
 186     (* nd_cancell becomes RVar;;RuCanL *)
 187     eapply nd_comp;
 188       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
 189       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 190       apply Flat_RArrange.
 191
 192     (* nd_cancelr becomes RVar;;RuCanR *)
 193     eapply nd_comp;
 194       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
 195       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 196       apply Flat_RArrange.
 197
 198     (* nd_llecnac becomes RVar;;RCanL *)
 199     eapply nd_comp;
 200       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
 201       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 202       apply Flat_RArrange.
 203
 204     (* nd_rlecnac becomes RVar;;RCanR *)
 205     eapply nd_comp;
 206       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
 207       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 208       apply Flat_RArrange.
 209
 210     (* nd_assoc becomes RVar;;RAssoc *)
 211     eapply nd_comp;
 212       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 213       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 214       apply Flat_RArrange.
 215
 216     (* nd_cossa becomes RVar;;RCossa *)
 217     eapply nd_comp;
 218       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 219       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 220       apply Flat_RArrange.
 221
 222       destruct r as [r rp].
 223       rename h into h'.
 224       rename c into c'.
 225       rename r into r'.
 226
 227       refine (match rp as R in @Rule_PCF _ _ _ H C _
 228                 return
 229                 ND (OrgR Γ Δ) []
 230                 [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
 231                   (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
 232                 with
 233                 | PCF_RArrange         h c r q          => let case_RURule        := tt in _
 234                 | PCF_RLit             lit              => let case_RLit          := tt in _
 235                 | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
 236                 | PCF_RVar             σ                => let case_RVar          := tt in _
 237                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
 238                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
 239                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
 240                 | PCF_RJoin    b c d e          => let case_RJoin := tt in _
 241                 | PCF_RVoid                       => let case_RVoid   := tt in _
 242               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
 243               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
 244               end); simpl in *.
 245       clear rp h' c' r'.
 246
 247       rewrite (unlev_lemma h (ec::nil)).
 248       rewrite (unlev_lemma c (ec::nil)).
 249       destruct case_RURule.
 250         refine (match q as Q in Arrange H C
 251                 return
 252                 H=(h @@@ (ec :: nil)) ->
 253                 C=(c @@@ (ec :: nil)) ->
 254                 ND (OrgR Γ Δ) []
 255                 [sequent
 256                   [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
 257                   [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
 258                   with
 259           | RLeft   a b c r => let case_RLeft  := tt in _
 260           | RRight  a b c r => let case_RRight := tt in _
 261           | RCanL     b     => let case_RCanL  := tt in _
 262           | RCanR     b     => let case_RCanR  := tt in _
 263           | RuCanL    b     => let case_RuCanL := tt in _
 264           | RuCanR    b     => let case_RuCanR := tt in _
 265           | RAssoc    b c d => let case_RAssoc := tt in _
 266           | RCossa    b c d => let case_RCossa := tt in _
 267           | RExch     b c   => let case_RExch  := tt in _
 268           | RWeak     b     => let case_RWeak  := tt in _
 269           | RCont     b     => let case_RCont  := tt in _
 270           | RComp a b c f g => let case_RComp  := tt in _
 271         end (refl_equal _) (refl_equal _));
 272         intros; simpl in *;
 273         subst;
 274         try rewrite <- unlev_lemma in *.
 275
 276       destruct case_RCanL.
 277         apply magic.
 278         apply ga_uncancell.
 279
 280       destruct case_RCanR.
 281         apply magic.
 282         apply ga_uncancelr.
 283
 284       destruct case_RuCanL.
 285         apply magic.
 286         apply ga_cancell.
 287
 288       destruct case_RuCanR.
 289         apply magic.
 290         apply ga_cancelr.
 291
 292       destruct case_RAssoc.
 293         apply magic.
 294         apply ga_assoc.
 295
 296       destruct case_RCossa.
 297         apply magic.
 298         apply ga_unassoc.
 299
 300       destruct case_RExch.
 301         apply magic.
 302         apply ga_swap.
 303
 304       destruct case_RWeak.
 305         apply magic.
 306         apply ga_drop.
 307
 308       destruct case_RCont.
 309         apply magic.
 310         apply ga_copy.
 311
 312       destruct case_RLeft.
 313         apply magic.
 314         (*apply ga_second.*)
 315         admit.
 316
 317       destruct case_RRight.
 318         apply magic.
 319         (*apply ga_first.*)
 320         admit.
 321
 322       destruct case_RComp.
 323         apply magic.
 324         (*apply ga_comp.*)
 325         admit.
 326
 327       destruct case_RLit.
 328         apply ga_lit.
 329
 330       (* hey cool, I figured out how to pass CoreNote's through... *)
 331       destruct case_RNote.
 332         eapply nd_comp.
 333         eapply nd_rule.
 334         eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
 335         apply Flat_RVar.
 336         apply nd_rule.
 337         apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
 338         apply Flat_RNote.
 339
 340       destruct case_RVar.
 341         apply ga_id.
 342
 343       (*
 344        *   class GArrow g (**) u => GArrowApply g (**) u (~>) where
 345        *     ga_applyl    :: g (x**(x~>y)   ) y
 346        *     ga_applyr    :: g (   (x~>y)**x) y
 347        *
 348        *   class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 349        *     ga_curryl    :: g (x**y) z  ->  g x (y~>z)
 350        *     ga_curryr    :: g (x**y) z  ->  g y (x~>z)
 351        *)
 352       destruct case_RLam.
 353         (* GArrowCurry.ga_curry *)
 354         admit.
 355
 356       destruct case_RApp.
 357         (* GArrowApply.ga_apply *)
 358         admit.
 359
 360       destruct case_RLet.
 361         admit.
 362
 363       destruct case_RVoid.
 364         apply ga_id.
 365
 366       destruct case_RJoin.
 367         (* this assumes we want effects to occur in syntactically-left-to-right order *)
 368         admit.
 369         Defined.
 370
 371 (*
 372   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
 373     { fmor := FlatteningFunctor_fmor }.
 374     Admitted.
 375
 376   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 377     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 378     Admitted.
 379
 380   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 381     refine {| plsmme_pl := PCF n Γ Δ |}.
 382     admit.
 383     Defined.
 384
 385   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 386     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 387     admit.
 388     Defined.
 389
 390   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 391     admit.
 392     Defined.
 393
 394   (* 5.1.4 *)
 395   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 396     admit.
 397     Defined.
 398 *)
 399   (*  ... and the retraction exists *)
 400
 401 End HaskFlattener.
 402