X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FPCF.v;h=373519b72a1431f4b989a701480c22254fdfc427;hp=00ffd77e7832b8ba1d0e216340cbae924621c04e;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=94ad996f571e3c9fd622bc56d9b57118a7e5333a

diff --git a/src/PCF.v b/src/PCF.v
index 00ffd77..373519b 100644
--- a/src/PCF.v
+++ b/src/PCF.v
@@ -29,7 +29,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.
@@ -60,9 +61,9 @@ Section PCF.
   Context {ndr_systemfc:@ND_Relation _ Rule}.
   Context Γ (Δ:CoercionEnv Γ).
 
-  Definition PCFJudg (ec:HaskTyVar Γ ★) :=
+  Definition PCFJudg (ec:HaskTyVar Γ ECKind) :=
     @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
-  Definition pcfjudg (ec:HaskTyVar Γ ★) :=
+  Definition pcfjudg (ec:HaskTyVar Γ ECKind) :=
     @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
 
   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
@@ -73,7 +74,7 @@ Section PCF.
       (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
       end.
 
-  Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
+  Definition pcf_vars {Γ}(ec:HaskTyVar Γ ECKind)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
     := mapOptionTreeAndFlatten (fun lt =>
       match lt with t @@ l => match l with
                                 | ec'::nil => if eqd_dec ec ec' then [t] else []
@@ -96,7 +97,7 @@ Section PCF.
   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
-  Inductive Rule_PCF (ec:HaskTyVar Γ ★)
+  Inductive Rule_PCF (ec:HaskTyVar Γ ECKind)
     : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
@@ -182,8 +183,8 @@ Section PCF.
       eapply nd_prod.
       apply nd_id.
       apply (PCF_Arrange [h] ([],,[h]) [h0]).
-      apply RuCanL.
-      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
+      apply AuCanL.
+      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].
       apply nd_rule.
       (*
       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
@@ -240,27 +241,27 @@ Section PCF.
   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
+      exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).
       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
+      exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).
       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanL _)).
+      exists (RArrange _ _ _ _ _ (ACanL _)).
       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanR _)).
+      exists (RArrange _ _ _ _ _ (ACanR _)).
       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanL _)).
+      exists (RArrange _ _ _ _ _ (AuCanL _)).
       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanR _)).
+      exists (RArrange _ _ _ _ _ (AuCanR _)).
       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
       Defined.