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