----------------------------------------------------------------------------- --- Default Rules Preprocessor --- ========================== --- --- This module contains the implementation of a preprocessor --- for Curry programs in order to implement default rules --- and deterministic operations. --- --- A default rule for a function `f` processed by this preprocessor --- must be defined as a rule defining the operation `f'default`, e.g., --- --- nlookup key (_ ++ [(key,value)] ++ _) = Just value --- nlookup'default _ _ = Nothing --- --- The concept of default rules and their implementation are described in --- --- Sergio Antoy, Michael Hanus: Default Rules for Curry --- Theory and Practice of Logic Programming, --- Vol. 17, No. 2, pp. 121-147, 2017 --- --- An operation can be marked as deterministic by decorating the --- result type with `DET`, e.g., --- --- psort :: [Int] -> DET [Int] --- --- The concept of deterministic operations and their implementation --- are described in --- --- Sergio Antoy, Michael Hanus: --- Eliminating Irrelevant Non-determinism in Functional Logic Programs --- Proc. 19th Int. Symp. on Practical Aspects of Declarative Languages, --- Springer LNCS 10137, pp. 1-18, 2017 --- --- This preprocessor can be invoked by the Curry preprocessor `currypp` --- with the option `defaultrules` (provided as a CYMAKE option, --- see the example programs in the directory `examples/DefaultRules`). --- --- @author Michael Hanus --- @version October 2019 ----------------------------------------------------------------------------- module CPP.DefaultRules ( translateDefaultRulesAndDetOps ) where import Distribution ( curryCompiler ) import FilePath ( takeDirectory ) import List ( partition ) import AbstractCurry.Types import AbstractCurry.Files import AbstractCurry.Select import AbstractCurry.Build import AbstractCurry.Pretty import DefaultRuleUsage import System.CurryPath ( modNameToPath ) import TheoremUsage ( determinismTheoremFor, existsProofFor , getModuleProofFiles, isProofFileNameFor ) import CPP.CompileWithFrontend ( compileImportedModule ) -------------------------------------------------------------------- banner :: String banner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "Transformation Tool for Curry with Default Rules (Version of 11/10/19)" bannerLine = take (length bannerText) (repeat '=') ------------------------------------------------------------------------ -- Available translation schemes data TransScheme = SpecScheme -- as specified in the PADL'16 paper | NoDupScheme -- scheme without checking conditions twice deriving (Eq,Show) -- The default translation scheme: defaultTransScheme :: TransScheme defaultTransScheme = if curryCompiler == "kics2" then SpecScheme -- due to bug in KiCS2 else SpecScheme -- NoDupScheme ------------------------------------------------------------------------ --- Start default rules/deterministic operations transformation --- in "preprocessor mode". --- It is assumed that the Curry program passed as the last argument --- was read with `readUntypedCurry` which is important to --- process DET annotations! translateDefaultRulesAndDetOps :: Int -> [String] -> String -> CurryProg -> IO (Maybe CurryProg) translateDefaultRulesAndDetOps verb moreopts _ prog = do when (verb>1) $ putStr banner trscm <- processOpts moreopts when (verb>1) $ putStrLn ("Translation scheme: " ++ show trscm) mbtransprog <- translateProg verb trscm prog maybe (return Nothing) (\ (detfuncnames,newprog) -> do -- check whether we have files with determinism proofs: let mname = progName prog prfiles <- getModuleProofFiles (takeDirectory (modNameToPath mname)) mname detfuncnamesWOproofs <- filterProofObligation verb prfiles detfuncnames when (verb>0) $ printProofObligation detfuncnamesWOproofs return (Just newprog)) mbtransprog where processOpts opts = case opts of [] -> return defaultTransScheme [scheme] -> if scheme == "nodupscheme" then if curryCompiler == "kics2" then return SpecScheme -- due to bug in KiCS2!!! else return NoDupScheme else if scheme == "specscheme" then return SpecScheme else showError _ -> showError where showError = do putStrLn $ "Unknown options (ignored): " ++ unwords opts return defaultTransScheme -- Filter proof obligations for determinism annotation w.r.t. to existence -- of proof files: filterProofObligation :: Int -> [String] -> [QName] -> IO [QName] filterProofObligation _ _ [] = return [] filterProofObligation verb prooffiles (qf@(mn,fn) : qfs) = do let dettheoname = (mn, determinismTheoremFor fn) hasdetproof = existsProofFor dettheoname prooffiles when (hasdetproof && verb>0) $ putStrLn $ "Proofs for determinism property of " ++ showQName qf ++ " found:\n" ++ unlines (filter (isProofFileNameFor dettheoname) prooffiles) filterqfs <- filterProofObligation verb prooffiles qfs return (if hasdetproof then filterqfs else qf : filterqfs) printProofObligation :: [QName] -> IO () printProofObligation qfs = unless (null qfs) $ do putStrLn line putStrLn "PROOF OBLIGATIONS:" mapIO_ (\qn -> putStrLn $ showQName qn ++" is a deterministic operation.") qfs putStrLn line where line = take 70 (repeat '=') showQName :: QName -> String showQName (qn,fn) = "'" ++ qn ++ "." ++ fn ++ "'" ------------------------------------------------------------------------ -- Main transformation: transform a Curry program with default rules -- and deterministic functions into a new Curry program where these -- features are implemented by standard Curry features. -- Moreover, the list of deterministic functions is returned -- (to show the proof obligations to ensure completeness of the -- transformation). -- If the program was not transformed, `Nothing` is returned. translateProg :: Int -> TransScheme -> CurryProg -> IO (Maybe ([QName],CurryProg)) translateProg verb trscm prog@(CurryProg mn imps dfltdecl clsdecls instdecls tdecls fdecls ops) = do let usageerrors = checkDefaultRules prog unless (null usageerrors) $ do putStr (unlines $ "ERROR: ILLEGAL USE OF DEFAULT RULES:" : map (\ ((_,fn),err) -> fn ++ " (module " ++ mn ++ "): " ++ err) usageerrors) error "Transformation aborted" -- now we do not have to check the correct usage of default rules... unless (setFunMod `elem` imps) $ compileImportedModule verb setFunMod return $ if null deffuncs && null detfuncnames then Nothing else Just (detfuncnames, CurryProg mn newimports dfltdecl clsdecls instdecls tdecls newfdecls ops) where newimports = if setFunMod `elem` imps then imps else setFunMod:imps detfuncnames = map funcName (filter isDetFun fdecls) undetfuncs = concatMap (transDetFun detfuncnames) fdecls (deffuncs,funcs) = partition isDefaultFunc undetfuncs defrules = map func2rule deffuncs newfdecls = concatMap (transFDecl trscm defrules) funcs ------------------------------------------------------------------------ -- implementation of deterministic function transformation: -- Is the function declaration marked as a deterministic function? isDetFun :: CFuncDecl -> Bool isDetFun (CmtFunc _ qf ar vis texp rules) = isDetFun (CFunc qf ar vis texp rules) isDetFun (CFunc _ _ _ (CQualType _ texp) _) = hasDetResultType texp where hasDetResultType (CTVar _) = False hasDetResultType (CTCons _) = False hasDetResultType (CFuncType _ rt) = hasDetResultType rt hasDetResultType (CTApply tc _) = tc == CTCons (pre "DET") -- translate a function (where the names of all deterministic functions -- is provided as a first argument): transDetFun :: [QName] -> CFuncDecl -> [CFuncDecl] transDetFun detfnames (CmtFunc _ qf ar vis texp rules) = transDetFun detfnames (CFunc qf ar vis texp rules) transDetFun detfnames fdecl@(CFunc qf@(mn,fn) ar vis texp rules) | qf `elem` detfnames = [CFunc qf ar vis (removeDetResultType texp) [newdetrule], CFunc neworgname ar Private (removeDetResultType texp) rules] | isDefaultFunc fdecl && (mn, fromDefaultName fn) `elem` detfnames -- rename default rule of a deterministic function: = [CFunc (mn, fromDefaultName fn ++ orgsuffix ++ "'default") ar vis texp rules] | otherwise = [fdecl] where -- new name for original function (TODO: check for unused name) neworgname = (mn,fn++orgsuffix) orgsuffix = "_ORGNDFUN" newdetrule = CRule (map CPVar argvars) (CSimpleRhs (applyF (setFunMod, "selectValue") [applyF (setFunMod, "set"++show ar) (CSymbol neworgname : map CVar argvars)]) []) argvars = map (\i->(i,"x"++show i)) [1..ar] removeDetResultType :: CQualTypeExpr -> CQualTypeExpr removeDetResultType (CQualType clsctxt te) = CQualType clsctxt (removeDet te) where removeDet tv@(CTVar _) = tv removeDet tc@(CTCons _) = tc removeDet (CFuncType t1 t2) = CFuncType t1 (removeDet t2) removeDet t@(CTApply tc ta) = if tc == CTCons (pre "DET") then ta else t ------------------------------------------------------------------------ -- implementation of default rule transformation: -- Extract the arity and default rule for a default function definition: func2rule :: CFuncDecl -> (QName,(Int,CRule)) func2rule (CFunc (mn,fn) ar _ _ rules) = ((mn, fromDefaultName fn), (ar, head rules)) func2rule (CmtFunc _ qf ar vis texp rules) = func2rule (CFunc qf ar vis texp rules) -- Translates a function declaration into a new one that respects -- the potential default rule (the second argument contains -- the list of all default rules). transFDecl :: TransScheme -> [(QName,(Int,CRule))] -> CFuncDecl -> [CFuncDecl] transFDecl trscm defrules (CmtFunc _ qf ar vis texp rules) = transFDecl trscm defrules (CFunc qf ar vis texp rules) transFDecl trscm defrules fdecl@(CFunc qf@(mn,fn) ar vis texp rules) = maybe [fdecl] (\ (_,defrule) -> if trscm == SpecScheme then [CFunc neworgname ar Private texp rules, transFDecl2ApplyCond applyname fdecl, CFunc deffunname ar Private texp [transDefaultRule applyname ar defrule], CFunc qf ar vis texp [neworgrule_SpecScheme]] else -- trscm == NoDupScheme [transFDecl2FunRHS applyname fdecl, CFunc deffunname ar Private texp [defrule], CFunc qf ar vis texp [neworgrule_NoDupScheme]] ) (lookup qf defrules) where -- new names for auxiliary functions (TODO: check for unused name) neworgname = (mn,fn++"_ORGRULES") applyname = (mn,fn++"_APPLICABLE") deffunname = (mn,fn++"_DEFAULT") neworgrule_SpecScheme = CRule (map CPVar argvars) (CSimpleRhs (applyF (pre "?") [applyF neworgname (map CVar argvars), applyF deffunname (map CVar argvars)]) []) neworgrule_NoDupScheme = CRule (map CPVar argvars) (CSimpleRhs (CLetDecl [CLocalPat (CPVar (0,"x0")) (CSimpleRhs (applyF (setFunMod,"set"++show ar) (CSymbol applyname : map CVar argvars)) [])] (applyF (pre "if_then_else") [applyF (setFunMod,"isEmpty") [CVar (0,"x0")], applyF deffunname (map CVar argvars), applyF (setFunMod,"chooseValue") [CVar (0,"x0"), preUnit]])) []) argvars = map (\i->(i,"x"++show i)) [1..ar] -- Translates a function declaration into one where the right-hand side -- is always Prelude.(), i.e., it just checks for applicability. -- The first argument is the new name of the translated function. transFDecl2ApplyCond :: QName -> CFuncDecl -> CFuncDecl transFDecl2ApplyCond nqf (CmtFunc _ qf ar vis texp rules) = transFDecl2ApplyCond nqf (CFunc qf ar vis texp rules) transFDecl2ApplyCond nqf (CFunc _ ar _ texp rules) = CFunc nqf ar Private (adjustResultTypeToUnit texp) (map rule2cond rules) where rule2cond (CRule rpats (CSimpleRhs _ rlocals)) = let singlepatvars = extractSingles (concatMap varsOfPat rpats ++ concatMap varsOfLDecl rlocals) in CRule (map (anonymPat singlepatvars) rpats) (CSimpleRhs preUnit rlocals) rule2cond (CRule rpats (CGuardedRhs gds rlocals)) = let singlepatvars = extractSingles (concatMap varsOfPat rpats ++ concatMap (varsOfExp . fst) gds ++ concatMap varsOfLDecl rlocals) in CRule (map (anonymPat singlepatvars) rpats) (CGuardedRhs (map (\gd -> (fst gd,preUnit)) gds) rlocals) -- Adjust the result type of a function type by setting this type to (): adjustResultTypeToUnit :: CQualTypeExpr -> CQualTypeExpr adjustResultTypeToUnit (CQualType clsctxt te) = CQualType clsctxt (adjustRType te) where adjustRType texp = if texp == preUntyped then texp else case texp of CFuncType te1 te2 -> CFuncType te1 (adjustRType te2) _ -> unitType -- Translates a function declaration into one where the right-hand side -- is encapsulated in a unary function, i.e., it just checks for applicability -- and can later be applied to evaluate its right-hand side. -- The first argument is the new name of the translated function. transFDecl2FunRHS :: QName -> CFuncDecl -> CFuncDecl transFDecl2FunRHS nqf (CmtFunc _ qf ar vis texp rules) = transFDecl2FunRHS nqf (CFunc qf ar vis texp rules) transFDecl2FunRHS nqf (CFunc _ ar _ texp rules) = CFunc nqf ar Private (adjustResultTypeToFunRHS texp) (map rule2funrhs rules) where rule2funrhs (CRule rpats (CSimpleRhs rhsexp rlocals)) = CRule rpats (CSimpleRhs (CLambda [CPVar (999,"_")] rhsexp) rlocals) rule2funrhs (CRule rpats (CGuardedRhs gds rlocals)) = CRule rpats (CGuardedRhs (map (\ (gd,rhs) -> (gd,(CLambda [CPVar (999,"_")] rhs))) gds) rlocals) -- Adjust the result type of a function type by setting the result type -- `te` to `() -> texp`: adjustResultTypeToFunRHS :: CQualTypeExpr -> CQualTypeExpr adjustResultTypeToFunRHS (CQualType clsctxt te) = CQualType clsctxt (adjustRType te) where adjustRType texp = if texp == preUntyped then texp else case texp of CFuncType te1 te2 -> CFuncType te1 (adjustRType te2) _ -> CFuncType unitType texp transDefaultRule :: QName -> Int -> CRule -> CRule transDefaultRule _ _ (CRule _ (CGuardedRhs _ _)) = error "Cannot yet transform guarded default rules!" transDefaultRule condfunname ar (CRule pats (CSimpleRhs exp locals)) = CRule newpats (CGuardedRhs [(checkCond,exp)] locals) where checkCond = applyF (setFunMod,"isEmpty") [applyF (setFunMod,"set"++show ar) (CSymbol condfunname : args)] (newpats,args) = unzip (map arg2patexp (zip [1001..] pats)) arg2patexp (i,pat) = case pat of CPVar v -> if snd v=="_" then let newvar = (i,"patvar_"++show i) in (CPVar newvar, CVar newvar) else (pat, CVar v) CPAs asv _ -> (pat, CVar asv) _ -> let newvar = (i,"patvar_"++show i) in (CPAs newvar pat, CVar newvar) ------------------------------------------------------------------------ preUnit :: CExpr preUnit = CSymbol (pre "()") preUntyped :: CTypeExpr preUntyped = CTCons (pre "untyped") setFunMod :: String setFunMod = "Control.SetFunctions" --- Extracts all elements with a single occurrence in a given list. extractSingles :: Eq a => [a] -> [a] extractSingles [] = [] extractSingles (x:xs) = if null (filter (==x) xs) then x : extractSingles xs else extractSingles (filter (/=x) xs) --- Replaces all variables occurring in the first argument by --- anonymous variables in a pattern. anonymPat :: [(Int,String)] -> CPattern -> CPattern anonymPat vs (CPVar v) = CPVar (if v `elem` vs then (fst v,"_") else v) anonymPat _ (CPLit l) = CPLit l anonymPat vs (CPComb qc pats) = CPComb qc (map (anonymPat vs) pats) anonymPat vs (CPAs v pat) = if v `elem` vs then anonymPat vs pat else CPAs v (anonymPat vs pat) anonymPat vs (CPFuncComb qf pats) = CPFuncComb qf (map (anonymPat vs) pats) anonymPat vs (CPLazy pat) = CPLazy (anonymPat vs pat) anonymPat vs (CPRecord qc recpats) = CPRecord qc (map (\ (n,p) -> (n, anonymPat vs p)) recpats) ------------------------------------------------------------------------