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 (*
  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 HaskProofFlattener.
  58
  59
  60 (*
  61   Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
  62     admit.
  63     Defined.
  64   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
  65       match t with
  66 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
  67         |                               _  => code2garrow0 ec unitType t
  68       end.
  69   Opaque code2garrow.
  70   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
  71       match ty as TY in RawHaskType _ K return RawHaskType TV K with
  72         | TCode ec t        => code2garrow _ ec t
  73         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
  74         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
  75         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
  76         | TVar   _ v        => TVar v
  77         | TArrow            => TArrow
  78         | TCon  tc          => TCon tc
  79         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
  80       end.
  81 *)
  82
  83
  84 (*
  85   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
  86       match t with
  87 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
  88         |                               _  => code2garrow0 ec unitType t
  89       end.
  90   Opaque code2garrow.
  91   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
  92       match ty as TY in RawHaskType _ K return RawHaskType TV K with
  93         | TCode ec t        => code2garrow _ ec t
  94         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
  95         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
  96         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
  97         | TVar   _ v        => TVar v
  98         | TArrow            => TArrow
  99         | TCon  tc          => TCon tc
 100         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 101       end.
 102
 103   Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★  :=
 104     match lht with
 105 (*      | t @@ nil       => (fun TV ite => typeMap (t TV ite)) @@ lev*)
 106       | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
 107     end.
 108 *)
 109
 110   (* gathers a tree of guest-language types into a single host-language types via the tensor *)
 111   Definition tensorizeType {Γ} (lt:Tree ??(HaskType Γ ★)) : HaskType Γ ★.
 112     admit.
 113     Defined.
 114
 115   Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
 116     admit.
 117     Defined.
 118
 119   Definition guestJudgmentAsGArrowType {Γ}{Δ}(lt:PCFJudg Γ Δ) : HaskType Γ ★ :=
 120     match lt with
 121       (x,y) => (mkGA (tensorizeType x) (tensorizeType y))
 122     end.
 123
 124   Definition obact {Γ}{Δ} (X:Tree ??(PCFJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
 125     mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
 126
 127   Hint Constructors Rule_Flat.
 128   Context {ndr:@ND_Relation _ Rule}.
 129
 130   (*
 131    * Here it is, what you've all been waiting for!  When reading this,
 132    * it might help to have the definition for "Inductive ND" (see
 133    * NaturalDeduction.v) handy as a cross-reference.
 134    *)
 135   Hint Constructors Rule_Flat.
 136   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
 137     : forall h c,
 138       (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) ->
 139       ((obact(Δ:=ec) h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact(Δ:=ec) c)).
 140
 141     set (@nil (HaskTyVar Γ ★)) as lev.
 142
 143     unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
 144
 145     induction X; simpl.
 146
 147     (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
 148     apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
 149
 150     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 151     apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
 152
 153     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
 154     eapply nd_comp;
 155       [ idtac
 156       | eapply nd_rule
 157       ; eapply (org_fc  _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
 158       ; auto ].
 159       eapply nd_rule.
 160       eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
 161       apply Flat_RArrange.
 162
 163     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
 164     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
 165       eapply nd_comp; [ apply nd_llecnac | idtac ].
 166       set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
 167         (mapOptionTree (guestJudgmentAsGArrowType(Δ:=ec)) h @@@ lev)) as q.
 168       eapply nd_comp.
 169       eapply nd_prod.
 170       apply q.
 171       apply q.
 172       apply nd_rule.
 173       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 174       destruct h; simpl.
 175       destruct o.
 176       simpl.
 177       apply Flat_RJoin.
 178       apply Flat_RJoin.
 179       apply Flat_RJoin.
 180       apply Flat_RArrange.
 181
 182     (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
 183     eapply nd_comp.
 184       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 185       apply nd_rule.
 186       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 187       apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
 188        (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
 189        (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
 190        (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
 191
 192     (* nd_comp becomes pl_subst (aka nd_cut) *)
 193     eapply nd_comp.
 194       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 195       clear IHX1 IHX2 X1 X2.
 196       (*
 197       apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
 198       *)
 199       admit.
 200
 201     (* nd_cancell becomes RVar;;RuCanL *)
 202     eapply nd_comp;
 203       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
 204       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 205       apply Flat_RArrange.
 206
 207     (* nd_cancelr becomes RVar;;RuCanR *)
 208     eapply nd_comp;
 209       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
 210       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 211       apply Flat_RArrange.
 212
 213     (* nd_llecnac becomes RVar;;RCanL *)
 214     eapply nd_comp;
 215       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
 216       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 217       apply Flat_RArrange.
 218
 219     (* nd_rlecnac becomes RVar;;RCanR *)
 220     eapply nd_comp;
 221       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
 222       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 223       apply Flat_RArrange.
 224
 225     (* nd_assoc becomes RVar;;RAssoc *)
 226     eapply nd_comp;
 227       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 228       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 229       apply Flat_RArrange.
 230
 231     (* nd_cossa becomes RVar;;RCossa *)
 232     eapply nd_comp;
 233       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 234       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 235       apply Flat_RArrange.
 236
 237       destruct r as [r rp].
 238       refine (match rp as R in @Rule_PCF _ _ _ H C _ with
 239                 | PCF_RArrange         h c r q          => let case_RURule        := tt in _
 240                 | PCF_RLit             lit              => let case_RLit          := tt in _
 241                 | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
 242                 | PCF_RVar             σ                => let case_RVar          := tt in _
 243                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
 244                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
 245                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
 246                 | PCF_RJoin    b c d e          => let case_RJoin := tt in _
 247                 | PCF_RVoid                       => let case_RVoid   := tt in _
 248               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
 249               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
 250               end); simpl in *.
 251       clear rp.
 252       clear r h c.
 253       rename r0 into r; rename h0 into h; rename c0 into c.
 254
 255       destruct case_RURule.
 256         refine (match q with
 257           | RLeft   a b c r => let case_RLeft  := tt in _
 258           | RRight  a b c r => let case_RRight := tt in _
 259           | RCanL     b     => let case_RCanL  := tt in _
 260           | RCanR     b     => let case_RCanR  := tt in _
 261           | RuCanL    b     => let case_RuCanL := tt in _
 262           | RuCanR    b     => let case_RuCanR := tt in _
 263           | RAssoc    b c d => let case_RAssoc := tt in _
 264           | RCossa    b c d => let case_RCossa := tt in _
 265           | RExch     b c   => let case_RExch  := tt in _
 266           | RWeak     b     => let case_RWeak  := tt in _
 267           | RCont     b     => let case_RCont  := tt in _
 268           | RComp a b c f g => let case_RComp  := tt in _
 269         end).
 270
 271       destruct case_RCanL.
 272         (* ga_cancell *)
 273         admit.
 274
 275       destruct case_RCanR.
 276         (* ga_cancelr *)
 277         admit.
 278
 279       destruct case_RuCanL.
 280         (* ga_uncancell *)
 281         admit.
 282
 283       destruct case_RuCanR.
 284         (* ga_uncancelr *)
 285         admit.
 286
 287       destruct case_RAssoc.
 288         (* ga_assoc *)
 289         admit.
 290
 291       destruct case_RCossa.
 292         (* ga_unassoc *)
 293         admit.
 294
 295       destruct case_RExch.
 296         (* ga_swap *)
 297         admit.
 298
 299       destruct case_RWeak.
 300         (* ga_drop *)
 301         admit.
 302
 303       destruct case_RCont.
 304         (* ga_copy *)
 305         admit.
 306
 307       destruct case_RLeft.
 308         (* ga_second *)
 309         admit.
 310
 311       destruct case_RRight.
 312         (* ga_first *)
 313         admit.
 314
 315       destruct case_RComp.
 316         (* ga_comp *)
 317         admit.
 318
 319       destruct case_RLit.
 320         (* ga_literal *)
 321         admit.
 322
 323       (* hey cool, I figured out how to pass CoreNote's through... *)
 324       destruct case_RNote.
 325         eapply nd_comp.
 326         eapply nd_rule.
 327         eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
 328         apply Flat_RVar.
 329         apply nd_rule.
 330         apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
 331         apply Flat_RNote.
 332
 333       destruct case_RVar.
 334         (* ga_id *)
 335         admit.
 336
 337       destruct case_RLam.
 338         (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
 339         admit.
 340
 341       destruct case_RApp.
 342         (* ga_apply *)
 343         admit.
 344
 345       destruct case_RLet.
 346         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
 347         admit.
 348
 349       destruct case_RVoid.
 350         (* ga_id u *)
 351         admit.
 352
 353       destruct case_RJoin.
 354         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
 355         admit.
 356
 357       Defined.
 358
 359   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
 360     { fmor := FlatteningFunctor_fmor }.
 361     admit.
 362     admit.
 363     admit.
 364     Defined.
 365
 366   (*
 367   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 368     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 369     unfold ReificationFunctor_fmor; simpl.
 370     admit.
 371     unfold ReificationFunctor_fmor; simpl.
 372     admit.
 373     unfold ReificationFunctor_fmor; simpl.
 374     admit.
 375     Defined.
 376
 377   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 378     refine {| plsmme_pl := PCF n Γ Δ |}.
 379     admit.
 380     Defined.
 381
 382   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 383     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 384     admit.
 385     Defined.
 386
 387   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 388     admit.
 389     Defined.
 390
 391   (* 5.1.4 *)
 392   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 393     admit.
 394     (*  ... and the retraction exists *)
 395     Defined.
 396   *)
 397   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 398    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 399   (*
 400   Definition HaskProof_to_SystemFCa :
 401     forall h c (pf:ND Rule h c),
 402       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 403       *)
 404   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 405
 406 End HaskProofFlattener.
 407