src/PCF.v

   1 (*********************************************************************************************************************************)
   2 (* PCF:                                                                                                          *)
   3 (*                                                                                                                               *)
   4 (*    An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous       *)
   5 (*    blocks.  This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to         *)
   6 (*    perform the flattening process.                                                                                            *)
   7 (*                                                                                                                               *)
   8 (*********************************************************************************************************************************)
   9
  10 Generalizable All Variables.
  11 Require Import Preamble.
  12 Require Import General.
  13 Require Import NaturalDeduction.
  14 Require Import Coq.Strings.String.
  15 Require Import Coq.Lists.List.
  16
  17 Require Import Algebras_ch4.
  18 Require Import Categories_ch1_3.
  19 Require Import Functors_ch1_4.
  20 Require Import Isomorphisms_ch1_5.
  21 Require Import ProductCategories_ch1_6_1.
  22 Require Import OppositeCategories_ch1_6_2.
  23 Require Import Enrichment_ch2_8.
  24 Require Import Subcategories_ch7_1.
  25 Require Import NaturalTransformations_ch7_4.
  26 Require Import NaturalIsomorphisms_ch7_5.
  27 Require Import MonoidalCategories_ch7_8.
  28 Require Import Coherence_ch7_8.
  29
  30 Require Import HaskKinds.
  31 Require Import HaskCoreTypes.
  32 Require Import HaskLiterals.
  33 Require Import HaskTyCons.
  34 Require Import HaskStrongTypes.
  35 Require Import HaskProof.
  36 Require Import NaturalDeduction.
  37 Require Import NaturalDeductionCategory.
  38
  39 Require Import HaskStrongTypes.
  40 Require Import HaskStrong.
  41 Require Import HaskProof.
  42 Require Import HaskStrongToProof.
  43 Require Import HaskProofToStrong.
  44 Require Import ProgrammingLanguage.
  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 PCF.
  58
  59   Section PCF.
  60
  61   Context {ndr_systemfc:@ND_Relation _ Rule}.
  62   Context Γ (Δ:CoercionEnv Γ).
  63
  64   Definition PCFJudg (ec:HaskTyVar Γ ECKind) :=
  65     @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
  66   Definition pcfjudg (ec:HaskTyVar Γ ECKind) :=
  67     @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
  68
  69   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
  70    * from depth (depth) by wrapping brackets around everything in the
  71    * succedent and repopulating *)
  72   Definition brakify {ec} (j:PCFJudg ec) : Judg :=
  73     match j with
  74       (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
  75       end.
  76
  77   Definition pcf_vars {Γ}(ec:HaskTyVar Γ ECKind)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  78     := mapOptionTreeAndFlatten (fun lt =>
  79       match lt with t @@ l => match l with
  80                                 | ec'::nil => if eqd_dec ec ec' then [t] else []
  81                                 | _ => []
  82                               end
  83       end) t.
  84
  85   Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
  86     | match_nil    : MatchingJudgments [] []
  87     | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
  88     | match_leaf   :
  89       forall Σ τ lev,
  90         MatchingJudgments
  91           [((pcf_vars ec Σ)         ,                              τ        )]
  92           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
  93
  94   Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
  95     match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
  96
  97   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
  98   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
  99   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
 100   Inductive Rule_PCF (ec:HaskTyVar Γ ECKind)
 101     : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
 102   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
 103   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
 104   | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [(_,[_])] [(_,[_])] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
 105   | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [([_],[_])] (RVar   Γ Δ    σ         (ec::nil)  )
 106   | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 107
 108   | PCF_RApp             : ∀ Σ Σ' tx te ,
 109     Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
 110     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 111
 112   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
 113     Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
 114     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 115
 116   | PCF_RVoid      :                 Rule_PCF ec [           ] [([],[])] (RVoid   Γ Δ  )
 117 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
 118   | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
 119     (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
 120   (* need int/boolean case *)
 121   Implicit Arguments Rule_PCF [ ].
 122
 123   Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
 124   End PCF.
 125
 126   Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 127     : ND Rule
 128     (mapOptionTree (brakify Γ Δ) h)
 129     (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
 130     apply nd_replicate; intros.
 131     destruct o; simpl in *.
 132     induction t0.
 133     destruct a; simpl.
 134     apply nd_rule.
 135     apply REsc.
 136     apply nd_id.
 137     apply (Prelude_error "mkEsc got multi-leaf succedent").
 138     Defined.
 139
 140   Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 141     : ND Rule
 142     (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
 143     (mapOptionTree (brakify Γ Δ) h).
 144     apply nd_replicate; intros.
 145     destruct o; simpl in *.
 146     induction t0.
 147     destruct a; simpl.
 148     apply nd_rule.
 149     apply RBrak.
 150     apply nd_id.
 151     apply (Prelude_error "mkBrak got multi-leaf succedent").
 152     Defined.
 153
 154   Definition pcfToND Γ Δ : forall ec h c,
 155     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
 156     intros.
 157     eapply (fun q => nd_map' _ q X).
 158     intros.
 159     destruct X0.
 160     apply nd_rule.
 161     apply x.
 162     Defined.
 163
 164   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
 165     { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
 166     Admitted.
 167
 168   Hint Constructors Rule_Flat.
 169
 170   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
 171     admit.
 172     Defined.
 173
 174   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
 175     intros.
 176     destruct b.
 177     destruct o.
 178     destruct c.
 179     destruct o.
 180
 181     (* when the cut is a single leaf and the RHS is a single leaf: *)
 182     eapply nd_comp.
 183       eapply nd_prod.
 184       apply nd_id.
 185       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 186       apply AuCanL.
 187       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].
 188       apply nd_rule.
 189       (*
 190       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 191       exists q.
 192       apply (PCF_RLet _ [] a h0 h).
 193     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 194     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 195     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 196     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 197     *)
 198     Admitted.
 199
 200   Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
 201     { snd_cut := PCF_cut Γ Δ lev }.
 202     apply Build_SequentND.
 203     intros.
 204     induction a.
 205     destruct a; simpl.
 206     apply nd_rule.
 207       exists (RVar _ _ _ _).
 208       apply PCF_RVar.
 209     apply nd_rule.
 210       exists (RVoid _ _ ).
 211       apply PCF_RVoid.
 212     eapply nd_comp.
 213       eapply nd_comp; [ apply nd_llecnac | idtac ].
 214       apply (nd_prod IHa1 IHa2).
 215       apply nd_rule.
 216         exists (RJoin _ _ _ _ _ _).
 217         apply PCF_RJoin.
 218       admit.
 219         Defined.
 220
 221   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
 222     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 223     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 224     apply nd_rule.
 225     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
 226     refine (existT _ _ _).
 227     apply q'.
 228     Admitted.
 229
 230   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
 231     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 232     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 233     apply nd_rule.
 234     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
 235     refine (existT _ _ _).
 236     apply q'.
 237     Admitted.
 238
 239   Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
 240   { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
 241   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 242
 243     intros; apply nd_rule. unfold PCFRule. simpl.
 244       exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).
 245       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 246
 247     intros; apply nd_rule. unfold PCFRule. simpl.
 248       exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).
 249       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 250
 251     intros; apply nd_rule. unfold PCFRule. simpl.
 252       exists (RArrange _ _ _ _ _ (ACanL _)).
 253       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 254
 255     intros; apply nd_rule. unfold PCFRule. simpl.
 256       exists (RArrange _ _ _ _ _ (ACanR _)).
 257       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 258
 259     intros; apply nd_rule. unfold PCFRule. simpl.
 260       exists (RArrange _ _ _ _ _ (AuCanL _)).
 261       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 262
 263     intros; apply nd_rule. unfold PCFRule. simpl.
 264       exists (RArrange _ _ _ _ _ (AuCanR _)).
 265       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
 266       Defined.
 267
 268   Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
 269     admit.
 270     Defined.
 271
 272   Definition OrgPCF_ContextND_Relation Γ Δ lev
 273     : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
 274     admit.
 275     Defined.
 276
 277   (* 5.1.3 *)
 278   Instance PCF Γ Δ lev : ProgrammingLanguage :=
 279   { pl_cnd     := PCF_sequent_join Γ Δ lev
 280   ; pl_eqv     := OrgPCF_ContextND_Relation Γ Δ lev
 281   }.
 282
 283 End PCF.