smt-lib 0.0.0 → 0.0.1
raw patch · 4 files changed
+850/−41 lines, 4 filesdep +arraydep +directory
Dependencies added: array, directory
Files
- Language/SMTLIB.hs +428/−34
- Language/SMTLIB/Lexer.x +55/−0
- dist/build/Language/SMTLIB/Lexer.hs +361/−0
- smt-lib.cabal +6/−7
Language/SMTLIB.hs view
@@ -1,7 +1,7 @@ -- | Parsing and printing SMT-LIB. module Language.SMTLIB (- -- * AST+ -- * Syntax Numeral , Symbol , Keyword@@ -26,7 +26,7 @@ , Option (..) , Info_flag (..) , Command (..)- , Script+ , Script (..) , Gen_response (..) , Error_behavior (..) , Reason_unknown (..)@@ -42,11 +42,20 @@ , Gv_response , T_valuation_pair , Gta_response+ -- * Parsing+ , parseScript+ -- * Parsing Verification+ , checkParser ) where import Data.List hiding (group)+import System.Directory+import System.IO+import Text.ParserCombinators.Poly.Plain hiding (Success) import Text.Printf +import Language.SMTLIB.Lexer+ type Numeral = Integer type Symbol = String type Keyword = String@@ -66,28 +75,40 @@ Spec_constant_binary a -> printf "#b%s" [ if a then '1' else '0' | a <- a ] Spec_constant_string a -> show a +spec_constant :: SMTLIB Spec_constant+spec_constant = oneOf+ [ numeral >>= return . Spec_constant_numeral+ , string >>= return . Spec_constant_string+ , do+ a <- satisfy (\ a -> case a of { Decimal _ -> True; Hex _ -> True; Bin _ -> True; _ -> False })+ case a of+ Decimal a -> return $ Spec_constant_decimal $ toRational a+ Hex a -> return $ Spec_constant_hexadecimal $ read $ "0x" ++ a --XXX Leading 0s will be dropped.+ Bin a -> return $ Spec_constant_binary $ map (== '1') a+ _ -> undefined+ ]+ 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+ S_exprs a -> group $ map show a +s_expr :: SMTLIB S_expr+s_expr = oneOf+ [ spec_constant >>= return . S_expr_constant+ , symbol >>= return . S_expr_symbol+ , keyword >>= return . S_expr_keyword+ , do { left; a <- many s_expr; right; return $ S_exprs a }+ ]+ data Identifier = Identifier Symbol | Identifier_ Symbol [Numeral]@@ -95,8 +116,14 @@ instance Show Identifier where show a = case a of Identifier a -> a- Identifier_ a b -> group $ items' ["_", a, items b]+ Identifier_ a b -> group $ ["_", a] ++ map show b +identifier :: SMTLIB Identifier+identifier = oneOf+ [ symbol >>= return . Identifier+ , do { left; tok (Symbol "_"); a <- symbol; b <- many1 numeral; right; return $ Identifier_ a b }+ ]+ data Sort = Sort_bool | Sort_identifier Identifier@@ -106,8 +133,15 @@ show a = case a of Sort_bool -> "Bool" Sort_identifier a -> show a- Sort_identifiers a b -> group $ show a ++ " " ++ items b+ Sort_identifiers a b -> group $ show a : map show b +sort' :: SMTLIB Sort+sort' = oneOf+ [ tok (Symbol "Bool") >> return Sort_bool+ , identifier >>= return . Sort_identifier+ , do { left; a <- identifier; b <- many1 sort'; right; return $ Sort_identifiers a b }+ ]+ data Attribute_value = Attribute_value_spec_constant Spec_constant | Attribute_value_symbol Symbol@@ -117,8 +151,15 @@ 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+ Attribute_value_s_expr a -> group $ map show a +attribute_value :: SMTLIB Attribute_value+attribute_value = oneOf+ [ spec_constant >>= return . Attribute_value_spec_constant+ , symbol >>= return . Attribute_value_symbol+ , do { left; a <- many s_expr; right; return $ Attribute_value_s_expr a }+ ]+ data Attribute = Attribute Keyword | Attribute_s_expr Keyword S_expr@@ -128,6 +169,12 @@ Attribute a -> a Attribute_s_expr a b -> a ++ " " ++ show b +attribute :: SMTLIB Attribute+attribute = oneOf+ [ do { a <- keyword; b <- s_expr; return $ Attribute_s_expr a b }+ , keyword >>= return . Attribute+ ]+ data Qual_identifier = Qual_identifier Identifier | Qual_identifier_sort Identifier Sort@@ -135,22 +182,34 @@ 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]+ Qual_identifier_sort a b -> group ["as", show a, show b] +qual_identifier :: SMTLIB Qual_identifier+qual_identifier = oneOf+ [ identifier >>= return . Qual_identifier+ , do { left; tok $ Symbol "as"; a <- identifier; b <- sort'; right; return $ Qual_identifier_sort a 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]+ Var_binding a b -> group [a, show b] +var_binding :: SMTLIB Var_binding+var_binding = do { left; a <- symbol; b <- term; right; return $ Var_binding a 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]+ Sorted_var a b -> group [a, show b] +sorted_var :: SMTLIB Sorted_var+sorted_var = do { left; a <- symbol; b <- sort'; right; return $ Sorted_var a b }+ data Term = Term_spec_constant Spec_constant | Term_qual_identifier Qual_identifier@@ -165,20 +224,35 @@ 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]+ Term_qual_identifier_ a b -> group $ show a : map show b+ Term_distinct a b -> group $ ["distinct", show a] ++ map show b+ Term_let a b -> group $ ["let", group $ map show a, show b]+ Term_forall a b -> group $ ["forall", group $ map show a, show b]+ Term_exists a b -> group $ ["exists", group $ map show a, show b]+ Term_attributes a b -> group $ ["!", show a] ++ map show b +term :: SMTLIB Term+term = oneOf+ [ spec_constant >>= return . Term_spec_constant+ , qual_identifier >>= return . Term_qual_identifier+ , do { left; a <- qual_identifier; b <- many1 term; right; return $ Term_qual_identifier_ a b }+ , do { left; tok $ Symbol "distinct"; a <- term; b <- many1 term; right; return $ Term_distinct a b }+ , do { left; tok $ Symbol "let"; left; a <- many1 var_binding; right; b <- term; right; return $ Term_let a b }+ , do { left; tok $ Symbol "forall"; left; a <- many1 sorted_var; right; b <- term; right; return $ Term_forall a b }+ , do { left; tok $ Symbol "exists"; left; a <- many1 sorted_var; right; b <- term; right; return $ Term_exists a b }+ , do { left; tok $ Symbol "!"; a <- term; b <- many1 attribute; right; return $ Term_attributes a 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]+ Sort_symbol_decl a b c -> group $ [show a, show b] ++ map show c +sort_symbol_decl :: SMTLIB Sort_symbol_decl+sort_symbol_decl = do { left; a <- identifier; b <- numeral; c <- many attribute; right; return $ Sort_symbol_decl a b c }+ data Meta_spec_constant = Meta_spec_constant_numeral | Meta_spec_constant_decimal@@ -190,18 +264,48 @@ Meta_spec_constant_decimal -> "DECIMAL" Meta_spec_constant_string -> "STRING" +meta_spec_constant :: SMTLIB Meta_spec_constant+meta_spec_constant = oneOf+ [ do { tok $ Symbol "NUMERAL"; return Meta_spec_constant_numeral }+ , do { tok $ Symbol "DECIMAL"; return Meta_spec_constant_decimal }+ , do { tok $ Symbol "STRING" ; return Meta_spec_constant_string }+ ]+ data Fun_symbol_decl- = Fun_symbol_decl_spec_constant Sort [Attribute]- | Fun_symbol_decl_meta_spec_constant Sort [Attribute]+ = Fun_symbol_decl_spec_constant Spec_constant Sort [Attribute]+ | Fun_symbol_decl_meta_spec_constant Meta_spec_constant Sort [Attribute] | Fun_symbol_decl Identifier [Sort] [Attribute] +instance Show Fun_symbol_decl where+ show a = case a of+ Fun_symbol_decl_spec_constant a b c -> group $ [show a, show b] ++ map show c+ Fun_symbol_decl_meta_spec_constant a b c -> group $ [show a, show b] ++ map show c+ Fun_symbol_decl a b c -> group $ [show a] ++ map show b ++ map show c++fun_symbol_decl :: SMTLIB Fun_symbol_decl+fun_symbol_decl = oneOf+ [ do { left; a <- spec_constant; b <- sort'; c <- many attribute; right; return $ Fun_symbol_decl_spec_constant a b c }+ , do { left; a <- meta_spec_constant; b <- sort'; c <- many attribute; right; return $ Fun_symbol_decl_meta_spec_constant a b c }+ , do { left; a <- identifier; b <- many1 sort'; c <- many attribute; right; return $ Fun_symbol_decl a b c }+ ]+ 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]+ | Par_fun_symbol_decl_symbols [Symbol] Identifier [Sort] [Attribute] +instance Show Par_fun_symbol_decl where+ show a = case a of+ Par_fun_symbol_decl a -> show a+ Par_fun_symbol_decl_symbols a b c d -> group ["par", group $ map show a, group $ [show b] ++ map show c ++ map show d]++par_fun_symbol_decl :: SMTLIB Par_fun_symbol_decl+par_fun_symbol_decl = oneOf+ [ fun_symbol_decl >>= return . Par_fun_symbol_decl+ , do { left; tok $ Symbol "par"; left; a <- many1 symbol; right; left; b <- identifier; c <- many1 sort'; d <- many attribute; right; right; return $ Par_fun_symbol_decl_symbols a b c d }+ ]+ data Theory_attribute- = Theory_attribute_sorts [Symbol]+ = Theory_attribute_sorts [Sort_symbol_decl] | Theory_attribute_funs [Par_fun_symbol_decl] | Theory_attribute_sorts_desc String | Theory_attribute_funs_desc String@@ -210,9 +314,39 @@ | Theory_attribute_notes String | Theory_attribute Attribute +instance Show Theory_attribute where+ show a = case a of+ Theory_attribute_sorts a -> ":sorts " ++ group (map show a)+ Theory_attribute_funs a -> ":funs " ++ group (map show a)+ Theory_attribute_sorts_desc a -> ":sorts-description " ++ show a+ Theory_attribute_funs_desc a -> ":funs-description " ++ show a+ Theory_attribute_definition a -> ":definition " ++ show a+ Theory_attribute_values a -> ":values " ++ show a+ Theory_attribute_notes a -> ":notes " ++ show a+ Theory_attribute a -> show a++theory_attribute :: SMTLIB Theory_attribute+theory_attribute = oneOf+ [ do { tok $ Keyword ":sorts"; left; a <- many1 sort_symbol_decl; right; return $ Theory_attribute_sorts a }+ , do { tok $ Keyword ":funs"; left; a <- many1 par_fun_symbol_decl; right; return $ Theory_attribute_funs a }+ , do { tok $ Keyword ":sorts-description"; a <- string; return $ Theory_attribute_sorts_desc a }+ , do { tok $ Keyword ":funs-description"; a <- string; return $ Theory_attribute_funs_desc a }+ , do { tok $ Keyword ":definition"; a <- string; return $ Theory_attribute_definition a }+ , do { tok $ Keyword ":values"; a <- string; return $ Theory_attribute_values a }+ , do { tok $ Keyword ":notes"; a <- string; return $ Theory_attribute_notes a }+ , attribute >>= return . Theory_attribute+ ]+ data Theory_decl = Theory_decl Symbol [Theory_attribute] +instance Show Theory_decl where+ show a = case a of+ Theory_decl a b -> group $ ["theory", show a] ++ map show b++theory_decl :: SMTLIB Theory_decl+theory_decl = do { left; tok $ Symbol "theory"; a <- symbol; b <- many1 theory_attribute; right; return $ Theory_decl a b }+ data Logic_attribute = Logic_attribute_theories [Symbol] | Logic_attribute_language String@@ -221,9 +355,35 @@ | Logic_attribute_notes String | Logic_attribute Attribute +instance Show Logic_attribute where+ show a = case a of+ Logic_attribute_theories a -> ":theories " ++ group (map show a)+ Logic_attribute_language a -> ":language " ++ show a+ Logic_attribute_extensions a -> ":extensions " ++ show a+ Logic_attribute_values a -> ":values " ++ show a+ Logic_attribute_notes a -> ":notes " ++ show a+ Logic_attribute a -> show a++logic_attribute :: SMTLIB Logic_attribute+logic_attribute = oneOf+ [ do { tok $ Keyword ":theories"; left; a <- many1 symbol; right; return $ Logic_attribute_theories a }+ , do { tok $ Keyword ":language"; left; a <- string; right; return $ Logic_attribute_language a }+ , do { tok $ Keyword ":extensions"; left; a <- string; right; return $ Logic_attribute_extensions a }+ , do { tok $ Keyword ":values"; left; a <- string; right; return $ Logic_attribute_values a }+ , do { tok $ Keyword ":notes"; left; a <- string; right; return $ Logic_attribute_notes a }+ , attribute >>= return . Logic_attribute+ ]+ data Logic = Logic Symbol [Logic_attribute] +instance Show Logic where+ show a = case a of+ Logic a b -> group $ ["logic", a] ++ map show b++logic :: SMTLIB Logic+logic = do { left; tok $ Symbol "logic"; a <- symbol; b <- many1 logic_attribute; right; return $ Logic a b }+ data Option = Print_success Bool | Expand_definitions Bool@@ -234,10 +394,41 @@ | Produce_assignments Bool | Regular_output_channel String | Diagnostic_output_channel String- | Random_seed Integer- | Verbosity Integer+ | Random_seed Int+ | Verbosity Int | Option_attribute Attribute +instance Show Option where+ show a = case a of+ Print_success a -> ":print-success " ++ showBool a+ Expand_definitions a -> ":expand-definitions " ++ showBool a+ Interactive_mode a -> ":interactive-mode " ++ showBool a+ Produce_proofs a -> ":produce-proofs " ++ showBool a+ Produce_unsat_cores a -> ":produce-unsat-cores " ++ showBool a+ Produce_models a -> ":produce-models " ++ showBool a+ Produce_assignments a -> ":produce-assignments " ++ showBool a+ Regular_output_channel a -> ":regular-output-channel " ++ show a+ Diagnostic_output_channel a -> ":diagnostic-output-channel " ++ show a+ Random_seed a -> ":random-seed " ++ show a+ Verbosity a -> ":verbosity " ++ show a+ Option_attribute a -> show a++option :: SMTLIB Option+option = oneOf+ [ do { tok $ Symbol ":print-success"; a <- b_value; return $ Print_success a }+ , do { tok $ Symbol ":expand-definitions"; a <- b_value; return $ Expand_definitions a }+ , do { tok $ Symbol ":interactive-mode"; a <- b_value; return $ Interactive_mode a }+ , do { tok $ Symbol ":produce-proofs"; a <- b_value; return $ Produce_proofs a }+ , do { tok $ Symbol ":produce-unsat-cores"; a <- b_value; return $ Produce_unsat_cores a }+ , do { tok $ Symbol ":produce-models"; a <- b_value; return $ Produce_models a }+ , do { tok $ Symbol ":produce-assignments"; a <- b_value; return $ Produce_assignments a }+ , do { tok $ Symbol ":regular-output-channel"; a <- string; return $ Regular_output_channel a }+ , do { tok $ Symbol ":diagnostic-output-channel"; a <- string; return $ Diagnostic_output_channel a }+ , do { tok $ Symbol ":random-seed"; a <- numeral; return $ Random_seed $ fromIntegral a }+ , do { tok $ Symbol ":verbosity"; a <- numeral; return $ Verbosity $ fromIntegral a }+ , attribute >>= return . Option_attribute+ ]+ data Info_flag = Error_behavior | Name@@ -248,6 +439,29 @@ | Info_flag Keyword | All_statistics +instance Show Info_flag where+ show a = case a of+ Error_behavior -> ":error-behavior"+ Name -> ":name"+ Authors -> ":authors"+ Version -> ":version"+ Status -> ":status"+ Reason_unknown -> ":reason-unknown"+ Info_flag a -> a+ All_statistics -> ":all-statistics"++info_flag :: SMTLIB Info_flag+info_flag = oneOf+ [ do { tok $ Keyword ":error-behavior"; return Error_behavior }+ , do { tok $ Keyword ":name" ; return Name }+ , do { tok $ Keyword ":authors" ; return Authors }+ , do { tok $ Keyword ":version" ; return Version }+ , do { tok $ Keyword ":status" ; return Status }+ , do { tok $ Keyword ":reason-unknown"; return Reason_unknown }+ , do { tok $ Keyword ":all-statistics"; return All_statistics }+ , keyword >>= return . Info_flag+ ]+ data Command = Set_logic Symbol | Set_option Option@@ -265,31 +479,105 @@ | Get_unsat_core | Get_value [Term] | Get_assignment- | Get_option [Keyword]+ | Get_option Keyword | Get_info Info_flag | Exit -type Script = [Command]+instance Show Command where+ show a = case a of+ Set_logic a -> group ["set-logic", a]+ Set_option a -> group ["set-option", show a]+ Set_info a -> group ["set-info", show a]+ Declare_sort a b -> group ["declare-sort", a, show b]+ Define_sort a b c -> group ["define-sort", a, group (map show b), show c]+ Declare_fun a b c -> group ["declare-fun", a, group (map show b), show c]+ Define_fun a b c d -> group ["define_fun", a, group (map show b), show c, show d]+ Push a -> group ["push", show a]+ Pop a -> group ["pop", show a]+ Assert a -> group ["assert", show a]+ Check_sat -> group ["check-sat"]+ Get_assertions -> group ["get-assertions"]+ Get_proof -> group ["get-proof"]+ Get_unsat_core -> group ["get-unsat-core"]+ Get_value a -> group ["get-value", group $ map show a]+ Get_assignment -> group ["get-assignment"]+ Get_option a -> group ["get-option", a]+ Get_info a -> group ["get-info", show a]+ Exit -> group ["exit"] +command :: SMTLIB Command+command = oneOf+ [ do { left; tok $ Symbol "set-logic"; a <- symbol; right; return $ Set_logic a }+ , do { left; tok $ Symbol "set-option"; a <- option; right; return $ Set_option a }+ , do { left; tok $ Symbol "set-info"; a <- attribute; right; return $ Set_info a }+ , do { left; tok $ Symbol "declare-sort"; a <- symbol; b <- numeral; right; return $ Declare_sort a b }+ , do { left; tok $ Symbol "define-sort"; a <- symbol; left; b <- many symbol; right; c <- sort'; right; return $ Define_sort a b c }+ , do { left; tok $ Symbol "declare-fun"; a <- symbol; left; b <- many sort'; right; c <- sort'; right; return $ Declare_fun a b c }+ , do { left; tok $ Symbol "define-fun"; a <- symbol; left; b <- many sorted_var; right; c <- sort'; d <- term; right; return $ Define_fun a b c d }+ , do { left; tok $ Symbol "push"; a <- numeral; right; return $ Push $ fromIntegral a }+ , do { left; tok $ Symbol "pop"; a <- numeral; right; return $ Pop $ fromIntegral a }+ , do { left; tok $ Symbol "assert"; a <- term; right; return $ Assert a }+ , do { left; tok $ Symbol "check-sat"; right; return $ Check_sat }+ , do { left; tok $ Symbol "get-assertions"; right; return $ Get_assertions }+ , do { left; tok $ Symbol "get-proof"; right; return $ Get_proof }+ , do { left; tok $ Symbol "get-unsat-core"; right; return $ Get_unsat_core }+ , do { left; tok $ Symbol "get-value"; left; a <- many1 term; right; right; return $ Get_value a }+ , do { left; tok $ Symbol "get-assignment"; right; return $ Get_assignment }+ , do { left; tok $ Symbol "get-option"; a <- keyword; right; return $ Get_option a }+ , do { left; tok $ Symbol "get-info"; a <- info_flag; right; return $ Get_info a }+ , do { left; tok $ Symbol "exit"; right; return $ Exit }+ ]++data Script = Script [Command]++instance Show Script where+ show (Script a) = unlines $ map show a++script :: SMTLIB Script+script = many command >>= return . Script+ data Gen_response = Unsupported | Success | Error String +instance Show Gen_response where+ show a = case a of+ Unsupported -> "unsupported"+ Success -> "sucess"+ Error a -> group ["error", show a]+ data Error_behavior = Immediate_exit | Continued_execution +instance Show Error_behavior where+ show a = case a of+ Immediate_exit -> "immediate-exit"+ Continued_execution -> "continued-execution"+ data Reason_unknown = Timeout | Memout | Incomplete +instance Show Reason_unknown where+ show a = case a of+ Timeout -> "timeout"+ Memout -> "memout"+ Incomplete -> "incomplete"+ data Status = Sat | Unsat | Unknown +instance Show Status where+ show a = case a of+ Sat -> "sat"+ Unsat -> "unsat"+ Unknown -> "unknown"+ data Info_response = Info_response_error_behavior Error_behavior | Info_response_name String@@ -299,6 +587,16 @@ | Info_response_reason_unknown Reason_unknown | Info_response_attribute Attribute +instance Show Info_response where+ show a = case a of+ Info_response_error_behavior a -> ":error-behavior " ++ show a+ Info_response_name a -> ":name " ++ show a+ Info_response_authors a -> ":authors " ++ show a+ Info_response_version a -> ":version " ++ show a+ Info_response_status a -> ":status " ++ show a+ Info_response_reason_unknown a -> ":reason-unknown " ++ show a+ Info_response_attribute a -> show a+ type Gi_response = [Info_response] type Cs_response = Status type Ga_response = [Term]@@ -309,4 +607,100 @@ type Gv_response = [Valuation_pair] type T_valuation_pair = (Symbol, Bool) type Gta_response = [T_valuation_pair]++group :: [String] -> String+group a = "( " ++ intercalate " " a ++ " )"++showBool :: Bool -> String+showBool a = if a then "true" else "false"++type SMTLIB a = Parser Token a++tok :: Token -> SMTLIB ()+tok a = satisfy (== a) >> return ()++left :: SMTLIB ()+left = tok LeftParen++right :: SMTLIB ()+right = tok RightParen++numeral :: SMTLIB Numeral+numeral = do+ a <- satisfy (\ a -> case a of { Numeral _ -> True; _ -> False })+ case a of+ Numeral a -> return a+ _ -> undefined++string :: SMTLIB String+string = do+ a <- satisfy (\ a -> case a of { String _ -> True; _ -> False })+ case a of+ String a -> return a+ _ -> undefined++symbol :: SMTLIB Symbol+symbol = do+ a <- satisfy (\ a -> case a of { Symbol _ -> True; _ -> False })+ case a of+ Symbol a -> return a+ _ -> undefined++keyword :: SMTLIB Keyword+keyword = do+ a <- satisfy (\ a -> case a of { Keyword _ -> True; _ -> False })+ case a of+ Keyword a -> return a+ _ -> undefined++b_value :: SMTLIB Bool+b_value = oneOf+ [ do { tok $ Symbol "true"; return True }+ , do { tok $ Symbol "false"; return False }+ ]++-- | Parses an SMT-LIB command script.+parseScript :: String -> Script+parseScript s = case runParser script $ lexSMTLIB s of+ (Left msg, _) -> error msg+ (Right a, _) -> a++-- | Checks the parsing of a command script.+checkScript :: String -> Bool+checkScript script = clean script == clean (show $ parseScript script)+ where+ clean = filter (flip notElem " \r\n\t") . unlines . map (takeWhile (/= ';')) . lines++-- | Recursively searches current directory for *.smt2 files to test the parser.+checkParser :: IO ()+checkParser = do+ result <- checkDir "."+ if result+ then putStrLn "\nall tests passed\n"+ else putStrLn "\nTESTS FAILED\n"+ where+ checkDir :: FilePath -> IO Bool+ checkDir dir = getDirectoryContents dir >>= mapM checkFile >>= return . and+ where+ checkFile :: FilePath -> IO Bool+ checkFile file = do+ let f = dir ++ "/" ++ file+ a <- doesDirectoryExist f+ if (a && notElem file [".", ".."])+ then checkDir f+ else if (isSuffixOf ".smt2" f)+ then do+ putStr $ "testing file " ++ f ++ " ... "+ hFlush stdout+ a <- readFile f+ let pass = checkScript a+ putStrLn (if pass then "pass" else "FAIL")+ hFlush stdout+ return pass+ else return True++ +++
+ Language/SMTLIB/Lexer.x view
@@ -0,0 +1,55 @@+{+module Language.SMTLIB.Lexer+ ( Token (..)+ , lexSMTLIB+ , alexScanTokens+ , alexAndPred+ , alexPrevCharIs+ , alexPrevCharIsOneOf+ , alexRightContext+ , iUnbox+ , alexInputPrevChar+ ) where+}++%wrapper "basic"++$digit = 0-9 -- digits+$alpha = [a-zA-Z] -- alphabetic characters+$other = [\+\-\/\*\=\%\?\!\.\$\_\~\&\^\<\>\@]+$sym = [$digit$alpha$other]+$hex = [a-fA-F$digit]+$bin = 0-1++tokens :-++ $white+ ;+ \;.* ;+ [$sym # $digit]$sym* { Symbol }+ \|[$printable \n # \|]*\| { Symbol }+ \:$sym+ { Keyword }+ $digit+\.$digit+ { Decimal . read }+ $digit { Numeral . read }+ \( { const LeftParen }+ \) { const RightParen }+ \"(([$printable \n # \\]|\\.)*)\" { String . read }+ "#x"$hex+ { Hex . drop 2 }+ "#b"$bin+ { Bin . drop 2 }+ . { \ s -> error $ "unexpected character: '" ++ s ++ "'" }++{+data Token+ = Numeral Integer+ | Decimal Double+ | Hex String+ | Bin String+ | String String+ | Symbol String+ | Keyword String+ | LeftParen+ | RightParen+ deriving (Eq,Show)++lexSMTLIB :: String -> [Token]+lexSMTLIB a = alexScanTokens a+}
+ dist/build/Language/SMTLIB/Lexer.hs view
@@ -0,0 +1,361 @@+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# LINE 1 "Language/SMTLIB/Lexer.x" #-}++module Language.SMTLIB.Lexer+ ( Token (..)+ , lexSMTLIB+ , alexScanTokens+ , alexAndPred+ , alexPrevCharIs+ , alexPrevCharIsOneOf+ , alexRightContext+ , iUnbox+ , alexInputPrevChar+ ) where++#if __GLASGOW_HASKELL__ >= 603+#include "ghcconfig.h"+#elif defined(__GLASGOW_HASKELL__)+#include "config.h"+#endif+#if __GLASGOW_HASKELL__ >= 503+import Data.Array+import Data.Char (ord)+import Data.Array.Base (unsafeAt)+#else+import Array+import Char (ord)+#endif+#if __GLASGOW_HASKELL__ >= 503+import GHC.Exts+#else+import GlaExts+#endif+{-# LINE 1 "templates/wrappers.hs" #-}+{-# LINE 1 "templates/wrappers.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/wrappers.hs" #-}+-- -----------------------------------------------------------------------------+-- Alex wrapper code.+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++{-# LINE 18 "templates/wrappers.hs" #-}++-- -----------------------------------------------------------------------------+-- The input type++{-# LINE 35 "templates/wrappers.hs" #-}++{-# LINE 51 "templates/wrappers.hs" #-}++-- -----------------------------------------------------------------------------+-- Token positions++-- `Posn' records the location of a token in the input text. It has three+-- fields: the address (number of chacaters preceding the token), line number+-- and column of a token within the file. `start_pos' gives the position of the+-- start of the file and `eof_pos' a standard encoding for the end of file.+-- `move_pos' calculates the new position after traversing a given character,+-- assuming the usual eight character tab stops.++{-# LINE 74 "templates/wrappers.hs" #-}++-- -----------------------------------------------------------------------------+-- Default monad++{-# LINE 162 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Monad (with ByteString input)++{-# LINE 251 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Basic wrapper+++type AlexInput = (Char,String)++alexGetChar (_, []) = Nothing+alexGetChar (_, c:cs) = Just (c, (c,cs))++alexInputPrevChar (c,_) = c++-- alexScanTokens :: String -> [token]+alexScanTokens str = go ('\n',str)+ where go inp@(_,str) =+ case alexScan inp 0 of+ AlexEOF -> []+ AlexError _ -> error "lexical error"+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> act (take len str) : go inp'++++-- -----------------------------------------------------------------------------+-- Basic wrapper, ByteString version++{-# LINE 297 "templates/wrappers.hs" #-}++{-# LINE 322 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Posn wrapper++-- Adds text positions to the basic model.++{-# LINE 339 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Posn wrapper, ByteString version++{-# LINE 354 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- GScan wrapper++-- For compatibility with previous versions of Alex, and because we can.++alex_base :: AlexAddr+alex_base = AlexA# "\xf8\xff\xff\xff\xff\xff\xff\xff\x04\x00\x00\x00\xfc\xff\xff\xff\xfd\xff\xff\xff\x54\x00\x00\x00\xaf\x00\x00\x00\x20\x01\x00\x00\x95\x01\x00\x00\x0a\x02\x00\x00\x68\x02\x00\x00\xc3\x02\x00\x00\xfe\x00\x00\x00\x70\x01\x00\x00\xe7\x01\x00\x00\x12\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x03\x00\x00\xa9\x03\x00\x00\x1e\x04\x00\x00\x32\x00\x00\x00\x6d\x04\x00\x00\x84\x04\x00\x00\x46\x04\x00\x00\xe2\xff\xff\xff\xe4\xff\xff\xff\x00\x00\x00\x00"#++alex_table :: AlexAddr+alex_table = AlexA# "\x00\x00\x02\x00\x01\x00\x02\x00\x02\x00\x02\x00\xff\xff\xff\xff\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x01\x00\x19\x00\x19\x00\x19\x00\x19\x00\x00\x00\x00\x00\x02\x00\x05\x00\x13\x00\x18\x00\x05\x00\x05\x00\x05\x00\x01\x00\x10\x00\x11\x00\x05\x00\x05\x00\x01\x00\x05\x00\x05\x00\x05\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0f\x00\x0b\x00\x03\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x00\x00\x12\x00\x00\x00\x05\x00\x05\x00\x00\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x00\x00\x08\x00\x06\x00\x05\x00\x00\x00\x06\x00\x06\x00\x06\x00\x00\x00\x00\x00\x00\x00\x06\x00\x06\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x15\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x00\x00\x00\x00\x00\x00\x06\x00\x06\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x00\x00\x06\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x00\x00\x00\x00\x00\x00\x06\x00\x06\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x00\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x00\x00\x00\x00\x00\x00\x06\x00\x06\x00\x00\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x06\x00\x09\x00\x00\x00\x00\x00\x06\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x07\x00\x09\x00\x09\x00\x09\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x07\x00\x09\x00\x09\x00\x09\x00\x0d\x00\x00\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x07\x00\x09\x00\x09\x00\x0a\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x14\x00\x00\x00\x0d\x00\x0a\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x14\x00\x14\x00\x12\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x15\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x14\x00\x14\x00\x12\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x15\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x14\x00\x14\x00\x12\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x15\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x00\x00\x1a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x00\x00\x00\x00\x00\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x16\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++alex_check :: AlexAddr+alex_check = AlexA# "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0a\x00\x0a\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x30\x00\x31\x00\x30\x00\x31\x00\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x20\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x20\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\x22\x00\xff\xff\x5e\x00\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\x7c\x00\x21\x00\x7e\x00\xff\xff\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\xff\xff\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x5c\x00\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\x5e\x00\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\x21\x00\xff\xff\x7e\x00\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\xff\xff\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\x5e\x00\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x0a\x00\xff\xff\xff\xff\x7e\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x0a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x0a\x00\x2e\x00\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x21\x00\xff\xff\xff\xff\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\xff\xff\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\x5e\x00\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\x21\x00\xff\xff\x7e\x00\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\xff\xff\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\x5e\x00\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x0a\x00\xff\xff\x2e\x00\x7e\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x0a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x0a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x62\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x78\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\xff\xff\xff\xff\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_deflt :: AlexAddr+alex_deflt = AlexA# "\x1b\x00\xff\xff\xff\xff\x04\x00\x04\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x14\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_accept = listArray (0::Int,27) [[],[(AlexAccSkip)],[(AlexAccSkip)],[(AlexAccSkip)],[(AlexAccSkip)],[(AlexAcc (alex_action_2))],[(AlexAcc (alex_action_2))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_12))],[],[(AlexAcc (alex_action_4))],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_5))],[],[],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_7))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_9))],[(AlexAcc (alex_action_12))],[],[],[(AlexAcc (alex_action_10))],[],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_11))],[],[(AlexAcc (alex_action_12))]]+{-# LINE 40 "Language/SMTLIB/Lexer.x" #-}++data Token+ = Numeral Integer+ | Decimal Double+ | Hex String+ | Bin String+ | String String+ | Symbol String+ | Keyword String+ | LeftParen+ | RightParen+ deriving (Eq,Show)++lexSMTLIB :: String -> [Token]+lexSMTLIB a = alexScanTokens a++alex_action_2 = Symbol +alex_action_3 = Symbol +alex_action_4 = Keyword +alex_action_5 = Decimal . read +alex_action_6 = Numeral . read +alex_action_7 = const LeftParen +alex_action_8 = const RightParen +alex_action_9 = String . read +alex_action_10 = Hex . drop 2 +alex_action_11 = Bin . drop 2 +alex_action_12 = \ s -> error $ "unexpected character: '" ++ s ++ "'" +{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- -----------------------------------------------------------------------------+-- ALEX TEMPLATE+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++-- -----------------------------------------------------------------------------+-- INTERNALS and main scanner engine++{-# LINE 37 "templates/GenericTemplate.hs" #-}++{-# LINE 47 "templates/GenericTemplate.hs" #-}+++data AlexAddr = AlexA# Addr#++#if __GLASGOW_HASKELL__ < 503+uncheckedShiftL# = shiftL#+#endif++{-# INLINE alexIndexInt16OffAddr #-}+alexIndexInt16OffAddr (AlexA# arr) off =+#ifdef WORDS_BIGENDIAN+ narrow16Int# i+ where+ i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+ high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ low = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 2#+#else+ indexInt16OffAddr# arr off+#endif++++++{-# INLINE alexIndexInt32OffAddr #-}+alexIndexInt32OffAddr (AlexA# arr) off = +#ifdef WORDS_BIGENDIAN+ narrow32Int# i+ where+ i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`+ (b2 `uncheckedShiftL#` 16#) `or#`+ (b1 `uncheckedShiftL#` 8#) `or#` b0)+ b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))+ b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))+ b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ b0 = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 4#+#else+ indexInt32OffAddr# arr off+#endif++++++#if __GLASGOW_HASKELL__ < 503+quickIndex arr i = arr ! i+#else+-- GHC >= 503, unsafeAt is available from Data.Array.Base.+quickIndex = unsafeAt+#endif+++++-- -----------------------------------------------------------------------------+-- Main lexing routines++data AlexReturn a+ = AlexEOF+ | AlexError !AlexInput+ | AlexSkip !AlexInput !Int+ | AlexToken !AlexInput !Int a++-- alexScan :: AlexInput -> StartCode -> AlexReturn a+alexScan input (I# (sc))+ = alexScanUser undefined input (I# (sc))++alexScanUser user input (I# (sc))+ = case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, input') ->+ case alexGetChar input of+ Nothing -> ++++ AlexEOF+ Just _ ->++++ AlexError input'++ (AlexLastSkip input'' len, _) ->++++ AlexSkip input'' len++ (AlexLastAcc k input''' len, _) ->++++ AlexToken input''' len k+++-- Push the input through the DFA, remembering the most recent accepting+-- state it encountered.++alex_scan_tkn user orig_input len input s last_acc =+ input `seq` -- strict in the input+ let + new_acc = check_accs (alex_accept `quickIndex` (I# (s)))+ in+ new_acc `seq`+ case alexGetChar input of+ Nothing -> (new_acc, input)+ Just (c, new_input) -> ++++ let+ !(base) = alexIndexInt32OffAddr alex_base s+ !((I# (ord_c))) = ord c+ !(offset) = (base +# ord_c)+ !(check) = alexIndexInt16OffAddr alex_check offset+ + !(new_s) = if (offset >=# 0#) && (check ==# ord_c)+ then alexIndexInt16OffAddr alex_table offset+ else alexIndexInt16OffAddr alex_deflt s+ in+ case new_s of + -1# -> (new_acc, input)+ -- on an error, we want to keep the input *before* the+ -- character that failed, not after.+ _ -> alex_scan_tkn user orig_input (len +# 1#) + new_input new_s new_acc++ where+ check_accs [] = last_acc+ check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))+ check_accs (AlexAccPred a predx : rest)+ | predx user orig_input (I# (len)) input+ = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkipPred predx : rest)+ | predx user orig_input (I# (len)) input+ = AlexLastSkip input (I# (len))+ check_accs (_ : rest) = check_accs rest++data AlexLastAcc a+ = AlexNone+ | AlexLastAcc a !AlexInput !Int+ | AlexLastSkip !AlexInput !Int++data AlexAcc a user+ = AlexAcc a+ | AlexAccSkip+ | AlexAccPred a (AlexAccPred user)+ | AlexAccSkipPred (AlexAccPred user)++type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool++-- -----------------------------------------------------------------------------+-- Predicates on a rule++alexAndPred p1 p2 user in1 len in2+ = p1 user in1 len in2 && p2 user in1 len in2++--alexPrevCharIsPred :: Char -> AlexAccPred _ +alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input++--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ +alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input++--alexRightContext :: Int -> AlexAccPred _+alexRightContext (I# (sc)) user _ _ input = + case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, _) -> False+ _ -> True+ -- TODO: there's no need to find the longest+ -- match when checking the right context, just+ -- the first match will do.++-- used by wrappers+iUnbox (I# (i)) = i
smt-lib.cabal view
@@ -1,12 +1,12 @@ name: smt-lib-version: 0.0.0+version: 0.0.1 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.+ SMT-LIB 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>@@ -23,16 +23,15 @@ library build-depends: base >= 4.0 && < 5.0,+ directory >= 1.0 && < 1.1,+ array >= 0.3 && < 0.4, polyparse >= 1.4 exposed-modules: Language.SMTLIB---- extensions:+ Language.SMTLIB.Lexer - if impl(ghc > 6.8)- ghc-options: -fwarn-tabs- ghc-options: -W+ ghc-options: -W source-repository head type: git