src/HaskProofToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofToStrong: convert HaskProof to HaskStrong                                                                            *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskStrongTypes.
  14 Require Import HaskStrong.
  15 Require Import HaskProof.
  16
  17 Section HaskProofToStrong.
  18
  19   Context
  20     {VV:Type}
  21     {eqdec_vv:EqDecidable VV}
  22     {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}.
  23
  24   Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ)(τ:Tree ??(LeveledHaskType Γ)) :=
  25     ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
  26
  27   Definition judg2exprType (j:Judg) : Type :=
  28     match j with
  29       (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ & Exprs Γ Δ ξ τ }
  30       end.
  31
  32   (* reminder: need to pass around uniq-supplies *)
  33   Definition rule2expr
  34     : forall h j
  35       (r:Rule h [j]),
  36       ITree _ judg2exprType h ->
  37       judg2exprType j.
  38
  39       intros.
  40       destruct j.
  41       refine (match r as R in Rule H C return C=[Γ > Δ > t |- t0] -> _ with
  42       | RURule a b c d e    => let case_RURule := tt in _
  43       | RNote   x n z        => let case_RNote := tt in _
  44       | RLit    Γ Δ l     _    => let case_RLit := tt in _
  45       | RVar    Γ Δ σ         p => let case_RVar := tt in _
  46       | RLam    Γ Δ Σ tx te   p x => let case_RLam := tt in _
  47       | RCast   Γ Δ Σ σ τ γ   p x => let case_RCast := tt in _
  48       | RAbsT   Γ Δ Σ κ σ a    => let case_RAbsT := tt in _
  49       | RAppT   Γ Δ Σ κ σ τ   p y => let case_RAppT := tt in _
  50       | RAppCo  Γ Δ Σ κ σ₁ σ₂ σ γ p  => let case_RAppCo := tt in _
  51       | RAbsCo  Γ Δ Σ κ σ cc σ₁ σ₂ p y => let case_RAbsCo := tt in _
  52       | RApp    Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
  53       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
  54       | RLetRec Γ p lri x y => let case_RLetRec := tt in _
  55       | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
  56       | REmptyGroup _ _ => let case_REmptyGroup := tt in _
  57       | RCase   Σ Γ T κlen κ θ ldcd τ  => let case_RCase := tt in _
  58       | RBrak   Σ a b c n m => let case_RBrak := tt in _
  59       | REsc    Σ a b c n m => let case_REsc := tt in _
  60               end (refl_equal _)  ); intros.
  61
  62     destruct case_RURule.
  63       destruct d; [ destruct o | idtac ]; inversion H; subst.
  64       clear H.
  65       destruct u.
  66       refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with
  67       | RLeft   h c ctx r   => let case_RLeft := tt in _
  68       | RRight  h c ctx r   => let case_RRight := tt in _
  69       | RCanL   t a       => let case_RCanL := tt in _
  70       | RCanR   t a       => let case_RCanR := tt in _
  71       | RuCanL  t a       => let case_RuCanL := tt in _
  72       | RuCanR  t a       => let case_RuCanR := tt in _
  73       | RAssoc  t a b c   => let case_RAssoc := tt in _
  74       | RCossa  t a b c   => let case_RCossa := tt in _
  75       | RExch   t a b     => let case_RExch := tt in _
  76       | RWeak   t a       => let case_RWeak := tt in _
  77       | RCont   t a       => let case_RCont := tt in _
  78               end (refl_equal _)  ); intros.
  79
  80       destruct case_RCanL. admit.
  81       destruct case_RCanR. admit.
  82       destruct case_RuCanL. admit.
  83       destruct case_RuCanR. admit.
  84       destruct case_RAssoc. admit.
  85       destruct case_RCossa. admit.
  86       destruct case_RLeft. admit.
  87       destruct case_RRight. admit.
  88       destruct case_RExch. admit.
  89       destruct case_RWeak. admit.
  90       destruct case_RCont. admit.
  91       destruct case_RBrak. admit.
  92       destruct case_REsc. admit.
  93       destruct case_RNote. admit.
  94       destruct case_RLit. admit.
  95       destruct case_RVar. admit.
  96       destruct case_RLam. admit.
  97       destruct case_RCast. admit.
  98       destruct case_RBindingGroup. admit.
  99       destruct case_RApp. admit.
 100       destruct case_RLet. admit.
 101       destruct case_REmptyGroup. admit.
 102       destruct case_RAppT. admit.
 103       destruct case_RAbsT. admit.
 104       destruct case_RAppCo. admit.
 105       destruct case_RAbsCo. admit.
 106       destruct case_RLetRec. admit.
 107       destruct case_RCase. admit.
 108       Defined.
 109
 110   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 111     refine ((
 112       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 113       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 114       | cnd_weak             => let case_nil    := tt in _
 115       | cnd_rule h c cnd' r  => let case_rule   := tt in (fun rest => _) (closed2expr' _ cnd')
 116       | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
 117       end)); clear closed2expr'; intros; subst.
 118
 119       destruct case_nil.
 120         apply INone.
 121
 122       destruct case_rule.
 123         set (@rule2expr h) as q.
 124         destruct c.
 125         destruct o.
 126         apply ILeaf.
 127         eapply rule2expr.
 128         apply r.
 129         apply rest.
 130
 131         apply no_rules_with_empty_conclusion in r.
 132         inversion r.
 133         auto.
 134
 135         simpl.
 136         apply systemfc_all_rules_one_conclusion in r.
 137         inversion r.
 138
 139       destruct case_branch.
 140         apply IBranch.
 141         apply rest1.
 142         apply rest2.
 143         Defined.
 144
 145   Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ & Expr Γ Δ ξ τ }.
 146     intro pf.
 147     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 148     apply closed2expr in cnd.
 149     inversion cnd; subst.
 150     simpl in X.
 151     clear cnd pf.
 152     destruct X.
 153     exists x.
 154     inversion e.
 155     subst.
 156     apply X.
 157     Defined.
 158
 159 End HaskProofToStrong.