|
definition:
|
addSingleCase :: TermDomain a => Int -> QName -> [Int] -> VerifyStateM a ()
addSingleCase casevar qc branchvars = do
st <- get
let siblings = siblingsOfCons (vstConsInfos st) qc
catchbranch = if null siblings then []
else [Branch (Pattern anonCons []) fcFalse]
put $ st { vstCondition =
\c -> (vstCondition st)
(Case Rigid (Var casevar)
([Branch (Pattern qc branchvars) c] ++ catchbranch)) }
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Adds to the current condition an equality between a variable and
-- a constructor applied to a list of fresh pattern variables.
-- This condition is expressed as a case expression where
-- the hole of the current condition is in the branch for the given
-- constructor and all alternative branches return a `False` value.
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
name:
|
addSingleCase
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Analysis.TermDomain.TermDomain a => Prelude.Int -> (String, String)
-> [Prelude.Int]
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO ()
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|