X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProgrammingLanguage.v;h=30a0ae82e12578862d17338cce9d5908f6a299ac;hp=0d612d683962c70aa12120ee1f20811618e40242;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=d6342fb07462cc126df948459ce98ea9caadb95c

diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v
index 0d612d6..30a0ae8 100644
--- a/src/HaskProgrammingLanguage.v
+++ b/src/HaskProgrammingLanguage.v
@@ -27,7 +27,8 @@ Require Import Coherence_ch7_8.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
@@ -39,48 +40,26 @@ Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
 Require Import ProgrammingLanguage.
-Require Import PCF.
 
 Open Scope nd_scope.
 
+(* The judgments any specific Γ,Δ form a category with proofs as morphisms *)
 Section HaskProgrammingLanguage.
 
   Context (ndr_systemfc:@ND_Relation _ Rule).
-  Context Γ (Δ:CoercionEnv Γ).
-
-  (* An organized deduction has been reorganized into contiguous blocks whose
-   * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
-   * indicates if non-PCF rules have been used *)
-  Inductive OrgR : Tree ??(@FCJudg Γ) -> Tree ??(@FCJudg Γ) -> Type :=
 
-  | org_fc        : forall (h c:Tree ??(FCJudg Γ))
-    (r:Rule (mapOptionTree (fcjudg2judg Γ Δ) h) (mapOptionTree (fcjudg2judg Γ Δ) c)),
-    Rule_Flat r ->
-    OrgR h c
+  Context Γ (Δ:CoercionEnv Γ).
 
-  | org_pcf      : forall ec h c,
-    ND (PCFRule Γ Δ ec)  h c  ->
-    OrgR                (mapOptionTree (pcfjudg2fcjudg Γ ec) h)  (mapOptionTree (pcfjudg2fcjudg Γ ec) c).
+  
+  Definition JudgΓΔ := prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
 
-  (* any proof in organized form can be "dis-organized" *)
-  (*
-  Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
-    intros.
-    induction X.
-      apply nd_rule.
-      apply r.
-    eapply nd_comp.
-      (*
-      apply (mkEsc h).
-      eapply nd_comp; [ idtac |  apply (mkBrak c) ].
-      apply pcfToND.
-      apply n.
-      *)
-      Admitted.
-  Definition unOrgND Γ Δ h c :  ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
-  *)
+  Definition RuleΓΔ : Tree ??JudgΓΔ -> Tree ??JudgΓΔ -> Type :=
+    fun h c =>
+      Rule
+      (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) h)
+      (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) c).
 
-  Definition SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)].
+  Definition SystemFCa_cut : forall a b c, ND RuleΓΔ ([(a,b)],,[(b,c)]) [(a,c)].
     intros.
     destruct b.
     destruct o.
@@ -94,10 +73,10 @@ Section HaskProgrammingLanguage.
       apply nd_id.
       eapply nd_rule.
       set (@org_fc) as ofc.
-      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
-      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
+      set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule.
+      apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])).
       auto.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
+      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ].
       apply nd_rule.
       destruct l.
       destruct l0.
@@ -114,7 +93,7 @@ Section HaskProgrammingLanguage.
     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
     Defined.
 
-  Instance SystemFCa_sequents : @SequentND _ OrgR _ _ :=
+  Instance SystemFCa_sequents : @SequentND _ RuleΓΔ _ _ :=
   { snd_cut := SystemFCa_cut }.
     apply Build_SequentND.
     intros.
@@ -142,7 +121,7 @@ Section HaskProgrammingLanguage.
       admit.
       Defined.
 
-  Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))].
+  Definition SystemFCa_left a b c : ND RuleΓΔ [(b,c)] [((a,,b),(a,,c))].
     admit.
     (*
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
@@ -153,7 +132,7 @@ Section HaskProgrammingLanguage.
     *)
     Defined.
 
-  Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))].
+  Definition SystemFCa_right a b c : ND RuleΓΔ [(b,c)] [((b,,a),(c,,a))].
     admit.
     (*
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
@@ -169,23 +148,23 @@ Section HaskProgrammingLanguage.
   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
     (*
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))).
       auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.
 
     intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.
       *)
       admit.
       admit.
@@ -195,7 +174,7 @@ Section HaskProgrammingLanguage.
       admit.
       Defined.
 
-  Instance OrgFC : @ND_Relation _ OrgR.
+  Instance OrgFC : @ND_Relation _ RuleΓΔ.
     Admitted.
 
   Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.