VictorCMiraldo / reg-diff

Diffing experiment for a simpler universe
0 stars 0 forks source link

Non-strictly positive HasChange type. #1

Closed VictorCMiraldo closed 8 years ago

VictorCMiraldo commented 8 years ago

Agda does not like HC type.

  data Allₗ {a b}{A : Set a}(P : A → Set b) 
            : {n : ℕ} → Vec A n → Set (lvl a b) where
    _∷_ : {n : ℕ}{v : A}{vs : Vec A n}
        → P v → Allₗ P vs → Allₗ P (v ∷ vs)
    []  : Allₗ P []

  data Some {a b}{A : Set a}(P : A → Set b) 
            : {n : ℕ} → Vec A n → Set (lvl a b) where
    only : {n : ℕ}{v : A}{vs : Vec A n}
         → P v → Allₗ (λ k → ¬ (P k)) vs → Some P (v ∷ vs)
    and  : {n : ℕ}{v : A}{vs : Vec A n}
         → P v → Some P vs → Some P (v ∷ vs)`

   mutual
    data Eμ (P : U → Set)(ty : U) : Set where
      ea  : P ty → Eμ P ty → Eμ P ty
      cpy : Eμ P ty
      ins : (x : ⟦ ty ⟧ Unit)
          → Al (μ ty) (ar ty x)
          → Eμ P ty
          → Eμ P ty
      del : (x : ⟦ ty ⟧ Unit)
          → Al (μ ty) (ar ty x)
          → Eμ P ty
          → Eμ P ty
      mod : (x y : ⟦ ty ⟧ Unit)
          → (hip : ar ty x ≡ ar ty y)
          → Vec (Eμ P ty) (ar ty x)
          → Eμ P ty

    data HCμ (P : U → Set){ty : U} : Eμ P ty → Set₁ where
      HCμins : (x : ⟦ ty ⟧ Unit)
             → (al : Al (μ ty) (ar ty x))
             → (d : Eμ P ty)
             → HCμ P (ins x al d)
      HCμdel : (x : ⟦ ty ⟧ Unit)
             → (al : Al (μ ty) (ar ty x))
             → (d : Eμ P ty)
             → HCμ P (del x al d)
      HCμmod : (x y : ⟦ ty ⟧ Unit)
             → (hip : ar ty x ≡ ar ty y)
             → (v : Vec (Eμ P ty) (ar ty x))
             → Some (HCμ P) v
             → HCμ P (mod x y hip v)