(*********************************************************************************************************************************)
(* HaskProgrammingLanguage:                                                                                                      *)
(*                                                                                                                               *)
(*    System FC^\alpha is a ProgrammingLanguage.                                                                                 *)
(*                                                                                                                               *)
(*********************************************************************************************************************************)

Generalizable All Variables.
Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.

Require Import Algebras_ch4.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Require Import ProductCategories_ch1_6_1.
Require Import OppositeCategories_ch1_6_2.
Require Import Enrichment_ch2_8.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.

Require Import HaskKinds.
Require Import HaskCoreTypes.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskProof.
Require Import NaturalDeduction.
Require Import NaturalDeductionCategory.

Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskProof.
Require Import HaskStrongToProof.
Require Import HaskProofToStrong.
Require Import ProgrammingLanguage.
Require Import PCF.

Open Scope nd_scope.

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

  | org_pcf      : forall ec h c,
    ND (PCFRule Γ Δ ec)  h c  ->
    OrgR                (mapOptionTree (pcfjudg2fcjudg Γ ec) h)  (mapOptionTree (pcfjudg2fcjudg Γ ec) c).

  (* 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 SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)].
    intros.
    destruct b.
    destruct o.
    destruct c.
    destruct o.

    (* when the cut is a single leaf and the RHS is a single leaf: *)
    (*
    eapply nd_comp.
      eapply nd_prod.
      apply nd_id.
      eapply nd_rule.
      set (@org_fc) as ofc.
      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
      auto.
      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
      apply nd_rule.
      destruct l.
      destruct l0.
      assert (h0=h2). admit.
      subst.
      apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2). 
      auto.
      auto.
      *)
    admit.
    apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
    apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
    apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
    apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
    Defined.

  Instance SystemFCa_sequents : @SequentND _ OrgR _ _ :=
  { snd_cut := SystemFCa_cut }.
    apply Build_SequentND.
    intros.
    induction a.
    destruct a; simpl.
    (*
    apply nd_rule.
      destruct l.
      apply org_fc with (r:=RVar _ _ _ _).
      auto.
    apply nd_rule.
      apply org_fc with (r:=RVoid _ _ ).
      auto.
    eapply nd_comp.
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply (nd_prod IHa1 IHa2).
      apply nd_rule.
        apply org_fc with (r:=RJoin _ _ _ _ _ _). 
        auto.
      admit.
      *)
      admit.
      admit.
      admit.
      admit.
      Defined.

  Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))].
    admit.
    (*
    eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
    eapply nd_prod; [ apply snd_initial | apply nd_id ].
    apply nd_rule.
    apply org_fc with (r:=RJoin Γ Δ a b a c).
    auto.
    *)
    Defined.

  Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))].
    admit.
    (*
    eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
    eapply nd_prod; [ apply nd_id | apply snd_initial ].
    apply nd_rule.
    apply org_fc with (r:=RJoin Γ Δ b a c a).
    auto.
    *)
    Defined.

  Instance SystemFCa_sequent_join : @ContextND _ _ _ _ SystemFCa_sequents :=
  { cnd_expand_left  := fun a b c => SystemFCa_left  c a b
  ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
    (*
    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
      auto.

    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.

    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.

    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.

    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.

    intros; apply nd_rule. simpl.
      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
      *)
      admit.
      admit.
      admit.
      admit.
      admit.
      admit.
      Defined.

  Instance OrgFC : @ND_Relation _ OrgR.
    Admitted.

  Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.
    admit.
    Defined.

  Definition OrgFC_ContextND_Relation
    : @ContextND_Relation _ _ _ _ _ SystemFCa_sequent_join OrgFC OrgFC_SequentND_Relation.
    admit.
    Defined.

  (* 5.1.2 *)
  Instance SystemFCa : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
  { pl_eqv                := OrgFC_ContextND_Relation
  ; pl_snd                := SystemFCa_sequents
  }.

End HaskProgrammingLanguage.