From e02c5b355984328114e9b7bbe41da8937b879396 Mon Sep 17 00:00:00 2001
From: sneeker <s@cpl0.zip>
Date: Wed, 5 Feb 2020 12:00:00 +0000
Subject: [PATCH] specialise matrices by constructors and default cases

---
 src/Tessera/Analyze.hs | 109 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)
 create mode 100644 src/Tessera/Analyze.hs

diff --git a/src/Tessera/Analyze.hs b/src/Tessera/Analyze.hs
new file mode 100644
index 0000000..940655f
--- /dev/null
+++ b/src/Tessera/Analyze.hs
@@ -0,0 +1,109 @@
+module Tessera.Analyze where
+
+import qualified Data.Map.Strict as Map
+
+import Tessera.Env
+import Tessera.Eval (Value (..), sourceSelect)
+import Tessera.Matrix
+import Tessera.Syntax
+
+data ClauseStatus
+  = ClauseUseful
+  | ClauseRedundant
+  deriving (Eq, Show)
+
+data ClauseReport = ClauseReport
+  { reportClauseIndex :: Int
+  , reportClauseStatus :: ClauseStatus
+  , reportClauseExample :: Maybe [Value]
+  } deriving (Eq, Show)
+
+data MatchReport = MatchReport
+  { reportMatchName :: String
+  , reportExhaustive :: Bool
+  , reportInconclusive :: Bool
+  , reportMissingCase :: Maybe [Value]
+  , reportClauseReports :: [ClauseReport]
+  , reportInhabitedTypes :: Map.Map String Bool
+  } deriving (Eq, Show)
+
+analysisBudget :: Int
+analysisBudget = 500
+
+analyzeMatch :: Env -> Declaration -> Maybe MatchReport
+analyzeMatch env (MatchDeclaration name arguments _ clauses) =
+  let types = map snd arguments
+      matrixAll = map clausePatterns clauses
+      outcome = witness env analysisBudget types matrixAll
+      missing = case outcome of
+        NotCovered patterns -> witnessValues patterns
+        Covered -> Nothing
+        SearchExhausted -> Nothing
+      inconclusive = case outcome of
+        SearchExhausted -> True
+        NotCovered patterns -> witnessValues patterns == Nothing
+        Covered -> False
+      clauseReports = [ analyzeClause env types index clauses | index <- [0 .. length clauses - 1] ]
+  in Just MatchReport
+      { reportMatchName = name
+      , reportExhaustive = outcome == Covered
+      , reportInconclusive = inconclusive
+      , reportMissingCase = missing
+      , reportClauseReports = clauseReports
+      , reportInhabitedTypes = finiteInhabitants env
+      }
+analyzeMatch _ _ = Nothing
+
+analyzeClause :: Env -> [Type] -> Int -> [Clause] -> ClauseReport
+analyzeClause env types index clauses =
+  let previous = map clausePatterns (take index clauses)
+      current = clausePatterns (clauses !! index)
+      isUseful = useful env types previous current
+      example = if isUseful then exampleForClause env types index clauses else Nothing
+  in ClauseReport
+      { reportClauseIndex = index
+      , reportClauseStatus = if isUseful then ClauseUseful else ClauseRedundant
+      , reportClauseExample = example
+      }
+
+exampleForClause :: Env -> [Type] -> Int -> [Clause] -> Maybe [Value]
+exampleForClause env types index clauses = case drop index clauses of
+  (clause : _) ->
+    let filled = sequence (zipWith (fillPattern env 8) types (clausePatterns clause))
+        candidate = filled >>= \patterns -> sequence (map patternValue patterns)
+    in case candidate of
+        Nothing -> Nothing
+        Just values -> case sourceSelect (map clausePatterns clauses) values of
+          Just selected | selected == index -> Just values
+          _ -> Nothing
+  [] -> Nothing
+
+fillPattern :: Env -> Int -> Type -> Pattern -> Maybe Pattern
+fillPattern env depth ty pattern' = case pattern' of
+  PVar _ -> Just (sample env depth ty)
+  PWild -> Just (sample env depth ty)
+  PInt _ -> Just pattern'
+  PBool _ -> Just pattern'
+  PTuple patterns -> case ty of
+    TTuple types -> PTuple <$> sequence (zipWith (fillPattern env (depth - 1)) types patterns)
+    _ -> Nothing
+  PCon name patterns -> case signature env ty of
+    FiniteSignature constructors -> case lookup (KeyCon name) constructors of
+      Just argumentTypes -> PCon name <$> sequence (zipWith (fillPattern env (depth - 1)) argumentTypes patterns)
+      Nothing -> Nothing
+    IntegerSignature -> Nothing
+
+patternValue :: Pattern -> Maybe Value
+patternValue pattern' = case pattern' of
+  PInt n -> Just (VInt n)
+  PBool b -> Just (VBool b)
+  PCon name arguments -> VCon name <$> mapM patternValue arguments
+  PTuple elements -> VTuple <$> mapM patternValue elements
+  PVar _ -> Nothing
+  PWild -> Nothing
+
+witnessValues :: [Pattern] -> Maybe [Value]
+witnessValues = sequence . map patternValue
+
+validateWitness :: [Clause] -> [Value] -> Bool
+validateWitness clauses values = sourceSelect (map clausePatterns clauses) values == Nothing