{-# 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 :: Trans a -> Maybe a
toMaybe res :: Trans a
res =
case Trans a
res of
OK a :: a
a -> a -> Maybe a
forall a. a -> Maybe a
Just a
a
Fail _ -> Maybe a
forall a. Maybe a
Nothing
toEither :: Trans a -> Either Doc a
toEither :: Trans a -> Either Doc a
toEither res :: Trans a
res =
case Trans a
res of
OK a :: a
a -> a -> Either Doc a
forall a b. b -> Either a b
Right a
a
Fail msg :: Doc
msg -> Doc -> Either Doc a
forall a b. a -> Either a b
Left Doc
msg
instance Functor Trans where
fmap :: (a -> b) -> Trans a -> Trans b
fmap f :: a -> b
f res :: Trans a
res =
case Trans a
res of
OK a :: a
a -> b -> Trans b
forall a. a -> Trans a
OK (a -> b
f a
a)
Fail msg :: Doc
msg -> Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
msg
instance Applicative Trans where
pure :: a -> Trans a
pure x :: a
x = a -> Trans a
forall a. a -> Trans a
OK a
x
OK f :: a -> b
f <*> :: Trans (a -> b) -> Trans a -> Trans b
<*> OK x :: a
x = b -> Trans b
forall a. a -> Trans a
OK (a -> b
f a
x)
Fail x :: Doc
x <*> OK _ = Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
x
OK _ <*> Fail x :: Doc
x = Doc -> Trans b
forall a. Doc -> Trans a
Fail Doc
x
Fail x :: Doc
x <*> Fail y :: Doc
y = Doc -> Trans b
forall a. Doc -> Trans a
Fail (Doc
x Doc -> Doc -> Doc
$$ Doc
y)
err :: Doc -> Trans a
err :: Doc -> Trans a
err msg :: Doc
msg = Doc -> Trans a
forall a. Doc -> Trans a
Fail Doc
msg
name :: V1.Name -> V2.Name
name :: Name -> Name
name (V1.N x :: String
x) = String -> Name
V2.N String
x
ident :: V1.Ident -> V2.Ident
ident :: Ident -> Ident
ident (V1.I x :: Name
x ns :: [Integer]
ns) = Name -> [Integer] -> Ident
V2.I (Name -> Name
name Name
x) [Integer]
ns
quant :: V1.Quant -> V2.Quant
quant :: Quant -> Quant
quant q :: Quant
q =
case Quant
q of
V1.Exists -> Quant
V2.Exists
V1.Forall -> Quant
V2.Forall
binder :: V1.Binder -> V2.Binder
binder :: Binder -> Binder
binder b :: 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 x :: Ident
x = Ident -> [Type] -> Type
V2.TApp (Ident -> Ident
ident Ident
x) []
literal :: V1.Literal -> V2.Literal
literal :: Literal -> Literal
literal lit :: Literal
lit =
case Literal
lit of
V1.LitNum n :: Integer
n -> Integer -> Literal
V2.LitNum Integer
n
V1.LitFrac r :: Rational
r -> Rational -> Literal
V2.LitFrac Rational
r
V1.LitStr s :: String
s -> String -> Literal
V2.LitStr String
s
term :: V1.Term -> Trans V2.Expr
term :: Term -> Trans Expr
term te :: Term
te =
case Term
te of
V1.Var x :: 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 i :: Ident
i ts :: [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 l :: 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 f :: Formula
f t1 :: Term
t1 t2 :: 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 t :: Term
t a :: [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 form :: Formula
form =
case Formula
form of
V1.FTrue -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.true
V1.FFalse -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.false
V1.FPred p :: Ident
p ts :: [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 x :: 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 c :: Conn
c es :: [Formula]
es ->
case (Conn
c,[Formula]
es) of
(V1.Not, [e :: 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
(V1.Implies, [e1 :: Formula
e1,e2 :: 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
(V1.And, _) ->
case [Formula]
es of
[] -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.true
_ -> (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
(V1.Or, _) ->
case [Formula]
es of
[] -> Expr -> Trans Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
V2.false
_ -> (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
(V1.Xor, _ : _) -> (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
(V1.Iff, [e1 :: Formula
e1,e2 :: 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
(V1.IfThenElse, [e1 :: Formula
e1,e2 :: Formula
e2,e3 :: 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
_ -> Doc -> Trans Expr
forall a. Doc -> Trans a
err (String -> Doc
text "Unsupported connective:" Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
V1.pp Formula
form)
V1.Quant q :: Quant
q bs :: [Binder]
bs f :: 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 x :: Name
x t :: Term
t f :: 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 e :: Expr
e = [Defn] -> Expr -> Expr
V2.Let [ Name -> Expr -> Defn
V2.Defn (Name -> Name
name Name
x) Expr
e ]
V1.FLet x :: Name
x f1 :: Formula
f1 f2 :: 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 e :: Expr
e = [Defn] -> Expr -> Expr
V2.Let [ Name -> Expr -> Defn
V2.Defn (Name -> Name
name Name
x) Expr
e ]
V1.FAnnot t :: Formula
t a :: [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 x :: Annot
x = case Annot -> Maybe String
V1.attrVal Annot
x of
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
}
_ -> Doc -> Trans Attr
forall a. Doc -> Trans a
err (String -> Doc
text "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 com :: Command
com =
case Command
com of
V1.CmdLogic l :: 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 f :: 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 f :: 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 s :: Status
s ->
case Status
s of
V1.Sat -> [Command] -> Trans [Command]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Command
V2.CmdCheckSat ]
_ -> Doc -> Trans [Command]
forall a. Doc -> Trans a
err (String -> Doc
text "Unsupported command:" Doc -> Doc -> Doc
<+> Command -> Doc
forall t. PP t => t -> Doc
V1.pp Command
com)
V1.CmdExtraSorts xs :: [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 x :: Name
x = Name -> Integer -> Command
V2.CmdDeclareType Name
x 0
V1.CmdExtraFuns fs :: [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 f :: 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))
_ -> Doc -> Trans Command
forall a. Doc -> Trans a
err (String -> Doc
text "Annotation in function declaration" Doc -> Doc -> Doc
<+>
Command -> Doc
forall t. PP t => t -> Doc
V1.pp Command
com)
V1.CmdExtraPreds fs :: [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 f :: 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
_ -> Doc -> Trans Command
forall a. Doc -> Trans a
err (String -> Doc
text "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 a :: 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 x :: a
x = [a
x]
simpleIdent :: Ident -> Trans Name
simpleIdent (V1.I x :: Name
x []) = Name -> Trans Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Name
name Name
x)
simpleIdent d :: Ident
d =
Doc -> Trans Name
forall a. Doc -> Trans a
err (String -> Doc
text "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 s :: 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)