diff --git a/Language/SMTLIB.hs b/Language/SMTLIB.hs --- a/Language/SMTLIB.hs +++ b/Language/SMTLIB.hs @@ -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 + + + + + diff --git a/Language/SMTLIB/Lexer.x b/Language/SMTLIB/Lexer.x new file mode 100644 --- /dev/null +++ b/Language/SMTLIB/Lexer.x @@ -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 +} diff --git a/dist/build/Language/SMTLIB/Lexer.hs b/dist/build/Language/SMTLIB/Lexer.hs new file mode 100644 --- /dev/null +++ b/dist/build/Language/SMTLIB/Lexer.hs @@ -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 "" #-} +{-# LINE 1 "" #-} +{-# 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 "" #-} +{-# LINE 1 "" #-} +{-# 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 diff --git a/smt-lib.cabal b/smt-lib.cabal --- a/smt-lib.cabal +++ b/smt-lib.cabal @@ -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 @@ -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