|
definition:
|
verifyBranch :: TermDomain a => Int -> Int -> BranchExpr
-> VerifyStateM a (VarTypesMap a)
verifyBranch casevar ve (Branch (LPattern l) e) = do
bstate <- getBranchState
vts <- getVarTypes
let branchvartypes = bindVarInIOTypes casevar (aLit l) vts
printIfVerb 4 $ "BRANCH WITH LITERAL '" ++ show l ++ "'"
addEquVarCondition casevar (Lit l)
if isEmptyType (getVarType casevar branchvartypes)
then return [] -- unreachable branch
else do setVarTypes branchvartypes
iots <- verifyVarExpr ve e
restoreBranchState bstate
return iots
verifyBranch casevar ve (Branch (Pattern qc vs) e) = do
bstate <- getBranchState
ves <- getVarExps
consinfos <- getConsInfos
let vet = maybe unknownType snd3 (find ((== casevar) . fst3) ves)
addVarExps (map (\ (v,vt) -> (v, vt, Var v))
(zip vs (if vet == unknownType
then repeat unknownType
else patArgTypes consinfos vet)))
vts <- getVarTypes
let pattype = aCons qc (anyTypes (length vs))
branchvartypes = simplifyVarTypes (bindVarInIOTypes casevar pattype vts)
casevartype = getVarType casevar branchvartypes
-- add single case for case variable and pattern to the current condition:
if null vs then addEquVarCondition casevar (Comb ConsCall qc [])
else addSingleCase casevar qc vs
printIfVerb 4 $ "BRANCH WITH CONSTRUCTOR '" ++ snd qc ++ "'"
showVarExpTypes
if isEmptyType casevartype
then do restoreBranchState bstate
return [] -- unreachable branch
else do setVarTypes branchvartypes
mapM_ (\(v,t) -> addVarType v (ioVarType t))
(zip vs (argTypesOfCons qc (length vs) casevartype))
iots <- verifyVarExpr ve e
restoreBranchState bstate
return iots
where
-- compute the argument types from the result type `pt` of the branch variable
-- where some regularly occurring constructors are directly implemented
patArgTypes consinfos pt
| qc == pre ":"
= case pt of TCons tc [et] | tc == pre "[]" -> [et, pt]
_ -> noPatTypeErr
| qc == pre "(,)"
= case pt of TCons tc [t1,t2] | tc == pre "(,)" -> [t1,t2]
_ -> noPatTypeErr
| qc == pre "Just"
= case pt of TCons tc [t] | tc == pre "Maybe" -> [t]
_ -> noPatTypeErr
| otherwise
= maybe (error $ "Info about constructor '" ++ snd qc ++ "' not found!")
(\(_,ConsType tes tc tvs,_) ->
case pt of
TCons dtc ats | tc == dtc -> map (applyTSubst (zip tvs ats)) tes
_ -> noPatTypeErr
)
(lookup qc consinfos)
noPatTypeErr = error $
"verifyBranch: cannot compute pattern argument types for " ++ snd qc
|