{-# LANGUAGE Safe #-}
module SMTLib2.Compat1 where
import qualified SMTLib1.AST as V1
import qualified SMTLib1.PP as V1
import qualified SMTLib2.AST as V2
import qualified SMTLib2.Core as V2
import Control.Applicative(Applicative(..), (<$>))
import Data.Traversable(traverse)
import Text.PrettyPrint
data Trans a = OK a | Fail Doc
toMaybe :: Trans a -> Maybe a
toMaybe :: forall a. Trans a -> Maybe a
toMaybe Trans a
res =
case Trans a
res of
OK a
a -> a -> Maybe a
forall a. a -> Maybe a
Just a
a
Fail Doc
_ -> Maybe a
forall a. Maybe a
Nothing
toEither :: Trans a -> Either Doc a
toEither :: forall a. Trans a -> Either Doc a
toEither Trans a
res =
case Trans a
res of
OK a
a -> a -> Either Doc a
forall a b. b -> Either a b
Right a
a
Fail Doc
msg -> Doc -> Either Doc a
forall a b. a -> Either a b
Left Doc
msg
instance Functor Trans where
fmap :: forall a b. (a -> b) -> Trans a -> Trans b
fmap a -> b
f Trans a
res =
case Trans a
res of
OK a
a -> b -> Trans b
forall a. a -> Trans a
OK (a -> b
f a
a)
Fail Doc
msg -> Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
msg
instance Applicative Trans where
pure :: forall a. a -> Trans a
pure a
x = a -> Trans a
forall a. a -> Trans a
OK a
x
OK a -> b
f <*> :: forall a b. Trans (a -> b) -> Trans a -> Trans b
<*> OK a
x = b -> Trans b
forall a. a -> Trans a
OK (a -> b
f a
x)
Fail Doc
x <*> OK a
_ = Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
x
OK a -> b
_ <*> Fail Doc
x = Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
x
Fail Doc
x <*> Fail Doc
y = Doc -> Trans b
forall a. Doc -> Trans a
Fail (Doc
x Doc -> Doc -> Doc
$$ Doc
y)
err :: Doc -> Trans a
err :: forall a. Doc -> Trans a
err Doc
msg = Doc -> Trans a
forall a. Doc -> Trans a
Fail Doc
msg
name :: V1.Name -> V2.Name
name :: Name -> Name
name (V1.N String
x) = String -> Name
V2.N String
x
ident :: V1.Ident -> V2.Ident
ident :: Ident -> Ident
ident (V1.I Name
x [Integer]
ns) = Name -> [Integer] -> Ident
V2.I (Name -> Name
name Name
x) [Integer]
ns
quant :: V1.Quant -> V2.Quant
quant :: Quant -> Quant
quant Quant
q =
case Quant
q of
Quant
V1.Exists -> Quant
V2.Exists
Quant
V1.Forall -> Quant
V2.Forall
binder :: V1.Binder -> V2.Binder
binder :: Binder -> Binder
binder Binder
b = Bind :: Name -> Type -> Binder
V2.Bind { bindVar :: Name
V2.bindVar = Name -> Name
name (Binder -> Name
V1.bindVar Binder
b)
, bindType :: Type
V2.bindType = Ident -> Type
sort (Binder -> Ident
V1.bindSort Binder
b)
}
sort :: V1.Sort -> V2.Type
sort :: Ident -> Type
sort Ident
x = Ident -> [Type] -> Type
V2.TApp (Ident -> Ident
ident Ident
x) []
literal :: V1.Literal -> V2.Literal
literal :: Literal -> Literal
literal Literal
lit =
case Literal
lit of
V1.LitNum Integer
n -> Integer -> Literal
V2.LitNum Integer
n
V1.LitFrac Rational
r -> Rational -> Literal
V2.LitFrac Rational
r
V1.LitStr String
s -> String -> Literal
V2.LitStr String
s
term :: V1.Term -> Trans V2.Expr
term :: Term -> Trans Expr
term Term
te =
case Term
te of
V1.Var Name
x -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> [Expr] -> Expr
V2.app (Name -> [Integer] -> Ident
V2.I (Name -> Name
name Name
x) []) [])
V1.App Ident
i [Term]
ts -> Ident -> [Expr] -> Expr
V2.app (Ident -> Ident
ident Ident
i) ([Expr] -> Expr) -> Trans [Expr] -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Trans Expr) -> [Term] -> Trans [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> Trans Expr
term [Term]
ts
V1.Lit Literal
l -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Literal -> Expr
V2.Lit (Literal -> Literal
literal Literal
l))
V1.ITE Formula
f Term
t1 Term
t2 -> Expr -> Expr -> Expr -> Expr
V2.ite (Expr -> Expr -> Expr -> Expr)
-> Trans Expr -> Trans (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
f Trans (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Trans Expr
term Term
t1 Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Trans Expr
term Term
t2
V1.TAnnot Term
t [Annot]
a -> Expr -> [Attr] -> Expr
V2.Annot (Expr -> [Attr] -> Expr) -> Trans Expr -> Trans ([Attr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Trans Expr
term Term
t Trans ([Attr] -> Expr) -> Trans [Attr] -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Annot -> Trans Attr) -> [Annot] -> Trans [Attr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Annot -> Trans Attr
annot [Annot]
a
formula :: V1.Formula -> Trans V2.Expr
formula :: Formula -> Trans Expr
formula Formula
form =
case Formula
form of
Formula
V1.FTrue -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.true
Formula
V1.FFalse -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.false
V1.FPred Ident
p [Term]
ts -> Ident -> [Expr] -> Expr
V2.app (Ident -> Ident
ident Ident
p) ([Expr] -> Expr) -> Trans [Expr] -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Trans Expr) -> [Term] -> Trans [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> Trans Expr
term [Term]
ts
V1.FVar Name
x -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> [Expr] -> Expr
V2.app (Name -> [Integer] -> Ident
V2.I (Name -> Name
name Name
x) []) [])
V1.Conn Conn
c [Formula]
es ->
case (Conn
c,[Formula]
es) of
(Conn
V1.Not, [Formula
e]) -> Expr -> Expr
V2.not (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
e
(Conn
V1.Implies, [Formula
e1,Formula
e2]) -> Expr -> Expr -> Expr
(V2.==>) (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
e1 Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
e2
(Conn
V1.And, [Formula]
_) ->
case [Formula]
es of
[] -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.true
[Formula]
_ -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Expr -> Expr -> Expr
V2.and ([Expr] -> Expr) -> Trans [Expr] -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> Trans Expr) -> [Formula] -> Trans [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Formula -> Trans Expr
formula [Formula]
es
(Conn
V1.Or, [Formula]
_) ->
case [Formula]
es of
[] -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.false
[Formula]
_ -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Expr -> Expr -> Expr
V2.or ([Expr] -> Expr) -> Trans [Expr] -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> Trans Expr) -> [Formula] -> Trans [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Formula -> Trans Expr
formula [Formula]
es
(Conn
V1.Xor, Formula
_ : [Formula]
_) -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Expr -> Expr -> Expr
V2.xor ([Expr] -> Expr) -> Trans [Expr] -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> Trans Expr) -> [Formula] -> Trans [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Formula -> Trans Expr
formula [Formula]
es
(Conn
V1.Iff, [Formula
e1,Formula
e2]) -> Expr -> Expr -> Expr
(V2.===) (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
e1 Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
e2
(Conn
V1.IfThenElse, [Formula
e1,Formula
e2,Formula
e3]) -> Expr -> Expr -> Expr -> Expr
V2.ite (Expr -> Expr -> Expr -> Expr)
-> Trans Expr -> Trans (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
e1
Trans (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
e2
Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
e3
(Conn, [Formula])
_ -> Doc -> Trans Expr
forall a. Doc -> Trans a
err (String -> Doc
text String
"Unsupported connective:" Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
V1.pp Formula
form)
V1.Quant Quant
q [Binder]
bs Formula
f -> Quant -> [Binder] -> Expr -> Expr
V2.Quant (Quant -> Quant
quant Quant
q) ((Binder -> Binder) -> [Binder] -> [Binder]
forall a b. (a -> b) -> [a] -> [b]
map Binder -> Binder
binder [Binder]
bs) (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
f
V1.Let Name
x Term
t Formula
f -> Expr -> Expr -> Expr
mkLet (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Trans Expr
term Term
t Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
f
where mkLet :: Expr -> Expr -> Expr
mkLet Expr
e = [Defn] -> Expr -> Expr
V2.Let [ Name -> Expr -> Defn
V2.Defn (Name -> Name
name Name
x) Expr
e ]
V1.FLet Name
x Formula
f1 Formula
f2 -> Expr -> Expr -> Expr
mkLet (Expr -> Expr -> Expr) -> Trans Expr -> Trans (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
f1 Trans (Expr -> Expr) -> Trans Expr -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Trans Expr
formula Formula
f2
where mkLet :: Expr -> Expr -> Expr
mkLet Expr
e = [Defn] -> Expr -> Expr
V2.Let [ Name -> Expr -> Defn
V2.Defn (Name -> Name
name Name
x) Expr
e ]
V1.FAnnot Formula
t [Annot]
a -> Expr -> [Attr] -> Expr
V2.Annot (Expr -> [Attr] -> Expr) -> Trans Expr -> Trans ([Attr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
t Trans ([Attr] -> Expr) -> Trans [Attr] -> Trans Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Annot -> Trans Attr) -> [Annot] -> Trans [Attr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Annot -> Trans Attr
annot [Annot]
a
annot :: V1.Annot -> Trans V2.Attr
annot :: Annot -> Trans Attr
annot Annot
x = case Annot -> Maybe String
V1.attrVal Annot
x of
Maybe String
Nothing -> Attr -> Trans Attr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Attr :: Name -> Maybe Expr -> Attr
V2.Attr { attrName :: Name
V2.attrName = Name -> Name
name (Annot -> Name
V1.attrName Annot
x)
, attrVal :: Maybe Expr
V2.attrVal = Maybe Expr
forall a. Maybe a
Nothing
}
Maybe String
_ -> Doc -> Trans Attr
forall a. Doc -> Trans a
err (String -> Doc
text String
"Unsupported annotation:" Doc -> Doc -> Doc
<+> Annot -> Doc
forall t. PP t => t -> Doc
V1.pp Annot
x)
command :: V1.Command -> Trans [V2.Command]
command :: Command -> Trans [Command]
command Command
com =
case Command
com of
V1.CmdLogic Ident
l -> Command -> [Command]
forall {a}. a -> [a]
one (Command -> [Command]) -> (Name -> Command) -> Name -> [Command]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Command
V2.CmdSetLogic (Name -> [Command]) -> Trans Name -> Trans [Command]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Trans Name
simpleIdent Ident
l
V1.CmdAssumption Formula
f -> Command -> [Command]
forall {a}. a -> [a]
one (Command -> [Command]) -> (Expr -> Command) -> Expr -> [Command]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Command
V2.CmdAssert (Expr -> [Command]) -> Trans Expr -> Trans [Command]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
f
V1.CmdFormula Formula
f -> Command -> [Command]
forall {a}. a -> [a]
one (Command -> [Command]) -> (Expr -> Command) -> Expr -> [Command]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Command
V2.CmdAssert (Expr -> [Command]) -> Trans Expr -> Trans [Command]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> Trans Expr
formula Formula
f
V1.CmdStatus Status
s ->
case Status
s of
Status
V1.Sat -> [Command] -> Trans [Command]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Command
V2.CmdCheckSat ]
Status
_ -> Doc -> Trans [Command]
forall a. Doc -> Trans a
err (String -> Doc
text String
"Unsupported command:" Doc -> Doc -> Doc
<+> Command -> Doc
forall t. PP t => t -> Doc
V1.pp Command
com)
V1.CmdExtraSorts [Ident]
xs -> (Name -> Command) -> [Name] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Command
decl ([Name] -> [Command]) -> Trans [Name] -> Trans [Command]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ident -> Trans Name) -> [Ident] -> Trans [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Ident -> Trans Name
simpleIdent [Ident]
xs
where decl :: Name -> Command
decl Name
x = Name -> Integer -> Command
V2.CmdDeclareType Name
x Integer
0
V1.CmdExtraFuns [FunDecl]
fs -> (FunDecl -> Trans Command) -> [FunDecl] -> Trans [Command]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse FunDecl -> Trans Command
decl [FunDecl]
fs
where decl :: FunDecl -> Trans Command
decl FunDecl
f = case FunDecl -> [Annot]
V1.funAnnots FunDecl
f of
[] -> Name -> [Type] -> Type -> Command
V2.CmdDeclareFun
(Name -> [Type] -> Type -> Command)
-> Trans Name -> Trans ([Type] -> Type -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Trans Name
simpleIdent (FunDecl -> Ident
V1.funName FunDecl
f)
Trans ([Type] -> Type -> Command)
-> Trans [Type] -> Trans (Type -> Command)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type] -> Trans [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Ident -> Type) -> [Ident] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Type
sort (FunDecl -> [Ident]
V1.funArgs FunDecl
f))
Trans (Type -> Command) -> Trans Type -> Trans Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Trans Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> Type
sort (FunDecl -> Ident
V1.funRes FunDecl
f))
[Annot]
_ -> Doc -> Trans Command
forall a. Doc -> Trans a
err (String -> Doc
text String
"Annotation in function declaration" Doc -> Doc -> Doc
<+>
Command -> Doc
forall t. PP t => t -> Doc
V1.pp Command
com)
V1.CmdExtraPreds [PredDecl]
fs -> (PredDecl -> Trans Command) -> [PredDecl] -> Trans [Command]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PredDecl -> Trans Command
decl [PredDecl]
fs
where decl :: PredDecl -> Trans Command
decl PredDecl
f = case PredDecl -> [Annot]
V1.predAnnots PredDecl
f of
[] -> Name -> [Type] -> Type -> Command
V2.CmdDeclareFun
(Name -> [Type] -> Type -> Command)
-> Trans Name -> Trans ([Type] -> Type -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Trans Name
simpleIdent (PredDecl -> Ident
V1.predName PredDecl
f)
Trans ([Type] -> Type -> Command)
-> Trans [Type] -> Trans (Type -> Command)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type] -> Trans [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Ident -> Type) -> [Ident] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Type
sort (PredDecl -> [Ident]
V1.predArgs PredDecl
f))
Trans (Type -> Command) -> Trans Type -> Trans Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Trans Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
V2.tBool
[Annot]
_ -> Doc -> Trans Command
forall a. Doc -> Trans a
err (String -> Doc
text String
"Annotation in predicate declaration" Doc -> Doc -> Doc
<+>
Command -> Doc
forall t. PP t => t -> Doc
V1.pp Command
com)
V1.CmdNotes {} -> [Command] -> Trans [Command]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
V1.CmdAnnot Annot
a -> Command -> [Command]
forall {a}. a -> [a]
one (Command -> [Command]) -> (Attr -> Command) -> Attr -> [Command]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> Command
V2.CmdSetInfo (Attr -> [Command]) -> Trans Attr -> Trans [Command]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annot -> Trans Attr
annot Annot
a
where one :: a -> [a]
one a
x = [a
x]
simpleIdent :: Ident -> Trans Name
simpleIdent (V1.I Name
x []) = Name -> Trans Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Name
name Name
x)
simpleIdent Ident
d =
Doc -> Trans Name
forall a. Doc -> Trans a
err (String -> Doc
text String
"Unsupported identifier in command:" Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. PP t => t -> Doc
V1.pp Ident
d)
script :: V1.Script -> Trans V2.Script
script :: Script -> Trans Script
script Script
s = [Command] -> Script
V2.Script ([Command] -> Script)
-> ([[Command]] -> [Command]) -> [[Command]] -> Script
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Command]] -> [Command]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Command]] -> Script) -> Trans [[Command]] -> Trans Script
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Command -> Trans [Command]) -> [Command] -> Trans [[Command]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Command -> Trans [Command]
command (Script -> [Command]
V1.scrCommands Script
s)