src/HaskProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProgrammingLanguage:                                                                                                      *)
   3 (*                                                                                                                               *)
   4 (*    System FC^\alpha is a ProgrammingLanguage.                                                                                 *)
   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 Algebras_ch4.
  16 Require Import Categories_ch1_3.
  17 Require Import Functors_ch1_4.
  18 Require Import Isomorphisms_ch1_5.
  19 Require Import ProductCategories_ch1_6_1.
  20 Require Import OppositeCategories_ch1_6_2.
  21 Require Import Enrichment_ch2_8.
  22 Require Import Subcategories_ch7_1.
  23 Require Import NaturalTransformations_ch7_4.
  24 Require Import NaturalIsomorphisms_ch7_5.
  25 Require Import MonoidalCategories_ch7_8.
  26 Require Import Coherence_ch7_8.
  27
  28 Require Import HaskKinds.
  29 Require Import HaskCoreTypes.
  30 Require Import HaskLiterals.
  31 Require Import HaskTyCons.
  32 Require Import HaskStrongTypes.
  33 Require Import HaskProof.
  34 Require Import NaturalDeduction.
  35 Require Import NaturalDeductionCategory.
  36
  37 Require Import HaskStrongTypes.
  38 Require Import HaskStrong.
  39 Require Import HaskProof.
  40 Require Import HaskStrongToProof.
  41 Require Import HaskProofToStrong.
  42 Require Import ProgrammingLanguage.
  43
  44 Open Scope nd_scope.
  45
  46 (* The judgments any specific Γ,Δ form a category with proofs as morphisms *)
  47 Section HaskProgrammingLanguage.
  48
  49   Context (ndr_systemfc:@ND_Relation _ Rule).
  50
  51   Context Γ (Δ:CoercionEnv Γ).
  52
  53
  54   Definition JudgΓΔ := prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
  55
  56   Definition RuleΓΔ : Tree ??JudgΓΔ -> Tree ??JudgΓΔ -> Type :=
  57     fun h c =>
  58       Rule
  59       (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) h)
  60       (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) c).
  61
  62   Definition SystemFCa_cut : forall a b c, ND RuleΓΔ ([(a,b)],,[(b,c)]) [(a,c)].
  63     intros.
  64     destruct b.
  65     destruct o.
  66     destruct c.
  67     destruct o.
  68
  69     (* when the cut is a single leaf and the RHS is a single leaf: *)
  70     (*
  71     eapply nd_comp.
  72       eapply nd_prod.
  73       apply nd_id.
  74       eapply nd_rule.
  75       set (@org_fc) as ofc.
  76       set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule.
  77       apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])).
  78       auto.
  79       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ].
  80       apply nd_rule.
  81       destruct l.
  82       destruct l0.
  83       assert (h0=h2). admit.
  84       subst.
  85       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
  86       auto.
  87       auto.
  88       *)
  89     admit.
  90     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
  91     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
  92     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
  93     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
  94     Defined.
  95
  96   Instance SystemFCa_sequents : @SequentND _ RuleΓΔ _ _ :=
  97   { snd_cut := SystemFCa_cut }.
  98     apply Build_SequentND.
  99     intros.
 100     induction a.
 101     destruct a; simpl.
 102     (*
 103     apply nd_rule.
 104       destruct l.
 105       apply org_fc with (r:=RVar _ _ _ _).
 106       auto.
 107     apply nd_rule.
 108       apply org_fc with (r:=RVoid _ _ ).
 109       auto.
 110     eapply nd_comp.
 111       eapply nd_comp; [ apply nd_llecnac | idtac ].
 112       apply (nd_prod IHa1 IHa2).
 113       apply nd_rule.
 114         apply org_fc with (r:=RJoin _ _ _ _ _ _).
 115         auto.
 116       admit.
 117       *)
 118       admit.
 119       admit.
 120       admit.
 121       admit.
 122       Defined.
 123
 124   Definition SystemFCa_left a b c : ND RuleΓΔ [(b,c)] [((a,,b),(a,,c))].
 125     admit.
 126     (*
 127     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 128     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 129     apply nd_rule.
 130     apply org_fc with (r:=RJoin Γ Δ a b a c).
 131     auto.
 132     *)
 133     Defined.
 134
 135   Definition SystemFCa_right a b c : ND RuleΓΔ [(b,c)] [((b,,a),(c,,a))].
 136     admit.
 137     (*
 138     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 139     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 140     apply nd_rule.
 141     apply org_fc with (r:=RJoin Γ Δ b a c a).
 142     auto.
 143     *)
 144     Defined.
 145
 146   Instance SystemFCa_sequent_join : @ContextND _ _ _ _ SystemFCa_sequents :=
 147   { cnd_expand_left  := fun a b c => SystemFCa_left  c a b
 148   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
 149     (*
 150     intros; apply nd_rule. simpl.
 151       apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))).
 152       auto.
 153
 154     intros; apply nd_rule. simpl.
 155       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.
 156
 157     intros; apply nd_rule. simpl.
 158       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.
 159
 160     intros; apply nd_rule. simpl.
 161       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.
 162
 163     intros; apply nd_rule. simpl.
 164       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.
 165
 166     intros; apply nd_rule. simpl.
 167       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.
 168       *)
 169       admit.
 170       admit.
 171       admit.
 172       admit.
 173       admit.
 174       admit.
 175       Defined.
 176
 177   Instance OrgFC : @ND_Relation _ RuleΓΔ.
 178     Admitted.
 179
 180   Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.
 181     admit.
 182     Defined.
 183
 184   Definition OrgFC_ContextND_Relation
 185     : @ContextND_Relation _ _ _ _ _ SystemFCa_sequent_join OrgFC OrgFC_SequentND_Relation.
 186     admit.
 187     Defined.
 188
 189   (* 5.1.2 *)
 190   Instance SystemFCa : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
 191   { pl_eqv                := OrgFC_ContextND_Relation
 192   ; pl_snd                := SystemFCa_sequents
 193   }.
 194
 195 End HaskProgrammingLanguage.