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