|
sourcecode:
|
module Verify.WithSMT
where
import Control.Monad ( unless, when )
import Data.Either ( partitionEithers, rights )
import Data.IORef
import Data.List ( (\\), find, init, isPrefixOf, last, maximum, nub
, partition, union )
import Data.Maybe ( catMaybes, fromMaybe, isJust )
import Numeric ( readHex )
import System.CPUTime ( getCPUTime )
import System.Directory ( doesFileExist )
import Debug.Trace
import Control.Monad.Trans.State
import Data.Tuple.Extra ( both )
import FlatCurry.AddTypes
import FlatCurry.Build
import FlatCurry.Goodies
import FlatCurry.Names
import FlatCurry.Print
import FlatCurry.Simplify
import FlatCurry.Types as FC
import System.FilePath ( (</>) )
import System.IOExts ( evalCmd )
import Text.Pretty ( pPrint, pretty, text )
import Verify.ESMT as SMT
import Verify.Helpers
import Verify.Options
import Verify.ProgInfo
import PackageConfig ( getPackagePath )
------------------------------------------------------------------------------
-- Calls the SMT solver to check whether an assertion implies some
-- property (represented as FlatCurry expressions).
-- If the implication is `False`, the unsatisfiability of the assertion
-- is checked.
-- `Nothing` is returned if there is some error w.r.t. SMT solving.
checkUnsatisfiabilityWithSMT :: Options -> QName -> String -> IORef ProgInfo
-> [(QName,ConsInfo)] -> [(Int,TypeExpr)] -> Expr -> IO (Maybe Bool)
checkUnsatisfiabilityWithSMT opts qf scripttitle pistore consinfos
vartypes assertionexp0 = do
let assertionexp = wrapCaseWithId assertionexp0
(cnames,fnames) = both nub
(partitionEithers (allQNamesInExp assertionexp))
cnamesreq = filter (`notElem` [pre "False", pre "True", anonCons]) cnames
--printInfoLine $ "ASSERTION EXPRESSION: " ++ showExp assertionexp
--printInfoLine $ "NAMES IN ASSERTION: " ++ show (cnamesreq ++ fnames)
loadModulesForQNames opts pistore (cnamesreq ++ fnames)
pinfos <- fmap progInfos $ readIORef pistore
let typedassertion = addTypes2VarExp pinfos vartypes assertionexp fcBool
--printInfoLine $ "TYPED ASSERTION EXPRESSION: " ++ showExp typedassertion
let foassertexp = replaceHigherOrderInExp (simpExpr typedassertion)
foassertfuncs = rights (allQNamesInExp foassertexp)
--printInfoLine $ "SIMPLE TYPED ASSERTION EXPRESSION: " ++ showExp foassertexp
maybe
(transExpError typedassertion)
(\ (assertion,varsorts) ->
catch (checkUnsatWithSMT opts qf scripttitle pistore consinfos vartypes
varsorts assertion cnamesreq foassertfuncs)
(\e -> print e >> return Nothing))
(exp2SMTWithVars (maximum (0 : map fst vartypes))
Nothing foassertexp)
where
transExpError e = do printInfoLine $ "Cannot translate expression:\n" ++ showExp e
return Nothing
-- Wrap all case arguments with the identity operation.
-- This is a work-around to fix a problem with pattern matching
-- w.r.t. algebraic data types occurring in Z3 version 4.13.0
-- (see example Z3BUG/match-error.smt).
wrapCaseWithId =
updCases (\ct e brs -> Case ct (Comb FuncCall (pre "id") [e]) brs)
checkUnsatWithSMT :: Options -> QName -> String -> IORef ProgInfo
-> [(QName,ConsInfo)]
-> [(Int,TypeExpr)] -> [(Int,Sort)]
-> Term -> [QName] -> [QName] -> IO (Maybe Bool)
checkUnsatWithSMT opts qf title pistore consinfos vartypes
extravars -- variables representing h.o. subexps
assertion -- assertion to be checked
assertioncons -- constructors occurring in the assertion
assertfuncs = -- defined functions occurring in assertion
flip catch (\e -> print e >> return Nothing) $ do
--let allsyms = nub (catMaybes
-- (map (\n -> maybe Nothing Just (untransOpName n))
-- (map qidName (allQIdsOfTerm assertion))))
unless (null assertfuncs) $ printWhenDetails opts $
"Translating operations into SMT: " ++ unwords (map showQName assertfuncs)
fdecls0 <- getAllFunctions opts pistore assertfuncs
pinfos <- fmap progInfos $ readIORef pistore
let fdecls1 = addTypes2FuncDecls pinfos
(map (completeBranchesInFunc consinfos True) fdecls0)
-- reduce to functions reachable from assertion after eliminating h.o.:
fdecls = usedFunctions assertfuncs
(map (updFuncBody replaceHigherOrderInExp) fdecls1)
--printInfoLine $ "OPERATIONS TO BE TRANSLATED:\n" ++ unlines (map showFuncDecl fdecls)
let smtfuncs = maybe (Comment $ "ERROR translating " ++
show (map funcName fdecls))
(\fds -> DefineSigsRec fds)
(mapM fun2SMT fdecls)
fdecltvars = nub (concatMap allTVarsInFuncDecl fdecls)
--printInfoLine $ "TRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
--let title1 = title ++ "\nTRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
let vartypestcons = foldr union [] (map (tconsOfTypeExpr . snd) vartypes)
funcstcons = foldr union [] (map (tconsOfTypeExpr . funcType) fdecls)
asserttcons = map (\(ConsType _ tc _) -> tc)
(map (snd3 . infoOfCons consinfos) assertioncons)
(primtypes,usertypes) =
partition ((== "Prelude") . fst)
(union funcstcons (union vartypestcons asserttcons))
decls <- mapM (getTypeDeclOf pistore) usertypes
-- collect all type parameters in order to declare them as sorts:
let tvarsInVars = foldr union []
(map (typeParamsOfSort . type2sort)
(map snd vartypes ++ map TVar fdecltvars))
varsorts = map (\(i,te) -> (i, type2sort te)) vartypes ++ extravars
--printInfoLine $ "Assertion: " ++ pPrint (pretty assertion)
let smt = concatMap preludeType2SMT (map snd primtypes) ++
[ EmptyLine ] ++
(if null decls
then []
else [ Comment "User-defined datatypes:" ] ++
map tdecl2SMT decls) ++
(if null tvarsInVars
then []
else [ EmptyLine, Comment "Polymorphic sorts:" ] ++
map (\tv -> DeclareSort tv 0) tvarsInVars) ++
[ EmptyLine, smtfuncs, EmptyLine
, Comment "Free variables:" ] ++
map (\(i,s) -> DeclareVar (SV i s)) varsorts ++
[ EmptyLine
, Comment "Boolean formula of assertion (known properties):"
, sAssert assertion, EmptyLine
, Comment "check satisfiability:"
, CheckSat
]
--printInfoLine $ "SMT commands as Curry term:\n" ++ show smt
let preludesmt = if all ((`elem` defaultSMTTypes) . snd) primtypes
then "Prelude_min.smt"
else "Prelude.smt"
smtprelude <- readIncludeFile preludesmt
let scripttitle = unlines (map ("; "++) (lines title))
printWhenAll opts $
"RAW SMT SCRIPT:\n" ++ scripttitle ++ "\n\n" ++ showSMTRaw smt
let smtinput = scripttitle ++ "\n" ++ smtprelude ++ showSMT smt
printWhenDetails opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
let z3opts = ["-smt2", "-T:2"]
when (optStoreSMT opts) (storeSMT "SMT-" z3opts smtinput >> return ())
printWhenDetails opts $
"CALLING Z3 (with options: " ++ unwords z3opts ++ ")..."
(ecode,out,err) <- evalCmd "z3" ("-in" : z3opts) smtinput
when (ecode > 0) $ do
printWhenStatus opts $ "EXIT CODE: " ++ show ecode
outfile <- storeSMT "smterror-" z3opts smtinput
when (optVerb opts < 3) $ printWhenStatus opts $
"ERROR in SMT script (saved in '" ++ outfile ++ "'):\n" ++
out ++ "\n" ++ err
printWhenDetails opts $ "RESULT:\n" ++ out
unless (null err) $ printWhenDetails opts $ "ERROR:\n" ++ err
let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat"
return (if ecode>0 then Nothing else Just pcvalid)
where
defaultSMTTypes = ["Int","Float","Bool", "Char", "[]"]
storeSMT fileprefix z3opts script = do
ctime <- getCPUTime
let outfile = fileprefix ++ transOpName qf ++ "-" ++ show ctime ++ ".smt"
execcmt = unwords $ ["; Run with: z3"] ++ z3opts ++ [outfile]
writeFile outfile (execcmt ++ "\n\n" ++ script)
return outfile
--- Try to read a file in the `include` directory of the package
-- or, if this does not exists, in a local `include` directory.
readIncludeFile :: String -> IO String
readIncludeFile incfile = do
ppinclude <- fmap (</> "include" </> incfile) getPackagePath
exppinclude <- doesFileExist ppinclude
if exppinclude
then readFile ppinclude
else do
let localinclude = "include" </> incfile
exlocalinclude <- doesFileExist localinclude
if exlocalinclude
then readFile localinclude
else do printInfoLine $
"Warning: " ++ localinclude ++ " not found!\n" ++
"SMT script might be incomplete!"
return ""
-- Translate a typed variable into an SMT declaration:
typedVar2SMT :: (Int,TypeExpr) -> Command
typedVar2SMT (i,te) = DeclareVar (SV i (type2sort te))
-- Gets all type constructors occurring in a type expression.
tconsOfTypeExpr :: TypeExpr -> [QName]
tconsOfTypeExpr (TVar _) = []
tconsOfTypeExpr (FuncType a b) = union (tconsOfTypeExpr a) (tconsOfTypeExpr b)
tconsOfTypeExpr (TCons qName texps) =
foldr union [qName] (map tconsOfTypeExpr texps)
tconsOfTypeExpr (ForallType _ te) = tconsOfTypeExpr te
------------------------------------------------------------------------------
-- Get all qualified names occurring in an expression which are either
-- constructor or defined function names.
allQNamesInExp :: Expr -> [Either QName QName]
allQNamesInExp e =
trExpr (const id) (const id) comb lt fr (.) cas branch const e []
where
comb ct qn exp = ((classifyName ct) qn:) . foldr (.) id exp
where classifyName FuncCall = Right
classifyName (FuncPartCall _) = Right
classifyName ConsCall = Left
classifyName (ConsPartCall _) = Left
lt bs exp = exp . foldr (.) id (map snd bs)
fr _ exp = exp
cas _ exp bs = exp . foldr (.) id bs
branch pat exp = ((args pat)++) . exp
args (Pattern qc _) = [Left qc]
args (LPattern _) = []
------------------------------------------------------------------------------
--- Shows a text with line numbers prefixed:
showWithLineNums :: String -> String
showWithLineNums txt =
let txtlines = lines txt
maxlog = ilog (length txtlines + 1)
showNum n = (take (maxlog - ilog n) (repeat ' ')) ++ show n ++ ": "
in unlines . map (uncurry (++)) . zip (map showNum [1..]) $ txtlines
--- The value of `ilog n` is the floor of the logarithm
--- in the base 10 of `n`.
--- Fails if `n <= 0`.
--- For positive integers, the returned value is
--- 1 less the number of digits in the decimal representation of `n`.
---
--- @param n - The argument.
--- @return the floor of the logarithm in the base 10 of `n`.
ilog :: Int -> Int
ilog n | n>0 = if n<10 then 0 else 1 + ilog (n `div` 10)
---------------------------------------------------------------------------
--- Translates a type declaration into an SMT datatype declaration.
tdecl2SMT :: TypeDecl -> Command
tdecl2SMT (TypeSyn tc _ _ _) =
error $ "Cannot translate type synonym '" ++ showQName tc ++ "' into SMT!"
tdecl2SMT (TypeNew tc _ _ _) =
error $ "Cannot translate newtype '" ++ showQName tc ++ "' into SMT!"
tdecl2SMT (Type tc _ tvars consdecls) =
DeclareDatatypes
[(tcons2SMT tc, length tvars,
DT (map (\ (v,_) -> 'T' : show v) tvars) (map tconsdecl consdecls))]
where
tconsdecl (Cons qn _ _ texps) =
let cname = transOpName qn
in DCons cname (map (texp2sel qn) (zip [1..] texps))
texp2sel cname (i,texp) = (genSelName cname i, type2sortD True texp)
--- Generates the name of the i-th selector for a given constructor.
genSelName :: QName -> Int -> String
genSelName qc@(mn,fn) i
| mn == "Prelude" && take 3 fn == "(,,"
= transOpName qc ++ "_" ++ show i
| otherwise
= "sel" ++ show i ++ '-' : transOpName qc
--- Translates a prelude type into an SMT datatype declaration,
--- if necessary.
preludeType2SMT :: String -> [Command]
preludeType2SMT tn
| take 3 tn == "(,,"
= let arity = length tn -1
in [ Comment "Declaration of tuple type:"
, DeclareDatatypes
[(tcons2SMT (pre tn), arity,
DT (map (\v -> 'T' : show v) [1 .. arity])
[DCons (transOpName (pre tn)) (map texp2sel [1 .. arity])])]]
| otherwise
= []
where
texp2sel i = (genSelName (pre tn) i, SComb ('T' : show i) [])
---------------------------------------------------------------------------
-- Translates a function declaration into a (possibly polymorphic)
-- SMT function declaration.
fun2SMT :: FuncDecl -> Maybe ([Ident],FunSig,Term)
fun2SMT (Func qn _ _ texp rule) = do
let fsig = FunSig (transOpName qn)
(map type2sort (argTypes texp))
(type2sort (resultType texp))
srule <- rule2SMT rule
let tpars = union (typeParamsOfFunSig fsig) (typeParamsOfTerm srule)
return (tpars, fsig, srule)
where
rule2SMT (External s) = return $
tEqu (tComb (transOpName qn) []) (tComb ("External:" ++ s) [])
rule2SMT (Rule vs exp) = do
let isnd = ndExpr exp
lhs = tComb (transOpName qn) (map TSVar vs)
(rhs,varsorts) <- exp2SMTWithVars (maximum (0:vs))
(if isnd then Just lhs else Nothing)
(simpExpr exp)
return $
Forall (map (\ (v,t) -> SV v (type2sort t))
(funcType2TypedVars vs texp))
(Exists (map (\ (v,s) -> SV v s) varsorts)
(if isnd then rhs else tEqu lhs rhs))
--- Returns `True` if the expression is non-deterministic,
--- i.e., if `Or` or `Free` occurs in the expression.
ndExpr :: Expr -> Bool
ndExpr = trExpr (\_ -> False)
(\_ -> False)
(\_ _ nds -> or nds)
(\bs nd -> nd || any snd bs)
(\_ _ -> True)
(\_ _ -> True)
(\_ nd bs -> nd || or bs)
(\_ -> id)
(\nd _ -> nd)
-- Replace higher-order features, like occurrences of `Prelude.apply` and
-- partial applications, by `Prelude.failed` in an expression since they
-- cannot be handled by SMT. Later, occurrences of `Prelude.failed` in
-- SMT terms are replaced by fresh variables so that they are unspecified
-- values.
replaceHigherOrderInExp :: Expr -> Expr
replaceHigherOrderInExp =
trExpr Var Lit updComb FC.Let Free Or Case Branch Typed
where
updComb ct qn args = case ct of
FuncPartCall _ -> fcFailed
ConsPartCall _ -> fcFailed
FuncCall | qn == pre "apply" -> fcFailed
_ -> Comb ct qn args
-- Translates a (Boolean) FlatCurry expression into an SMT expression.
-- If the second argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
-- If successful, the translated SMT expression together with new variables
-- (which are replacements for higher-order applications) are returned.
-- The first argument is the maximum index of already used variables.
exp2SMTWithVars :: Int -> Maybe Term -> Expr -> Maybe (Term, [(Int,Sort)])
exp2SMTWithVars maxusedvar lhs exp =
maybe Nothing
(\t -> Just $ elimFailed maxusedvar t)
(exp2SMT lhs (replaceHigherOrderInExp exp))
-- Translates a (Boolean) FlatCurry expression into an SMT expression.
-- If the first argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
exp2SMT :: Maybe Term -> Expr -> Maybe Term
exp2SMT lhs exp = case exp of
Var i -> Just $ makeRHS (TSVar i)
Lit l -> Just $ makeRHS (lit2SMT l)
Comb _ qf args -> mapM (exp2SMT Nothing) args >>= comb2SMT qf
Case _ e bs -> do t <- exp2SMT Nothing e
bts <- mapM branch2SMT bs
return $ makeRHS (Match t bts)
FC.Let bs e -> do tbs <- mapM (\(v,be) -> do t <- exp2SMT Nothing be
return (v,t))
bs
t <- exp2SMT lhs e
return $ tLet tbs t
Free _ _ -> Nothing --error "exp2SMT: Free"
Typed e te -> case e of
Comb _ qf args | all isTyped args
-> mapM (exp2SMT Nothing) args >>=
return . makeRHS .
TComb (As (transOpName qf)
(type2sort (foldr FuncType te (map exprType args))))
_ -> exp2SMT lhs e
Or e1 e2 -> do t1 <- exp2SMT lhs e1
t2 <- exp2SMT lhs e2
return $ tDisj [t1,t2]
where
comb2SMT qf targs
| qf `elem` map pre ["chr", "ord"] && length targs == 1
= return $ makeRHS (head targs) -- chars are integers --> no conversion
| otherwise
= return $ makeRHS (tComb (transOpName qf) targs)
makeRHS rhs = maybe rhs (\l -> tEqu l rhs) lhs
branch2SMT (Branch (LPattern _) _) = Nothing -- literal patterns not supported
branch2SMT (Branch (Pattern qf vs) e) = do
t <- exp2SMT lhs e
return (PComb (Id (transOpName qf)) vs, t)
--- Is a expression typed? (should go into FlatCurry.Goodies)
isTyped :: Expr -> Bool
isTyped e = case e of
Typed _ _ -> True
_ -> False
--- Gets the type of a typed expression. (should go into FlatCurry.Goodies)
exprType :: Expr -> TypeExpr
exprType e = case e of
Typed _ te -> te
_ -> error "FlatCurry.Goodies.exprType: not a typed expression"
--- Translates a literal into an SMT expression.
--- We represent character as ints.
lit2SMT :: Literal -> Term
lit2SMT (Intc i) = TConst (TInt i)
lit2SMT (Floatc f) = TConst (TFloat f)
lit2SMT (Charc c) = TConst (TInt (ord c))
----------------------------------------------------------------------------
-- Implementation of a transformation which replaces occurrences of
-- `Prelude_apply` by new fresh variables.
-- The state for this transformation.
data TransApplyState = TransApplyState
{ tsFreshVarIndex :: Int -- fresh variable index
, tsNewVars :: [(Int,Sort)] -- new typed variables
}
type TAState a = State TransApplyState a
-- Transforms a term by replacing occurrences of
-- `Prelude_failed` with new fresh variables.
-- The first argument is the maximum index of already used variables.
elimFailed :: Int -> Term -> (Term, [(Int,Sort)])
elimFailed maxusedvar trm =
let st0 = TransApplyState (maximum (maxusedvar : allVarsInTerm trm) + 1) []
(ntrm,st1) = runState (elimFailedInTerm trm) st0
in (ntrm, reverse (tsNewVars st1))
elimFailedInTerm :: Term -> TAState Term
elimFailedInTerm t = case t of
TConst _ -> return t
TSVar _ -> return t
TComb (As n srt) [] | n == "Prelude_failed"
-> do st <- get
let fv = tsFreshVarIndex st
fvt = (fv, srt) -- sort is type of `failed`
put st { tsFreshVarIndex = tsFreshVarIndex st + 1
, tsNewVars = fvt : tsNewVars st }
return (TSVar fv)
TComb qid ts -> mapM elimFailedInTerm ts >>= return . TComb qid
SMT.Let bs bt -> do trbs <- mapM (elimFailedInTerm . snd) bs
trbt <- elimFailedInTerm bt
return $ SMT.Let (zip (map fst bs) trbs) trbt
Forall vs te -> elimFailedInTerm te >>= return . Forall vs
Exists vs te -> elimFailedInTerm te >>= return . Exists vs
Match mt brs -> do trmt <- elimFailedInTerm mt
trbs <- mapM (elimFailedInTerm . snd) brs
return $ Match trmt (zip (map fst brs) trbs)
-- All variables occurring in a SMT term.
allVarsInTerm :: Term -> [SVar]
allVarsInTerm (TConst _) = []
allVarsInTerm (TSVar v) = [v]
allVarsInTerm (TComb _ args) = foldr union [] (map allVarsInTerm args)
allVarsInTerm (Forall vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (Exists vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (SMT.Let bs e) =
foldr union (map fst bs) (map allVarsInTerm (e : map snd bs))
allVarsInTerm (Match e ps) =
foldr union [] (map allVarsInTerm (e : map snd ps) ++ map (patVars . fst) ps)
where
patVars (PComb _ vs) = vs
varOfSV :: SortedVar -> SVar
varOfSV (SV v _) = v
----------------------------------------------------------------------------
--- Translates a FlatCurry type expression into a corresponding SMT sort.
--- Type variables are translated into the sort `TVar` where a
--- type variable index is appended (`TVari`) in order to generate
--- a polymorphic sort (which will later be translated by the
--- SMT translator).
--- The types `TVar` and `Func` are defined in the SMT prelude
--- which is always loaded.
type2sort :: TypeExpr -> Sort
type2sort = type2sortD False
--- Similarly as 'type2sort' but type variables are shown as `Ti`
--- if the first argument is true, which is used when generating
--- algebraic data tyep declarations.
type2sortD :: Bool -> TypeExpr -> Sort
type2sortD dt = t2s
where
t2s texp = case texp of
TVar i -> SComb ((if dt then "T" else "TVar") ++ show i) []
TCons qc targs -> SComb (tcons2SMT qc) (map t2s targs)
FuncType dom ran -> SComb "Func" (map t2s [dom,ran])
ForallType _ te -> t2s te
--error "Veriy.WithSMT.type2SMT: cannot translate ForallType"
--- Translates a FlatCurry type constructor name into SMT.
tcons2SMT :: QName -> String
tcons2SMT (mn,tc)
| "_Dict#" `isPrefixOf` tc
= "Dict" -- since we do not yet consider class dictionaries...
| mn == "Prelude" && take 3 tc == "(,,"
= "Tuple" ++ show (length tc - 1)
| mn == "Prelude"
= maybe (encodeSpecialChars tc) id (lookup tc transPrimTCons)
| otherwise
= mn ++ "_" ++ encodeSpecialChars tc
--- Primitive type constructors from the prelude and their SMT names.
transPrimTCons :: [(String,String)]
transPrimTCons =
[("Int","Int")
,("Float","Real")
,("Char","Int") -- Char is represented as Int
,("[]","List")
,("()","Unit")
,("(,)","Pair")
,("Maybe","Maybe")
,("Either","Either")
,("Ordering","Ordering")
]
--- Encode special characters in strings
encodeSpecialChars :: String -> String
encodeSpecialChars = concatMap encChar
where
encChar c | c `elem` "#$%[]()!,"
= let oc = ord c
in ['%', int2hex (oc `div` 16), int2hex(oc `mod` 16)]
| otherwise = [c]
int2hex i = if i<10 then chr (ord '0' + i)
else chr (ord 'A' + i - 10)
--- Translates urlencoded string into equivalent ASCII string.
decodeSpecialChars :: String -> String
decodeSpecialChars [] = []
decodeSpecialChars (c:cs)
| c == '%' = let n = case readHex (take 2 cs) of
[(h,"")] -> h
_ -> 0
in chr n : decodeSpecialChars (drop 2 cs)
| otherwise = c : decodeSpecialChars cs
--- Translates a qualified FlatCurry name into an SMT string.
transOpName :: QName -> String
transOpName (mn,fn)
| mn=="Prelude" = fromMaybe tname (lookup fn primNames)
| otherwise = tname
where
tname = mn ++ "_" ++ encodeSpecialChars fn
--- Translates a (translated) SMT string back into qualified FlatCurry name.
--- Returns Nothing if it was not a qualified name.
untransOpName :: String -> Maybe QName
untransOpName s =
let (mn,ufn) = break (=='_') s
in if null ufn
then Nothing
else Just (mn, decodeSpecialChars (tail ufn))
----------------------------------------------------------------------------
--- Some primitive names of the prelude and their SMT names.
primNames :: [(String,String)]
primNames =
[ -- Operations
("&&","and")
,("||","or")
,("not","not")
,("==","=")
,("/=","/=")
,("===","=")
,("/==","/=")
,("=","=")
,("<","<")
,("<=","<=")
,(">",">")
,(">=",">=")
,("+","+")
,("-","-")
,("*","*")
-- Constructors:
,("True","true")
,("False","false")
,("[]","nil")
,(":","insert")
,("()","unit")
,("(,)","mk-pair")
,("LT","LT")
,("EQ","EQ")
,("GT","GT")
,("Nothing","Nothing")
,("Just","Just")
,("Left","Left")
,("Right","Right")
,("_","_") -- for anonymous patterns in case expressions
] ++
map (\i -> ('(' : take (i-1) (repeat ',') ++ ")", "Tuple" ++ show i)) [3..15]
------------------------------------------------------------------------------
--- Extract all user-defined FlatCurry functions that might be called
--- by a given list of function names provided as the last argument.
--- The second argument is an `IORef` to the currently loaded modules.
--- Its contents will be extended when necessary.
getAllFunctions :: Options -> IORef ProgInfo -> [QName] -> IO [FuncDecl]
getAllFunctions opts pistore newfuns = do
mods <- fmap (map (miProg . snd) . progInfos) $ readIORef pistore
getAllFuncs mods preloadedFuncDecls newfuns
where
getAllFuncs _ currfuncs [] = return (reverse currfuncs)
getAllFuncs allmods currfuncs (newfun:newfuncs)
| newfun `elem` excludedCurryOperations ||
newfun `elem` map (pre . fst) primNames ||
newfun `elem` map funcName currfuncs || isPrimOp newfun
= getAllFuncs allmods currfuncs newfuncs
| fst newfun `elem` map progName allmods -- module already loaded:
= maybe (error $ "getAllFunctions: " ++ show newfun ++ " not found!")
(\fdecl -> --print fdecl >>
getAllFuncs allmods (fdecl : currfuncs)
(newfuncs ++
filter (`notElem` excludedCurryOperations)
(funcsOfFuncDecl fdecl)))
(find (\fd -> funcName fd == newfun)
(maybe []
progFuncs
(find (\m -> progName m == fst newfun) allmods)))
| otherwise -- we must load a new module
= do let mname = fst newfun
printWhenStatus opts $
"Loading module '" ++ mname ++ "' for '"++ snd newfun ++"'"
addModInfoFor pistore mname
newmod <- fmap miProg $ getModInfoFor pistore mname
getAllFuncs (newmod : allmods) currfuncs (newfun:newfuncs)
--- Removes from a list of function declarations the functions not used
--- by an initial list of function names.
--- It is assumed that the list of functions is already sorted by
--- dependencies (ealier functions might call later ones).
usedFunctions :: [QName] -> [FuncDecl] -> [FuncDecl]
usedFunctions _ [] = []
usedFunctions usedfns (fdecl : fdecls)
| funcName fdecl `elem` usedfns
= fdecl : usedFunctions (union (funcsOfFuncDecl fdecl) usedfns) fdecls
| otherwise
= usedFunctions usedfns fdecls
--- Extract all user-defined FlatCurry functions that might be called
--- by a given list of function names provided as the last argument.
--- The second argument is an `IORef` to the currently loaded modules.
--- Its contents will be extended when necessary.
loadModulesForQNames :: Options -> IORef ProgInfo -> [QName] -> IO ()
loadModulesForQNames opts pistore qns = mapM_ loadMod (nub (map fst qns))
where
loadMod m = do
mloaded <- hasModInfoFor pistore m
unless mloaded $ do -- we must load a new module
printWhenStatus opts $ "Loading module '" ++ m ++ "'..."
addModInfoFor pistore m
-- Pre-loaded operations from the prelude to avoid reading the prelude
-- for simple operations.
preloadedFuncDecls :: [FuncDecl]
preloadedFuncDecls =
[Func (pre "id") 1 Public
(FuncType (TVar 0) (TVar 0))
(Rule [1] (Var 1)),
Func (pre "not") 1 Public
(FuncType fcBool fcBool)
(Rule [1] (Case Flex (Var 1)
[Branch (Pattern (pre "True") [] ) fcFalse,
Branch (Pattern (pre "False") []) fcTrue])),
Func (pre "null") 1 Public
(FuncType (fcList (TVar 0)) fcBool)
(Rule [1] (Case Flex (Var 1)
[Branch (Pattern (pre "[]") []) fcTrue,
Branch (Pattern (pre ":") [2,3]) fcFalse]))
]
--- Exclude character-related operations since characters are treated as
--- integers so that these operations are not required.
excludedCurryOperations :: [QName]
excludedCurryOperations =
map pre ["apply", "failed", "chr", "ord"]
--- Returns the names of all functions occurring in the
--- body of a function declaration.
funcsOfFuncDecl :: FuncDecl -> [QName]
funcsOfFuncDecl fd =
nub (trRule (\_ e -> funcsInExpr e) (\_ -> []) (funcRule fd))
------------------------------------------------------------------------------
|