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