------------------------------------------------------------------------- --- A transformation of Curry programs into Agda programs. --- --- @author Michael Hanus --- @version October 2016 ------------------------------------------------------------------------- module ToAgda(theoremToAgda) where import AbstractCurry.Types import AbstractCurry.Select import AbstractCurry.Build import Directory import FilePath (()) import List import Maybe (fromJust) import Rewriting.Files import Rewriting.Term import Rewriting.Rules import Rewriting.CriticalPairs import Time 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") $ mapIO_ 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 -------------------------------------------------------------------------