Add arrays to metatheory #7127
Add arrays to metatheory #7127
Conversation
Co-authored-by: Yura <[email protected]>
Co-authored-by: Yura <[email protected]>
Co-authored-by: Yura <[email protected]>
|
There was a problem hiding this comment.
Happy that the typeclass FFI stuff helped!
If I understand correctly, you've managed to find a way to pass the correct Eq instance to eqArray with the {{HE}} thing, right?
I have some minor comments.
Also, there are some Haskell modules in the metatheory in which I had to match on builtins and added error to the array cases. Those should be fixed in this PR as well.
| -- Arrays | ||
| lengthOfArray : Builtin | ||
| listToArray : Builtin | ||
| indexArray : Builtin |
There was a problem hiding this comment.
Nitpicking: indentation
| signature lengthOfArray = ∀a [ array a ]⟶ integer ↑ | ||
| signature listToArray = ∀a [ list a ]⟶ array a | ||
| signature indexArray = ∀a [ array a , integer ↑ ]⟶ a ↑ |
There was a problem hiding this comment.
Nitpicking: indentation again 😁
| @@ -0,0 +1,27 @@ | |||
| module MinBS where | |||
There was a problem hiding this comment.
Is this supposed to be checked in?
| @@ -85,6 +84,7 @@ data Tag : Set → Set where | |||
| pdata : Tag (Esc DATA) | |||
| pair : ∀{A B} → Tag (Esc A) → Tag (Esc B) → Tag (Esc (A × B)) | |||
| list : ∀{A} → Tag (Esc A) → Tag (Esc (List A)) | |||
| array : ∀{A} → Tag (Esc A) → Tag (Esc (Array A)) | |||
There was a problem hiding this comment.
Now I'm wondering whether GitHub is messing up the indentation. If that's the case then please ignore all my nitpicking.
| @@ -98,6 +98,7 @@ data Tag : Set → Set where | |||
| {-# FOREIGN GHC pattern TagData = DefaultUniData #-} | |||
| {-# FOREIGN GHC pattern TagPair ta tb = DefaultUniPair ta tb #-} | |||
| {-# FOREIGN GHC pattern TagList ta = DefaultUniList ta #-} | |||
| {-# FOREIGN GHC pattern TagArray ta = DefaultUniArray ta #-} | |||
| @@ -136,22 +184,26 @@ decTagCon' unit ⊤ unit ⊤ = true | |||
| decTagCon' pdata d pdata d' = eqDATA d d' | |||
| decTagCon' (pair t₁ t₂) (x₁ , x₂) (pair u₁ u₂) (y₁ , y₂) = decTagCon' t₁ x₁ u₁ y₁ | |||
| ∧ decTagCon' t₂ x₂ u₂ y₂ | |||
| decTagCon' (list t) [] (list t') [] = true -- TODO: check that the tags t and t' are equal | |||
| decTagCon' (list t) [] (list t') [] = true -- FIXME: Should compare tags | |||
There was a problem hiding this comment.
Please add an issue which tracks this and add the link here.
| decTagCon' (list t) (x ∷ xs) (list t') (y ∷ ys) = decTagCon' t x t' y | ||
| ∧ decTagCon' (list t) xs (list t') ys | ||
| decTagCon' (array t) x (array t') y = false -- FIXME: eqArray |
There was a problem hiding this comment.
Please add an issue which tracks this and add the link here.
| HsEqArray : {A : Set} {{HE : HasEq A}} {{ _ : HsEq A}} → HsEq (U.Array A) | ||
| HsEqArray {{HE = HE}} = record { hsEq = eqArray {{HE}}} |
| @@ -251,21 +262,24 @@ decEq-⟦ _⊢♯.list t ⟧tag (x U.∷ v) (x₁ U.∷ v₁) with decEq-⟦ t | |||
| ... | yes refl with decEq-⟦ _⊢♯.list t ⟧tag v v₁ | |||
| ... | yes refl = yes refl | |||
| ... | no ¬v=v₁ = no λ { refl → ¬v=v₁ refl } | |||
| decEq-⟦ _⊢♯.pair t t₁ ⟧tag (proj₁ U., proj₂) (proj₃ U., proj₄) with (decEq-⟦ t ⟧tag proj₁ proj₃) ×-dec (decEq-⟦ t₁ ⟧tag proj₂ proj₄) | |||
| decEq-⟦ _⊢♯.array t ⟧tag = decEq-Array-TyTag {t} decEq-⟦ t ⟧tag | |||
There was a problem hiding this comment.
Since decEq-Array-TyTag is postulated and doesn't have a Haskell definition, won't this crash at runtime?
|
|
||
| postulate | ||
| instance | ||
| hasEq-TyTag : {t : TyTag} → HasEq ⟦ t ⟧tag |
There was a problem hiding this comment.
Do you use this anywhere?
Fixes https://github.com/IntersectMBO/plutus-private/issues/1465