From 96a643df2bc89276f100fe4366719342f93b4ccc Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sun, 25 Aug 2024 11:41:02 +0300 Subject: [PATCH] [ example ] Implement CLI options in the pil-fun example --- examples/pil-fun/pil-fun.ipkg | 1 + .../pil-fun/src/Language/PilFun/Pretty.idr | 8 + .../src/Language/PilFun/Pretty/Scala3.idr | 6 +- examples/pil-fun/src/Runner.idr | 140 ++++++++++++++++-- 4 files changed, 137 insertions(+), 18 deletions(-) diff --git a/examples/pil-fun/pil-fun.ipkg b/examples/pil-fun/pil-fun.ipkg index 8f2119842..29134011d 100644 --- a/examples/pil-fun/pil-fun.ipkg +++ b/examples/pil-fun/pil-fun.ipkg @@ -10,6 +10,7 @@ builddir = ".build" prebuild = "sh .derive-in-parallel" depends = deptycheck + , getopts , prettier executable = "pil-fun" diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index d581ae336..0d1d280b8 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -102,3 +102,11 @@ getExprs (sx: (indeed : Bool) -> Doc opts -> Doc opts -> Doc opts wrapBrIf False pre x = pre `vappend` indent' 2 x wrapBrIf True pre x = ifMultiline (pre <++> "{" <++> x <++> "}") (vsep [pre <++> "{", indent' 2 x, "}"]) + +public export +0 PP : Type +PP = {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames funs vars) => + (newNames : Gen0 String) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc opts diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr index 567a42d0d..b61fec4dc 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr @@ -170,9 +170,5 @@ printStmts fl tl $ Ret x = wrapMain {funs} {vars} fl tl Nothing $ printExpr Open printStmts fl tl $ Nop = wrapMain {funs} {vars} fl tl Nothing $ pure empty export -printScala3 : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => - (newNames : Gen0 String) => - Fuel -> - Stmts funs vars retTy -> Gen0 $ Doc opts +printScala3 : PP printScala3 fl = printStmts {names} {newNames} fl True diff --git a/examples/pil-fun/src/Runner.idr b/examples/pil-fun/src/Runner.idr index 7dc5aa9f6..4e8c1412b 100644 --- a/examples/pil-fun/src/Runner.idr +++ b/examples/pil-fun/src/Runner.idr @@ -2,6 +2,9 @@ module Runner import Data.Fuel import Data.List.Lazy +import Data.List1 +import Data.SortedMap +import Data.String import Language.PilFun.Derived import Language.PilFun.Pretty.Derived @@ -12,12 +15,110 @@ import Test.DepTyCheck.Gen import Text.PrettyPrint.Bernardy +import System +import System.GetOpts import System.Random.Pure.StdGen %default total -stdFuns : NamedCtxt -stdFuns = do +------------------- +--- CLI options --- +------------------- + +record Config where + constructor MkConfig + usedSeed : IO StdGen + layoutOpts : LayoutOpts + testsCnt : Nat + modelFuel : Fuel + ppFuel : Fuel + +defaultConfig : Config +defaultConfig = MkConfig + { usedSeed = initSeed + , layoutOpts = Opts 152 + , testsCnt = 10 + , modelFuel = limit 8 + , ppFuel = limit 1000000 + } + +parseSeed : String -> Either String $ Config -> Config +parseSeed str = do + let n1:::n2::[] = trim <$> split (== ',') str + | _ => Left "we expect two numbers divided by a comma" + let Just n1 = parsePositive n1 + | Nothing => Left "expected a positive number at the first component, given `\{n1}`" + let Just n2 = parsePositive {a=Bits64} n2 + | Nothing => Left "expected a positive number at the second component, given `\{n2}`" + let Yes prf = decSo $ testBit n2 0 + | No _ => Left "second component must be odd" + Right {usedSeed := pure $ rawStdGen n1 n2} + +parsePPWidth : String -> Either String $ Config -> Config +parsePPWidth str = case parsePositive str of + Just n => Right {layoutOpts := Opts n} + Nothing => Left "can't parse max width for the pretty-printer" + +parseTestsCount : String -> Either String $ Config -> Config +parseTestsCount str = case parsePositive str of + Just n => Right {testsCnt := n} + Nothing => Left "can't parse given count of tests" + +parseModelFuel : String -> Either String $ Config -> Config +parseModelFuel str = case parsePositive str of + Just n => Right {modelFuel := limit n} + Nothing => Left "can't parse given model fuel" + +parsePPFuel : String -> Either String $ Config -> Config +parsePPFuel str = case parsePositive str of + Just n => Right {ppFuel := limit n} + Nothing => Left "can't parse given pretty-printer fuel" + +cliOpts : List $ OptDescr $ Config -> Config +cliOpts = + [ MkOpt [] ["seed"] + (ReqArg' parseSeed ",") + "Sets particular random seed to start with." + , MkOpt ['w'] ["pp-width"] + (ReqArg' parsePPWidth "") + "Sets the max length for the pretty-printer." + , MkOpt ['n'] ["tests-count"] + (ReqArg' parseTestsCount "") + "Sets the count of tests to generate." + , MkOpt [] ["model-fuel"] + (ReqArg' parseModelFuel "") + "Sets how much fuel there is for generation of the model." + , MkOpt [] ["pp-fuel"] + (ReqArg' parsePPFuel "") + "Sets how much fuel there is for pretty-printing." + ] + +--------------- +--- Running --- +--------------- + +namesGen : Gen0 String +namesGen = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + +run : Config -> + NamedCtxt -> + (pp : PP) -> + IO () +run conf ctxt pp = do + seed <- conf.usedSeed + let vals = unGenTryN conf.testsCnt seed $ + genStmts conf.modelFuel ctxt.functions ctxt.variables Nothing >>= + pp @{ctxt.fvNames} @{namesGen} conf.ppFuel + Lazy.for_ vals $ \val => do + putStrLn "-------------------\n" + putStr $ render conf.layoutOpts val + +----------------------- +--- Language config --- +----------------------- + +scala3StdFuns : NamedCtxt +scala3StdFuns = do AddFun True "+" $ [< Int', Int'] ==> Just Int' AddFun True "<" $ [< Int', Int'] ==> Just Bool' AddFun True "<=" $ [< Int', Int'] ==> Just Bool' @@ -28,19 +129,32 @@ stdFuns = do AddFun False "Console.println" $ [< Int'] ==> Nothing Enough -prettyOpts : LayoutOpts -prettyOpts = Opts 152 +supportedLanguages : SortedMap String (NamedCtxt, PP) +supportedLanguages = fromList + [ ("scala3", scala3StdFuns, printScala3) + ] -namesGen : Gen0 String -namesGen = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) +--------------- +--- Startup --- +--------------- export main : IO () main = do - let modelFuel = limit 8 - let ppFuel = limit 1000000 - let vals = unGenTryN 10 someStdGen $ - genStmts modelFuel stdFuns.functions stdFuns.variables Nothing >>= printScala3 @{stdFuns.fvNames} @{namesGen} ppFuel - Lazy.for_ vals $ \val => do - putStrLn "///////////////////\n" - putStr $ render prettyOpts val + args <- getArgs + let usage : Lazy String := usageInfo "Usage: \{fromMaybe "pil-fun" $ head' args} [options] " cliOpts + let langs : Lazy String := joinBy ", " $ SortedSet.toList $ keySet supportedLanguages + let MkResult options nonOptions [] [] = getOpt Permute cliOpts $ drop 1 args + | MkResult {unrecognized=unrecOpts@(_::_), _} => if "help" `elem` unrecOpts + then putStrLn usage + else die "unrecodnised options \{show unrecOpts}\n\{usage}" + | MkResult {errors=es@(_::_), _} => die "arguments parse errors \{show es}\n\{usage}" + let [lang] = nonOptions + | [] => die "no language is given, supported languages: \{langs}\n\{usage}" + | many => die "too many languages are given\n\{usage}" + let Just (ctxt, pp) = lookup lang supportedLanguages + | Nothing => die "unknown language \{lang}, supported languages \{langs}\n\{usage}" + + let config = foldl (flip apply) defaultConfig options + + run config ctxt pp