[Turned Record into a record type. Nils Anders Danielsson **20110622090529 Ignore-this: 8c3e59f5d1188a10a0f86b33a082a49b ] hunk ./src/Record.agda 63 - -- Record is a data type to ensure that the signature can be + -- Record is a record type to ensure that the signature can be hunk ./src/Record.agda 66 - data Record {s} (Sig : Signature s) : Set s where - rec : (r : Record-fun Sig) → Record Sig + record Record {s} (Sig : Signature s) : Set s where + constructor rec + field fun : Record-fun Sig hunk ./src/Record.agda 75 --- A projection function for Record. (Unfortunately Agda as of version --- 2.2.10 does not allow us to turn Record into a record type.) - -rec-fun : ∀ {s} {Sig : Signature s} → Record Sig → Record-fun Sig -rec-fun (rec r) = r - hunk ./src/Record.agda 111 - Rec⇒Rec′ ∅ r = rec-fun r - Rec⇒Rec′ (Sig , ℓ ∶ A) r = (Rec⇒Rec′ _ (Σ.proj₁ r′) , Σ.proj₂ r′) - where r′ = rec-fun r - Rec⇒Rec′ (Sig , ℓ ≔ a) r = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r′) ,) - where r′ = rec-fun r + Rec⇒Rec′ ∅ (rec r) = r + Rec⇒Rec′ (Sig , ℓ ∶ A) (rec r) = (Rec⇒Rec′ _ (Σ.proj₁ r) , Σ.proj₂ r) + Rec⇒Rec′ (Sig , ℓ ≔ a) (rec r) = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r) ,) hunk ./src/Record.agda 181 -_∣_ {Sig = ∅} r ℓ {} -_∣_ {Sig = Sig , ℓ′ ∶ A} r ℓ with ℓ ≟ ℓ′ -... | yes _ = Σ.proj₁ (rec-fun r) -... | no _ = Σ.proj₁ (rec-fun r) ∣ ℓ -_∣_ {Sig = Sig , ℓ′ ≔ a} r ℓ with ℓ ≟ ℓ′ -... | yes _ = Manifest-Σ.proj₁ (rec-fun r) -... | no _ = Manifest-Σ.proj₁ (rec-fun r) ∣ ℓ +_∣_ {Sig = ∅} r ℓ {} +_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′ +... | yes _ = Σ.proj₁ r +... | no _ = Σ.proj₁ r ∣ ℓ +_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′ +... | yes _ = Manifest-Σ.proj₁ r +... | no _ = Manifest-Σ.proj₁ r ∣ ℓ hunk ./src/Record.agda 194 -_·_ {Sig = ∅} r ℓ {} -_·_ {Sig = Sig , ℓ′ ∶ A} r ℓ with ℓ ≟ ℓ′ -... | yes _ = Σ.proj₂ (rec-fun r) -... | no _ = Σ.proj₁ (rec-fun r) · ℓ -_·_ {Sig = Sig , ℓ′ ≔ a} r ℓ with ℓ ≟ ℓ′ -... | yes _ = Manifest-Σ.proj₂ (rec-fun r) -... | no _ = Manifest-Σ.proj₁ (rec-fun r) · ℓ +_·_ {Sig = ∅} r ℓ {} +_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′ +... | yes _ = Σ.proj₂ r +... | no _ = Σ.proj₁ r · ℓ +_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′ +... | yes _ = Manifest-Σ.proj₂ r +... | no _ = Manifest-Σ.proj₁ r · ℓ hunk ./src/Record.agda 225 - drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} r with ℓ ≟ ℓ′ - ... | yes _ = rec (proj₁ (rec-fun r) , proj₂ (rec-fun r)) - where open Manifest-Σ - ... | no _ = rec ( drop-With (Σ.proj₁ (rec-fun r)) - , Σ.proj₂ (rec-fun r) - ) - drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} r with ℓ ≟ ℓ′ - ... | yes _ = rec (Manifest-Σ.proj₁ (rec-fun r) ,) - ... | no _ = rec (drop-With (Manifest-Σ.proj₁ (rec-fun r)) ,) + drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′ + ... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r) + ... | no _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r) + drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′ + ... | yes _ = rec (Manifest-Σ.proj₁ r ,) + ... | no _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)