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 (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (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       apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))).
 188
 189     (* nd_cancell becomes RVar;;RuCanL *)
 190     eapply nd_comp;
 191       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
 192       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 193       auto.
 194
 195     (* nd_cancelr becomes RVar;;RuCanR *)
 196     eapply nd_comp;
 197       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
 198       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 199       auto.
 200
 201     (* nd_llecnac becomes RVar;;RCanL *)
 202     eapply nd_comp;
 203       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
 204       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 205       auto.
 206
 207     (* nd_rlecnac becomes RVar;;RCanR *)
 208     eapply nd_comp;
 209       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
 210       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 211       auto.
 212
 213     (* nd_assoc becomes RVar;;RAssoc *)
 214     eapply nd_comp;
 215       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 216       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 217       auto.
 218
 219     (* nd_cossa becomes RVar;;RCossa *)
 220     eapply nd_comp;
 221       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 222       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
 223       auto.
 224
 225       destruct r as [r rp].
 226       refine (match rp as R in @Rule_PCF _ _ _ H C _ 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.
 240       clear r h c.
 241       rename r0 into r; rename h0 into h; rename c0 into c.
 242
 243       destruct case_RURule.
 244         refine (match q with
 245           | RLeft   a b c r => let case_RLeft  := tt in _
 246           | RRight  a b c r => let case_RRight := tt in _
 247           | RCanL     b     => let case_RCanL  := tt in _
 248           | RCanR     b     => let case_RCanR  := tt in _
 249           | RuCanL    b     => let case_RuCanL := tt in _
 250           | RuCanR    b     => let case_RuCanR := tt in _
 251           | RAssoc    b c d => let case_RAssoc := tt in _
 252           | RCossa    b c d => let case_RCossa := tt in _
 253           | RExch     b c   => let case_RExch  := tt in _
 254           | RWeak     b     => let case_RWeak  := tt in _
 255           | RCont     b     => let case_RCont  := tt in _
 256           | RComp a b c f g => let case_RComp  := tt in _
 257         end).
 258
 259       destruct case_RCanL.
 260         (* ga_cancell *)
 261         admit.
 262
 263       destruct case_RCanR.
 264         (* ga_cancelr *)
 265         admit.
 266
 267       destruct case_RuCanL.
 268         (* ga_uncancell *)
 269         admit.
 270
 271       destruct case_RuCanR.
 272         (* ga_uncancelr *)
 273         admit.
 274
 275       destruct case_RAssoc.
 276         (* ga_assoc *)
 277         admit.
 278
 279       destruct case_RCossa.
 280         (* ga_unassoc *)
 281         admit.
 282
 283       destruct case_RExch.
 284         (* ga_swap *)
 285         admit.
 286
 287       destruct case_RWeak.
 288         (* ga_drop *)
 289         admit.
 290
 291       destruct case_RCont.
 292         (* ga_copy *)
 293         admit.
 294
 295       destruct case_RLeft.
 296         (* ga_second *)
 297         admit.
 298
 299       destruct case_RRight.
 300         (* ga_first *)
 301         admit.
 302
 303       destruct case_RComp.
 304         (* ga_comp *)
 305         admit.
 306
 307       destruct case_RLit.
 308         (* ga_literal *)
 309         admit.
 310
 311       (* hey cool, I figured out how to pass CoreNote's through... *)
 312       destruct case_RNote.
 313         eapply nd_comp.
 314         eapply nd_rule.
 315         eapply (org_fc _ _ (RVar _ _ _ _)) . auto.
 316         apply nd_rule.
 317         apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto.
 318
 319       destruct case_RVar.
 320         (* ga_id *)
 321         admit.
 322
 323       destruct case_RLam.
 324         (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
 325         admit.
 326
 327       destruct case_RApp.
 328         (* ga_apply *)
 329         admit.
 330
 331       destruct case_RLet.
 332         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
 333         admit.
 334
 335       destruct case_RVoid.
 336         (* ga_id u *)
 337         admit.
 338
 339       destruct case_RJoin.
 340         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
 341         admit.
 342
 343       Defined.
 344
 345   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) :=
 346     { fmor := FlatteningFunctor_fmor }.
 347     admit.
 348     admit.
 349     admit.
 350     Defined.
 351 (*
 352     Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 353       refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 354       unfold ReificationFunctor_fmor; simpl.
 355       admit.
 356       unfold ReificationFunctor_fmor; simpl.
 357       admit.
 358       unfold ReificationFunctor_fmor; simpl.
 359       admit.
 360       Defined.
 361
 362
 363   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 364     refine {| plsmme_pl := PCF n Γ Δ |}.
 365     admit.
 366     Defined.
 367
 368   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 369     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 370     admit.
 371     Defined.
 372
 373   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 374     admit.
 375     Defined.
 376
 377   (* 5.1.4 *)
 378   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 379     admit.
 380     (*  ... and the retraction exists *)
 381     Defined.
 382 *)
 383   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 384    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 385   (*
 386   Definition HaskProof_to_SystemFCa :
 387     forall h c (pf:ND Rule h c),
 388       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 389       *)
 390
 391   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 392
 393 End HaskProofFlattener.
 394