module Main where import Data.List (intercalate) import qualified Data.Map.Strict as Map import Data.Time.Clock (diffUTCTime, getCurrentTime) import Tessera.Check (checkProgram) import Tessera.Env import Tessera.Eval import Tessera.Matrix (witness, Outcome (..)) import Tessera.Parser (parseProgram) import Tessera.Syntax import Tessera.Tree main :: IO () main = do putStrLn "strategy,nodes,depth,witness_ms" mapM_ runSize [4, 6, 8, 10] runSize :: Int -> IO () runSize size = do let source = declaration size program = either (error . show) id (parseProgram source) env = either (error . show) id (checkProgram program) match' = head [m | m@(MatchDeclaration _ _ _ _) <- program] clauses = matchClauses match' rows = zip (map clausePatterns clauses) [0 .. length clauses - 1] types = map snd (matchArgumentsOf match') leftmost = compileMatch env Leftmost types rows (initialOccurrences (length types)) heuristic = compileMatch env Heuristic types rows (initialOccurrences (length types)) start <- getCurrentTime let outcome = witness env 2000 types (map clausePatterns clauses) end <- getCurrentTime putStrLn (intercalate "," [ "leftmost", show (treeSize leftmost), show (treeDepth leftmost), show (diffUTCTime end start)]) putStrLn (intercalate "," [ "heuristic", show (treeSize heuristic), show (treeDepth heuristic), show (diffUTCTime end start)]) putStrLn (intercalate "," [ "outcome", show (outcome == Covered), "", ""]) matchArgumentsOf :: Declaration -> [(String, Type)] matchArgumentsOf (MatchDeclaration _ arguments _ _) = arguments matchArgumentsOf _ = [] declaration :: Int -> String declaration size = let constructors = intercalate " | " ["C" ++ show i ++ " Int" | i <- [1 .. size]] patterns = concat [" | C" ++ show i ++ " n -> n\n" | i <- [1 .. size]] in "data T = " ++ constructors ++ "\n\nmatch classify (t : T) : Int =\n" ++ patterns