<commit_before>open import Nat
open import Prelude
open import List
open import core

module expansion-unicity where
  mutual
    expansion-unicity-synth : (Γ : tctx) (e : hexp) (τ1 τ2 : htyp) (d1 d2 : dhexp) (Δ1 Δ2 : hctx) →
                            Γ ⊢ e ⇒ τ1 ~> d1 ⊣ Δ1 →
                            Γ ⊢ e ⇒ τ2 ~> d2 ⊣ Δ2 →
                            τ1 == τ2 × d1 == d2 × Δ1 == Δ2
    expansion-unicity-synth = {!!}

    expansion-unicity-ana : (Γ : tctx) (e : hexp) (τ1 τ1' τ2 τ2' : htyp) (d1 d2 : dhexp) (Δ1 Δ2 : hctx) →
                          Γ ⊢ e ⇐ τ1 ~> d1 :: τ1' ⊣ Δ1 →
                          Γ ⊢ e ⇐ τ2 ~> d2 :: τ2' ⊣ Δ2 →
                          τ1 == τ2 × d1 == d2 × τ1' == τ2' × Δ1 == Δ2
    expansion-unicity-ana = {!!}<commit_msg>easy cases<commit_after>open import Nat
open import Prelude
open import List
open import core
open import contexts

module expansion-unicity where
  mutual
    expansion-unicity-synth : {Γ : tctx} {e : hexp} {τ1 τ2 : htyp} {d1 d2 : dhexp} {Δ1 Δ2 : hctx} →
                            Γ ⊢ e ⇒ τ1 ~> d1 ⊣ Δ1 →
                            Γ ⊢ e ⇒ τ2 ~> d2 ⊣ Δ2 →
                            τ1 == τ2 × d1 == d2 × Δ1 == Δ2
    expansion-unicity-synth ESConst ESConst = refl , refl , refl
    expansion-unicity-synth (ESVar {Γ = Γ} x₁) (ESVar x₂) = ctxunicity {Γ = Γ} x₁ x₂ , refl , refl
    expansion-unicity-synth (ESLam d1) (ESLam d2) with expansion-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = ap1 _ ih1  , ap1 _ ih2 , refl
    expansion-unicity-synth (ESAp1 x x₁ x₂ x₃) (ESAp1 x₄ x₅ x₆ x₇) = {!!}
    expansion-unicity-synth (ESAp1 x x₁ x₂ x₃) (ESAp2 x₄ d5 x₅ x₆) = {!!}
    expansion-unicity-synth (ESAp1 x x₁ x₂ x₃) (ESAp3 x₄ d5 x₅) = {!!}
    expansion-unicity-synth (ESAp2 x d5 x₁ x₂) (ESAp1 x₃ x₄ x₅ x₆) = {!!}
    expansion-unicity-synth (ESAp2 x d5 x₁ x₂) (ESAp2 x₃ d6 x₄ x₅) = {!!}
    expansion-unicity-synth (ESAp2 x d5 x₁ x₂) (ESAp3 x₃ d6 x₄) = {!!}
    expansion-unicity-synth (ESAp3 x d5 x₁) (ESAp1 x₂ x₃ x₄ x₅) = {!!}
    expansion-unicity-synth (ESAp3 x d5 x₁) (ESAp2 x₂ d6 x₃ x₄) = {!!}
    expansion-unicity-synth (ESAp3 x d5 x₁) (ESAp3 x₂ d6 x₃) = {!!}
    expansion-unicity-synth ESEHole ESEHole = refl , refl , refl
    expansion-unicity-synth (ESNEHole d1) (ESNEHole d2) with expansion-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = refl , ap1 _ ih2 , ap1 _ ih3
    expansion-unicity-synth (ESAsc1 x x₁) (ESAsc1 x₂ x₃) = {!!}
    expansion-unicity-synth (ESAsc1 x x₁) (ESAsc2 x₂) = {!!}
    expansion-unicity-synth (ESAsc2 x) (ESAsc1 x₁ x₂) = {!!}
    expansion-unicity-synth (ESAsc2 x) (ESAsc2 x₁) = {!!}

    expansion-unicity-ana : {Γ : tctx} {e : hexp} {τ1 τ1' τ2 τ2' : htyp} {d1 d2 : dhexp} {Δ1 Δ2 : hctx} →
                          Γ ⊢ e ⇐ τ1 ~> d1 :: τ1' ⊣ Δ1 →
                          Γ ⊢ e ⇐ τ2 ~> d2 :: τ2' ⊣ Δ2 →
                          τ1 == τ2 × d1 == d2 × τ1' == τ2' × Δ1 == Δ2
    expansion-unicity-ana (EALam d1) (EALam d2) = {!!}
    expansion-unicity-ana (EALam d1) (EASubsume x₁ x₂ x₃ x₄) = {!!}
    expansion-unicity-ana (EASubsume x₁ x₂ x₃ x₄) (EALam d2) = {!!}
    expansion-unicity-ana (EASubsume x x₁ x₂ x₃) (EASubsume x₄ x₅ x₆ x₇) = {!!}
    expansion-unicity-ana (EASubsume x x₁ x₂ x₃) EAEHole = {!!}
    expansion-unicity-ana (EASubsume x x₁ x₂ x₃) (EANEHole x₄ x₅) = {!!}
    expansion-unicity-ana EAEHole (EASubsume x x₁ x₂ x₃) = {!!}
    expansion-unicity-ana EAEHole EAEHole = {!!}
    expansion-unicity-ana (EANEHole x x₁) (EASubsume x₂ x₃ x₄ x₅) = {!!}
    expansion-unicity-ana (EANEHole x x₁) (EANEHole x₂ x₃) = {!!}
{'fraction_non_alphanumeric': 0.14350282485875707, 'fraction_numerical': 0.04180790960451977, 'mean_word_length': 2.0737847222222223, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '78750', 'n_tokens_mistral': 1705, 'n_tokens_neox': 1724, 'n_words': 467}