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 pcfjudg2judg ec (cj:PCFJudg ec) :=
  94     match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
  95
  96   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
  97   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
  98   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
  99   Inductive Rule_PCF (ec:HaskTyVar Γ ★)
 100     : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
 101   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
 102   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
 103   | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [(_,[_])] [(_,[_])] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
 104   | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [([_],[_])] (RVar   Γ Δ    σ         (ec::nil)  )
 105   | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 106
 107   | PCF_RApp             : ∀ Σ Σ' tx te ,
 108     Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
 109     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 110
 111   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
 112     Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
 113     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 114
 115   | PCF_RVoid      :                 Rule_PCF ec [           ] [([],[])] (RVoid   Γ Δ  )
 116 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
 117   | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
 118     (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
 119   (* need int/boolean case *)
 120   Implicit Arguments Rule_PCF [ ].
 121
 122   Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
 123   End PCF.
 124
 125   Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 126     : ND Rule
 127     (mapOptionTree (brakify Γ Δ) h)
 128     (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
 129     apply nd_replicate; intros.
 130     destruct o; simpl in *.
 131     induction t0.
 132     destruct a; simpl.
 133     apply nd_rule.
 134     apply REsc.
 135     apply nd_id.
 136     apply (Prelude_error "mkEsc got multi-leaf succedent").
 137     Defined.
 138
 139   Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
 140     : ND Rule
 141     (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
 142     (mapOptionTree (brakify Γ Δ) h).
 143     apply nd_replicate; intros.
 144     destruct o; simpl in *.
 145     induction t0.
 146     destruct a; simpl.
 147     apply nd_rule.
 148     apply RBrak.
 149     apply nd_id.
 150     apply (Prelude_error "mkBrak got multi-leaf succedent").
 151     Defined.
 152
 153   Definition pcfToND Γ Δ : forall ec h c,
 154     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
 155     intros.
 156     eapply (fun q => nd_map' _ q X).
 157     intros.
 158     destruct X0.
 159     apply nd_rule.
 160     apply x.
 161     Defined.
 162
 163   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
 164     { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
 165     Admitted.
 166
 167   Hint Constructors Rule_Flat.
 168
 169   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
 170     admit.
 171     Defined.
 172
 173   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
 174     intros.
 175     destruct b.
 176     destruct o.
 177     destruct c.
 178     destruct o.
 179
 180     (* when the cut is a single leaf and the RHS is a single leaf: *)
 181     eapply nd_comp.
 182       eapply nd_prod.
 183       apply nd_id.
 184       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 185       apply RuCanL.
 186       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
 187       apply nd_rule.
 188       (*
 189       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 190       exists q.
 191       apply (PCF_RLet _ [] a h0 h).
 192     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 193     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 194     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 195     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 196     *)
 197     Admitted.
 198
 199   Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
 200     { snd_cut := PCF_cut Γ Δ lev }.
 201     apply Build_SequentND.
 202     intros.
 203     induction a.
 204     destruct a; simpl.
 205     apply nd_rule.
 206       exists (RVar _ _ _ _).
 207       apply PCF_RVar.
 208     apply nd_rule.
 209       exists (RVoid _ _ ).
 210       apply PCF_RVoid.
 211     eapply nd_comp.
 212       eapply nd_comp; [ apply nd_llecnac | idtac ].
 213       apply (nd_prod IHa1 IHa2).
 214       apply nd_rule.
 215         exists (RJoin _ _ _ _ _ _).
 216         apply PCF_RJoin.
 217       admit.
 218         Defined.
 219
 220   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
 221     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 222     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 223     apply nd_rule.
 224     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
 225     refine (existT _ _ _).
 226     apply q'.
 227     Admitted.
 228
 229   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
 230     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 231     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 232     apply nd_rule.
 233     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
 234     refine (existT _ _ _).
 235     apply q'.
 236     Admitted.
 237
 238   Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
 239   { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
 240   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 241
 242     intros; apply nd_rule. unfold PCFRule. simpl.
 243       exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
 244       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 245
 246     intros; apply nd_rule. unfold PCFRule. simpl.
 247       exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
 248       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 249
 250     intros; apply nd_rule. unfold PCFRule. simpl.
 251       exists (RArrange _ _ _ _ _ (RCanL _)).
 252       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 253
 254     intros; apply nd_rule. unfold PCFRule. simpl.
 255       exists (RArrange _ _ _ _ _ (RCanR _)).
 256       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 257
 258     intros; apply nd_rule. unfold PCFRule. simpl.
 259       exists (RArrange _ _ _ _ _ (RuCanL _)).
 260       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 261
 262     intros; apply nd_rule. unfold PCFRule. simpl.
 263       exists (RArrange _ _ _ _ _ (RuCanR _)).
 264       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
 265       Defined.
 266
 267   Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
 268     admit.
 269     Defined.
 270
 271   Definition OrgPCF_ContextND_Relation Γ Δ lev
 272     : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
 273     admit.
 274     Defined.
 275
 276   (* 5.1.3 *)
 277   Instance PCF Γ Δ lev : ProgrammingLanguage :=
 278   { pl_cnd     := PCF_sequent_join Γ Δ lev
 279   ; pl_eqv     := OrgPCF_ContextND_Relation Γ Δ lev
 280   }.
 281
 282 End PCF.