1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182

-------------------------------------------------------------------------
--- A transformation of Curry programs into verification tools.
---
--- @author Michael Hanus
--- @version April 2021
-------------------------------------------------------------------------

module ToVerifier where

import Control.Monad           ( unless, when )
import Data.List
import Data.Maybe              ( fromJust )
import System.Console.GetOpt
import System.Environment      ( getArgs )

import AbstractCurry.Types
import AbstractCurry.Files
import AbstractCurry.Select
import AbstractCurry.Transform

import Rewriting.Files         ( showQName )
import System.CurryPath        ( stripCurrySuffix )
import System.Process          ( exitWith )
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)
  mapM_ (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 = mapM_ (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 "()"]

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