|
definition:
|
verifyVarExpr :: TermDomain a => Int -> Expr -> VerifyStateM a (VarTypesMap a)
verifyVarExpr ve exp = case exp of
Var v -> if v == ve
then return []
else do
--lift $ printInfoLine $
-- "Expression with different vars: " ++ show (v,ve)
--showVarExpTypes
vtypes <- getVarTypeOf v
-- TODO: improve by handling equality constraint v==ve
-- instead of copying the current types for v to ve:
return $ [(ve, vtypes)]
Lit l -> return [(ve, [(IOT [([], aLit l)], [])])]
Comb ct qf es -> checkPredefinedOp exp $ do
vs <- if isEncSearchOp qf
then -- for encapsulated search, failures in arguments are hidden
mapM (verifyExpr False) es
else if isSetFunOp qf
then -- for a set function, the function argument is hidden
mapM (\ (i,e) -> verifyExpr (i>0) e)
(zip [0..] es)
else mapM (verifyExpr True) es
case ct of
FuncCall -> do verifyFuncCall exp qf vs
ftype <- getFuncType qf (length vs)
return [(ve, [(ftype, vs)])]
FuncPartCall n -> -- note: also partial calls are considered as constr.
do ctype <- getCallType qf (n + length es)
unless (isTotalACallType ctype) $ do
printIfVerb 3 $ "UNSATISFIED ABSTRACT CALL TYPE: " ++
"partial application of non-total function\n"
addFailedFunc exp Nothing fcTrue
-- note: also partial calls are considered as constructors
returnConsIOType qf vs ve
_ -> returnConsIOType qf vs ve
Let bs e -> do addVarExps (map (\(v,be) -> (v, unknownType, be)) bs)
mapM_ (addVarAnyType . fst) bs
iotss <- mapM (\ (v,be) -> verifyVarExpr v be) bs
-- remove initially set anyType's for the bound vars:
mapM_ (removeVarAnyType . fst) bs
addVarTypes (concat iotss)
mapM_ (addAnyTypeIfUnknown . fst) bs
verifyVarExpr ve e
Free vs e -> do addVarExps (map (\v -> (v, unknownType, Var v)) vs)
mapM_ addVarAnyType vs
verifyVarExpr ve e
Or e1 e2 -> do iots1 <- verifyVarExpr ve e1 --
iots2 <- verifyVarExpr ve e2
return (concVarTypesMap iots1 iots2)
Case _ ce bs -> do cv <- verifyExpr True ce
verifyMissingBranches exp cv bs
iotss <- mapM (verifyBranch cv ve) bs
return (foldr concVarTypesMap [] iotss)
Typed e _ -> verifyVarExpr ve e -- TODO: use type info
where
-- adds Any type for a variable if it is unknown
addAnyTypeIfUnknown v = do
vts <- getVarTypeOf v
when (null vts) (addVarAnyType v)
-- Return an input/output type for a constructor and its arguments
returnConsIOType qc vs rv = do
vts <- getVarTypes
let vstypes = map (flip getVarType vts) vs
--let anys = anyTypes (length vs) -- TODO: use vs types from VarTypes!!!!
--return [(rv, IOT [(anys, aCons qc anys)], vs)]
return [(rv, [(IOT [(vstypes, aCons qc vstypes)], vs)])]
|