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