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       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 249       | RVoid    _ _                   => let case_RVoid := tt   in _
 250       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 251       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 252       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 253       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 254       end); clear X h c.
 255
 256       destruct case_RArrange.
 257         simpl.
 258         destruct (getjlev x).
 259         apply nd_rule.
 260         apply SFlat.
 261         apply RArrange.
 262         apply d.
 263         apply nd_rule.
 264         apply SFlat.
 265         apply RArrange.
 266         apply RRight.
 267         apply d.
 268
 269       destruct case_RBrak.
 270         simpl.
 271         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 272         apply nd_rule.
 273         apply SBrak.
 274
 275       destruct case_REsc.
 276         simpl.
 277         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 278         apply nd_rule.
 279         apply SEsc.
 280
 281       destruct case_RNote.
 282         apply nd_rule.
 283         apply SFlat.
 284         simpl.
 285         destruct l.
 286         apply RNote.
 287         apply n.
 288         apply RNote.
 289         apply n.
 290
 291       destruct case_RLit.
 292         simpl.
 293         destruct l0.
 294         apply nd_rule.
 295         apply SFlat.
 296         apply RLit.
 297         set (check_hof (@literalType l Γ)) as hof.
 298         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 299         destruct a.
 300         rewrite H.
 301         rewrite H0.
 302         simpl.
 303         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
 304         apply nd_rule.
 305         apply SFlat.
 306         apply RLit.
 307
 308       destruct case_RVar.
 309         simpl.
 310         destruct lev.
 311         apply nd_rule; apply SFlat; apply RVar.
 312         set (check_hof σ) as hof.
 313         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 314         destruct a.
 315         rewrite H.
 316         rewrite H0.
 317         simpl.
 318         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 319         apply nd_rule.
 320         apply SFlat.
 321         apply RVar.
 322
 323       destruct case_RGlobal.
 324         simpl.
 325         destruct σ.
 326         apply nd_rule; apply SFlat; apply RGlobal.
 327         set (check_hof (l wev)) as hof.
 328         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 329         destruct a.
 330         rewrite H.
 331         rewrite H0.
 332         simpl.
 333         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
 334         apply nd_rule.
 335         apply SFlat.
 336         apply RGlobal.
 337
 338       destruct case_RLam.
 339         destruct lev.
 340           apply nd_rule.
 341           apply SFlat.
 342           simpl.
 343           apply RLam.
 344         simpl.
 345         rewrite drop_works.
 346         apply nd_rule.
 347           apply SFlat.
 348           apply RArrange.
 349           eapply RComp.
 350           apply RCossa.
 351           apply RLeft.
 352           apply take_arrange.
 353
 354       destruct case_RCast.
 355         simpl.
 356         destruct lev.
 357         apply nd_rule.
 358         apply SFlat.
 359         apply RCast.
 360         apply γ.
 361         apply (Prelude_error "found RCast at level >0").
 362
 363       destruct case_RJoin.
 364         simpl.
 365         destruct (getjlev x).
 366         destruct (getjlev q).
 367         apply nd_rule.
 368         apply SFlat.
 369         apply RJoin.
 370         apply (Prelude_error "found RJoin at level >0").
 371         apply (Prelude_error "found RJoin at level >0").
 372
 373       destruct case_RApp.
 374         simpl.
 375         destruct lev.
 376         apply nd_rule.
 377         apply SFlat.
 378         apply RApp.
 379         rewrite drop_works.
 380         set (check_hof tx) as hof_tx.
 381         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 382         destruct a.
 383         rewrite H.
 384         rewrite H0.
 385         simpl.
 386         set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
 387         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 388         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
 389         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
 390         clear q.
 391         apply nd_prod.
 392         apply nd_rule.
 393         apply SFlat.
 394         apply RArrange.
 395         apply RCanR.
 396         apply nd_rule.
 397           apply SFlat.
 398           apply RArrange.
 399           eapply RComp; [ idtac | eapply RAssoc ].
 400           apply RLeft.
 401           eapply RComp; [ idtac | apply RExch ].
 402           apply take_unarrange.
 403
 404       destruct case_RLet.
 405         simpl.
 406         destruct lev.
 407         apply nd_rule.
 408         apply SFlat.
 409         apply RLet.
 410         set (check_hof σ₂) as hof_tx.
 411         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 412         destruct a.
 413         rewrite H.
 414         rewrite H0.
 415         set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
 416         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 417         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
 418         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
 419         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
 420         clear q.
 421         apply nd_prod.
 422         apply nd_rule.
 423         apply SFlat.
 424         apply RArrange.
 425         apply RCanR.
 426         eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
 427         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
 428         apply nd_rule.
 429         apply SFlat.
 430         apply RArrange.
 431         apply RLeft.
 432         eapply RExch.
 433
 434       destruct case_RVoid.
 435         simpl.
 436         apply nd_rule.
 437         apply SFlat.
 438         apply RVoid.
 439
 440       destruct case_RAppT.
 441         simpl.
 442         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 443         apply (Prelude_error "RAppT at depth>0").
 444
 445       destruct case_RAbsT.
 446         simpl.
 447         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 448         apply (Prelude_error "RAbsT at depth>0").
 449
 450       destruct case_RAppCo.
 451         simpl.
 452         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 453         apply γ.
 454         apply (Prelude_error "RAppCo at depth>0").
 455
 456       destruct case_RAbsCo.
 457         simpl.
 458         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 459         apply (Prelude_error "RAbsCo at depth>0").
 460
 461       destruct case_RLetRec.
 462         simpl.
 463         destruct t.
 464         destruct (getjlev (y @@@ nil)).
 465         apply nd_rule.
 466         apply SFlat.
 467         apply (@RLetRec Γ Δ lri x y nil).
 468         apply (Prelude_error "RLetRec at depth>0").
 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   Transparent take_arg_types_as_tree.
 476
 477 End HaskSkolemizer.