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