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