diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Tom Hawkins 2010
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
diff --git a/Language/SMTLIB.hs b/Language/SMTLIB.hs
new file mode 100644
--- /dev/null
+++ b/Language/SMTLIB.hs
@@ -0,0 +1,312 @@
+-- | Parsing and printing SMT-LIB.
+module Language.SMTLIB
+  (
+  -- * AST
+    Numeral
+  , Symbol
+  , Keyword
+  , Spec_constant        (..)
+  , S_expr               (..)
+  , Identifier           (..)
+  , Sort                 (..)
+  , Attribute_value      (..)
+  , Attribute            (..)
+  , Qual_identifier      (..)
+  , Var_binding          (..)
+  , Sorted_var           (..)
+  , Term                 (..)
+  , Sort_symbol_decl     (..)
+  , Meta_spec_constant   (..)
+  , Fun_symbol_decl      (..)
+  , Par_fun_symbol_decl  (..)
+  , Theory_attribute     (..)
+  , Theory_decl          (..)
+  , Logic_attribute      (..)
+  , Logic                (..)
+  , Option               (..)
+  , Info_flag            (..)
+  , Command              (..)
+  , Script
+  , Gen_response         (..)
+  , Error_behavior       (..)
+  , Reason_unknown       (..)
+  , Status               (..)
+  , Info_response        (..)
+  , Gi_response
+  , Cs_response
+  , Ga_response
+  , Proof
+  , Gp_response
+  , Guc_response
+  , Valuation_pair
+  , Gv_response
+  , T_valuation_pair
+  , Gta_response
+  ) where
+
+import Data.List hiding (group)
+import Text.Printf
+
+type Numeral      = Integer
+type Symbol       = String
+type Keyword      = String
+
+data Spec_constant
+  = Spec_constant_numeral     Numeral
+  | Spec_constant_decimal     Rational
+  | Spec_constant_hexadecimal Integer
+  | Spec_constant_binary      [Bool]
+  | Spec_constant_string      String
+
+instance Show Spec_constant where
+  show a = case a of
+    Spec_constant_numeral     a -> show a
+    Spec_constant_decimal     a -> show (realToFrac a :: Double)
+    Spec_constant_hexadecimal a -> printf "#x%x" a
+    Spec_constant_binary      a -> printf "#b%s" [ if a then '1' else '0' | a <- a ]
+    Spec_constant_string      a -> show a
+
+data S_expr
+  = S_expr_constant Spec_constant
+  | S_expr_symbol   Symbol
+  | S_expr_keyword  Keyword
+  | S_exprs         [S_expr]
+
+group :: String -> String
+group a = "( " ++ a ++ " )"
+
+items :: Show a => [a] -> String
+items = items' . map show
+
+items' :: [String] -> String
+items' = intercalate " "
+
+instance Show S_expr where
+  show a = case a of
+    S_expr_constant a -> show a
+    S_expr_symbol   a -> a
+    S_expr_keyword  a -> a
+    S_exprs         a -> group $ items a
+
+data Identifier
+  = Identifier  Symbol
+  | Identifier_ Symbol [Numeral]
+
+instance Show Identifier where
+  show a = case a of
+    Identifier  a -> a
+    Identifier_ a b -> group $ items' ["_", a, items b]
+
+data Sort
+  = Sort_bool
+  | Sort_identifier  Identifier
+  | Sort_identifiers Identifier [Sort]
+
+instance Show Sort where
+  show a = case a of
+    Sort_bool -> "Bool"
+    Sort_identifier  a -> show a
+    Sort_identifiers a b -> group $ show a ++ " " ++ items b
+
+data Attribute_value
+  = Attribute_value_spec_constant Spec_constant
+  | Attribute_value_symbol        Symbol
+  | Attribute_value_s_expr        [S_expr]
+
+instance Show Attribute_value where
+  show a = case a of
+    Attribute_value_spec_constant a -> show a
+    Attribute_value_symbol        a -> a
+    Attribute_value_s_expr        a -> group $ items a
+
+data Attribute
+  = Attribute        Keyword
+  | Attribute_s_expr Keyword S_expr
+
+instance Show Attribute where
+  show a = case a of
+    Attribute        a -> a
+    Attribute_s_expr a b -> a ++ " " ++ show b
+
+data Qual_identifier
+  = Qual_identifier      Identifier
+  | Qual_identifier_sort Identifier Sort
+
+instance Show Qual_identifier where
+  show a = case a of
+    Qual_identifier      a -> show a
+    Qual_identifier_sort a b -> group $ items' ["as", show a, show b]
+
+data Var_binding
+  = Var_binding Symbol Term
+
+instance Show Var_binding where
+  show a = case a of
+    Var_binding a b -> group $ items' [a, show b]
+
+data Sorted_var
+  = Sorted_var Symbol Sort
+
+instance Show Sorted_var where
+  show a = case a of
+    Sorted_var a b -> group $ items' [a, show b]
+
+data Term
+  = Term_spec_constant    Spec_constant
+  | Term_qual_identifier  Qual_identifier
+  | Term_qual_identifier_ Qual_identifier [Term]
+  | Term_distinct         Term [Term]
+  | Term_let              [Var_binding] Term
+  | Term_forall           [Sorted_var] Term
+  | Term_exists           [Sorted_var] Term
+  | Term_attributes       Term [Attribute]
+
+instance Show Term where
+  show a = case a of
+    Term_spec_constant    a -> show a
+    Term_qual_identifier  a -> show a
+    Term_qual_identifier_ a b -> group $ items' [show a, items b]
+    Term_distinct         a b -> group $ items' ["distinct", show a, items b]
+    Term_let              a b -> group $ items' ["let",    group $ items a, show b]
+    Term_forall           a b -> group $ items' ["forall", group $ items a, show b]
+    Term_exists           a b -> group $ items' ["exists", group $ items a, show b]
+    Term_attributes       a b -> group $ items' ["!", show a, items b]
+
+data Sort_symbol_decl
+  = Sort_symbol_decl Identifier Numeral [Attribute]
+
+instance Show Sort_symbol_decl where
+  show a = case a of
+    Sort_symbol_decl a b c -> group $ items' [show a, show b, items c]
+
+data Meta_spec_constant
+  = Meta_spec_constant_numeral
+  | Meta_spec_constant_decimal
+  | Meta_spec_constant_string
+
+instance Show Meta_spec_constant where
+  show a = case a of
+    Meta_spec_constant_numeral -> "NUMERAL"
+    Meta_spec_constant_decimal -> "DECIMAL"
+    Meta_spec_constant_string  -> "STRING"
+
+data Fun_symbol_decl
+  = Fun_symbol_decl_spec_constant      Sort [Attribute]
+  | Fun_symbol_decl_meta_spec_constant Sort [Attribute]
+  | Fun_symbol_decl                    Identifier [Sort] [Attribute]
+
+data Par_fun_symbol_decl
+  = Par_fun_symbol_decl Fun_symbol_decl
+  | Par_fun_symbol_decl_symbols [Symbol]
+  | Par_fun_symbol_decl_attribute Identifier [Sort] [Attribute]
+
+data Theory_attribute
+  = Theory_attribute_sorts [Symbol]
+  | Theory_attribute_funs  [Par_fun_symbol_decl]
+  | Theory_attribute_sorts_desc String
+  | Theory_attribute_funs_desc  String
+  | Theory_attribute_definition String
+  | Theory_attribute_values     String
+  | Theory_attribute_notes      String
+  | Theory_attribute            Attribute
+
+data Theory_decl
+  = Theory_decl Symbol [Theory_attribute]
+
+data Logic_attribute
+  = Logic_attribute_theories   [Symbol]
+  | Logic_attribute_language   String
+  | Logic_attribute_extensions String
+  | Logic_attribute_values     String
+  | Logic_attribute_notes      String
+  | Logic_attribute            Attribute
+
+data Logic
+  = Logic Symbol [Logic_attribute]
+
+data Option
+  = Print_success       Bool
+  | Expand_definitions  Bool
+  | Interactive_mode    Bool
+  | Produce_proofs      Bool
+  | Produce_unsat_cores Bool
+  | Produce_models      Bool
+  | Produce_assignments Bool
+  | Regular_output_channel String
+  | Diagnostic_output_channel String
+  | Random_seed Integer
+  | Verbosity Integer
+  | Option_attribute Attribute
+
+data Info_flag
+  = Error_behavior
+  | Name
+  | Authors
+  | Version
+  | Status
+  | Reason_unknown
+  | Info_flag Keyword
+  | All_statistics
+
+data Command
+  = Set_logic Symbol
+  | Set_option Option
+  | Set_info Attribute
+  | Declare_sort Symbol Numeral
+  | Define_sort  Symbol [Symbol] Sort
+  | Declare_fun  Symbol [Sort] Sort
+  | Define_fun   Symbol [Sorted_var] Sort Term
+  | Push Int
+  | Pop  Int
+  | Assert Term
+  | Check_sat
+  | Get_assertions
+  | Get_proof
+  | Get_unsat_core
+  | Get_value [Term]
+  | Get_assignment
+  | Get_option [Keyword]
+  | Get_info Info_flag
+  | Exit
+
+type Script = [Command]
+
+data Gen_response
+  = Unsupported
+  | Success
+  | Error String
+
+data Error_behavior
+  = Immediate_exit
+  | Continued_execution
+
+data Reason_unknown
+  = Timeout
+  | Memout
+  | Incomplete
+
+data Status
+  = Sat
+  | Unsat
+  | Unknown
+
+data Info_response
+  = Info_response_error_behavior Error_behavior
+  | Info_response_name    String
+  | Info_response_authors String
+  | Info_response_version String
+  | Info_response_status  Status
+  | Info_response_reason_unknown Reason_unknown
+  | Info_response_attribute Attribute
+
+type Gi_response      = [Info_response]
+type Cs_response      = Status
+type Ga_response      = [Term]
+type Proof            = S_expr
+type Gp_response      = Proof
+type Guc_response     = [Symbol]
+type Valuation_pair   = (Term, Term)
+type Gv_response      = [Valuation_pair]
+type T_valuation_pair = (Symbol, Bool)
+type Gta_response     = [T_valuation_pair]
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,8 @@
+#! /usr/bin/env runhaskell
+
+> module Main (main) where
+>
+> import Distribution.Simple (defaultMain)
+>
+> main :: IO ()
+> main = defaultMain
diff --git a/smt-lib.cabal b/smt-lib.cabal
new file mode 100644
--- /dev/null
+++ b/smt-lib.cabal
@@ -0,0 +1,40 @@
+name:    smt-lib
+version: 0.0.0
+
+category: Language
+
+synopsis: Parsing and printing SMT-LIB.
+
+description:
+  SMT-LIB (http://goedel.cs.uiowa.edu/smtlib/) is a common language used by many SMT solvers.
+  This library provides an SMT-LIB AST with parsing and printing utilities.
+
+author:     Tom Hawkins <tomahawkins@gmail.com>
+maintainer: Tom Hawkins <tomahawkins@gmail.com>
+
+license:      BSD3
+license-file: LICENSE
+
+homepage: http://tomahawkins.org
+
+build-type:    Simple
+cabal-version: >= 1.6
+
+library
+    build-depends:
+        base       >= 4.0 && < 5.0,
+        polyparse  >= 1.4
+
+    exposed-modules:
+        Language.SMTLIB
+
+--    extensions:
+
+    if impl(ghc > 6.8)
+          ghc-options: -fwarn-tabs
+    ghc-options:       -W
+
+source-repository head
+    type:     git
+    location: git://github.com/tomahawkins/smt-lib.git
+