-------------------------------------------------------------------------
--- A transformation of Curry programs into verification tools.
---
--- @author Michael Hanus
--- @version January 2019
-------------------------------------------------------------------------

module ToVerifier where

import AbstractCurry.Types
import AbstractCurry.Files
import AbstractCurry.Select
import AbstractCurry.Transform
import GetOpt
import List
import Maybe             ( fromJust )
import System            ( exitWith, getArgs )

import Rewriting.Files   ( showQName )
import System.CurryPath  ( stripCurrySuffix )
import PropertyUsage

-- to use the determinism analysis:
import Analysis.ProgInfo
import Analysis.Deterministic  ( Deterministic(..), nondetAnalysis )
import Analysis.TotallyDefined ( Completeness(..), patCompAnalysis )
import CASS.Server             ( analyzeGeneric )
import Data.SCC                ( scc )

import ToAgda
import VerifyOptions
import VerifyPackageConfig     ( packageVersion )

-- Banner of this tool:
cvBanner :: String
cvBanner = unlines [bannerLine,bannerText,bannerLine]
 where
   bannerText = "curry-verify: Curry programs -> Verifiers (Version " ++
                packageVersion ++ " of 02/01/2019)"
   bannerLine = take (length bannerText) (repeat '-')

-- Help text
usageText :: String
usageText = usageInfo ("Usage: curry-verify [options] <module names>\n") options
  
main :: IO ()
main = do
  argv <- getArgs
  let (funopts, args, opterrors) = getOpt Permute options argv
      opts = foldl (flip id) defaultOptions funopts
  unless (null opterrors)
         (putStr (unlines opterrors) >> putStrLn usageText >> exitWith 1)
  when (optVerb opts > 0) $ putStr cvBanner 
  when (null args || optHelp opts) (putStrLn usageText >> exitWith 1)
  mapIO_ (generateTheoremsForModule opts) (map stripCurrySuffix args)

-------------------------------------------------------------------------

-- Generate a file for each theorem found in a module.
generateTheoremsForModule :: Options -> String -> IO ()
generateTheoremsForModule opts mname = do
  prog <- readCurry mname
  let propNames = map funcName (filter isProperty (functions prog))
      optNames  = nub (filter (\ (mn,_) -> null mn || mn == progName prog)
                              (optTheorems opts))
  if null optNames
   then if null propNames
        then putStrLn $ "No properties found in module `"++mname++"'!"
        else generateTheorems opts { optTheorems = propNames}
   else let qnames = map (\ (mn,pn) ->
                            (if null mn then progName prog else mn, pn))
                         optNames
         in if all (`elem` propNames) qnames
             then generateTheorems (opts { optTheorems = qnames })
             else error $ unwords ("Properties not found:" :
                                   map (\ (mn,pn) -> '`':mn++"."++pn++"'")
                                       (filter (`notElem` propNames) qnames))

-- Generate a proof file for each theorem in option `optTheorems`.
generateTheorems :: Options -> IO ()
generateTheorems opts = mapIO_ (generateTheorem opts) (optTheorems opts)

-- Generate a proof file for a given property name.
generateTheorem :: Options -> QName -> IO ()
generateTheorem opts qpropname = do
  (newopts, allprogs, allfuncs) <- getAllFunctions opts [] [] [qpropname]
  let alltypenames = foldr union []
                       (map (\fd -> tconsOfType (typeOfQualType (funcType fd)))
                            allfuncs)
      noproptypenames = filter ((/= propTypesModule) . fst) alltypenames
  alltypes <- getAllTypeDecls opts allprogs noproptypenames []
  when (optVerb opts > 2) $ do
    putStrLn $ "Theorem `" ++ snd qpropname ++ "':\nInvolved operations:"
    putStrLn $ unwords (map (showQName . funcName) allfuncs)
    putStrLn $ "Involved types:"
    putStrLn $ unwords (map (showQName . typeName) alltypes)
  case optTarget opts of
    "agda" -> theoremToAgda newopts qpropname allfuncs alltypes
    t      -> error $ "Unknown translation target: " ++ t

