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.

Sign up for GitHub

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

Jump to bottom

[Exe] Generalize 'withL' to 'withLangGeneral' #5918

Merged
merged 1 commit into from
May 29, 2024
Merged

[Exe] Generalize 'withL' to 'withLangGeneral' #5918

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 7 additions & 7 deletions plutus-core/executables/plutus/AnyProgram/IO.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ readProgram sngS fileS =
case parseProgram @ParserErrorBundle sngS $ T.decodeUtf8Lenient bs of
Left err -> failE $ show err
Right res -> pure res
Flat_ -> withFlatL sngS $ do
Flat_ -> withLang @Flat sngS $ do
bs <- readFileName (fromJust $ fileS^.fName)
case unflat bs of
Left err -> failE $ show err
Expand All @@ -59,7 +59,7 @@ readProgram sngS fileS =
case deserialiseOrFail $ BSL.fromStrict bs of
Left err -> failE $ show err
Right res -> pure res
_ -> withFlatL sngS $
_ -> withLang @Flat sngS $
-- this is a cbor-embedded bytestring of the Flat encoding
-- so we use the SerialiseViaFlat newtype wrapper.
case deserialiseOrFail $ BSL.fromStrict bs of
Expand All @@ -74,7 +74,7 @@ writeProgram sng ast file =
Just fn -> do
printED $ show $ "Outputting" <+> pretty file
case file^.fType.fFormat of
Flat_ -> writeFileName fn $ withFlatL sng $ flat ast
Flat_ -> writeFileName fn $ withLang @Flat sng $ flat ast
Text -> writeFileName fn
$ T.encodeUtf8
$ renderStrict
Expand All @@ -84,7 +84,7 @@ writeProgram sng ast file =
Cbor -> writeFileName fn $ BSL.toStrict $
case sng %~ SData of
Proved Refl -> serialise ast
_ -> withFlatL sng $ serialise (SerialiseViaFlat ast)
_ -> withLang @Flat sng $ serialise (SerialiseViaFlat ast)
Json -> error "FIXME: not implemented yet"
_ -> printE "Program passed all checks. No output file was written, use -o or --stdout."

Expand All @@ -98,11 +98,11 @@ prettyWithStyle = \case
readFileName :: (?opts :: Opts)
=> FileName -> IO BS.ByteString
readFileName = \case
StdOut -> failE "should not happen"
StdIn -> BS.hGetContents stdin
StdOut -> failE "should not happen"
StdIn -> BS.hGetContents stdin
AbsolutePath fp -> BS.readFile fp
-- TODO: it needs some restructuring in Types, Example is not a FileName and cannot be IO-read
Example{} -> failE "should not happen"
Example{} -> failE "should not happen"

writeFileName :: (?opts :: Opts)
=> FileName -> BS.ByteString -> IO ()
Expand Down
108 changes: 79 additions & 29 deletions plutus-core/executables/plutus/AnyProgram/With.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,28 +1,41 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-orphans #-}
-- | BOILERPLATE needed to support Hasochism.
-- See <https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf>
module AnyProgram.With where

import PlutusCore qualified as PLC
import PlutusCore.Data qualified as PLC
import PlutusCore.Pretty as PLC
import PlutusIR qualified as PIR
import UntypedPlutusCore qualified as UPLC

import Data.Kind (Constraint)
import Flat
import Types

-- for: (typeclass `compose` type)
type ComposeC :: forall a b. (b -> Constraint) -> (a -> b) -> a -> Constraint
class constr (f x) => ComposeC constr f x
instance constr (f x) => ComposeC constr f x

type UnitC :: forall a. a -> Constraint
class UnitC x
instance UnitC x

type AndC :: forall a. (a -> Constraint) -> (a -> Constraint) -> a -> Constraint
class (constr1 x, constr2 x) => AndC constr1 constr2 x
instance (constr1 x, constr2 x) => AndC constr1 constr2 x

withN :: forall constr s r
Copy link
Contributor Author

Choose a reason for hiding this comment

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

I hate these names BTW, withName wouldn't be much longer and it would be much more readable.

