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 {Γ}{Δ}{ec}(lt:PCFJudg Γ Δ ec) : HaskType Γ ★ :=
 120     match lt with
 121       pcfjudg x y =>
 122       (mkGA (tensorizeType x) (tensorizeType y))
 123     end.
 124
 125   Definition obact {Γ}{Δ} ec (X:Tree ??(PCFJudg Γ Δ ec)) : Tree ??(LeveledHaskType Γ ★) :=
 126     mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
 127
 128   Hint Constructors Rule_Flat.
 129   Context {ndr:@ND_Relation _ Rule}.
 130
 131   (*
 132    * Here it is, what you've all been waiting for!  When reading this,
 133    * it might help to have the definition for "Inductive ND" (see
 134    * NaturalDeduction.v) handy as a cross-reference.
 135    *)
 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 _ _ )). auto.
 149
 150     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 151     apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
 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.
 161
 162     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
 163     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
 164       eapply nd_comp; [ apply nd_llecnac | idtac ].
 165       set (snd_initial(SequentND:=@pl_snd  _ _ _ _ (SystemFCa Γ Δ))
 166         (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
 167       eapply nd_comp.
 168       eapply nd_prod.
 169       apply q.
 170       apply q.
 171       apply nd_rule.
 172       eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
 173       auto.
 174       auto.
 175
 176     (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
 177     eapply nd_comp.
 178       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 179       apply nd_rule.
 180       eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
 181       auto.
 182
 183     (* nd_comp becomes pl_subst (aka nd_cut) *)
 184     eapply nd_comp.
 185       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 186       clear IHX1 IHX2 X1 X2.
 187       (*
 188       apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
 189       *)
 190       admit.
 191
 192     (* nd_cancell becomes RVar;;RuCanL *)
 193     eapply nd_comp;
 194       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
 195       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 196       auto.
 197
 198     (* nd_cancelr becomes RVar;;RuCanR *)
 199     eapply nd_comp;
 200       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
 201       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 202       auto.
 203
 204     (* nd_llecnac becomes RVar;;RCanL *)
 205     eapply nd_comp;
 206       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
 207       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 208       auto.
 209
 210     (* nd_rlecnac becomes RVar;;RCanR *)
 211     eapply nd_comp;
 212       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
 213       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 214       auto.
 215
 216     (* nd_assoc becomes RVar;;RAssoc *)
 217     eapply nd_comp;
 218       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 219       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 220       auto.
 221
 222     (* nd_cossa becomes RVar;;RCossa *)
 223     eapply nd_comp;
 224       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 225       apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
 226       auto.
 227
 228       destruct r as [r rp].
 229       refine (match rp as R in @Rule_PCF _ _ _ H C _ with
 230                 | PCF_RArrange         h c r q          => let case_RURule        := tt in _
 231                 | PCF_RLit             lit              => let case_RLit          := tt in _
 232                 | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
 233                 | PCF_RVar             σ                => let case_RVar          := tt in _
 234                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
 235                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
 236                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
 237                 | PCF_RJoin    b c d e          => let case_RJoin := tt in _
 238                 | PCF_RVoid                       => let case_RVoid   := tt in _
 239               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
 240               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
 241               end); simpl in *.
 242       clear rp.
 243       clear r h c.
 244       rename r0 into r; rename h0 into h; rename c0 into c.
 245
 246       destruct case_RURule.
 247         refine (match q with
 248           | RLeft   a b c r => let case_RLeft  := tt in _
 249           | RRight  a b c r => let case_RRight := tt in _
 250           | RCanL     b     => let case_RCanL  := tt in _
 251           | RCanR     b     => let case_RCanR  := tt in _
 252           | RuCanL    b     => let case_RuCanL := tt in _
 253           | RuCanR    b     => let case_RuCanR := tt in _
 254           | RAssoc    b c d => let case_RAssoc := tt in _
 255           | RCossa    b c d => let case_RCossa := tt in _
 256           | RExch     b c   => let case_RExch  := tt in _
 257           | RWeak     b     => let case_RWeak  := tt in _
 258           | RCont     b     => let case_RCont  := tt in _
 259           | RComp a b c f g => let case_RComp  := tt in _
 260         end).
 261
 262       destruct case_RCanL.
 263         (* ga_cancell *)
 264         admit.
 265
 266       destruct case_RCanR.
 267         (* ga_cancelr *)
 268         admit.
 269
 270       destruct case_RuCanL.
 271         (* ga_uncancell *)
 272         admit.
 273
 274       destruct case_RuCanR.
 275         (* ga_uncancelr *)
 276         admit.
 277
 278       destruct case_RAssoc.
 279         (* ga_assoc *)
 280         admit.
 281
 282       destruct case_RCossa.
 283         (* ga_unassoc *)
 284         admit.
 285
 286       destruct case_RExch.
 287         (* ga_swap *)
 288         admit.
 289
 290       destruct case_RWeak.
 291         (* ga_drop *)
 292         admit.
 293
 294       destruct case_RCont.
 295         (* ga_copy *)
 296         admit.
 297
 298       destruct case_RLeft.
 299         (* ga_second *)
 300         admit.
 301
 302       destruct case_RRight.
 303         (* ga_first *)
 304         admit.
 305
 306       destruct case_RComp.
 307         (* ga_comp *)
 308         admit.
 309
 310       destruct case_RLit.
 311         (* ga_literal *)
 312         admit.
 313
 314       (* hey cool, I figured out how to pass CoreNote's through... *)
 315       destruct case_RNote.
 316         eapply nd_comp.
 317         eapply nd_rule.
 318         eapply (org_fc _ _ (RVar _ _ _ _)) . auto.
 319         apply nd_rule.
 320         apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto.
 321
 322       destruct case_RVar.
 323         (* ga_id *)
 324         admit.
 325
 326       destruct case_RLam.
 327         (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
 328         admit.
 329
 330       destruct case_RApp.
 331         (* ga_apply *)
 332         admit.
 333
 334       destruct case_RLet.
 335         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
 336         admit.
 337
 338       destruct case_RVoid.
 339         (* ga_id u *)
 340         admit.
 341
 342       destruct case_RJoin.
 343         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
 344         admit.
 345
 346       Defined.
 347
 348   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
 349     { fmor := FlatteningFunctor_fmor }.
 350     admit.
 351     admit.
 352     admit.
 353     Defined.
 354 (*
 355     Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 356       refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 357       unfold ReificationFunctor_fmor; simpl.
 358       admit.
 359       unfold ReificationFunctor_fmor; simpl.
 360       admit.
 361       unfold ReificationFunctor_fmor; simpl.
 362       admit.
 363       Defined.
 364
 365
 366   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 367     refine {| plsmme_pl := PCF n Γ Δ |}.
 368     admit.
 369     Defined.
 370
 371   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 372     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 373     admit.
 374     Defined.
 375
 376   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 377     admit.
 378     Defined.
 379
 380   (* 5.1.4 *)
 381   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 382     admit.
 383     (*  ... and the retraction exists *)
 384     Defined.
 385 *)
 386   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 387    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 388   (*
 389   Definition HaskProof_to_SystemFCa :
 390     forall h c (pf:ND Rule h c),
 391       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 392       *)
 393
 394   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 395
 396 End HaskProofFlattener.
 397