-------------------------------------------------------------------------
--- Extract all type declarations that are refererred in the types
--- of the given functions.
getAllTypeDecls :: Options -> [CurryProg] -> [QName] -> [CTypeDecl]
               -> IO [CTypeDecl]
getAllTypeDecls _ _ [] currtypes = return (sortTypeDecls currtypes)
getAllTypeDecls opts currmods (tc:tcs) currtypes
  | tc `elem` primTypes opts ++ map typeName currtypes
  = getAllTypeDecls opts currmods tcs currtypes
  | fst tc `elem` map progName currmods
  = maybe
      (-- if we don't find the qname, it must be a primitive type:
        getAllTypeDecls opts currmods tcs currtypes)
      (\tdecl -> getAllTypeDecls opts currmods
                                 (tcs ++ nub (typesOfCTypeDecl tdecl))
                                 (tdecl : currtypes))
      (find (\td -> typeName td == tc)
            (types (fromJust (find (\m -> progName m == fst tc) currmods))))
  | otherwise -- we must load a new module
  = do let mname = fst tc
       when (optVerb opts > 0) $
         putStrLn $ "Loading module '" ++ mname ++ "'..."
       newmod <- readCurry mname
       getAllTypeDecls opts (newmod:currmods) (tc:tcs) currtypes

-- Sort the type declarations according to their dependencies.
sortTypeDecls :: [CTypeDecl] -> [CTypeDecl]
sortTypeDecls tdecls = concat (scc definedBy usedIn tdecls)
 where
  definedBy tdecl = [typeName tdecl]
  usedIn (CType    _ _ _ cdecls _) = nub (concatMap typesOfConsDecl cdecls)
  usedIn (CTypeSyn _ _ _ texp)     = nub (typesOfTypeExpr texp)
  usedIn (CNewType _ _ _ cdecl _)  = nub (typesOfConsDecl cdecl)

-------------------------------------------------------------------------

--- Extract all functions that might be called by a given function.
getAllFunctions :: Options -> [CFuncDecl] -> [CurryProg] -> [QName]
                -> IO (Options, [CurryProg], [CFuncDecl])
getAllFunctions opts currfuncs currmods [] = return (opts, currmods, currfuncs)
getAllFunctions opts currfuncs currmods (newfun:newfuncs)
  | newfun `elem` standardConstructors ++ map funcName currfuncs
    || isPrimFunc opts newfun
  = getAllFunctions opts currfuncs currmods newfuncs
  | null (fst newfun) -- local declarations have empty module qualifier
  = getAllFunctions opts currfuncs currmods newfuncs
  | fst newfun `elem` map progName currmods
  = maybe
       (-- if we don't find the qname, it must be a constructor:
        getAllFunctions opts currfuncs currmods newfuncs)
      (\fdecl -> getAllFunctions opts
                    (if null (funcRules fdecl)
                      then currfuncs -- ignore external functions
                      else fdecl : currfuncs)
                    currmods (newfuncs ++ nub (funcsOfCFuncDecl fdecl)))
      (find (\fd -> funcName fd == newfun)
            (functions
               (fromJust (find (\m -> progName m == fst newfun) currmods))))
  | otherwise -- we must load a new module
  = do let mname = fst newfun
       when (optVerb opts > 0) $
         putStrLn $ "Loading module '" ++ mname ++ "'..."
       newmod <- readCurry mname
       when (optVerb opts > 0) $
         putStrLn $ "Analyzing module '" ++ mname ++ "'..."
       pdetinfo <- analyzeGeneric nondetAnalysis mname
                                                >>= return . either id error
       pcmpinfo <- analyzeGeneric patCompAnalysis mname
                                                >>= return . either id error
       getAllFunctions
         opts { detInfos = combineProgInfo (detInfos opts) pdetinfo
              , patInfos = combineProgInfo (patInfos opts) pcmpinfo }
         currfuncs (newmod:currmods) (newfun:newfuncs)

-- Some standard constructors from the prelude.
standardConstructors :: [QName]
standardConstructors = [pre "[]", pre ":", pre "()"]

-------------------------------------------------------------------------