    {-# 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 = 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 a. a -> Trans a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Term -> Trans Expr
    term [Term]
    ts
        V1.Lit Literal
    l       -> Expr -> Trans Expr
    forall a. a -> Trans a
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a. a -> Trans a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    V2.true

        Formula
    V1.FFalse     -> Expr -> Trans Expr
    forall a. a -> Trans a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Term -> Trans Expr
    term [Term]
    ts

        V1.FVar Name
    x     -> Expr -> Trans Expr
    forall a. a -> Trans a
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a. a -> Trans a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    V2.true
                 [Formula]
    _  -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
    forall a. (a -> a -> a) -> [a] -> a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Formula -> Trans Expr
    formula [Formula]
    es
            (Conn
    V1.Or, [Formula]
    _) ->
               case [Formula]
    es of
                 [] -> Expr -> Trans Expr
    forall a. a -> Trans a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    V2.false
                 [Formula]
    _  -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
    forall a. (a -> a -> a) -> [a] -> a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Formula -> Trans Expr
    formula [Formula]
    es
            (Conn
    V1.Xor, Formula
    _ : [Formula]
    _)             -> (Expr -> Expr -> Expr) -> [Expr] -> Expr
    forall a. (a -> a -> a) -> [a] -> a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a. a -> Trans a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure 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 a. a -> Trans a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a b. Trans (a -> b) -> Trans a -> Trans b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Type] -> Trans [Type]
    forall a. a -> Trans a
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> Trans Type
    forall a. a -> Trans a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a b. Trans (a -> b) -> Trans a -> Trans b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Type] -> Trans [Type]
    forall a. a -> Trans a
    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 a b. Trans (a -> b) -> Trans a -> Trans b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> Trans Type
    forall a. a -> Trans a
    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 a. a -> Trans a
    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 a. a -> Trans a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Command -> Trans [Command]
    command (Script -> [Command]
    V1.scrCommands Script
    s)