[ example ] Implement CLI options in the pil-fun example

examples/pil-fun/pil-fun.ipkg

@@ -10,6 +10,7 @@ builddir = ".build"
 prebuild = "sh .derive-in-parallel"
 
 depends = deptycheck
+        , getopts
         , prettier
 
 executable = "pil-fun"

examples/pil-fun/src/Language/PilFun/Pretty.idr

@@ -102,3 +102,11 @@ getExprs (sx:<x) = getExprs sx :< Evidence _ x
 wrapBrIf : {opts : _} -> (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

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

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 "<seed>,<gamma>")
+      "Sets particular random seed to start with."
+  , MkOpt ['w'] ["pp-width"]
+      (ReqArg' parsePPWidth "<nat>")
+      "Sets the max length for the pretty-printer."
+  , MkOpt ['n'] ["tests-count"]
+      (ReqArg' parseTestsCount "<tests-count>")
+      "Sets the count of tests to generate."
+  , MkOpt [] ["model-fuel"]
+      (ReqArg' parseModelFuel "<fuel>")
+      "Sets how much fuel there is for generation of the model."
+  , MkOpt [] ["pp-fuel"]
+      (ReqArg' parsePPFuel "<fuel>")
+      "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] <language>" 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