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 {VV:Type} {eqdec_vv:EqDecidable VV}.
  20
  21   Definition Exprs Γ Δ ξ τ :=
  22     ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
  23
  24   Definition judg2exprType (j:Judg) : Type :=
  25     match j with
  26       (Γ > Δ > Σ |- τ) => forall (ξ:VV -> LeveledHaskType Γ ★ ) vars, Σ=mapOptionTree ξ vars -> Exprs Γ Δ ξ τ
  27       end.
  28
  29   Definition judges2exprType (j:Tree ??Judg) : Type :=
  30     ITree _ judg2exprType j.
  31
  32   Definition urule2expr Γ Δ : forall h j (r:@URule Γ Δ h j),
  33     judges2exprType (mapOptionTree UJudg2judg h) -> judges2exprType (mapOptionTree UJudg2judg j).
  34
  35     intros h j r.
  36
  37       refine (match r as R in URule H C
  38                   return judges2exprType (mapOptionTree UJudg2judg H) -> judges2exprType (mapOptionTree UJudg2judg C) with
  39       | RLeft   h c ctx r => let case_RLeft := tt in _
  40       | RRight  h c ctx r => let case_RRight := tt in _
  41       | RCanL   t a       => let case_RCanL := tt in _
  42       | RCanR   t a       => let case_RCanR := tt in _
  43       | RuCanL  t a       => let case_RuCanL := tt in _
  44       | RuCanR  t a       => let case_RuCanR := tt in _
  45       | RAssoc  t a b c   => let case_RAssoc := tt in _
  46       | RCossa  t a b c   => let case_RCossa := tt in _
  47       | RExch   t a b     => let case_RExch := tt in _
  48       | RWeak   t a       => let case_RWeak := tt in _
  49       | RCont   t a       => let case_RCont := tt in _
  50               end   ); intros.
  51
  52       destruct case_RCanL.
  53         apply ILeaf; simpl; intros.
  54         inversion X.
  55         simpl in X0.
  56         apply (X0 ξ ([],,vars)).
  57         simpl; rewrite <- H; auto.
  58
  59       destruct case_RCanR.
  60         apply ILeaf; simpl; intros.
  61         inversion X.
  62         simpl in X0.
  63         apply (X0 ξ (vars,,[])).
  64         simpl; rewrite <- H; auto.
  65
  66       destruct case_RuCanL.
  67         apply ILeaf; simpl; intros.
  68         destruct vars; try destruct o; inversion H.
  69         inversion X.
  70         simpl in X0.
  71         apply (X0 ξ vars2); auto.
  72
  73       destruct case_RuCanR.
  74         apply ILeaf; simpl; intros.
  75         destruct vars; try destruct o; inversion H.
  76         inversion X.
  77         simpl in X0.
  78         apply (X0 ξ vars1); auto.
  79
  80       destruct case_RAssoc.
  81         apply ILeaf; simpl; intros.
  82         inversion X.
  83         simpl in X0.
  84         destruct vars; try destruct o; inversion H.
  85         destruct vars1; try destruct o; inversion H.
  86         apply (X0 ξ (vars1_1,,(vars1_2,,vars2))).
  87         subst; auto.
  88
  89       destruct case_RCossa.
  90         apply ILeaf; simpl; intros.
  91         inversion X.
  92         simpl in X0.
  93         destruct vars; try destruct o; inversion H.
  94         destruct vars2; try destruct o; inversion H.
  95         apply (X0 ξ ((vars1,,vars2_1),,vars2_2)).
  96         subst; auto.
  97
  98       destruct case_RLeft.
  99         (* this will require recursion *)
 100         admit.
 101
 102       destruct case_RRight.
 103         (* this will require recursion *)
 104         admit.
 105
 106       destruct case_RExch.
 107         apply ILeaf; simpl; intros.
 108         inversion X.
 109         simpl in X0.
 110         destruct vars; try destruct o; inversion H.
 111         apply (X0 ξ (vars2,,vars1)).
 112         inversion H; subst; auto.
 113
 114       destruct case_RWeak.
 115         apply ILeaf; simpl; intros.
 116         inversion X.
 117         simpl in X0.
 118         apply (X0 ξ []).
 119         auto.
 120
 121       destruct case_RCont.
 122         apply ILeaf; simpl; intros.
 123         inversion X.
 124         simpl in X0.
 125         apply (X0 ξ (vars,,vars)).
 126         simpl.
 127         rewrite <- H.
 128         auto.
 129         Defined.
 130
 131   Definition rule2expr : forall h j (r:Rule h j), judges2exprType h -> judges2exprType j.
 132
 133     intros h j r.
 134
 135       refine (match r as R in Rule H C return judges2exprType H -> judges2exprType C with
 136       | RURule a b c d e    => let case_RURule := tt in _
 137       | RNote   Γ Δ Σ τ l n         => let case_RNote := tt in _
 138       | RLit    Γ Δ l     _    => let case_RLit := tt in _
 139       | RVar    Γ Δ σ         p => let case_RVar := tt in _
 140       | RGlobal Γ Δ σ l wev     => let case_RGlobal := tt in _
 141       | RLam    Γ Δ Σ tx te     x => let case_RLam := tt in _
 142       | RCast   Γ Δ Σ σ τ γ     x => let case_RCast := tt in _
 143       | RAbsT   Γ Δ Σ κ σ a    => let case_RAbsT := tt in _
 144       | RAppT   Γ Δ Σ κ σ τ     y => let case_RAppT := tt in _
 145       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
 146       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y => let case_RAbsCo := tt in _
 147       | RApp    Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
 148       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
 149       | RLetRec Γ p lri x y => let case_RLetRec := tt in _
 150       | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
 151       | REmptyGroup _ _ => let case_REmptyGroup := tt in _
 152       | RCase   Σ Γ T κlen κ θ ldcd τ  => let case_RCase := tt in _
 153       | RBrak   Σ a b c n m => let case_RBrak := tt in _
 154       | REsc    Σ a b c n m => let case_REsc := tt in _
 155       end); intros.
 156
 157   destruct case_RURule.
 158     eapply urule2expr.
 159     apply e.
 160     apply X.
 161
 162   destruct case_RBrak.
 163     apply ILeaf; simpl; intros; apply ILeaf.
 164     apply EBrak.
 165     inversion X.
 166     set (X0 ξ vars H) as X'.
 167     inversion X'.
 168     apply X1.
 169
 170   destruct case_REsc.
 171     apply ILeaf; simpl; intros; apply ILeaf.
 172     apply EEsc.
 173     inversion X.
 174     set (X0 ξ vars H) as X'.
 175     inversion X'.
 176     apply X1.
 177
 178   destruct case_RNote.
 179     apply ILeaf; simpl; intros; apply ILeaf.
 180     inversion X.
 181     apply ENote.
 182     apply n.
 183     simpl in X0.
 184     set (X0 ξ vars H) as x1.
 185     inversion x1.
 186     apply X1.
 187
 188   destruct case_RLit.
 189     apply ILeaf; simpl; intros; apply ILeaf.
 190     apply ELit.
 191
 192   destruct case_RVar.
 193     apply ILeaf; simpl; intros; apply ILeaf.
 194     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 195     apply EVar.
 196     inversion H.
 197
 198   destruct case_RGlobal.
 199     apply ILeaf; simpl; intros; apply ILeaf.
 200     apply EGlobal.
 201     apply wev.
 202
 203   destruct case_RLam.
 204     apply ILeaf; simpl; intros; apply ILeaf.
 205     (* need a fresh variable here *)
 206     admit.
 207
 208   destruct case_RCast.
 209     apply ILeaf; simpl; intros; apply ILeaf.
 210     eapply ECast.
 211     apply x.
 212     inversion X.
 213     simpl in X0.
 214     set (X0 ξ vars H) as q.
 215     inversion q.
 216     apply X1.
 217
 218   destruct case_RBindingGroup.
 219     apply ILeaf; simpl; intros.
 220     inversion X.
 221     inversion X0.
 222     inversion X1.
 223     destruct vars; inversion H.
 224     destruct o; inversion H5.
 225     set (X2 _ _ H5) as q1.
 226     set (X3 _ _ H6) as q2.
 227     apply IBranch; auto.
 228
 229   destruct case_RApp.
 230     apply ILeaf; simpl; intros; apply ILeaf.
 231     inversion X.
 232     inversion X0.
 233     inversion X1.
 234     destruct vars; try destruct o; inversion H.
 235     set (X2 _ _ H5) as q1.
 236     set (X3 _ _ H6) as q2.
 237     eapply EApp.
 238       inversion q1.
 239       apply X4.
 240       inversion q2.
 241       apply X4.
 242
 243   destruct case_RLet.
 244     apply ILeaf; simpl; intros; apply ILeaf.
 245     (* FIXME: need a var here, and other work *)
 246     admit.
 247
 248   destruct case_REmptyGroup.
 249     apply ILeaf; simpl; intros.
 250     apply INone.
 251
 252   destruct case_RAppT.
 253     apply ILeaf; simpl; intros; apply ILeaf.
 254     apply ETyApp.
 255     inversion X.
 256     set (X0 _ _ H) as q.
 257     inversion q.
 258     apply X1.
 259
 260   destruct case_RAbsT.
 261     apply ILeaf; simpl; intros; apply ILeaf.
 262     apply ETyLam.
 263     inversion X.
 264     simpl in *.
 265     set (X0 (weakLT ○ ξ) vars) as q.
 266     rewrite mapOptionTree_compose in q.
 267     rewrite <- H in q.
 268     set (q (refl_equal _)) as q'.
 269     inversion q'.
 270     apply X1.
 271
 272   destruct case_RAppCo.
 273     apply ILeaf; simpl; intros; apply ILeaf.
 274     eapply ECoApp.
 275     apply γ.
 276     inversion X.
 277     set (X0 _ _ H) as q.
 278     inversion q.
 279     apply X1.
 280
 281   destruct case_RAbsCo.
 282     apply ILeaf; simpl; intros; apply ILeaf.
 283     eapply ECoLam.
 284     inversion X.
 285     set (X0 _ _ H) as q.
 286     inversion q; auto.
 287
 288   destruct case_RLetRec.
 289     admit.
 290
 291   destruct case_RCase.
 292     admit.
 293
 294       Defined.
 295
 296   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 297     refine ((
 298       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 299       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 300       | cnd_weak             => let case_nil    := tt in _
 301       | cnd_rule h c cnd' r  => let case_rule   := tt in (fun rest => _) (closed2expr' _ cnd')
 302       | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
 303       end)); clear closed2expr'; intros; subst.
 304
 305       destruct case_nil.
 306         apply INone.
 307
 308       destruct case_rule.
 309         eapply rule2expr.
 310         apply r.
 311         apply rest.
 312
 313       destruct case_branch.
 314         apply IBranch.
 315         apply rest1.
 316         apply rest2.
 317         Defined.
 318
 319   Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }.
 320     intro pf.
 321     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 322     apply closed2expr in cnd.
 323     inversion cnd; subst.
 324     simpl in X.
 325     clear cnd pf.
 326     destruct X.
 327     exists x.
 328     inversion e.
 329     subst.
 330     apply X.
 331     Defined.
 332
 333 End HaskProofToStrong.