47 lines
1.9 KiB
Haskell
47 lines
1.9 KiB
Haskell
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
|