src/HaskProofFlattener.v

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