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
(Σ,τ) => Γ > Δ > (Σ@@@(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 []
(* 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))
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.
; 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.