add HaskProofToStrong skeleton implementation

diff --git a/src/Extraction.v b/src/Extraction.v
index 363e17f..1a26e58 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -25,7 +25,7 @@ Require Import HaskProof.
 Require Import HaskCoreToWeak.
 Require Import HaskWeakToStrong.
 Require Import HaskStrongToProof.
-(*Require Import HaskProofToStrong.*)
+Require Import HaskProofToStrong.
 Require Import HaskProofToLatex.
 Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
new file mode 100644 (file)
index 0000000..5039004
--- /dev/null
+++ b/src/HaskProofToStrong.v
@@ -0,0 +1,159 @@
+(*********************************************************************************************************************************)
+(* HaskProofToStrong: convert HaskProof to HaskStrong                                                                            *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Coq.Init.Specif.
+Require Import HaskKinds.
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+Require Import HaskProof.
+
+Section HaskProofToStrong.
+
+  Context
+    {VV:Type}
+    {eqdec_vv:EqDecidable VV}
+    {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}.
+
+  Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ)(τ:Tree ??(LeveledHaskType Γ)) :=
+    ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
+
+  Definition judg2exprType (j:Judg) : Type :=
+    match j with
+      (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ & Exprs Γ Δ ξ τ }
+      end.
+
+  (* reminder: need to pass around uniq-supplies *)
+  Definition rule2expr
+    : forall h j
+      (r:Rule h [j]),
+      ITree _ judg2exprType h ->
+      judg2exprType j.
+  
+      intros.
+      destruct j.
+      refine (match r as R in Rule H C return C=[Γ > Δ > t |- t0] -> _ with
+      | RURule a b c d e    => let case_RURule := tt in _
+      | RNote   x n z        => let case_RNote := tt in _
+      | RLit    Γ Δ l     _    => let case_RLit := tt in _
+      | RVar    Γ Δ σ         p => let case_RVar := tt in _
+      | RLam    Γ Δ Σ tx te   p x => let case_RLam := tt in _
+      | RCast   Γ Δ Σ σ τ γ   p x => let case_RCast := tt in _
+      | RAbsT   Γ Δ Σ κ σ a    => let case_RAbsT := tt in _
+      | RAppT   Γ Δ Σ κ σ τ   p y => let case_RAppT := tt in _
+      | RAppCo  Γ Δ Σ κ σ₁ σ₂ σ γ p  => let case_RAppCo := tt in _
+      | RAbsCo  Γ Δ Σ κ σ cc σ₁ σ₂ p y => let case_RAbsCo := tt in _
+      | RApp    Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
+      | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
+      | RLetRec Γ p lri x y => let case_RLetRec := tt in _
+      | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
+      | REmptyGroup _ _ => let case_REmptyGroup := tt in _
+      | RCase   Σ Γ T κlen κ θ ldcd τ  => let case_RCase := tt in _
+      | RBrak   Σ a b c n m => let case_RBrak := tt in _
+      | REsc    Σ a b c n m => let case_REsc := tt in _
+              end (refl_equal _)  ); intros.
+
+    destruct case_RURule.
+      destruct d; [ destruct o | idtac ]; inversion H; subst.
+      clear H.
+      destruct u.
+      refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with
+      | RLeft   h c ctx r   => let case_RLeft := tt in _
+      | RRight  h c ctx r   => let case_RRight := tt in _
+      | RCanL   t a       => let case_RCanL := tt in _
+      | RCanR   t a       => let case_RCanR := tt in _
+      | RuCanL  t a       => let case_RuCanL := tt in _
+      | RuCanR  t a       => let case_RuCanR := tt in _
+      | RAssoc  t a b c   => let case_RAssoc := tt in _
+      | RCossa  t a b c   => let case_RCossa := tt in _
+      | RExch   t a b     => let case_RExch := tt in _
+      | RWeak   t a       => let case_RWeak := tt in _
+      | RCont   t a       => let case_RCont := tt in _
+              end (refl_equal _)  ); intros.
+
+      destruct case_RCanL. admit.
+      destruct case_RCanR. admit.
+      destruct case_RuCanL. admit.
+      destruct case_RuCanR. admit.
+      destruct case_RAssoc. admit.
+      destruct case_RCossa. admit.
+      destruct case_RLeft. admit.
+      destruct case_RRight. admit.
+      destruct case_RExch. admit.
+      destruct case_RWeak. admit.
+      destruct case_RCont. admit.
+      destruct case_RBrak. admit.
+      destruct case_REsc. admit.
+      destruct case_RNote. admit.
+      destruct case_RLit. admit.
+      destruct case_RVar. admit.
+      destruct case_RLam. admit.
+      destruct case_RCast. admit.
+      destruct case_RBindingGroup. admit.
+      destruct case_RApp. admit.
+      destruct case_RLet. admit.
+      destruct case_REmptyGroup. admit.
+      destruct case_RAppT. admit.
+      destruct case_RAbsT. admit.
+      destruct case_RAppCo. admit.
+      destruct case_RAbsCo. admit.
+      destruct case_RLetRec. admit.
+      destruct case_RCase. admit.
+      Defined.
+
+  Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
+    refine ((
+      fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
+      match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
+      | cnd_weak             => let case_nil    := tt in _
+      | cnd_rule h c cnd' r  => let case_rule   := tt in (fun rest => _) (closed2expr' _ cnd')
+      | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
+      end)); clear closed2expr'; intros; subst.
+
+      destruct case_nil.
+        apply INone.
+
+      destruct case_rule.
+        set (@rule2expr h) as q.
+        destruct c.
+        destruct o.
+        apply ILeaf.
+        eapply rule2expr.
+        apply r.
+        apply rest.
+
+        apply no_rules_with_empty_conclusion in r.
+        inversion r.
+        auto.
+
+        simpl.
+        apply systemfc_all_rules_one_conclusion in r.
+        inversion r.
+
+      destruct case_branch.
+        apply IBranch.
+        apply rest1.
+        apply rest2.
+        Defined.
+
+  Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ & Expr Γ Δ ξ τ }.
+    intro pf.
+    set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+    apply closed2expr in cnd.
+    inversion cnd; subst.
+    simpl in X.
+    clear cnd pf.
+    destruct X.
+    exists x.
+    inversion e.
+    subst.
+    apply X.
+    Defined.
+
+End HaskProofToStrong.