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 HaskLiteralsAndTyCons.
  33 Require Import HaskStrongTypes.
  34 Require Import HaskProof.
  35 Require Import NaturalDeduction.
  36 Require Import NaturalDeductionCategory.
  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
  45 Open Scope nd_scope.
  46
  47
  48 (*
  49  *  The flattening transformation.  Currently only TWO-level languages are
  50  *  supported, and the level-1 sublanguage is rather limited.
  51 *
  52  *  This file abuses terminology pretty badly.  For purposes of this file,
  53  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  54  *  the whole language (level-0 language including bracketed level-1 terms)
  55  *)
  56 Section PCF.
  57
  58   Section PCF.
  59
  60   Context {ndr_systemfc:@ND_Relation _ Rule}.
  61   Context Γ (Δ:CoercionEnv Γ).
  62
  63   Definition PCFJudg (ec:HaskTyVar Γ ★) :=
  64     @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
  65   Definition pcfjudg (ec:HaskTyVar Γ ★) :=
  66     @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
  67
  68   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
  69    * from depth (depth) by wrapping brackets around everything in the
  70    * succedent and repopulating *)
  71   Definition brakify {ec} (j:PCFJudg ec) : Judg :=
  72     match j with
  73       (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
  74       end.
  75
  76   Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  77     := mapOptionTreeAndFlatten (fun lt =>
  78       match lt with t @@ l => match l with
  79                                 | ec'::nil => if eqd_dec ec ec' then [t] else []
  80                                 | _ => []
  81                               end
  82       end) t.
  83
  84   Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
  85     | match_nil    : MatchingJudgments [] []
  86     | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
  87     | match_leaf   :
  88       forall Σ τ lev,
  89         MatchingJudgments
  90           [((pcf_vars ec Σ)         ,                              τ        )]
  91           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
  92
  93   Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  94     := mapOptionTreeAndFlatten (fun lt =>
  95       match lt with t @@ l => match l with
  96                                 | ec'::nil => if eqd_dec ec ec' then [] else [t]
  97                                 | _ => []
  98                               end
  99       end) t.
 100
 101   Definition FCJudg :=
 102     @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
 103   Definition fcjudg2judg (fc:FCJudg) :=
 104     match fc with
 105       (x,y) => Γ > Δ > x |- y
 106         end.
 107   Coercion fcjudg2judg : FCJudg >-> Judg.
 108
 109   Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
 110     match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
 111
 112   Definition pcfjudg2fcjudg ec (fc:PCFJudg ec) : FCJudg :=
 113     match fc with
 114       (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
 115         end.
 116
 117   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
 118   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
 119   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
 120   Inductive Rule_PCF (ec:HaskTyVar Γ ★)
 121     : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
 122   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
 123   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
 124   | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [(_,[_])] [(_,[_])] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
 125   | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [([_],[_])] (RVar   Γ Δ    σ         (ec::nil)  )
 126   | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 127
 128   | PCF_RApp             : ∀ Σ Σ' tx te ,
 129     Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
 130     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 131
 132   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
 133     Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
 134     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 135
 136   | PCF_RVoid      :                 Rule_PCF ec [           ] [([],[])] (RVoid   Γ Δ  )
 137 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
 138   | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
 139     (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
 140   (* need int/boolean case *)
 141   Implicit Arguments Rule_PCF [ ].
 142
 143   Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
 144   End PCF.
 145
 146   Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 147     : ND Rule
 148     (mapOptionTree (brakify Γ Δ) h)
 149     (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
 150     apply nd_replicate; intros.
 151     destruct o; simpl in *.
 152     induction t0.
 153     destruct a; simpl.
 154     apply nd_rule.
 155     apply REsc.
 156     apply nd_id.
 157     apply (Prelude_error "mkEsc got multi-leaf succedent").
 158     Defined.
 159
 160   Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 161     : ND Rule
 162     (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
 163     (mapOptionTree (brakify Γ Δ) h).
 164     apply nd_replicate; intros.
 165     destruct o; simpl in *.
 166     induction t0.
 167     destruct a; simpl.
 168     apply nd_rule.
 169     apply RBrak.
 170     apply nd_id.
 171     apply (Prelude_error "mkBrak got multi-leaf succedent").
 172     Defined.
 173
 174     (*
 175   Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
 176     { vars:(_ * _) |
 177       fc_vars  ec Σ = fst vars /\
 178       pcf_vars ec Σ = snd vars }.
 179       *)
 180
 181   Definition pcfToND Γ Δ : forall ec h c,
 182     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
 183     intros.
 184     eapply (fun q => nd_map' _ q X).
 185     intros.
 186     destruct X0.
 187     apply nd_rule.
 188     apply x.
 189     Defined.
 190
 191   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
 192     { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
 193     Admitted.
 194
 195   (*
 196    * An intermediate representation necessitated by Coq's termination
 197    * conditions.  This is basically a tree where each node is a
 198    * subproof which is either entirely level-1 or entirely level-0
 199    *)
 200   Inductive Alternating : Tree ??Judg -> Type :=
 201
 202     | alt_nil    : Alternating []
 203
 204     | alt_branch : forall a b,
 205       Alternating a -> Alternating b -> Alternating (a,,b)
 206
 207     | alt_fc     : forall h c,
 208       Alternating h ->
 209       ND Rule h c ->
 210       Alternating c
 211
 212     | alt_pcf    : forall Γ Δ ec h c h' c',
 213       MatchingJudgments Γ Δ  h  h' ->
 214       MatchingJudgments Γ Δ  c  c' ->
 215       Alternating h' ->
 216       ND (PCFRule Γ Δ ec) h c ->
 217       Alternating c'.
 218
 219   Require Import Coq.Logic.Eqdep.
 220 (*
 221   Lemma magic a b c d ec e :
 222     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
 223     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
 224     admit.
 225     Defined.
 226
 227   Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 228
 229     refine (
 230       fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
 231         let case_main := tt in _
 232       with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
 233       (match c as C return C=c -> Alternating C with
 234         | T_Leaf None                    => fun _ => alt_nil
 235         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
 236         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
 237       end (refl_equal _))
 238       with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
 239         (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
 240         let case_pcf := tt in _
 241       for orgify_fc').
 242
 243       destruct case_main.
 244       inversion pf; subst.
 245       set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
 246       refine (match X0 as R in Rule H C return
 247                 match C with
 248                   | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
 249                     h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
 250                   | _                              => True
 251                 end
 252                  with
 253                 | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
 254                 | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
 255                 | _ => fun pf' x => x
 256               end (refl_equal _) backup).
 257       clear backup0 backup.
 258
 259       destruct case_RBrak.
 260         rename c into ec.
 261         set (@match_leaf Σ0 a ec n [b] m) as q.
 262         set (orgify_pcf Σ0 a ec _ _ q) as q'.
 263         apply q'.
 264         simpl.
 265         rewrite pf' in X.
 266         apply magic in X.
 267         apply X.
 268
 269       destruct case_REsc.
 270         apply (Prelude_error "encountered Esc in wrong side of mkalt").
 271
 272     destruct case_leaf.
 273       apply orgify_fc'.
 274       rewrite eqpf.
 275       apply pf.
 276
 277     destruct case_branch.
 278       rewrite <- eqpf in pf.
 279       inversion pf; subst.
 280       apply no_rules_with_multiple_conclusions in X0.
 281       inversion X0.
 282       exists b1. exists b2.
 283       auto.
 284       apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
 285
 286     destruct case_pcf.
 287     Admitted.
 288
 289   Definition pcfify Γ Δ ec : forall Σ τ,
 290     ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
 291       -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
 292
 293     refine ((
 294       fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
 295       : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
 296      (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
 297       | cnd_weak             => let case_nil    := tt in _
 298       | cnd_rule h c cnd' r  => let case_rule   := tt in _
 299       | cnd_branch _ _ c1 c2 => let case_branch := tt in _
 300       end (refl_equal _)))).
 301       intros.
 302       inversion H.
 303       intros.
 304       destruct c; try destruct o; inversion H.
 305       destruct j.
 306       Admitted.
 307 *)
 308
 309   Hint Constructors Rule_Flat.
 310
 311   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
 312     admit.
 313     Defined.
 314
 315   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
 316     intros.
 317     destruct b.
 318     destruct o.
 319     destruct c.
 320     destruct o.
 321
 322     (* when the cut is a single leaf and the RHS is a single leaf: *)
 323     eapply nd_comp.
 324       eapply nd_prod.
 325       apply nd_id.
 326       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 327       apply RuCanL.
 328       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
 329       apply nd_rule.
 330       (*
 331       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 332       exists q.
 333       apply (PCF_RLet _ [] a h0 h).
 334     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 335     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 336     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 337     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 338     *)
 339     Admitted.
 340
 341   Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
 342     { snd_cut := PCF_cut Γ Δ lev }.
 343     apply Build_SequentND.
 344     intros.
 345     induction a.
 346     destruct a; simpl.
 347     apply nd_rule.
 348       exists (RVar _ _ _ _).
 349       apply PCF_RVar.
 350     apply nd_rule.
 351       exists (RVoid _ _ ).
 352       apply PCF_RVoid.
 353     eapply nd_comp.
 354       eapply nd_comp; [ apply nd_llecnac | idtac ].
 355       apply (nd_prod IHa1 IHa2).
 356       apply nd_rule.
 357         exists (RJoin _ _ _ _ _ _).
 358         apply PCF_RJoin.
 359       admit.
 360         Defined.
 361
 362   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
 363     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 364     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 365     apply nd_rule.
 366     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
 367     refine (existT _ _ _).
 368     apply q'.
 369     Admitted.
 370
 371   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
 372     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 373     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 374     apply nd_rule.
 375     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
 376     refine (existT _ _ _).
 377     apply q'.
 378     Admitted.
 379
 380   Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
 381   { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
 382   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 383
 384     intros; apply nd_rule. unfold PCFRule. simpl.
 385       exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
 386       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 387
 388     intros; apply nd_rule. unfold PCFRule. simpl.
 389       exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
 390       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 391
 392     intros; apply nd_rule. unfold PCFRule. simpl.
 393       exists (RArrange _ _ _ _ _ (RCanL _)).
 394       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 395
 396     intros; apply nd_rule. unfold PCFRule. simpl.
 397       exists (RArrange _ _ _ _ _ (RCanR _)).
 398       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 399
 400     intros; apply nd_rule. unfold PCFRule. simpl.
 401       exists (RArrange _ _ _ _ _ (RuCanL _)).
 402       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 403
 404     intros; apply nd_rule. unfold PCFRule. simpl.
 405       exists (RArrange _ _ _ _ _ (RuCanR _)).
 406       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
 407       Defined.
 408
 409   Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
 410     admit.
 411     Defined.
 412
 413   Definition OrgPCF_ContextND_Relation Γ Δ lev
 414     : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
 415     admit.
 416     Defined.
 417
 418   (* 5.1.3 *)
 419   Instance PCF Γ Δ lev : ProgrammingLanguage :=
 420   { pl_cnd     := PCF_sequent_join Γ Δ lev
 421   ; pl_eqv     := OrgPCF_ContextND_Relation Γ Δ lev
 422   }.
 423
 424 End PCF.