Skip to content

Commit

Permalink
Make plutus-metatheory work with the BLS builtins to some extent
Browse files Browse the repository at this point in the history
  • Loading branch information
@kwxm
kwxm committed Mar 16, 2023
1 parent 2a2659e commit 8385fbf
Show file tree
Hide file tree
Showing 27 changed files with 519 additions and 95 deletions.
29 changes: 25 additions & 4 deletions plutus-metatheory/src/Algorithmic/CEK.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,8 +231,9 @@ BUILTIN' b {az = az} p q
... | inj₂ V = discharge V
... | inj₁ A = error _
bappTermLem : ∀ b {A}{az as}(p : az <>> (Term ∷ as) ∈ arity b)
→ BApp b p A → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A''
postulate bappTermLem : ∀ b {A}{az as}(p : az <>> (Term ∷ as) ∈ arity b) → BApp b p A → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A''
{-
bappTermLem addInteger _ base = _ ,, _ ,, refl
bappTermLem addInteger {as = as} .(bubble p) (app {az = az} p q x)
with <>>-cancel-both az (([] :< Term) :< Term) as p
Expand Down Expand Up @@ -575,9 +576,11 @@ bappTermLem indexByteString (bubble (start _)) (app _ base _)
bappTermLem blake2b-256 {az = az} {as} p q
with <>>-cancel-both az ([] :< Term) as p
bappTermLem blake2b-256 (start _) base | refl ,, refl = _ ,, _ ,, refl
-}
postulate bappTypeLem : ∀ b {A}{az as}(p : az <>> (Type ∷ as) ∈ arity b) → BApp b p A → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B
bappTypeLem : ∀ b {A}{az as}(p : az <>> (Type ∷ as) ∈ arity b)
→ BApp b p A → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B
{-
bappTypeLem addInteger {as = as} .(bubble p) (app {az = az} p q x)
with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl
... | refl ,, refl ,, ()
Expand Down Expand Up @@ -842,6 +845,7 @@ bappTypeLem indexByteString (bubble {as = az} p) q
bappTypeLem blake2b-256 {az = az} p q
with <>>-cancel-both' az _ ([] :< Term) _ p refl
... | refl ,, refl ,, ()
-}
V-I : ∀ b {A : ∅ ⊢Nf⋆ *}{a as as'}
→ (p : as <>> a ∷ as' ∈ arity b)
Expand Down Expand Up @@ -933,6 +937,23 @@ ival sliceByteString = V-I⇒ sliceByteString (start _) base
ival lengthOfByteString = V-I⇒ lengthOfByteString (start _) base
ival indexByteString = V-I⇒ indexByteString (start _) base
ival blake2b-256 = V-I⇒ blake2b-256 (start _) base
ival bls12-381-G1-add = V-I⇒ bls12-381-G1-add (start _) base
ival bls12-381-G1-neg = V-I⇒ bls12-381-G1-neg (start _) base
ival bls12-381-G1-scalarMul = V-I⇒ bls12-381-G1-scalarMul (start _) base
ival bls12-381-G1-equal = V-I⇒ bls12-381-G1-equal (start _) base
ival bls12-381-G1-hashToCurve = V-I⇒ bls12-381-G1-hashToCurve (start _) base
ival bls12-381-G1-compress = V-I⇒ bls12-381-G1-compress (start _) base
ival bls12-381-G1-uncompress = V-I⇒ bls12-381-G1-uncompress (start _) base
ival bls12-381-G2-add = V-I⇒ bls12-381-G2-add (start _) base
ival bls12-381-G2-neg = V-I⇒ bls12-381-G2-neg (start _) base
ival bls12-381-G2-scalarMul = V-I⇒ bls12-381-G2-scalarMul (start _) base
ival bls12-381-G2-equal = V-I⇒ bls12-381-G2-equal (start _) base
ival bls12-381-G2-hashToCurve = V-I⇒ bls12-381-G2-hashToCurve (start _) base
ival bls12-381-G2-compress = V-I⇒ bls12-381-G2-compress (start _) base
ival bls12-381-G2-uncompress = V-I⇒ bls12-381-G2-uncompress (start _) base
ival bls12-381-pairing = V-I⇒ bls12-381-pairing (start _) base
ival bls12-381-mulMlResult = V-I⇒ bls12-381-mulMlResult (start _) base
ival bls12-381-finalVerify = V-I⇒ bls12-381-finalVerify (start _) base
step : ∀{T} → State T → State T
step (s ; ρ ▻ ` x) = s ◅ lookup x ρ
Expand Down
3 changes: 3 additions & 0 deletions plutus-metatheory/src/Algorithmic/Completeness.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,9 @@ nfTypeTC (STermCon.string s) = NTermCon.string s
nfTypeTC (STermCon.bool b) = NTermCon.bool b
nfTypeTC STermCon.unit = NTermCon.unit
nfTypeTC (STermCon.pdata d) = NTermCon.pdata d
nfTypeTC (STermCon.g1elt e) = NTermCon.g1elt e
nfTypeTC (STermCon.g2elt e) = NTermCon.g2elt e
nfTypeTC (STermCon.mlresult r) = NTermCon.mlresult r

lemσ : ∀{Γ Δ Δ'}
→ (σ : Sub Δ Γ)
Expand Down
13 changes: 11 additions & 2 deletions plutus-metatheory/src/Algorithmic/Erasure.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,9 @@ eraseTC (AC.string s) = string s
eraseTC (AC.bool b) = bool b
eraseTC AC.unit = unit
eraseTC (AC.pdata d) = pdata d
eraseTC (AC.g1elt e) = g1elt e
eraseTC (AC.g2elt e) = g2elt e
eraseTC (AC.mlresult r) = mlresult r

erase : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ⊢ A → len Γ ⊢
erase (` α) = ` (eraseVar α)
Expand Down Expand Up @@ -118,7 +121,10 @@ sameTC (DC.bytestring b) = refl
sameTC (DC.string s) = refl
sameTC (DC.bool b) = refl
sameTC DC.unit = refl
sameTC (DC.pdata d) = refl
sameTC (DC.pdata d) = refl
sameTC (DC.g1elt e) = refl
sameTC (DC.g2elt e) = refl
sameTC (DC.mlresult r) = refl


lem≡Ctx : ∀{Φ}{Γ Γ' : Ctx Φ} → Γ ≡ Γ' → len Γ ≡ len Γ'
Expand Down Expand Up @@ -247,7 +253,10 @@ same'TC (AC.bytestring b) = refl
same'TC (AC.string s) = refl
same'TC (AC.bool b) = refl
same'TC AC.unit = refl
same'TC (AC.pdata d) = refl
same'TC (AC.pdata d) = refl
same'TC (AC.g1elt e) = refl
same'TC (AC.g2elt e) = refl
same'TC (AC.mlresult r) = refl

same' : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *}(x : Γ A.⊢ A)
→ erase x ≡ subst _⊢ (same'Len Γ) (D.erase (emb x))
Expand Down
30 changes: 26 additions & 4 deletions plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -405,8 +405,9 @@ data _—↠_ : {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → ∅ ⊢ A → Set
-- HINT: pattern matching on p rather than the next arg (q) generates
-- fewer cases
bappTermLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> Term ∷ as ∈ arity b)
→ BApp b p M → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A''
postulate bappTermLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> Term ∷ as ∈ arity b) → BApp b p M → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A''
-- FIXME: This is commented out just to get past teh typechecker in the absence of the BLS builtins.
{-
bappTermLem addInteger _ (start _) (base refl) = _ ,, _ ,, refl
bappTermLem addInteger {as = as} _ (bubble {as = az} p) q
with <>>-cancel-both' az _ ([] :< Term :< Term) as p refl
Expand Down Expand Up @@ -718,11 +719,14 @@ bappTermLem indexByteString _ (bubble (start _)) (step _ (base refl) _)
bappTermLem blake2b-256 {az = az} {as} M p q
with <>>-cancel-both az ([] :< Term) as p
bappTermLem blake2b-256 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl
bappTermLem _ _ _ _ = error -- FIXME!!!
-}
```

```
bappTypeLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> (Type ∷ as) ∈ arity b)
→ BApp b p M → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B
postulate bappTypeLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> (Type ∷ as) ∈ arity b) → BApp b p M → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B
{-
bappTypeLem addInteger _ (bubble {as = az} p) _
with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl
... | refl ,, refl ,, ()
Expand Down Expand Up @@ -904,6 +908,7 @@ bappTypeLem indexByteString _ (bubble {as = az} p) q
bappTypeLem blake2b-256 {az = az} _ p q
with <>>-cancel-both' az _ ([] :< Term) _ p refl
... | refl ,, refl ,, ()
-}
```

A smart constructor that looks at the arity and then puts on the
Expand Down Expand Up @@ -983,4 +988,21 @@ ival sliceByteString = V-I⇒ sliceByteString (start _) (base refl)
ival lengthOfByteString = V-I⇒ lengthOfByteString (start _) (base refl)
ival indexByteString = V-I⇒ indexByteString (start _) (base refl)
ival blake2b-256 = V-I⇒ blake2b-256 (start _) (base refl)
ival bls12-381-G1-add = V-I⇒ bls12-381-G1-add (start _) (base refl)
ival bls12-381-G1-neg = V-I⇒ bls12-381-G1-neg (start _) (base refl)
ival bls12-381-G1-scalarMul = V-I⇒ bls12-381-G1-scalarMul (start _) (base refl)
ival bls12-381-G1-equal = V-I⇒ bls12-381-G1-equal (start _) (base refl)
ival bls12-381-G1-hashToCurve = V-I⇒ bls12-381-G1-hashToCurve (start _) (base refl)
ival bls12-381-G1-compress = V-I⇒ bls12-381-G1-compress (start _) (base refl)
ival bls12-381-G1-uncompress = V-I⇒ bls12-381-G1-uncompress (start _) (base refl)
ival bls12-381-G2-add = V-I⇒ bls12-381-G2-add (start _) (base refl)
ival bls12-381-G2-neg = V-I⇒ bls12-381-G2-neg (start _) (base refl)
ival bls12-381-G2-scalarMul = V-I⇒ bls12-381-G2-scalarMul (start _) (base refl)
ival bls12-381-G2-equal = V-I⇒ bls12-381-G2-equal (start _) (base refl)
ival bls12-381-G2-hashToCurve = V-I⇒ bls12-381-G2-hashToCurve (start _) (base refl)
ival bls12-381-G2-compress = V-I⇒ bls12-381-G2-compress (start _) (base refl)
ival bls12-381-G2-uncompress = V-I⇒ bls12-381-G2-uncompress (start _) (base refl)
ival bls12-381-pairing = V-I⇒ bls12-381-pairing (start _) (base refl)
ival bls12-381-mulMlResult = V-I⇒ bls12-381-mulMlResult (start _) (base refl)
ival bls12-381-finalVerify = V-I⇒ bls12-381-finalVerify (start _) (base refl)
```
10 changes: 8 additions & 2 deletions plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,10 @@ renTermCon ρ⋆ (bytestring b) = bytestring b
renTermCon ρ⋆ (string s) = string s
renTermCon ρ⋆ (bool b) = bool b
renTermCon ρ⋆ unit = unit
renTermCon ρ⋆ (pdata d) = pdata d
renTermCon ρ⋆ (pdata d) = pdata d
renTermCon ρ⋆ (g1elt e) = g1elt e
renTermCon ρ⋆ (g2elt e) = g2elt e
renTermCon ρ⋆ (mlresult r) = mlresult r
\end{code}

\begin{code}
Expand Down Expand Up @@ -155,7 +158,10 @@ subTermCon σ⋆ (bytestring b) = bytestring b
subTermCon σ⋆ (string s) = string s
subTermCon σ⋆ (bool b) = bool b
subTermCon σ⋆ unit = unit
subTermCon σ⋆ (pdata d) = pdata d
subTermCon σ⋆ (pdata d) = pdata d
subTermCon σ⋆ (g1elt e) = g1elt e
subTermCon σ⋆ (g2elt e) = g2elt e
subTermCon σ⋆ (mlresult r) = mlresult r
\end{code}

\begin{code}
Expand Down
3 changes: 3 additions & 0 deletions plutus-metatheory/src/Algorithmic/Soundness.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,9 @@ embTC (NTermCon.string s) = STermCon.string s
embTC (NTermCon.bool b) = STermCon.bool b
embTC NTermCon.unit = STermCon.unit
embTC (NTermCon.pdata d) = STermCon.pdata d
embTC (NTermCon.g1elt e) = STermCon.g1elt e
embTC (NTermCon.g2elt e) = STermCon.g2elt e
embTC (NTermCon.mlresult r) = STermCon.mlresult r
\end{code}

\begin{code}
Expand Down
75 changes: 67 additions & 8 deletions plutus-metatheory/src/Builtin.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ open import Data.Bool using (Bool)
open import Agda.Builtin.Int using (Int)
open import Agda.Builtin.String using (String)
open import Utils using (ByteString;Maybe;DATA)
open import Builtin.Signature using (Sig;sig;_⊢♯;con;`;Args)
open import Builtin.Signature using (Sig;sig;_⊢♯;con;`;Args)
import Builtin.Constant.Type ℕ (_⊢♯) as T
```

Expand Down Expand Up @@ -61,7 +61,7 @@ data Builtin : Set where
appendString : Builtin
equalsString : Builtin
encodeUtf8 : Builtin
decodeUtf8 : Builtin
decodeUtf8 : Builtin
-- Bool
ifThenElse : Builtin
-- Unit
Expand Down Expand Up @@ -95,6 +95,28 @@ data Builtin : Set where
mkPairData : Builtin
mkNilData : Builtin
mkNilPairData : Builtin
-- BLS12_381
-- G1
bls12-381-G1-add : Builtin
bls12-381-G1-neg : Builtin
bls12-381-G1-scalarMul : Builtin
bls12-381-G1-equal : Builtin
bls12-381-G1-hashToCurve : Builtin
bls12-381-G1-compress : Builtin
bls12-381-G1-uncompress : Builtin
-- G2
bls12-381-G2-add : Builtin
bls12-381-G2-neg : Builtin
bls12-381-G2-scalarMul : Builtin
bls12-381-G2-equal : Builtin
bls12-381-G2-hashToCurve : Builtin
bls12-381-G2-compress : Builtin
bls12-381-G2-uncompress : Builtin
-- Pairing
bls12-381-pairing : Builtin
bls12-381-mulMlResult : Builtin
bls12-381-finalVerify : Builtin
```

## Signatures
Expand All @@ -116,13 +138,16 @@ This is defined in its own module so that these definitions are not exported.
∀b,a = 2
-- shortened names for type constants and type constructors
integer bool bytestring string unit pdata : ∀{n} → n ⊢♯
integer bool bytestring string unit pdata g1elt g2elt mlresult : ∀{n} → n ⊢♯
integer = con T.integer
bool = con T.bool
bytestring = con T.bytestring
string = con T.string
unit = con T.unit
pdata = con T.pdata
g1elt = con T.g1elt
g2elt = con T.g2elt
mlresult = con T.mlresult
pair : ∀{n} → n ⊢♯ → n ⊢♯ → n ⊢♯
pair x y = con (T.pair x y)
Expand Down Expand Up @@ -168,7 +193,7 @@ This is defined in its own module so that these definitions are not exported.
signature lessThanEqualsInteger = ∙ [ integer , integer ]⟶ bool
signature appendByteString = ∙ [ bytestring , bytestring ]⟶ bytestring
signature consByteString = ∙ [ integer , bytestring ]⟶ bytestring
signature sliceByteString = ∙ [ integer , integer , bytestring ]⟶ bytestring
signature sliceByteString = ∙ [ integer , integer , bytestring ]⟶ bytestring
signature lengthOfByteString = ∙ [ bytestring ]⟶ integer
signature indexByteString = ∙ [ bytestring , integer ]⟶ integer
signature equalsByteString = ∙ [ bytestring , bytestring ]⟶ bool
Expand All @@ -183,7 +208,7 @@ This is defined in its own module so that these definitions are not exported.
signature appendString = ∙ [ string , string ]⟶ string
signature equalsString = ∙ [ string , string ]⟶ bool
signature encodeUtf8 = ∙ [ string ]⟶ bytestring
signature decodeUtf8 = ∙ [ bytestring ]⟶ string
signature decodeUtf8 = ∙ [ bytestring ]⟶ string
signature ifThenElse = ∀a [ bool , a , a ]⟶ a
signature chooseUnit = ∀a [ a , unit ]⟶ a
signature trace = ∀a [ string , a ]⟶ a
Expand All @@ -210,6 +235,23 @@ This is defined in its own module so that these definitions are not exported.
signature mkPairData = ∙ [ pdata , pdata ]⟶ pair pdata pdata
signature mkNilData = ∙ [ unit ]⟶ list pdata
signature mkNilPairData = ∙ [ unit ]⟶ list (pair pdata pdata)
signature bls12-381-G1-add = ∙ [ g1elt , g1elt ]⟶ g1elt
signature bls12-381-G1-neg = ∙ [ g1elt ]⟶ g1elt
signature bls12-381-G1-scalarMul = ∙ [ integer , g1elt ]⟶ g1elt
signature bls12-381-G1-equal = ∙ [ g1elt , g1elt ]⟶ bool
signature bls12-381-G1-hashToCurve = ∙ [ bytestring ]⟶ g1elt
signature bls12-381-G1-compress = ∙ [ g1elt ]⟶ bytestring
signature bls12-381-G1-uncompress = ∙ [ bytestring ]⟶ g1elt
signature bls12-381-G2-add = ∙ [ g2elt , g2elt ]⟶ g2elt
signature bls12-381-G2-neg = ∙ [ g2elt ]⟶ g2elt
signature bls12-381-G2-scalarMul = ∙ [ integer , g2elt ]⟶ g2elt
signature bls12-381-G2-equal = ∙ [ g2elt , g2elt ]⟶ bool
signature bls12-381-G2-hashToCurve = ∙ [ bytestring ]⟶ g2elt
signature bls12-381-G2-compress = ∙ [ g2elt ]⟶ bytestring
signature bls12-381-G2-uncompress = ∙ [ bytestring ]⟶ g2elt
signature bls12-381-pairing = ∙ [ g1elt , g2elt ]⟶ mlresult
signature bls12-381-mulMlResult = ∙ [ mlresult , mlresult ]⟶ mlresult
signature bls12-381-finalVerify = ∙ [ mlresult , mlresult ]⟶ bool

open SugaredSignature using (signature) public
```
Expand Down Expand Up @@ -274,12 +316,30 @@ Each Agda built-in name must be mapped to a Haskell name.
| MkPairData
| MkNilData
| MkNilPairData
) #-}
| Bls12_381_G1_add
| Bls12_381_G1_neg
| Bls12_381_G1_scalarMul
| Bls12_381_G1_equal
| Bls12_381_G1_hashToCurve
| Bls12_381_G1_compress
| Bls12_381_G1_uncompress
| Bls12_381_G2_add
| Bls12_381_G2_neg
| Bls12_381_G2_scalarMul
| Bls12_381_G2_equal
| Bls12_381_G2_hashToCurve
| Bls12_381_G2_compress
| Bls12_381_G2_uncompress
| Bls12_381_pairing
| Bls12_381_mulMlResult
| Bls12_381_finalVerify

) #-}
```
### Abstract semantics of builtins
We need to postulate the Agda type of built-in functions
We need to postulate the Agda type of built-in functions
whose semantics are provided by a Haskell funciton.
```
Expand Down Expand Up @@ -370,4 +430,3 @@ postulate
-- no binding needed for appendStr
-- no binding needed for traceStr
```
6 changes: 5 additions & 1 deletion plutus-metatheory/src/Builtin/Constant/Term.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,5 +37,9 @@ data TermCon {Φ} : Φ ⊢⋆ * → Set where
(b : Bool)
→ TermCon (con bool)
unit : TermCon (con unit)
pdata : DATA → TermCon (con pdata)
pdata : DATA → TermCon (con pdata)
g1elt : G1Elt → TermCon (con g1elt)
g2elt : G2Elt → TermCon (con g2elt)
mlresult : MlResult → TermCon (con mlresult)
```
29 changes: 17 additions & 12 deletions plutus-metatheory/src/Builtin/Constant/Type.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ module Builtin.Constant.Type

