src/HaskSkolemizer.v

   1 (*********************************************************************************************************************************)
   2 (* HaskSkolemizer:                                                                                                               *)
   3 (*                                                                                                                               *)
   4 (*   Skolemizes the portion of a proof which uses judgments at level >0                                                          *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskCoreVars.
  18 Require Import HaskWeakTypes.
  19 Require Import HaskWeakVars.
  20 Require Import HaskLiterals.
  21 Require Import HaskTyCons.
  22 Require Import HaskStrongTypes.
  23 Require Import HaskProof.
  24 Require Import NaturalDeduction.
  25
  26 Require Import HaskStrongTypes.
  27 Require Import HaskStrong.
  28 Require Import HaskProof.
  29 Require Import HaskStrongToProof.
  30 Require Import HaskProofToStrong.
  31 Require Import HaskWeakToStrong.
  32
  33 Open Scope nd_scope.
  34 Set Printing Width 130.
  35
  36 Section HaskSkolemizer.
  37
  38 (*
  39   Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
  40      match exp with
  41     | TVar    _  x          => x
  42     | TAll     _ y          => TAll   _  (fun v => debruijn2phoas  (y (TVar v)))
  43     | TApp   _ _ x y        => TApp      (debruijn2phoas  x) (debruijn2phoas  y)
  44     | TCon       tc         => TCon      tc
  45     | TCoerc _ t1 t2 t      => TCoerc    (debruijn2phoas  t1) (debruijn2phoas  t2)   (debruijn2phoas  t)
  46     | TArrow                => TArrow
  47     | TCode      v e        => TCode     (debruijn2phoas  v) (debruijn2phoas  e)
  48     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
  49     end
  50     with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
  51     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
  52     | TyFunApp_nil               => TyFunApp_nil
  53     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas  t) (debruijn2phoasyFunApp _ rest)
  54     end.
  55 *)
  56   Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
  57     match r with
  58       | RBrak _ _ _ _ _ _ => False
  59       | REsc  _ _ _ _ _ _ => False
  60       | _                 => True
  61     end.
  62
  63   Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
  64     match lt with
  65       | nil => t
  66       | a::b => mkArrows b (a ---> t)
  67     end.
  68
  69 (*
  70   Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
  71     match l with
  72       | nil  => t
  73       | a::b => unleaves_ (t,,[a @@ lev]) b lev
  74     end.
  75 *)
  76   (* weak inverse of "leaves" *)
  77   Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
  78     match l with
  79       | nil      => []
  80       | (a::nil) => [a]
  81       | (a::b)   => [a],,(unleaves_ b)
  82     end.
  83
  84   (* rules of skolemized proofs *)
  85   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.
  86
  87   Fixpoint take_trustme {Γ}
  88     (n:nat)
  89     (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
  90     : list (HaskType Γ ★) :=
  91
  92     match n with
  93       | 0    => nil
  94       | S n' => (fun TV ite => match l TV ite with
  95                 | nil  => Prelude_error "impossible"
  96                 | a::b => a
  97                 end)
  98                 ::
  99                 take_trustme n' (fun TV ite => match l TV ite with
 100                 | nil  => Prelude_error "impossible"
 101                 | a::b => b
 102                 end)
 103     end.
 104
 105   Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
 106     (forall tv ite, f tv ite = g tv ite) -> f=g.
 107
 108   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
 109     unleaves_
 110     (take_trustme
 111       (count_arg_types (ht _ (ite_unit _)))
 112       (fun TV ite => take_arg_types (ht TV ite))).
 113
 114   Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
 115     fun TV ite => drop_arg_types (ht TV ite).
 116
 117   Implicit Arguments take_arg_types_as_tree [[Γ]].
 118   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 119
 120   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 121     Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
 122       (take_arg_types_as_tree (tx ---> te) @@@ lev).
 123     intros.
 124     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 125       rewrite <- e.
 126       simpl.
 127       apply RId.
 128     unfold take_arg_types_as_tree.
 129       Opaque take_arg_types_as_tree.
 130       simpl.
 131       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 132       simpl.
 133       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 134       apply RCanR.
 135         apply phoas_extensionality.
 136         reflexivity.
 137     apply (Prelude_error "should not be possible").
 138     Defined.
 139     Transparent take_arg_types_as_tree.
 140
 141   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 142     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
 143       ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
 144     intros.
 145     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 146       rewrite <- e.
 147       simpl.
 148       apply RId.
 149     unfold take_arg_types_as_tree.
 150       Opaque take_arg_types_as_tree.
 151       simpl.
 152       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 153       simpl.
 154       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 155       apply RuCanR.
 156         apply phoas_extensionality.
 157         reflexivity.
 158     apply (Prelude_error "should not be possible").
 159     Defined.
 160     Transparent take_arg_types_as_tree.
 161
 162   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
 163     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
 164     intros.
 165     unfold drop_arg_types_as_tree.
 166     simpl.
 167     reflexivity.
 168     Qed.
 169
 170   Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
 171 (*  | SFlat  : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
 172   | SFlat  : forall h c, Rule h c -> SRule h c
 173   | SBrak  : forall Γ Δ t ec Σ l,
 174     SRule
 175     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        ] @ (ec::l)]
 176     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 177
 178   | SEsc   : forall Γ Δ t ec Σ l,
 179     SRule
 180     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 181     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t         ] @ (ec::l)]
 182     .
 183
 184   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 185     match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
 186
 187   Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 188     match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
 189
 190   Definition skolemize_judgment (j:Judg) : Judg :=
 191     match j with
 192       | Γ > Δ > Σ₁ |- Σ₂ @ nil       => j
 193         | Γ > Δ > Σ₁ |- Σ₂ @ lev =>
 194           Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev
 195     end.
 196
 197   Definition check_hof : forall {Γ}(t:HaskType Γ ★),
 198     sumbool
 199     True
 200     (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
 201     intros.
 202     destruct (eqd_dec (take_arg_types_as_tree t) []);
 203     destruct (eqd_dec (drop_arg_types_as_tree t) t).
 204     right; auto.
 205     left; auto.
 206     left; auto.
 207     left; auto.
 208     Defined.
 209
 210   Opaque take_arg_types_as_tree.
 211   Definition skolemize_proof :
 212     forall  {h}{c},
 213       ND Rule  h c ->
 214       ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
 215     intros.
 216     eapply nd_map'; [ idtac | apply X ].
 217     clear h c X.
 218     intros.
 219
 220     refine (match X as R in Rule H C with
 221       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 222       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 223       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 224       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 225       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 226       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 227       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 228       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 229       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 230       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 231       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 232       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 233       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 234       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
 235       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
 236       | RVoid    _ _           l       => let case_RVoid := tt   in _
 237       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
 238       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
 239       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 240       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 241       end); clear X h c.
 242
 243       destruct case_RArrange.
 244         simpl.
 245         destruct l.
 246         apply nd_rule.
 247         apply SFlat.
 248         apply RArrange.
 249         apply d.
 250         apply nd_rule.
 251         apply SFlat.
 252         apply RArrange.
 253         apply RRight.
 254         apply d.
 255
 256       destruct case_RBrak.
 257         simpl.
 258         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 259         apply nd_rule.
 260         apply SBrak.
 261
 262       destruct case_REsc.
 263         simpl.
 264         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 265         apply nd_rule.
 266         apply SEsc.
 267
 268       destruct case_RNote.
 269         apply nd_rule.
 270         apply SFlat.
 271         simpl.
 272         destruct l.
 273         apply RNote.
 274         apply n.
 275         apply RNote.
 276         apply n.
 277
 278       destruct case_RLit.
 279         simpl.
 280         destruct l0.
 281         apply nd_rule.
 282         apply SFlat.
 283         apply RLit.
 284         set (check_hof (@literalType l Γ)) as hof.
 285         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 286         destruct a.
 287         rewrite H.
 288         rewrite H0.
 289         simpl.
 290         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
 291         apply nd_rule.
 292         apply SFlat.
 293         apply RLit.
 294
 295       destruct case_RVar.
 296         simpl.
 297         destruct lev.
 298         apply nd_rule; apply SFlat; apply RVar.
 299         set (check_hof σ) as hof.
 300         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 301         destruct a.
 302         rewrite H.
 303         rewrite H0.
 304         simpl.
 305         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 306         apply nd_rule.
 307         apply SFlat.
 308         apply RVar.
 309
 310       destruct case_RGlobal.
 311         simpl.
 312         destruct σ.
 313         apply nd_rule; apply SFlat; apply RGlobal.
 314         set (check_hof (l wev)) as hof.
 315         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 316         destruct a.
 317         rewrite H.
 318         rewrite H0.
 319         simpl.
 320         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 321         apply nd_rule.
 322         apply SFlat.
 323         apply RGlobal.
 324
 325       destruct case_RLam.
 326         destruct lev.
 327           apply nd_rule.
 328           apply SFlat.
 329           simpl.
 330           apply RLam.
 331         simpl.
 332         rewrite drop_works.
 333         apply nd_rule.
 334           apply SFlat.
 335           apply RArrange.
 336           eapply RComp.
 337           eapply RCossa.
 338           eapply RLeft.
 339           apply take_arrange.
 340
 341       destruct case_RCast.
 342         simpl.
 343         destruct lev.
 344         apply nd_rule.
 345         apply SFlat.
 346         apply RCast.
 347         apply γ.
 348         apply (Prelude_error "found RCast at level >0").
 349
 350       destruct case_RJoin.
 351         simpl.
 352         destruct l.
 353         apply nd_rule.
 354         apply SFlat.
 355         apply RJoin.
 356         apply (Prelude_error "found RJoin at level >0").
 357
 358       destruct case_RApp.
 359         simpl.
 360         destruct lev.
 361         apply nd_rule.
 362         apply SFlat.
 363         apply RApp.
 364         rewrite drop_works.
 365         set (check_hof tx) as hof_tx.
 366         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 367         destruct a.
 368         rewrite H.
 369         rewrite H0.
 370         simpl.
 371         eapply nd_comp.
 372         eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
 373         eapply nd_rule.
 374         eapply SFlat.
 375         eapply RArrange.
 376         eapply RLeft.
 377         eapply take_unarrange.
 378
 379         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 380         eapply nd_rule; eapply SFlat; apply RWhere.
 381
 382       destruct case_RLet.
 383         simpl.
 384         destruct lev.
 385         apply nd_rule.
 386         apply SFlat.
 387         apply RLet.
 388         set (check_hof σ₁) as hof_tx.
 389         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 390         destruct a.
 391         rewrite H.
 392         rewrite H0.
 393
 394         eapply nd_comp.
 395         eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
 396
 397         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
 398         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 399         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
 400         apply nd_prod.
 401           apply nd_id.
 402           apply nd_rule.
 403           eapply SFlat.
 404           eapply RArrange.
 405           eapply RCossa.
 406
 407       destruct case_RWhere.
 408         simpl.
 409         destruct lev.
 410         apply nd_rule.
 411         apply SFlat.
 412         apply RWhere.
 413         set (check_hof σ₁) as hof_tx.
 414         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 415         destruct a.
 416         rewrite H.
 417         rewrite H0.
 418
 419         eapply nd_comp.
 420         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
 421         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
 422         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
 423         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
 424         apply nd_prod; [ idtac | eapply nd_id ].
 425         eapply nd_rule; apply SFlat; eapply RArrange.
 426         eapply RComp.
 427         eapply RCossa.
 428         apply RLeft.
 429         eapply RCossa.
 430
 431       destruct case_RVoid.
 432         simpl.
 433         destruct l.
 434         apply nd_rule.
 435         apply SFlat.
 436         apply RVoid.
 437         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ].
 438         apply nd_rule.
 439         apply SFlat.
 440         apply RVoid.
 441
 442       destruct case_RAppT.
 443         simpl.
 444         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 445         apply (Prelude_error "RAppT at depth>0").
 446
 447       destruct case_RAbsT.
 448         simpl.
 449         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 450         apply (Prelude_error "RAbsT at depth>0").
 451
 452       destruct case_RAppCo.
 453         simpl.
 454         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 455         apply γ.
 456         apply (Prelude_error "RAppCo at depth>0").
 457
 458       destruct case_RAbsCo.
 459         simpl.
 460         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 461         apply (Prelude_error "RAbsCo at depth>0").
 462
 463       destruct case_RLetRec.
 464         simpl.
 465         destruct t.
 466         apply nd_rule.
 467         apply SFlat.
 468         apply (@RLetRec Γ Δ lri x y nil).
 469         apply (Prelude_error "RLetRec at depth>0").
 470
 471       destruct case_RCase.
 472         simpl.
 473         apply (Prelude_error "CASE: BIG FIXME").
 474         Defined.
 475
 476   Transparent take_arg_types_as_tree.
 477
 478 End HaskSkolemizer.