Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Test] Dump types for 'stdlib' and 'examples' #5450

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions plutus-core/plutus-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ library
PlutusCore.Evaluation.Result
PlutusCore.Examples.Builtins
PlutusCore.Examples.Data.Data
PlutusCore.Examples.Data.Function
PlutusCore.Examples.Data.InterList
PlutusCore.Examples.Data.List
PlutusCore.Examples.Data.Pair
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
type CostingPart uni ExtensionFun = ()

data BuiltinVersion ExtensionFun = ExtensionFunV0 | ExtensionFunV1
deriving stock (Enum, Bounded, Show)

toBuiltinMeaning :: forall val. HasMeaningIn uni val
=> BuiltinVersion ExtensionFun
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{-# LANGUAGE OverloadedStrings #-}

module PlutusCore.Examples.Data.Function
( unsafeCoerce
) where

import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Quote

import PlutusCore.StdLib.Data.Function

unsafeCoerce :: Term TyName Name uni fun ()
unsafeCoerce = runQuote $ do
a <- freshTyName "a"
b <- freshTyName "b"
return
. TyAbs () a (Type ())
. TyAbs () b (Type ())
. Apply () (mkIterInstNoAnn fix [TyVar () a, TyVar () b])
. TyInst () idFun
$ TyFun () (TyVar () a) (TyVar () b)
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ import PlutusCore.StdLib.Type

import PlutusCore.Examples.Builtins
import PlutusCore.Examples.Data.Data
import PlutusCore.Examples.Data.Function
import PlutusCore.Examples.Data.InterList
import PlutusCore.Examples.Data.List
import PlutusCore.Examples.Data.Pair
Expand All @@ -38,6 +39,9 @@ examples =
[ plcTermFile "ofoldrData" ofoldrData
, plcTermFile "exampleData" exampleData
]
, treeFolderContents "Function"
[ plcTermFile "unsafeCoerce" unsafeCoerce
]
, treeFolderContents "InterList"
[ plcTypeFile "InterList" $ _recursiveType interListData
, plcTermFile "InterNil" interNil
Expand Down
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This file is called unsafeCoerce, because it has the type of Haskell's unsafeCoerce. What about its semantics?
Does it behave like unsafeCoerce as well? Or is it equivalent to

diverge : all b. b
diverge = ...
unsafeCoerce : all a b. a -> b
unsafeCoerce a = diverge

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I saw the comment on the other PR. It is indeed fix id, so while the typing corresponds to unsafeCoerce, it doesn't behave like it, so it's misleading to call it like that. It's not unsafe to execute it. Perhaps divergeCoerce would be more appropriate?

Copy link
Contributor Author

@effectfully effectfully Aug 3, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great point, I'll rename it. Thanks!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
/\a b ->
(/\a b ->
\(f : (a -> b) -> a -> b) ->
(/\a ->
\(s : (\a -> ifix (\(self :: * -> *) a -> self a -> a) a) a) ->
unwrap s s)
{a -> b}
(iwrap
(\(self :: * -> *) a -> self a -> a)
(a -> b)
(\(s : (\a -> ifix (\(self :: * -> *) a -> self a -> a) a) (a -> b))
(x : a) ->
f
((/\a ->
\(s :
(\a -> ifix (\(self :: * -> *) a -> self a -> a) a)
a) ->
unwrap s s)
{a -> b}
s)
x)))
{a}
{b}
((/\a -> \(x : a) -> x) {a -> b})

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

This file was deleted.

Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
string -> string -> string
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G1_element -> bls12_381_G1_element -> bls12_381_G1_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G1_element -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G1_element -> bls12_381_G1_element -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bls12_381_G1_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G1_element -> bls12_381_G1_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> bls12_381_G1_element -> bls12_381_G1_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bls12_381_G1_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G2_element -> bls12_381_G2_element -> bls12_381_G2_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G2_element -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G2_element -> bls12_381_G2_element -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bls12_381_G2_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G2_element -> bls12_381_G2_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> bls12_381_G2_element -> bls12_381_G2_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bls12_381_G2_element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_mlresult -> bls12_381_mlresult -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_G1_element -> bls12_381_G2_element -> bls12_381_mlresult
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bls12_381_mlresult -> bls12_381_mlresult -> bls12_381_mlresult
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. data -> a -> a -> a -> a -> a -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a b. list a -> b -> b -> b
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. unit -> a -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> list data -> data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> string
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
string -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
data -> data -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
string -> string -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a b. pair a b -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. list a -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. bool -> a -> a -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
list data -> data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
list (pair data data) -> data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. a -> list a -> list a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
unit -> list data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
unit -> list (pair data data)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
data -> data -> pair data data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. list a -> bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
data -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> bytestring -> bytestring
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a b. pair a b -> b
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
integer -> integer -> integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. list a -> list a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
all a. string -> a -> a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
data -> bytestring
Loading
Loading