## Type constants

We have six base types referred to as type constants:
We have twelve base types referred to as type constants:

```
data TyCon (Φ : Con) : Set where
Expand All @@ -34,18 +34,23 @@ data TyCon (Φ : Con) : Set where
list : Ty Φ → TyCon Φ
pair : Ty Φ → Ty Φ → TyCon Φ
pdata : TyCon Φ
g1elt : TyCon Φ
g2elt : TyCon Φ
mlresult : TyCon Φ
--{-# FOREIGN GHC {-# LANGUAGE GADTs, PatternSynonyms #-} #-}
--{-# FOREIGN GHC import PlutusCore #-}
--{-# FOREIGN GHC type TypeBuiltin = SomeTypeIn DefaultUni #-}
--{-# FOREIGN GHC pattern TyInteger = SomeTypeIn DefaultUniInteger #-}
--{-# FOREIGN GHC pattern TyByteString = SomeTypeIn DefaultUniByteString #-}
--{-# FOREIGN GHC pattern TyString = SomeTypeIn DefaultUniString #-}
--{-# FOREIGN GHC pattern TyUnit = SomeTypeIn DefaultUniUnit #-}
--{-# FOREIGN GHC pattern TyBool = SomeTypeIn DefaultUniBool #-}
--{-# FOREIGN GHC pattern TyList a = SomeTypeIn DefaultUniList a #-}
--{-# FOREIGN GHC pattern TyPair a b = SomeTypeIn DefaultUniPair a b #-}
--{-# FOREIGN GHC pattern TyData = SomeTypeIn DefaultUniData #-}
--{-# COMPILE GHC TyCon = data TypeBuiltin (TyInteger | TyByteString | TyString | TyUnit | TyBool | TyList | TyPair | TyData) #-}
--{-# FOREIGN GHC type TypeBuiltin = SomeTypeIn DefaultUni #-}
--{-# FOREIGN GHC pattern TyInteger = SomeTypeIn DefaultUniInteger #-}
--{-# FOREIGN GHC pattern TyByteString = SomeTypeIn DefaultUniByteString #-}
--{-# FOREIGN GHC pattern TyString = SomeTypeIn DefaultUniString #-}
--{-# FOREIGN GHC pattern TyUnit = SomeTypeIn DefaultUniUnit #-}
--{-# FOREIGN GHC pattern TyBool = SomeTypeIn DefaultUniBool #-}
--{-# FOREIGN GHC pattern TyList a = SomeTypeIn DefaultUniList a #-}
--{-# FOREIGN GHC pattern TyPair a b = SomeTypeIn DefaultUniPair a b #-}
--{-# FOREIGN GHC pattern TyData = SomeTypeIn DefaultUniData #-}
--{-# FOREIGN GHC pattern TyBLS12_381_G1_Element = SomeTypeIn DefaultUniBLS12_381_G1_Element #-}
--{-# FOREIGN GHC pattern TyBLS12_381_G2_Element = SomeTypeIn DefaultUniBLS12_381_G2_Element #-}
--{-# FOREIGN GHC pattern TyBLS12_381_MlResult = SomeTypeIn DefaultUniBLS12_381_MlResult #-}
--{-# COMPILE GHC TyCon = data TypeBuiltin (TyInteger | TyByteString | TyString | TyUnit | TyBool | TyList | TyPair | TyData | TyBLS12_381_G1_Element | TyBLS12_381_G2_Element | TyBLS12_381_MlResult) #-}
```

0 comments on commit 8385fbf

Please sign in to comment.