Commit f2382cf8 authored by Michael Hanus's avatar Michael Hanus
Browse files

curry2verify: option -p to specify translation property added

parent 5f6ebaa9
......@@ -14,7 +14,7 @@ solve (S x) y = L : solve x y
solve x (S y) = R : solve x y
-- Originally, we want to prove:
-- theorem'gamelength x y = len (solve x y) -=- add x y
-- gamelength x y = len (solve x y) -=- add x y
-- If we are interested in the spine, i.e., the list structure of
-- calls to solve, we see that solve is strict in both arguments, i.e.,
......
......@@ -2,7 +2,7 @@
open import bool
module PROOF-assoc
module PROOF-appendIsAssoc
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
......@@ -28,8 +28,8 @@ append (Cons y z) u = Cons y (append z u)
---------------------------------------------------------------------------
theorem'assoc : {a : Set} → (x : List a) → (y : List a) → (z : List a) → (append (append x y) z) ≡ (append x (append y z))
theorem'assoc Empty y z = refl
theorem'assoc (Cons x xs) y z rewrite theorem'assoc xs y z = refl
appendIsAssoc : {a : Set} → (x : List a) → (y : List a) → (z : List a) → (append (append x y) z) ≡ (append x (append y z))
appendIsAssoc Empty y z = refl
appendIsAssoc (Cons x xs) y z rewrite appendIsAssoc xs y z = refl
---------------------------------------------------------------------------
......@@ -43,8 +43,7 @@ even-add-x-x : ∀ (x : ℕ) → even (add x x) ≡ tt
even-add-x-x zero = refl
even-add-x-x (suc x) rewrite add-suc x x | even-add-x-x x = refl
theorem'evendouble : (c1 : Choice) → (x : ℕ)
→ (even (double (coin c1 x))) ≡ tt
theorem'evendouble c1 x rewrite even-add-x-x (coin c1 x) = refl
evendoublecoin : (c1 : Choice) → (x : ℕ) → (even (double (coin c1 x))) ≡ tt
evendoublecoin c1 x rewrite even-add-x-x (coin c1 x) = refl
---------------------------------------------------------------------------
......@@ -33,24 +33,24 @@ len (x :: y) = suc (len y)
---------------------------------------------------------------------------
-- Theorem: the length of every solution is the sum of the input arguments
theorem'gamelength : (x : ℕ) → (y : ℕ)
gamelength : (x : ℕ) → (y : ℕ)
→ (solve2 x y) satisfy (λ xs → length xs =ℕ x + y) ≡ tt
theorem'gamelength zero zero = refl
theorem'gamelength zero (suc y)
gamelength zero zero = refl
gamelength zero (suc y)
rewrite
satisfy-mapND (_::_ R) (solve2 zero y) (λ xs → length xs =ℕ zero + suc y)
| theorem'gamelength zero y = refl
theorem'gamelength (suc x) zero
| gamelength zero y = refl
gamelength (suc x) zero
rewrite
satisfy-mapND (_::_ L) (solve2 x zero) (λ xs → length xs =ℕ suc x + zero)
| theorem'gamelength x zero = refl
theorem'gamelength (suc x) (suc y)
| gamelength x zero = refl
gamelength (suc x) (suc y)
rewrite
satisfy-mapND (_::_ L) (solve2 x (suc y)) (λ xs → length xs =ℕ suc x + suc y)
| satisfy-mapND (_::_ R) (solve2 (suc x) y) (λ xs → length xs =ℕ suc x + suc y)
| theorem'gamelength x (suc y)
| gamelength x (suc y)
| +suc x y
| theorem'gamelength (suc x) y
| gamelength (suc x) y
= refl
---------------------------------------------------------------------------
......@@ -48,8 +48,7 @@ odd-add-x-x : ∀ (x : ℕ) → odd (add x x) ≡ ff
odd-add-x-x zero = refl
odd-add-x-x (suc x) rewrite add-suc x x | odd-add-x-x x = refl
theorem'odddoublecoin : (c1 : Choice) → (x : ℕ)
→ (odd (double (coin c1 x))) ≡ ff
theorem'odddoublecoin c1 x rewrite odd-add-x-x (coin c1 x) = refl
odddoublecoin : (c1 : Choice) → (x : ℕ) → (odd (double (coin c1 x))) ≡ ff
odddoublecoin c1 x rewrite odd-add-x-x (coin c1 x) = refl
---------------------------------------------------------------------------
......@@ -36,11 +36,11 @@ insert-inc-length ch x (y :: ys) with choose ch
... | ff rewrite insert-inc-length (lchoice ch) x ys = refl
theorem'permlength : {a : Set} → (c1 : Choice) → (x : 𝕃 a) → (length x) ≡ (length (perm c1 x))
theorem'permlength c1 [] = refl
theorem'permlength c1 (x :: xs)
permlength : {a : Set} → (c1 : Choice) → (x : 𝕃 a) → (length x) ≡ (length (perm c1 x))
permlength c1 [] = refl
permlength c1 (x :: xs)
rewrite insert-inc-length c1 x (perm (lchoice c1) xs)
| theorem'permlength (lchoice c1) xs
| permlength (lchoice c1) xs
= refl
---------------------------------------------------------------------------
......@@ -2,7 +2,7 @@
--- A transformation of Curry programs into Agda programs.
---
--- @author Michael Hanus
--- @version June 2016
--- @version August 2016
-------------------------------------------------------------------------
module ToAgda(theoremToAgda) where
......@@ -196,10 +196,10 @@ transformRuleWithChoices opts (fn,cmt,texp,trs)
choicevar = TermVar 46
transTheorem rl@(lhs,rhs) =
if isTheoremRule rl then (lhs, prop2agda rhs) else rl
if isTheoremRule opts rl then (lhs, prop2agda rhs) else rl
theoremComment rl@(_,rhs) =
if isTheoremRule rl
if isTheoremRule opts rl
then case rhs of
TermVar _ -> []
TermCons f _ ->
......@@ -299,7 +299,7 @@ transformRuleWithNondet opts (fn,cmt,texp,trs)
_ -> CTCons (pre "ND") [te]
addNondet rl@(lhs,rhs)
| isTheoremRule rl
| isTheoremRule opts rl
= (lhs, prop2agda $ case rhs of TermVar _ -> rhs -- impossible case
TermCons f args ->
TermCons f (map addNondetInTerm args))
......@@ -307,10 +307,10 @@ transformRuleWithNondet opts (fn,cmt,texp,trs)
= (lhs, addNondetInTerm rhs)
transTheorem rl@(lhs,rhs) =
if isTheoremRule rl then (lhs, prop2agda rhs) else rl
if isTheoremRule opts rl then (lhs, prop2agda rhs) else rl
theoremComment rl@(_,rhs) =
if isTheoremRule rl
if isTheoremRule opts rl
then case rhs of
TermVar _ -> []
TermCons f _ -> case snd f of
......@@ -539,11 +539,11 @@ ruleFunc rl@(TermVar _,_) = error $ "Rule with variable lhs: " ++
ruleFunc (TermCons f _,_) = f
-- Is this rule of a property of the source program?
isTheoremRule :: Rule QName -> Bool
isTheoremRule (_,rhs) =
case rhs of
isTheoremRule :: Options -> Rule QName -> Bool
isTheoremRule opts (lhs,_) =
case lhs of
TermVar _ -> False
TermCons f _ -> snd f `elem` ["-=-","<~>","always","eventually","failing"]
TermCons f _ -> f `elem` optTheorems opts
fst4 :: (a,b,c,d) -> a
fst4 (x,_,_,_) = x
......
......@@ -2,7 +2,7 @@
--- A transformation of Curry programs into verification tools.
---
--- @author Michael Hanus
--- @version June 2016
--- @version Augsut 2016
-------------------------------------------------------------------------
module ToVerifier where
......@@ -33,7 +33,7 @@ cvBanner :: String
cvBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText =
"curry2verify: Curry programs -> Verifiers (version of 15/08/2016)"
"curry2verify: Curry programs -> Verifiers (version of 16/08/2016)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -49,20 +49,35 @@ main = do
(putStr (unlines opterrors) >> putStrLn usageText >> exitWith 1)
when (optVerb opts > 0) $ putStr cvBanner
when (null args || optHelp opts) (putStrLn usageText >> exitWith 1)
mapIO_ (generateTheorems opts) (map stripCurrySuffix args)
mapIO_ (generateTheoremsForModule opts) (map stripCurrySuffix args)
-------------------------------------------------------------------------
-- Generate a file for each theorem found in a module.
generateTheorems :: Options -> String -> IO ()
generateTheorems opts mname = do
generateTheoremsForModule :: Options -> String -> IO ()
generateTheoremsForModule opts mname = do
prog <- readCurry mname
let properties = filter isProperty (functions prog)
if null properties
then putStrLn "No properties found!"
else mapIO_ (generateTheorem opts) (map funcName properties)
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 file for a given property name.
-- 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]
......
......@@ -2,7 +2,7 @@
--- The options of the Curry->Verifier translation tool.
---
--- @author Michael Hanus
--- @version May 2016
--- @version August 2016
-------------------------------------------------------------------------
module VerifyOptions where
......@@ -10,6 +10,7 @@ module VerifyOptions where
import AbstractCurry.Types
import Char (toLower)
import GetOpt
import List (intercalate, last, splitOn)
import ReadNumeric (readNat)
import GenericProgInfo
import Deterministic (Deterministic(..))
......@@ -19,29 +20,31 @@ import TotallyDefined (Completeness(..))
-- Representation of command line options and information relevant
-- for the translation process.
data Options = Options
{ optHelp :: Bool
, optVerb :: Int
, optStore :: Bool -- store result in file?
, optTarget :: String -- translation target
, optScheme :: String -- translation scheme
, isPrimFunc :: (QName -> Bool) -- primitive function? (not translated)
, primTypes :: [QName] -- primitive types (not translated)
, detInfos :: ProgInfo Deterministic -- info about deteterministic funcs
, patInfos :: ProgInfo Completeness -- info about pattern completeness
{ optHelp :: Bool
, optVerb :: Int
, optStore :: Bool -- store result in file?
, optTarget :: String -- translation target
, optScheme :: String -- translation scheme
, optTheorems :: [QName] -- names of theorems to be translated
, isPrimFunc :: (QName -> Bool) -- primitive function? (not translated)
, primTypes :: [QName] -- primitive types (not translated)
, detInfos :: ProgInfo Deterministic -- info about deteterministic funcs
, patInfos :: ProgInfo Completeness -- info about pattern completeness
}
-- Default command line options.
defaultOptions :: Options
defaultOptions = Options
{ optHelp = False
, optVerb = 1
, optStore = True
, optTarget = "agda"
, optScheme = "choice"
, isPrimFunc = isUntranslatedFunc
, primTypes = defPrimTypes
, detInfos = emptyProgInfo
, patInfos = emptyProgInfo
defaultOptions = Options
{ optHelp = False
, optVerb = 1
, optStore = True
, optTarget = "agda"
, optScheme = "choice"
, optTheorems = []
, isPrimFunc = isUntranslatedFunc
, primTypes = defPrimTypes
, detInfos = emptyProgInfo
, patInfos = emptyProgInfo
}
-- Primitive functions that are not extracted and translated to the verifier.
......@@ -69,6 +72,9 @@ options =
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show progress (default)\n2: show generated output (same as `-v')\n3: show generated output"
, Option "p" ["property"]
(ReqArg addPropName "<n>")
"name of property to be translated as theorem\n(default: translate all properties in module)"
, Option "n" ["nostore"]
(NoArg (\opts -> opts { optStore = False }))
"do not store translation (show only)"
......@@ -100,4 +106,14 @@ options =
then opts { optScheme = map toLower s }
else error $ "Illegal scheme `" ++ s ++ "' (try `-h' for help)"
-- support also qualified names:
addPropName name opts =
let nameparts = splitOn "." name
partnums = length nameparts
qname = if partnums < 2
then ("",name)
else (intercalate "." (take (partnums - 1) nameparts),
last nameparts)
in opts { optTheorems = qname : optTheorems opts }
-------------------------------------------------------------------------
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment