Skip to content

Commit d7a5c76

Browse files
effectfullyeffectfully
authored
[Exe] Generalize 'withL' to 'withLangGeneral' (#5918)
1 parent 85cf1ed commit d7a5c76

File tree

2 files changed

+86
-36
lines changed

2 files changed

+86
-36
lines changed

‎plutus-core/executables/plutus/AnyProgram/IO.hs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ readProgram sngS fileS =
4646
case parseProgram @ParserErrorBundle sngS $ T.decodeUtf8Lenient bs of
4747
Left err -> failE $ show err
4848
Right res -> pure res
49-
Flat_ -> withFlatL sngS $ do
49+
Flat_ -> withLang @Flat sngS $ do
5050
bs <- readFileName (fromJust $ fileS^.fName)
5151
case unflat bs of
5252
Left err -> failE $ show err
@@ -59,7 +59,7 @@ readProgram sngS fileS =
5959
case deserialiseOrFail $ BSL.fromStrict bs of
6060
Left err -> failE $ show err
6161
Right res -> pure res
62-
_ -> withFlatL sngS $
62+
_ -> withLang @Flat sngS $
6363
-- this is a cbor-embedded bytestring of the Flat encoding
6464
-- so we use the SerialiseViaFlat newtype wrapper.
6565
case deserialiseOrFail $ BSL.fromStrict bs of
@@ -74,7 +74,7 @@ writeProgram sng ast file =
7474
Just fn -> do
7575
printED $ show $ "Outputting" <+> pretty file
7676
case file^.fType.fFormat of
77-
Flat_ -> writeFileName fn $ withFlatL sng $ flat ast
77+
Flat_ -> writeFileName fn $ withLang @Flat sng $ flat ast
7878
Text -> writeFileName fn
7979
$ T.encodeUtf8
8080
$ renderStrict
@@ -84,7 +84,7 @@ writeProgram sng ast file =
8484
Cbor -> writeFileName fn $ BSL.toStrict $
8585
case sng %~ SData of
8686
Proved Refl -> serialise ast
87-
_ -> withFlatL sng $ serialise (SerialiseViaFlat ast)
87+
_ -> withLang @Flat sng $ serialise (SerialiseViaFlat ast)
8888
Json -> error "FIXME: not implemented yet"
8989
_ -> printE "Program passed all checks. No output file was written, use -o or --stdout."
9090

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

107107
writeFileName :: (?opts :: Opts)
108108
=> FileName -> BS.ByteString -> IO ()

‎plutus-core/executables/plutus/AnyProgram/With.hs

Lines changed: 79 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,41 @@
1+
{-# LANGUAGE AllowAmbiguousTypes #-}
12
{-# LANGUAGE DataKinds #-}
23
{-# LANGUAGE FlexibleInstances #-}
34
{-# LANGUAGE MultiParamTypeClasses #-}
45
{-# LANGUAGE PolyKinds #-}
6+
{-# LANGUAGE QuantifiedConstraints #-}
57
{-# LANGUAGE RankNTypes #-}
68
{-# LANGUAGE StandaloneKindSignatures #-}
9+
{-# LANGUAGE TypeOperators #-}
10+
{-# LANGUAGE UndecidableInstances #-}
711
{-# LANGUAGE UndecidableSuperClasses #-}
812
{-# OPTIONS_GHC -Wno-orphans #-}
913
-- | BOILERPLATE needed to support Hasochism.
1014
-- See <https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf>
1115
module AnyProgram.With where
1216

17+
import PlutusCore qualified as PLC
1318
import PlutusCore.Data qualified as PLC
1419
import PlutusCore.Pretty as PLC
20+
import PlutusIR qualified as PIR
1521
import UntypedPlutusCore qualified as UPLC
1622

1723
import Data.Kind (Constraint)
18-
import Flat
1924
import Types
2025

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

31+
type UnitC :: forall a. a -> Constraint
32+
class UnitC x
33+
instance UnitC x
34+
35+
type AndC :: forall a. (a -> Constraint) -> (a -> Constraint) -> a -> Constraint
36+
class (constr1 x, constr2 x) => AndC constr1 constr2 x
37+
instance (constr1 x, constr2 x) => AndC constr1 constr2 x
38+
2639
withN :: forall constr s r
2740
. ( constr (FromName 'Name)
2841
, constr (FromName 'DeBruijn)
@@ -52,34 +65,71 @@ withA s r = case s of
5265
SUnit -> r
5366
STxSrcSpans -> r
5467

55-
withFlatL :: forall s r. SLang s -> (Flat (FromLang s) => r) -> r
56-
withFlatL s r = case s of
57-
SPir sname sann -> withN @Flat sname $ withNT @Flat sname $ withA @Flat sann r
58-
SPlc sname sann -> withN @Flat sname $ withNT @Flat sname $ withA @Flat sann r
59-
SUplc sname sann -> withN @Flat sname $ withN @(ComposeC Flat UPLC.Binder) sname $
60-
withA @Flat sann r
61-
SData -> error "Flat is not available for Data"
68+
withLangGeneral
69+
:: forall constrTyName constrBinder constrName constrAnn constr s r.
70+
( constrTyName (FromNameTy 'Name)
71+
, constrTyName (FromNameTy 'DeBruijn)
72+
, constrTyName (FromNameTy 'NamedDeBruijn)
73+
, constrBinder (UPLC.Binder UPLC.Name)
74+
, constrBinder (UPLC.Binder UPLC.DeBruijn)
75+
, constrBinder (UPLC.Binder UPLC.NamedDeBruijn)
76+
, constrName (FromName 'Name)
77+
, constrName (FromName 'DeBruijn)
78+
, constrName (FromName 'NamedDeBruijn)
79+
, constrAnn (FromAnn 'Unit)
80+
, constrAnn (FromAnn 'TxSrcSpans)
81+
, (forall tyname name ann. (constrTyName tyname, constrName name, constrAnn ann) =>
82+
constr (PIR.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
83+
, (forall tyname name ann. (constrTyName tyname, constrName name, constrAnn ann) =>
84+
constr (PLC.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
85+
, (forall name ann. (constrBinder (UPLC.Binder name), constrName name, constrAnn ann) =>
86+
constr (UPLC.UnrestrictedProgram name UPLC.DefaultUni UPLC.DefaultFun ann))
87+
)
88+
=> SLang s -> (constr (FromLang s) => r) -> r
89+
withLangGeneral s r = case s of
90+
SPir sname sann ->
91+
withNT @constrTyName sname
92+
$ withN @constrName sname
93+
$ withA @constrAnn sann r
94+
SPlc sname sann ->
95+
withNT @constrTyName sname
96+
$ withN @constrName sname
97+
$ withA @constrAnn sann r
98+
SUplc sname sann ->
99+
withN @(ComposeC constrBinder UPLC.Binder) sname
100+
$ withN @constrName sname
101+
$ withA @constrAnn sann r
102+
SData -> error "not implemented yet"
62103

63-
withShowL :: forall s r. SLang s -> (Show (FromLang s) => r) -> r
64-
withShowL s r = case s of
65-
SPir sname sann -> withN @Show sname $ withNT @Show sname $ withA @Show sann r
66-
SPlc sname sann -> withN @Show sname $ withNT @Show sname $ withA @Show sann r
67-
SUplc sname sann -> withN @Show sname $ withN @(ComposeC Show UPLC.Binder) sname $
68-
withA @Show sann r
69-
SData -> r
104+
withLang
105+
:: forall constr s r.
106+
( constr (FromNameTy 'Name)
107+
, constr (FromNameTy 'DeBruijn)
108+
, constr (FromNameTy 'NamedDeBruijn)
109+
, constr (UPLC.Binder UPLC.Name)
110+
, constr (UPLC.Binder UPLC.DeBruijn)
111+
, constr (UPLC.Binder UPLC.NamedDeBruijn)
112+
, constr (FromName 'Name)
113+
, constr (FromName 'DeBruijn)
114+
, constr (FromName 'NamedDeBruijn)
115+
, constr (FromAnn 'Unit)
116+
, constr (FromAnn 'TxSrcSpans)
117+
, (forall tyname name ann. (constr tyname, constr name, constr ann) =>
118+
constr (PIR.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
119+
, (forall tyname name ann. (constr tyname, constr name, constr ann) =>
120+
constr (PLC.Program tyname name UPLC.DefaultUni UPLC.DefaultFun ann))
121+
, (forall name ann. (constr (UPLC.Binder name), constr name, constr ann) =>
122+
constr (UPLC.UnrestrictedProgram name UPLC.DefaultUni UPLC.DefaultFun ann))
123+
)
124+
=> SLang s -> (constr (FromLang s) => r) -> r
125+
withLang = withLangGeneral @constr @constr @constr @constr @constr
70126

71-
withPrettyPlcL :: forall s r. SLang s -> (PrettyBy PrettyConfigPlc (FromLang s) => r) -> r
72-
withPrettyPlcL s r = case s of
73-
SPir sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
74-
withNT @PrettyClassic sname $ withNT @PrettyReadable sname $
75-
withA @Pretty sann r
76-
SPlc sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
77-
withNT @PrettyClassic sname $ withNT @PrettyReadable sname $
78-
withA @Pretty sann r
79-
SUplc sname sann -> withN @PrettyClassic sname $ withN @PrettyReadable sname $
80-
withA @Pretty sann r
81-
SData -> r
127+
withPrettyPlcL :: forall s r. SLang s -> (PrettyPlc (FromLang s) => r) -> r
128+
withPrettyPlcL = withLangGeneral
129+
@(PrettyClassic `AndC` PrettyReadable)
130+
@UnitC
131+
@(PrettyClassic `AndC` PrettyReadable)
132+
@Pretty
133+
@PrettyPlc
82134

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

0 commit comments

Comments
 (0)