X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofFlattener.v;h=82bc678dae88477b25efe0ce616db5741df9fb0f;hp=980697dd96ed7cb4dde3725cdb89e6bb7ab84424;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hpb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index 980697d..82bc678 100644
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -30,6 +30,8 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 
@@ -134,90 +136,93 @@ Section HaskProofFlattener.
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
-      ((obact ec h)~~{TypesL _ _ (SystemFCa _ Γ Δ)}~~>(obact ec c)).
+      ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)).
 
     set (@nil (HaskTyVar Γ ★)) as lev.
 
-    unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
+    unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
 
     induction X; simpl.
 
-    (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
-    apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto.
+    (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
+    apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto.
 
     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
     apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
 
-    (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
+    (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
     eapply nd_comp;
       [ idtac
       | eapply nd_rule
       ; eapply (org_fc  _ _ (RArrange _ _ _ _ _ (RWeak _)))
       ; auto ].
       eapply nd_rule.
-      eapply (org_fc _ _ (REmptyGroup _ _)); auto.
+      eapply (org_fc _ _ (RVoid _ _)); auto.
     
-    (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
+    (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
-      set (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))
+      set (snd_initial(SequentND:=@pl_snd  _ _ _ _ (SystemFCa Γ Δ))
         (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
       eapply nd_comp.
       eapply nd_prod.
       apply q.
       apply q.
       apply nd_rule. 
-      eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
       auto.
       auto.
 
-    (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
+    (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
     eapply nd_comp.
       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
       apply nd_rule.
-      eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
       auto.
 
     (* nd_comp becomes pl_subst (aka nd_cut) *)
     eapply nd_comp.
       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
       clear IHX1 IHX2 X1 X2.
-      apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))).
+      (*
+      apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
+      *)
+      admit.
 
     (* nd_cancell becomes RVar;;RuCanL *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
     (* nd_cancelr becomes RVar;;RuCanR *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
     (* nd_llecnac becomes RVar;;RCanL *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
     (* nd_rlecnac becomes RVar;;RCanR *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
     (* nd_assoc becomes RVar;;RAssoc *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
     (* nd_cossa becomes RVar;;RCossa *)
     eapply nd_comp;
       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
-      apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa _ Γ Δ))).
+      apply (snd_initial(SequentND:=@pl_cnd  _ _ _ _ (SystemFCa Γ Δ))).
       auto.
 
       destruct r as [r rp].
@@ -229,8 +234,8 @@ Section HaskProofFlattener.
                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
-                | PCF_RBindingGroup    b c d e          => let case_RBindingGroup := tt in _
-                | PCF_REmptyGroup                       => let case_REmptyGroup   := tt in _
+                | PCF_RJoin    b c d e          => let case_RJoin := tt in _
+                | PCF_RVoid                       => let case_RVoid   := tt in _
               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
               end); simpl in *.
@@ -330,17 +335,17 @@ Section HaskProofFlattener.
         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
         admit.
 
-      destruct case_REmptyGroup.
+      destruct case_RVoid.
         (* ga_id u *)
         admit.
 
-      destruct case_RBindingGroup.
+      destruct case_RJoin.
         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
         admit.
 
       Defined.
 
-  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) :=
+  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
     { fmor := FlatteningFunctor_fmor }.
     admit.
     admit.