Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

show that removing id casts doesn't change evaluation behaivour #45

Open
ivoysey opened this issue Oct 5, 2018 · 0 comments
Open

show that removing id casts doesn't change evaluation behaivour #45

ivoysey opened this issue Oct 5, 2018 · 0 comments

Comments

@ivoysey
Copy link
Member

ivoysey commented Oct 5, 2018

A start of a proof of this once existed in cast-inert.agda but it's a little naïve. You need some sort of equality that lets you reason under binders because cast removal goes under binders -- or else you need to not really remove all the casts, which defeats the purpose. Removed this proof fragment before popl aoe because the static version that remains, just that the type doesn't change, is enough to back up the vague intuition we give in the paper. Developing an equational theory here would be an interesting future exercise.

  -- 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 = {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant