|
sourcecode:
|
module ToAgda ( theoremToAgda ) where
import Control.Monad ( unless, when )
import Data.List
import Data.Maybe ( fromJust )
import AbstractCurry.Types
import AbstractCurry.Select
import AbstractCurry.Build
import Data.Time
import Rewriting.Files
import Rewriting.Term
import Rewriting.Rules
import Rewriting.CriticalPairs
import System.Directory
import System.FilePath ( (</>) )
import PropertyUsage
import VerifyOptions
import VerifyPackageConfig ( packagePath )
-- to access the determinism analysis:
import Analysis.ProgInfo ( ProgInfo, lookupProgInfo )
import Analysis.Deterministic ( Deterministic(..) )
import Analysis.TotallyDefined ( Completeness(..) )
-------------------------------------------------------------------------
--- Generate an Agda program file for a given theorem name and the
--- list of all functions involved in this theorem.
theoremToAgda :: Options -> QName -> [CFuncDecl] -> [CTypeDecl] -> IO ()
theoremToAgda opts qtheo@(_,theoname) allfuncs alltypes = do
let (rename, orgtypedrules) = funcDeclsToTypedRules allfuncs
transform = if optScheme opts == "nondet" then transformRuleWithNondet
else transformRuleWithChoices
typedrules = concatMap (transform opts) orgtypedrules
(theorules,funcrules) = partition (\ (fn,_,_,_) -> fn == qtheo)
typedrules
mname = "TO-PROVE-" ++ theoname
hrule = take 75 (repeat '-')
agdaprog = unlines $
agdaHeader opts mname ++
[hrule, "-- Translated Curry operations:",""] ++
map typeDeclAsAgda alltypes ++
showTypedTRSAsAgda opts rename [] funcrules ++
[hrule, ""] ++
concatMap (theoremAsAgda rename) theorules ++
[hrule]
--putStr agdaprog
let agdafile = mname ++ ".agda"
when (optVerb opts > 1 || not (optStore opts)) $ putStr agdaprog
when (optStore opts) $ do
writeFile agdafile agdaprog
when (optScheme opts == "nondet") $
mapM_ copyImport ["nondet.agda","nondet-thms.agda"]
when (optVerb opts > 0) $ putStrLn $
"Agda module '" ++ agdafile ++ "' written.\n" ++
"If you completed the proof, rename it to 'PROOF-" ++ theoname ++ ".agda'."
agdaHeader :: Options -> String -> [String]
agdaHeader opts mname =
[ "-- Agda program using the Iowa Agda library\n"
, "open import bool\n"
, "module " ++ mname ] ++
(if optScheme opts == "choice"
then [" (Choice : Set)\n (choose : Choice → 𝔹)"
, " (lchoice : Choice → Choice)\n (rchoice : Choice → Choice)"]
else []) ++
[" where\n"
, unlines (map (\im -> "open import " ++ im)
(["eq","nat","list","maybe"] ++
(if optScheme opts == "nondet" then ["nondet","nondet-thms"]
else [])))
]
-------------------------------------------------------------------------
-- Map a list of function declarations into renaming function (for showing
-- identifiers in the the Agda code)
-- and a list of function names, comment lines, types, and TRS.
funcDeclsToTypedRules :: [CFuncDecl]
-> (QName -> String, [(QName, [String], CTypeExpr, TRS QName)])
funcDeclsToTypedRules fdecls = (rename, typedrules)
where
typedrules = map funcDeclToTypedRule fdecls
allrules = concatMap (\ (_,_,_,rules) -> rules) typedrules
rename = rename4agda (allNamesOfTRS allrules)
-- All function names occurring in a TRS.
allNamesOfTRS :: Eq a => TRS a -> [a]
allNamesOfTRS =
foldr union [] . map allNamesOfTerm . concatMap (\ (lhs,rhs) -> [lhs,rhs])
-- All function names occurring in a term.
allNamesOfTerm :: Eq a => Term a -> [a]
allNamesOfTerm (TermVar _) = []
allNamesOfTerm (TermCons f ts) = foldr union [f] (map allNamesOfTerm ts)
-- Perform some renamings of qualified names for Agda.
-- In particular, drop the module qualifier from a name if it is still unique
-- to improve the readability of the Agda code.
rename4agda :: [QName] -> QName -> String
rename4agda allnames qn@(mn,fn)
| (mn,fn) == pre ":" = "_::_"
| (mn,fn) == pre "+" = "_+_"
| (mn,fn) == pre "*" = "_*_"
| (mn,fn) == pre "True" = "tt"
| (mn,fn) == pre "False" = "ff"
| (mn,fn) == nat "Z" = "zero"
| (mn,fn) == nat "S" = "suc"
| (mn,fn) == pre "<" = "_<_"
| (mn,fn) == pre ">" = "_>_"
| (mn,fn) == pre "<=" = "_\x2264_"
| (mn,fn) == pre ">=" = "_\x2265_"
| otherwise
= maybe fn
(const (showQName qn))
(find (\ (q,f) -> f==fn && q /= mn) allnames)
-- Map a function declaration into the function name, comment, type, and TRS.
funcDeclToTypedRule :: CFuncDecl -> (QName, [String], CTypeExpr, TRS QName)
funcDeclToTypedRule (CFunc qn ar vis texp rules) =
funcDeclToTypedRule (CmtFunc "" qn ar vis texp rules)
funcDeclToTypedRule fdecl@(CmtFunc _ _ _ _ texp _) =
let (fn, trs) = fromFuncDecl fdecl
in (fn, [], typeOfQualType texp, trs)
-------------------------------------------------------------------------
-- Eliminate overlapping rules by introducing a new operation
-- for each rule.
elimOverlappingRules :: Options
-> Bool
-> (QName, [String], CTypeExpr, TRS QName)
-> [(QName, [String], CTypeExpr, TRS QName)]
elimOverlappingRules opts withpartialfail (fn,cmt,texp,trs)
| lookupProgInfo fn detinfo == Just Det || null critPairs
= [(fn,cmt,texp,trs)]
| otherwise
= (fn, cmt ++ [splitCmt], texp,
[(TermCons fn newargs,
foldr1 (\x y -> TermCons (pre "?") [x,y])
(map (\i -> TermCons (addRuleName fn i) newargs)
[1 .. length trs]))]) :
map (\ (i,(TermCons _ args, rhs)) ->
let rname = addRuleName fn i
in (rname,
["Rule " ++ show i ++ " of operation '" ++ showQName fn ++"':"],
texp,
[(TermCons rname args, rhs)] ++
if withpartialfail then [failRule rname] else []))
(zip [1 .. length trs] trs)
where
detinfo = detInfos opts
critPairs = cPairs trs
arity = case head trs of (TermCons _ args,_) -> length args
_ -> error "elimOverlappingRules: no arity"
newargs = map TermVar [1 .. arity]
failRule f = (TermCons f (map TermVar [0 .. (arity-1)]),
TermCons (pre "failed") [])
splitCmt = "Overlapping rules of '" ++ showQName fn ++
"' split into a new operation for each rule."
-- Add a rule with a number to a name (to implement overlapping rules):
addRuleName :: QName -> Int -> QName
addRuleName (mn,fn) i = (mn, fn ++ "-rule" ++ show i)
-- Revert `addRuleName`.
stripRuleName :: QName -> QName
stripRuleName (mn,fn) =
-- we assume that there are no more than 9 overlapping rules:
(mn, if take 5 (tail (reverse fn)) == "elur-"
then take (length fn - 6) fn
else fn )
-------------------------------------------------------------------------
-- Transform a TRS for a function according to transformation method
-- based on choice arguments:
-- TODO: implement partial functions
transformRuleWithChoices :: Options
-> (QName, [String], CTypeExpr, TRS QName)
-> [(QName, [String], CTypeExpr, TRS QName)]
transformRuleWithChoices opts (fn,cmt,texp,trs)
| lookupProgInfo fn detinfo == Just Det
= [(fn, cmt ++ concatMap theoremComment trs, texp, map transTheorem trs)]
| otherwise
= map (\ (f,c,t,rs) -> (f, c ++ concatMap theoremComment rs,
baseType (pre "Choice") ~> t,
map (transTheorem . addChoices) rs))
(elimOverlappingRules opts False (fn,cmt,texp,trs))
where
detinfo = detInfos opts
choicevar = TermVar 46
transTheorem rl@(lhs,rhs) =
if isTheoremRule opts rl then (lhs, prop2agda rhs) else rl
theoremComment rl@(_,rhs) =
if isTheoremRule opts rl
then case rhs of
TermVar _ -> []
TermCons f _ ->
case snd f of
"-=-" -> []
"<~>" -> []
"always" -> []
_ -> noTheoremTranslateCmt
else []
-- Translate CurryCheck proposition into Agda theorem:
prop2agda v@(TermVar _) = v
prop2agda t@(TermCons f args) =
case snd f of
"-=-" -> TermCons (pre "_\x2261_") args
"<~>" -> TermCons (pre "_\x2261_") args
"always" -> TermCons (pre "_\x2261_") (args ++ [agdaTrue])
_ -> t
addChoices (lhs,rhs) =
(addLhsChoice choicevar lhs,
snd (addChoiceInTerm (choicesFor (numNondetOps rhs) choicevar) rhs))
addLhsChoice _ v@(TermVar _) = v -- this case should not occur
addLhsChoice ch (TermCons f args) = TermCons f (ch : args)
isNondetOp f = lookupProgInfo (stripRuleName f) detinfo == Just NDet
-- compute number of non-deterministic operations in a term:
numNondetOps (TermVar _) = 0
numNondetOps (TermCons f args) =
(if f == curryChoice || isNondetOp f then 1 else 0) +
sum (map numNondetOps args)
addChoiceInTerm chs v@(TermVar _) = (chs,v)
addChoiceInTerm chs (TermCons f args)
| f == pre "?" && length args == 2
= let (chs1,cargs) = addChoiceInTerms (tail chs) args
in (chs1, TermCons (pre "if_then_else")
(TermCons (pre "choose") [head chs] : cargs))
| isNondetOp f
-- non-deterministic operation:
= let (chs1,cargs) = addChoiceInTerms (tail chs) args
in (chs1, TermCons f (head chs : cargs))
| otherwise
= let (chs1,cargs) = addChoiceInTerms chs args
in (chs1, TermCons f cargs)
addChoiceInTerms ch [] = (ch,[])
addChoiceInTerms ch (t:ts) = let (ch1,ct ) = addChoiceInTerm ch t
(ch2,cts) = addChoiceInTerms ch1 ts
in (ch2,ct:cts)
-- Compute a list of disjoint choices for a given number of choices
-- and a base choice variable.
choicesFor :: Int -> Term QName -> [Term QName]
choicesFor n ch =
if n <= 1
then [ch]
else
map (\c -> TermCons (pre "lchoice") [c]) (choicesFor (n `div` 2) ch) ++
map (\c -> TermCons (pre "rchoice") [c]) (choicesFor (n - n `div` 2) ch)
noTheoremTranslateCmt :: [String]
noTheoremTranslateCmt =
["WARNING: cannot translate property into an Agda theorem!"]
-------------------------------------------------------------------------
-- Transform a TRS for a function according to transformation method
-- based on trees of non-determistic values:
transformRuleWithNondet :: Options
-> (QName, [String], CTypeExpr, TRS QName)
-> [(QName, [String], CTypeExpr, TRS QName)]
transformRuleWithNondet opts (fn,cmt,texp,trs)
| lookupProgInfo fn detinfo == Just Det
= [(fn, cmt ++ concatMap theoremComment trs, texp, map transTheorem trs)]
| otherwise
= map (\ (f,c,t,rs) -> (f, c ++ concatMap theoremComment rs,
addNDToResultType t,
map addNondet rs ++ failRule f))
(elimOverlappingRules opts True (fn,cmt,texp,trs))
where
detinfo = detInfos opts
arity = case head trs of (TermCons _ args,_) -> length args
_ -> error "transformRuleWithNondet: no arity"
failRule f = if lookupProgInfo fn (patInfos opts) == Just Complete
|| not (null (cPairs trs))
then []
else [(TermCons f (map TermVar [0 .. (arity-1)]),
TermCons (nondet "Fail") [])]
addNDToResultType te = case te of
CFuncType t1 t2 -> CFuncType t1 (addNDToResultType t2)
_ -> applyTC (pre "ND") [te]
addNondet rl@(lhs,rhs)
| isTheoremRule opts rl
= (lhs, prop2agda $ case rhs of TermVar _ -> rhs -- impossible case
TermCons f args ->
TermCons f (map addNondetInTerm args))
| otherwise
= (lhs, addNondetInTerm rhs)
transTheorem rl@(lhs,rhs) =
if isTheoremRule opts rl then (lhs, prop2agda rhs) else rl
theoremComment rl@(_,rhs) =
if isTheoremRule opts rl
then case rhs of
TermVar _ -> []
TermCons f _ -> case snd f of
"-=-" -> adaptOrderCmt
"<~>" -> adaptOrderCmt
"always" -> []
"eventually"-> []
"failing" -> []
_ -> noTheoremTranslateCmt
else []
where
adaptOrderCmt =
["This theorem should be adapted since the left- and right-hand sides",
"might have their values in a different order in the tree!"]
prop2agda v@(TermVar _) = v
prop2agda t@(TermCons (mn,pn) args) =
case pn of
"-=-" -> TermCons (pre "_\x2261_") args -- to be changed by user
"<~>" -> TermCons (pre "_\x2261_") args -- to be changed by user
"always" -> TermCons (pre "_\x2261_")
[TermCons (mn,"always") args, agdaTrue]
"eventually" -> TermCons (pre "_\x2261_")
[TermCons (mn,"eventually") args, agdaTrue]
"failing" -> TermCons (pre "_\x2261_")
[TermCons (mn,"failing") args, agdaTrue]
_ -> t
isNondetOp f = lookupProgInfo (stripRuleName f) detinfo == Just NDet
addNondetInTerm v@(TermVar _) = agdaVal v
addNondetInTerm t@(TermCons f args)
| f == pre "?" && length args == 2
= TermCons (pre "_??_") (map addNondetInTerm args)
| f == pre "failed" && null args
= TermCons (nondet "Fail") []
| not (hasNondetSubterms t)
= agdaVal (TermCons f args)
| otherwise
= let (detargs,ndargs) = break hasNondetSubterms args
in if isNondetOp f
then
if null ndargs
then t
else addArgsWithNdArg
(TermCons (withNdArgName (length ndargs))
[TermCons f detargs, addNondetInTerm (head ndargs)])
(tail ndargs)
else addArgsWithNdArg
(TermCons (nondet "mapND")
[TermCons f detargs, addNondetInTerm (head ndargs)])
(tail ndargs)
addArgsWithNdArg t [] = t
addArgsWithNdArg t (arg:args) =
if hasNondetSubterms arg
then addArgsWithNdArg
(TermCons (nondet "apply-nd") [t, addNondetInTerm arg]) args
else addArgsWithNdArg (TermCons (nondet "apply-nd") [t,agdaVal arg]) args
withNdArgName i = nondet ("with-nd-arg" ++ (if i>1 then show i else ""))
hasNondetSubterms (TermVar _) = False
hasNondetSubterms (TermCons f args) =
f == (pre "?") || isNondetOp f || any hasNondetSubterms args
agdaVal :: Term QName -> Term QName
agdaVal t = TermCons (nondet "Val") [t]
-------------------------------------------------------------------------
-- Show typed rules (properties) as theorems in Agda.
theoremAsAgda :: (QName -> String) -> (QName, [String], CTypeExpr, TRS QName)
-> [String]
theoremAsAgda _ (_,_,_,[]) = []
theoremAsAgda _ (fn,_,_,(TermVar _ ,_) : _) =
error $ "Theorem '" ++ showQName fn ++ "': variable in left-hand side"
theoremAsAgda rn (fn, cmt, texp, (TermCons _ largs,rhs) : rules) =
map ("-- "++) cmt ++
[rn fn ++ " : " ++ (if null tvars then "" else showForAll tvars) ++
showTypeWOResult largs texp ++ showTermAsAgda False (mapTerm rn rhs)
,showTermAsAgda False (mapTerm rn (TermCons fn largs)) ++ " = ?", ""
] ++ theoremAsAgda rn (fn,cmt,texp,rules)
where
tvars = nub (tvarsOfType texp)
showTypeWOResult [] _ = ""
showTypeWOResult (arg:args) te = case te of
CFuncType t1 t2 -> "(" ++ showTermAsAgda False (mapTerm rn arg) ++ " : " ++
showTypeAsAgda False t1 ++
") \x2192 " ++ showTypeWOResult args t2
_ -> error $ "Inconsistent type in theorem '" ++ showQName fn ++ "': " ++
show te
-- Show a TRS for an operation whose type is given as Agda definitions.
-- Type signatures of mutual recursive functions must be written earlier.
-- Therefore, we pass the list of already printed functions as the
-- third argument.
showTypedTRSAsAgda :: Options -> (QName -> String) -> [QName]
-> [(QName,[String],CTypeExpr,TRS QName)] -> [String]
showTypedTRSAsAgda _ _ _ [] = []
showTypedTRSAsAgda opts rn prefuns ((fn,cmt,texp,trs) : morefuncs) =
(concatMap (\ff -> let (f,_,t,_) = fromJust (find (\tf -> fst4 tf == ff)
morefuncs)
in ["-- Forward declaration:",
showTypeSignatureAsAgda (rn f) t,""])
forwardfuncs) ++
map ("-- "++) cmt ++
(if lookupProgInfo fn (patInfos opts) == Just Complete
|| optScheme opts == "nondet"
then []
else ["-- WARNING: function '" ++ showQName fn ++
"' is partial: adapt the code!"] ) ++
(if fn `elem` prefuns then [] else [showTypeSignatureAsAgda (rn fn) texp]) ++
map (showRuleAsAgda rn) trs ++ [""] ++
showTypedTRSAsAgda opts rn (forwardfuncs ++ prefuns) morefuncs
where
forwardfuncs = filter (`elem` map fst4 morefuncs) (allNamesOfTRS trs \\ [fn])
showRuleAsAgda :: (QName -> String) -> Rule QName -> String
showRuleAsAgda rn (lhs,rhs) =
showTermAsAgda False (mapTerm rn lhs) ++ " = " ++
showTermAsAgda False (mapTerm rn rhs)
-- Show a term in Agda syntax with already renamed function names:
showTermAsAgda :: Bool -> Term String -> String
showTermAsAgda _ (TermVar v) = showVarAsAgda v
showTermAsAgda withbrackets (TermCons c args) = inBrackets $
if c == "if_then_else" && length args == 3
then let is = map (showTermAsAgda False) args
in unwords ["if", is!!0, "then", is!!1, "else", is!!2]
else
if c == "apply" && length ts == 2
then unwords ts
else
if isInfixOp c && length ts == 2
then unwords [head ts, take (length c - 2) (tail c), head (tail ts)]
else unwords (c : ts)
where
ts = map (showTermAsAgda True) args
inBrackets s = if not (null ts) && withbrackets then "(" ++ s ++ ")" else s
-- Is infix operators in Agda?
isInfixOp :: String -> Bool
isInfixOp s = length s > 2 && head s == '_' && last s == '_'
showVarAsAgda :: Int -> String
showVarAsAgda v | v >= 0 = if q == 0
then [c]
else c:(show q)
where
(q, r) = divMod v 26
c = "xyzuvwrstijklmnopqabcdefgh" !! r
-------------------------------------------------------------------------
--- Show a type declaration as an Agda data declaration.
typeDeclAsAgda :: CTypeDecl -> String
typeDeclAsAgda (CTypeSyn tc _ _ _) =
error $ "Type synonyms not supported: " ++ showQName tc
typeDeclAsAgda (CNewType tc vis tvars consdecl dvs) =
typeDeclAsAgda (CType tc vis tvars [consdecl] dvs)
typeDeclAsAgda (CType tc _ tvars constrs _) = unlines $
(unwords $
["data", snd tc] ++
map (\tv -> "("++ showTypeAsAgda False (CTVar tv) ++ " : Set)") tvars ++
[": Set where"]) : map typeConsDeclAsAgda constrs
where
typeConsDeclAsAgda (CCons qc _ texps) =
" " ++ snd qc ++ " : " ++
showTypeAsAgda False (foldr CFuncType (applyTC tc (map CTVar tvars)) texps)
typeConsDeclAsAgda (CRecord qc _ _) =
error $ "Records not yet supported: " ++ showQName qc
-------------------------------------------------------------------------
showTypeSignatureAsAgda :: String -> CTypeExpr -> String
showTypeSignatureAsAgda fn texp =
fn ++ " : " ++ (if null tvars then "" else showForAll tvars) ++
showTypeAsAgda False texp
where
tvars = nub (tvarsOfType texp)
showForAll :: [CTVarIName] -> String
showForAll tvars = "{" ++ unwords (map (showTypeAsAgda False . CTVar) tvars) ++
" : Set} \x2192 "
showTypeAsAgda :: Bool -> CTypeExpr -> String
showTypeAsAgda withbrackets texp = case texp of
CFuncType t1 t2 -> inBrackets $ showTypeAsAgda False t1 ++ " \x2192 " ++
showTypeAsAgda False t2
CTVar (i,_) -> showVarAsAgda (i + 18) -- to get 'a' for var index 0...
CTCons tc -> showTCon tc
CTApply _ _ ->
maybe (error $ "ToAgda.showTypeAsAgda: cannot translate complex type:\n" ++
show texp)
(\tc -> inBrackets $ unwords $
showTCon tc : map (showTypeAsAgda True) (targsOfApply texp))
(tconOfApply texp)
where
inBrackets s = if withbrackets then "(" ++ s ++ ")" else s
tconOfApply te = case te of CTApply (CTCons qn) _ -> Just qn
CTApply tc _ -> tconOfApply tc
_ -> Nothing
targsOfApply te = case te of
CTApply (CTCons _) ta -> [ta]
CTApply tc ta -> targsOfApply tc ++ [ta]
_ -> [] -- should not occur
showTCon :: QName -> String
showTCon tc
| tc == pre "[]" = "\x1d543"
| tc == pre "Int" = "\x2115"
| tc == pre "Bool" = "\x1d539"
| tc == pre "Maybe" = "maybe"
| tc == pre "Choice" = "Choice"
| tc == nat "Nat" = "\x2115"
| otherwise = snd tc
-------------------------------------------------------------------------
curryChoice :: QName
curryChoice = pre "?"
nat :: String -> QName
nat s = ("Nat",s)
nondet :: String -> QName
nondet s = ("nondet",s)
agdaTrue :: Term QName
agdaTrue = TermCons (pre "tt") []
agdaFalse :: Term QName
agdaFalse = TermCons (pre "ff") []
ruleFunc :: Rule QName -> QName
ruleFunc rl@(TermVar _,_) = error $ "Rule with variable lhs: " ++
showRule showQName rl
ruleFunc (TermCons f _,_) = f
-- Is this rule of a property of the source program?
isTheoremRule :: Options -> Rule QName -> Bool
isTheoremRule opts (lhs,_) =
case lhs of
TermVar _ -> False
TermCons f _ -> f `elem` optTheorems opts
fst4 :: (a,b,c,d) -> a
fst4 (x,_,_,_) = x
-------------------------------------------------------------------------
--- Copy file from import dir into current dir if it is not newer
--- in the current dir.
copyImport :: String -> IO ()
copyImport library = do
let importfile = packagePath </> "imports" </> library
libexists <- doesFileExist library
if not libexists
then copyFile importfile library
else do
itime <- getModificationTime importfile
ltime <- getModificationTime library
unless (compareClockTime ltime itime == GT) $ copyFile importfile library
-------------------------------------------------------------------------
|