removing busted proof of cast removal dynamics; see #45

hazelgrove · Oct 5, 2018 · d21bcd5 · d21bcd5
1 parent 64aeff2
commit d21bcd5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 70 deletions.
diff --git a/all.agda b/all.agda
@@ -41,7 +41,7 @@ open import progress
 open import preservation
 
 open import lemmas-complete
--- open import cast-inert
+open import cast-inert
 open import complete-preservation
 open import complete-progress
 open import complete-expansion

diff --git a/cast-inert.agda b/cast-inert.agda
@@ -52,72 +52,3 @@ module cast-inert where
   no-id-casts-type (TANEHole x wt x₁) (NICNEHole nic) = TANEHole x (no-id-casts-type wt nic) x₁
   no-id-casts-type (TACast wt x) (NICCast nic) = no-id-casts-type wt nic
   no-id-casts-type (TAFailedCast wt x x₁ x₂) (NICFailed nic) = TAFailedCast (no-id-casts-type wt nic) x x₁ x₂
-
-  -- simple lemma used below; if an application is final so is each
-  -- applicand. saves some redundant pattern matching.
-  ap-final : ∀{d1 d2} → (d1 ∘ d2) final → d1 final × d2 final
-  ap-final (FBoxed (BVVal ()))
-  ap-final (FIndet (IAp x x₁ x₂)) = FIndet x₁ , x₂
-
-  -- removing identity casts doesn't change the ultimate answer produced
-  remove-casts-same : ∀{Δ d1 d2 d1' d2' Γ τ } →
-                           Δ , Γ ⊢ d1 :: τ →
-                           no-id-casts d1 d2 →
-                           d1 ↦* d1' →
-                           d2 ↦* d2' →
-                           d1' final →
-                           d2' final →
-                           d1' == d2'
-  remove-casts-same TAConst NICConst step1 step2 f1 f2 = ! (finality* (FBoxed (BVVal VConst)) step1) · finality* (FBoxed (BVVal VConst)) step2
-
-  remove-casts-same (TAVar x₁) NICVar MSRefl step2 (FBoxed (BVVal ())) f2
-  remove-casts-same (TAVar x₁) NICVar MSRefl step2 (FIndet ()) f2
-  remove-casts-same (TAVar x₁) NICVar (MSStep (Step FHOuter () FHOuter) step1) step2 f1 f2
-
-  remove-casts-same (TALam x₁ wt) (NICLam nic) MSRefl MSRefl (FBoxed (BVVal VLam)) (FBoxed (BVVal VLam)) = {!!} -- ap1 (λ qq → ·λ _ [ _ ] qq) {!!}
-  remove-casts-same (TALam x₁ wt) (NICLam nic) MSRefl MSRefl _ (FIndet ())
-  remove-casts-same (TALam x₁ wt) (NICLam nic) MSRefl MSRefl (FIndet ()) _
-  remove-casts-same (TALam x₁ wt) (NICLam nic) _ (MSStep x₂ step2) f1 f2 = abort (boxedval-not-step (BVVal VLam) ( _ , x₂))
-  remove-casts-same (TALam x₁ wt) (NICLam nic) (MSStep x₂ step1) _ f1 f2 = abort (boxedval-not-step (BVVal VLam) ( _ , x₂))
-
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) MSRefl step2 (FBoxed (BVVal ())) f2
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) MSRefl MSRefl (FIndet (IAp x x₁ x₂)) f2 with remove-casts-same wt nic MSRefl MSRefl (FIndet x₁) (π1 (ap-final f2))
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) MSRefl MSRefl (FIndet (IAp x x₁ x₂)) f2 | refl with remove-casts-same wt₁ nic₁ MSRefl MSRefl x₂ (π2 (ap-final f2))
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) MSRefl MSRefl (FIndet (IAp x x₁ x₂)) f2 | refl | refl = refl
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) _ (MSStep x step2) (FIndet (IAp x₁ x₂ x₃)) f2 = {!!}
-  remove-casts-same (TAAp wt wt₁) (NICAp nic nic₁) (MSStep x step1) step2 f1 f2 = {!!}
-
-  remove-casts-same (TAEHole x x₁) NICHole MSRefl step2 (FBoxed (BVVal ())) f2
-  remove-casts-same (TAEHole x x₁) NICHole MSRefl MSRefl (FIndet IEHole) (FBoxed (BVVal ()))
-  remove-casts-same (TAEHole x x₁) NICHole MSRefl MSRefl (FIndet IEHole) (FIndet IEHole) = refl
-  remove-casts-same (TAEHole x x₁) NICHole MSRefl (MSStep (Step FHOuter () FHOuter) step2) (FIndet IEHole) f2
-  remove-casts-same (TAEHole x x₁) NICHole (MSStep (Step FHOuter () FHOuter) step1) step2 f1 f2
-
-  remove-casts-same (TANEHole x wt x₁) (NICNEHole nic) step1 step2 f1 f2 = {!!}
-
-  remove-casts-same (TACast wt x) (NICCast nic) MSRefl step2 (FBoxed (BVVal ())) f2
-  remove-casts-same (TACast wt TCRefl) (NICCast nic) MSRefl step2 (FBoxed (BVArrCast x₁ x₂)) f2 = abort (x₁ refl)
-  remove-casts-same (TACast wt (TCArr x x₁)) (NICCast nic) MSRefl step2 (FBoxed (BVArrCast x₂ x₃)) f2 = abort (x₂ refl)
-  remove-casts-same (TACast wt x) (NICCast nic) MSRefl step2 (FBoxed (BVHoleCast () x₂)) f2
-  remove-casts-same (TACast wt x) (NICCast nic) MSRefl step2 (FIndet (ICastArr x₁ x₂)) f2 = abort (x₁ refl)
-  remove-casts-same (TACast wt x) (NICCast nic) MSRefl step2 (FIndet (ICastGroundHole () x₂)) f2
-  remove-casts-same (TACast wt x) (NICCast nic) MSRefl step2 (FIndet (ICastHoleGround x₁ x₂ ())) f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step FHOuter ITCastID FHOuter) step1) step2 f1 f2 = remove-casts-same wt nic step1 step2 f1 f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step FHOuter (ITCastSucceed x₁) FHOuter) step1) step2 f1 f2 = remove-casts-same wt nic
-                                                                                                                         (MSStep (Step FHOuter ITCastID FHOuter) step1) step2 f1 f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step FHOuter (ITCastFail x₁ () x₃) FHOuter) step1) step2 f1 f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step FHOuter (ITGround ()) FHOuter) step1) step2 f1 f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step FHOuter (ITExpand ()) FHOuter) step1) step2 f1 f2
-  remove-casts-same (TACast wt x) (NICCast nic) (MSStep (Step (FHCast x₁) x₂ (FHCast x₃)) step1) step2 f1 f2 = {!!}
-
-    -- remove-casts-same wt nic (MSStep (Step x₁ x₂ x₃) {!!}) step2 f1 f2
-
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) MSRefl MSRefl (FBoxed (BVVal ())) f2
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) MSRefl MSRefl (FIndet (IFailedCast x₃ x₄ x₅ x₆)) (FBoxed (BVVal ()))
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) MSRefl MSRefl (FIndet (IFailedCast x₃ x₄ x₅ x₆)) (FIndet (IFailedCast x₇ x₈ x₉ x₁₀))
-    with remove-casts-same wt nic MSRefl MSRefl x₃ x₇
-  ... | refl = refl
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) MSRefl (MSStep x₃ step2) (FBoxed (BVVal ())) f2
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) MSRefl (MSStep x₃ step2) (FIndet (IFailedCast x₄ x₅ x₆ x₇)) f2 = {!!}
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) (MSStep x₃ step1) MSRefl f1 f2 = {!!}
-  remove-casts-same (TAFailedCast wt x x₁ x₂) (NICFailed nic) (MSStep x₃ step1) (MSStep x₄ step2) f1 f2 = {!!}