{-# 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) []) []) -- XXX: or add var?
    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) []) []) -- XXX: or add var?

    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)

    -- XXX: For now, we just ignore comments
    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)