+ Context (ndr_systemfc:@ND_Relation _ Rule).
+
+ (* 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 {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=
+ | PCF_RArrange : ∀ x y , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a ))
+ | PCF_RCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a ))
+ | PCF_RuCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a ))
+ | PCF_RuCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a ))
+ | PCF_RAssoc : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RAssoc t a b c ))
+ | PCF_RCossa : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCossa t a b c ))
+ | PCF_RLeft : ∀ h c x , Rule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
+ | PCF_RRight : ∀ h c x , Rule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
+ | PCF_RExch : ∀ t a b , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RExch t a b ))
+ | PCF_RWeak : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RWeak t a ))
+ | PCF_RCont : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCont t a ))
+
+ | PCF_RLit : ∀ Σ τ , Rule_PCF [ ] [_>>_>_|-_] (RLit Γ Δ Σ τ )
+ | PCF_RNote : ∀ Σ τ l n , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RNote Γ Δ Σ τ l n)
+ | PCF_RVar : ∀ σ l, Rule_PCF [ ] [_>>_>_|-_] (RVar Γ Δ σ l)
+ | PCF_RLam : ∀ Σ tx te q , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLam Γ Δ Σ tx te q )
+ | PCF_RApp : ∀ Σ tx te p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RApp Γ Δ Σ tx te p l)
+ | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RLet Γ Δ Σ σ₁ σ₂ p l)
+ | PCF_RBindingGroup : ∀ b c d e , Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RBindingGroup _ _ b c d e)
+ | PCF_REmptyGroup : Rule_PCF [ ] [_>>_>_|-_] (REmptyGroup _ _ ).
+
+(* | PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ lev , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).*)
+ Implicit Arguments Rule_PCF [ ].
+
+(* need int/boolean case *)
+(* | PCF_RCase : ∀ T κlen κ θ l x , Rule_PCF (RCase Γ Δ T κlen κ θ l x) (* FIXME: only for boolean and int *)*)
+
+ Definition PCFR Γ Δ h c := { r:_ & Rule_PCF Γ Δ h c r }.
+
+ (* this wraps code-brackets, with the specified environment classifier, around a type *)
+ Definition brakifyType {Γ} (ec:HaskTyVar Γ ★)(lt:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+ match lt with
+ t @@ l => HaskBrak ec t @@ l
+ end.
+
+ Definition brakifyu {Γ}{Δ}(v:HaskTyVar Γ ★)(j:UJudg Γ Δ) : UJudg Γ Δ :=
+ match j with
+ mkUJudg Σ τ =>
+ Γ >> Δ > mapOptionTree (brakifyType v) Σ |- mapOptionTree (brakifyType v) τ
+ end.
+
+
+ (* 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 : bool -> nat -> forall Γ Δ, Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
+
+ | org_pcf : forall n Γ Δ h c b,
+ PCFR Γ Δ h c -> OrgR b n Γ Δ h c
+
+ | org_fc : forall n Γ Δ h c,
+ ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR true n Γ Δ h c
+
+ | org_nest : forall n Γ Δ h c b v,
+ OrgR b n Γ Δ h c ->
+ OrgR b (S n) _ _ (mapOptionTree (brakifyu v) h) (mapOptionTree (brakifyu v) c)
+ .
+
+ Definition OrgND b n Γ Δ := ND (OrgR b n Γ Δ).
+
+ Definition mkEsc {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
+ : ND Rule
+ (mapOptionTree (@UJudg2judg Γ Δ) h)
+ (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h).
+ admit.
+ Defined.
+
+ Definition mkBrak {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
+ : ND Rule
+ (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h)
+ (mapOptionTree (@UJudg2judg Γ Δ ) h).
+ admit.
+ Defined.
+
+ (* any proof in organized form can be "dis-organized" *)
+ Definition unOrgR b n Γ Δ : forall h c, OrgR b n Γ Δ h c ->
+ ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c).
+
+ intros.
+
+ induction X.
+ apply nd_rule.
+ destruct p.
+ apply x.
+
+ apply n0.
+
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ eapply nd_comp.
+ apply (mkBrak h).
+ eapply nd_comp; [ idtac | apply (mkEsc c) ].
+ apply IHX.
+ Defined.
+
+ Definition unOrgND b n Γ Δ h c :
+ ND (OrgR b n Γ Δ) h c -> ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c)
+ := nd_map' (@UJudg2judg Γ Δ) (unOrgR b n Γ Δ).
+
+ Instance OrgNDR b n Γ Δ : @ND_Relation _ (OrgR b n Γ Δ) :=
+ { ndr_eqv := fun a b f g => (unOrgND _ _ _ _ _ _ f) === (unOrgND _ _ _ _ _ _ g) }.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ (*
+ Hint Constructors Rule_Flat.
+
+ Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
+ apply Build_SequentCalculus.
+ intro a.
+ induction a.
+ destruct a.
+ apply nd_rule.
+ destruct l.
+ apply sfc_flat with (r:=RVar _ _ _ _).
+ auto.
+ apply nd_rule.
+ apply sfc_flat with (r:=REmptyGroup _ _).
+ auto.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ apply IHa1.
+ apply IHa2.
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ Defined.
+
+ Existing Instance SystemFC_SC.
+
+ Lemma systemfc_cut n : ∀a b c,
+ ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
+ intros.
+ admit.
+ Defined.
+
+ Lemma systemfc_cutrule n
+ : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfc n) (SystemFC_SC n).
+ apply Build_CutRule with (nd_cut:=systemfc_cut n).
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ Focus 3.
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ idtac.
+ apply nd_seq_reflexive.
+ apply nd_id.
+ Defined.
+
+ Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ apply nd_id.
+ apply (nd_seq_reflexive a).
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ Defined.
+*)
+(*
+ Definition systemfc_expansion n
+ : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
+ Check (@Build_SequentExpansion).
+apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n) _ _ (systemfc_left n) (systemfc_right n)).
+ refine {| se_expand_left:=systemfc_left n
+ ; se_expand_right:=systemfc_right n |}.
+
+*)
+
+ (* 5.1.2 *)
+ Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true n Γ Δ) :=
+ { pl_eqv := OrgNDR true n Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
+ apply nd_rule; apply org_fc; apply nd_rule; simpl. apply (RURule _ _ _ _ (RCossa _ a b c)).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RAssoc _ a b c)).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanL _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanR _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanL _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanR _ a )).
+ Admitted.
+
+ (* "flat" SystemFC: no brackets allowed *)
+ Instance SystemFC Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true O Γ Δ) :=
+ { pl_eqv := OrgNDR true O Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ Admitted.
+
+ (* 5.1.3 *)
+ Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR false n Γ Δ) :=
+ { pl_eqv := OrgNDR false n Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
+ apply nd_rule; apply org_pcf; simpl; exists (RCossa _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RAssoc _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RuCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RuCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ Admitted.
+
+(*
+ Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
+ match t with
+(* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
+ | _ => code2garrow0 ec unitType t
+ end.
+ Opaque code2garrow.
+ Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
+ match ty as TY in RawHaskType _ K return RawHaskType TV K with
+ | TCode ec t => code2garrow _ ec t
+ | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
+ | TAll _ f => TAll _ (fun tv => typeMap (f tv))
+ | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
+ | TVar _ v => TVar v
+ | TArrow => TArrow
+ | TCon tc => TCon tc
+ | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
+ end.
+
+ Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+ match lht with
+(* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
+ | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
+ end.
+*)
+
+ (* gathers a tree of guest-language types into a single host-language types via the tensor *)
+ Definition tensorizeType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : HaskType Γ ★.