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   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
  87     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
  88   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
  89     match tt with
  90       | T_Leaf None              => nil
  91       | T_Leaf (Some (_ @@ lev)) => lev
  92       | T_Branch b1 b2 =>
  93         match getjlev b1 with
  94           | nil => getjlev b2
  95           | lev => lev
  96         end
  97     end.
  98
  99   Fixpoint take_trustme {Γ}
 100     (n:nat)
 101     (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
 102     : list (HaskType Γ ★) :=
 103
 104     match n with
 105       | 0    => nil
 106       | S n' => (fun TV ite => match l TV ite with
 107                 | nil  => Prelude_error "impossible"
 108                 | a::b => a
 109                 end)
 110                 ::
 111                 take_trustme n' (fun TV ite => match l TV ite with
 112                 | nil  => Prelude_error "impossible"
 113                 | a::b => b
 114                 end)
 115     end.
 116
 117   Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
 118     (forall tv ite, f tv ite = g tv ite) -> f=g.
 119
 120   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
 121     unleaves_
 122     (take_trustme
 123       (count_arg_types (ht _ (ite_unit _)))
 124       (fun TV ite => take_arg_types (ht TV ite))).
 125
 126   Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
 127     fun TV ite => drop_arg_types (ht TV ite).
 128
 129   Implicit Arguments take_arg_types_as_tree [[Γ]].
 130   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 131
 132   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 133     Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
 134       (take_arg_types_as_tree (tx ---> te) @@@ lev).
 135     intros.
 136     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 137       rewrite <- e.
 138       simpl.
 139       apply RId.
 140     unfold take_arg_types_as_tree.
 141       Opaque take_arg_types_as_tree.
 142       simpl.
 143       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 144       simpl.
 145       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 146       apply RCanR.
 147         apply phoas_extensionality.
 148         reflexivity.
 149     apply (Prelude_error "should not be possible").
 150     Defined.
 151     Transparent take_arg_types_as_tree.
 152
 153   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 154     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
 155       ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
 156     intros.
 157     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 158       rewrite <- e.
 159       simpl.
 160       apply RId.
 161     unfold take_arg_types_as_tree.
 162       Opaque take_arg_types_as_tree.
 163       simpl.
 164       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 165       simpl.
 166       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 167       apply RuCanR.
 168         apply phoas_extensionality.
 169         reflexivity.
 170     apply (Prelude_error "should not be possible").
 171     Defined.
 172     Transparent take_arg_types_as_tree.
 173
 174   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
 175     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
 176     intros.
 177     unfold drop_arg_types_as_tree.
 178     simpl.
 179     reflexivity.
 180     Qed.
 181
 182   Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
 183 (*  | SFlat  : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
 184   | SFlat  : forall h c, Rule h c -> SRule h c
 185   | SBrak  : forall Γ Δ t ec Σ l,
 186     SRule
 187     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
 188     [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
 189
 190   | SEsc   : forall Γ Δ t ec Σ l,
 191     SRule
 192     [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
 193     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
 194     .
 195
 196   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 197     match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
 198
 199   Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 200     match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
 201
 202   Definition skolemize_judgment (j:Judg) : Judg :=
 203     match j with
 204       Γ > Δ > Σ₁ |- Σ₂ =>
 205         match getjlev Σ₂ with
 206           | nil => j
 207           | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
 208         end
 209     end.
 210
 211   Definition check_hof : forall {Γ}(t:HaskType Γ ★),
 212     sumbool
 213     True
 214     (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
 215     intros.
 216     destruct (eqd_dec (take_arg_types_as_tree t) []);
 217     destruct (eqd_dec (drop_arg_types_as_tree t) t).
 218     right; auto.
 219     left; auto.
 220     left; auto.
 221     left; auto.
 222     Defined.
 223
 224   Opaque take_arg_types_as_tree.
 225   Definition skolemize_proof :
 226     forall  {h}{c},
 227       ND Rule  h c ->
 228       ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
 229     intros.
 230     eapply nd_map'; [ idtac | apply X ].
 231     clear h c X.
 232     intros.
 233
 234     refine (match X as R in Rule H C with
 235       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 236       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 237       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 238       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 239       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 240       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 241       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 242       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 243       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 244       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 245       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 246       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 247       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 248       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
 249       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 250       | RVoid    _ _                   => let case_RVoid := tt   in _
 251       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
 252       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
 253       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 254       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 255       end); clear X h c.
 256
 257       destruct case_RArrange.
 258         simpl.
 259         destruct (getjlev x).
 260         apply nd_rule.
 261         apply SFlat.
 262         apply RArrange.
 263         apply d.
 264         apply nd_rule.
 265         apply SFlat.
 266         apply RArrange.
 267         apply RRight.
 268         apply d.
 269
 270       destruct case_RBrak.
 271         simpl.
 272         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 273         apply nd_rule.
 274         apply SBrak.
 275
 276       destruct case_REsc.
 277         simpl.
 278         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 279         apply nd_rule.
 280         apply SEsc.
 281
 282       destruct case_RNote.
 283         apply nd_rule.
 284         apply SFlat.
 285         simpl.
 286         destruct l.
 287         apply RNote.
 288         apply n.
 289         apply RNote.
 290         apply n.
 291
 292       destruct case_RLit.
 293         simpl.
 294         destruct l0.
 295         apply nd_rule.
 296         apply SFlat.
 297         apply RLit.
 298         set (check_hof (@literalType l Γ)) as hof.
 299         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 300         destruct a.
 301         rewrite H.
 302         rewrite H0.
 303         simpl.
 304         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
 305         apply nd_rule.
 306         apply SFlat.
 307         apply RLit.
 308
 309       destruct case_RVar.
 310         simpl.
 311         destruct lev.
 312         apply nd_rule; apply SFlat; apply RVar.
 313         set (check_hof σ) as hof.
 314         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 315         destruct a.
 316         rewrite H.
 317         rewrite H0.
 318         simpl.
 319         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 320         apply nd_rule.
 321         apply SFlat.
 322         apply RVar.
 323
 324       destruct case_RGlobal.
 325         simpl.
 326         destruct σ.
 327         apply nd_rule; apply SFlat; apply RGlobal.
 328         set (check_hof (l wev)) as hof.
 329         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 330         destruct a.
 331         rewrite H.
 332         rewrite H0.
 333         simpl.
 334         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 335         apply nd_rule.
 336         apply SFlat.
 337         apply RGlobal.
 338
 339       destruct case_RLam.
 340         destruct lev.
 341           apply nd_rule.
 342           apply SFlat.
 343           simpl.
 344           apply RLam.
 345         simpl.
 346         rewrite drop_works.
 347         apply nd_rule.
 348           apply SFlat.
 349           apply RArrange.
 350           eapply RComp.
 351           eapply RCossa.
 352           eapply RLeft.
 353           apply take_arrange.
 354
 355       destruct case_RCast.
 356         simpl.
 357         destruct lev.
 358         apply nd_rule.
 359         apply SFlat.
 360         apply RCast.
 361         apply γ.
 362         apply (Prelude_error "found RCast at level >0").
 363
 364       destruct case_RJoin.
 365         simpl.
 366         destruct (getjlev x).
 367         destruct (getjlev q).
 368         apply nd_rule.
 369         apply SFlat.
 370         apply RJoin.
 371         apply (Prelude_error "found RJoin at level >0").
 372         apply (Prelude_error "found RJoin at level >0").
 373
 374       destruct case_RApp.
 375         simpl.
 376         destruct lev.
 377         apply nd_rule.
 378         apply SFlat.
 379         apply RApp.
 380         rewrite drop_works.
 381         set (check_hof tx) as hof_tx.
 382         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 383         destruct a.
 384         rewrite H.
 385         rewrite H0.
 386         simpl.
 387         eapply nd_comp.
 388         eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
 389         eapply nd_rule.
 390         eapply SFlat.
 391         eapply RArrange.
 392         eapply RLeft.
 393         eapply take_unarrange.
 394
 395         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 396         eapply nd_rule; eapply SFlat; apply RWhere.
 397
 398       destruct case_RLet.
 399         simpl.
 400         destruct lev.
 401         apply nd_rule.
 402         apply SFlat.
 403         apply RLet.
 404         set (check_hof σ₁) as hof_tx.
 405         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 406         destruct a.
 407         rewrite H.
 408         rewrite H0.
 409
 410         eapply nd_comp.
 411         eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
 412
 413         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
 414         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 415         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
 416         apply nd_prod.
 417           apply nd_id.
 418           apply nd_rule.
 419           eapply SFlat.
 420           eapply RArrange.
 421           eapply RCossa.
 422
 423       destruct case_RWhere.
 424         simpl.
 425         destruct lev.
 426         apply nd_rule.
 427         apply SFlat.
 428         apply RWhere.
 429         set (check_hof σ₁) as hof_tx.
 430         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 431         destruct a.
 432         rewrite H.
 433         rewrite H0.
 434
 435         eapply nd_comp.
 436         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
 437         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
 438         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
 439         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
 440         apply nd_prod; [ idtac | eapply nd_id ].
 441         eapply nd_rule; apply SFlat; eapply RArrange.
 442         eapply RComp.
 443         eapply RCossa.
 444         apply RLeft.
 445         eapply RCossa.
 446
 447       destruct case_RVoid.
 448         simpl.
 449         apply nd_rule.
 450         apply SFlat.
 451         apply RVoid.
 452
 453       destruct case_RAppT.
 454         simpl.
 455         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 456         apply (Prelude_error "RAppT at depth>0").
 457
 458       destruct case_RAbsT.
 459         simpl.
 460         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 461         apply (Prelude_error "RAbsT at depth>0").
 462
 463       destruct case_RAppCo.
 464         simpl.
 465         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 466         apply γ.
 467         apply (Prelude_error "RAppCo at depth>0").
 468
 469       destruct case_RAbsCo.
 470         simpl.
 471         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 472         apply (Prelude_error "RAbsCo at depth>0").
 473
 474       destruct case_RLetRec.
 475         simpl.
 476         destruct t.
 477         destruct (getjlev (y @@@ nil)).
 478         apply nd_rule.
 479         apply SFlat.
 480         apply (@RLetRec Γ Δ lri x y nil).
 481         apply (Prelude_error "RLetRec at depth>0").
 482         apply (Prelude_error "RLetRec at depth>0").
 483
 484       destruct case_RCase.
 485         simpl.
 486         apply (Prelude_error "CASE: BIG FIXME").
 487         Defined.
 488   Transparent take_arg_types_as_tree.
 489
 490 End HaskSkolemizer.