. ( constr (FromName 'Name)
, constr (FromName 'DeBruijn)
Expand Down Expand Up @@ -52,34 +65,71 @@ withA s r = case s of
SUnit -> r
STxSrcSpans -> r

withFlatL :: forall s r. SLang s -> (Flat (FromLang s) => r) -> r
withFlatL s r = case s of
SPir sname sann -> withN @Flat sname $ withNT @Flat sname $ withA @Flat sann r
SPlc sname sann -> withN @Flat sname $ withNT @Flat sname $ withA @Flat sann r
SUplc sname sann -> withN @Flat sname $ withN @(ComposeC Flat UPLC.Binder) sname $
withA @Flat sann r
SData -> error "Flat is not available for Data"
withLangGeneral
:: forall constrTyName constrBinder constrName constrAnn constr s r.
( constrTyName (FromNameTy 'Name)
, constrTyName (FromNameTy 'DeBruijn)
, constrTyName (FromNameTy 'NamedDeBruijn)
, constrBinder (UPLC.Binder UPLC.Name)
, constrBinder (UPLC.Binder UPLC.DeBruijn)
, constrBinder (UPLC.Binder UPLC.NamedDeBruijn)
, constrName (FromName 'Name)
, constrName (FromName 'DeBruijn)
, constrName (FromName 'NamedDeBruijn)
, constrAnn (FromAnn 'Unit)
, constrAnn (FromAnn 'TxSrcSpans)
, (forall tyname name ann. (constrTyName tyname, constrName name, constrAnn ann) =>
constr (PIR.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
, (forall tyname name ann. (constrTyName tyname, constrName name, constrAnn ann) =>
constr (PLC.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
, (forall name ann. (constrBinder (UPLC.Binder name), constrName name, constrAnn ann) =>
constr (UPLC.UnrestrictedProgram name UPLC.DefaultUni UPLC.DefaultFun ann))
)
=> SLang s -> (constr (FromLang s) => r) -> r
withLangGeneral s r = case s of
SPir sname sann ->
withNT @constrTyName sname
$ withN @constrName sname
$ withA @constrAnn sann r
SPlc sname sann ->
withNT @constrTyName sname
$ withN @constrName sname
$ withA @constrAnn sann r
SUplc sname sann ->
withN @(ComposeC constrBinder UPLC.Binder) sname
$ withN @constrName sname
$ withA @constrAnn sann r
SData -> error "not implemented yet"

withShowL :: forall s r. SLang s -> (Show (FromLang s) => r) -> r
withShowL s r = case s of
SPir sname sann -> withN @Show sname $ withNT @Show sname $ withA @Show sann r
SPlc sname sann -> withN @Show sname $ withNT @Show sname $ withA @Show sann r
SUplc sname sann -> withN @Show sname $ withN @(ComposeC Show UPLC.Binder) sname $
withA @Show sann r
SData -> r
withLang
:: forall constr s r.
( constr (FromNameTy 'Name)
, constr (FromNameTy 'DeBruijn)
, constr (FromNameTy 'NamedDeBruijn)
Copy link
Contributor Author

Choose a reason for hiding this comment

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

We could give these three constraints a single name and reuse it here, in withLangGeneral and in withNT, plus do the same with FromName, FromAnn etc constraints, but I'm not sure if it buys us much and we can always do that later.

, constr (UPLC.Binder UPLC.Name)
, constr (UPLC.Binder UPLC.DeBruijn)
, constr (UPLC.Binder UPLC.NamedDeBruijn)
, constr (FromName 'Name)
, constr (FromName 'DeBruijn)
, constr (FromName 'NamedDeBruijn)
, constr (FromAnn 'Unit)
, constr (FromAnn 'TxSrcSpans)
, (forall tyname name ann. (constr tyname, constr name, constr ann) =>
constr (PIR.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
, (forall tyname name ann. (constr tyname, constr name, constr ann) =>
constr (PLC.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
, (forall name ann. (constr (UPLC.Binder name), constr name, constr ann) =>
constr (UPLC.UnrestrictedProgram name UPLC.DefaultUni UPLC.DefaultFun ann))
)
=> SLang s -> (constr (FromLang s) => r) -> r
withLang = withLangGeneral @constr @constr @constr @constr @constr

withPrettyPlcL :: forall s r. SLang s -> (PrettyBy PrettyConfigPlc (FromLang s) => r) -> r
withPrettyPlcL s r = case s of
SPir sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
withNT @PrettyClassic sname $ withNT @PrettyReadable sname $
withA @Pretty sann r
SPlc sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
withNT @PrettyClassic sname $ withNT @PrettyReadable sname $
withA @Pretty sann r
SUplc sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
withA @Pretty sann r
SData -> r
withPrettyPlcL :: forall s r. SLang s -> (PrettyPlc (FromLang s) => r) -> r
withPrettyPlcL = withLangGeneral
@(PrettyClassic `AndC` PrettyReadable)
Copy link
Contributor

Choose a reason for hiding this comment

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

@effectfully : Just out of curiosity: is AndC strictly necessary here?

Could it alternatively be done by decomposing to two withLangGeneral calls? Something like:

withPrettyPlcL = withLangGeneral  @PrettyClassic ....   $ withLangGeneral @PrettyReadable ...

?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

is AndC strictly necessary here?

I believe so, you have to satisfy a qualified constraint (a, b, c) => d and you can't do that unless a, b and c are indeed as expected by d and so you have to provide the right a, b and c which forces you to use AndC. In particular, PrettyPlc can only hold if both PrettyClassic and PrettyReadable hold, so you can't just split the constraint for individual parts. I think it might be possible in theory to make it so that PrettyPlc is implied by some product of constraints and then satisfy those individually, but that's pointless, writing AndC is simply easier.

@UnitC
@(PrettyClassic `AndC` PrettyReadable)
@Pretty
@PrettyPlc

-- a dummy to make `withPrettyPlcL` work also with `Data`
instance PrettyBy PrettyConfigPlc PLC.Data where
prettyBy _ = pretty
instance PrettyBy PrettyConfigPlc PLC.Data