1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-15 01:52:11 +03:00
juvix/app/CommonOptions.hs

285 lines
7.7 KiB
Haskell
Raw Normal View History

2022-09-14 17:16:15 +03:00
-- | Contains common options reused in several commands.
module CommonOptions
( module CommonOptions,
module Juvix.Prelude,
module Options.Applicative,
)
where
import Control.Exception qualified as GHC
import Juvix.Compiler.Core.Data.TransformationId.Parser
2022-09-14 17:16:15 +03:00
import Juvix.Prelude
import Options.Applicative
import System.Process
import Text.Read (readMaybe)
2022-09-14 17:16:15 +03:00
import Prelude (show)
-- | Paths that are input are used to detect the root of the project.
2022-12-20 15:05:40 +03:00
data AppPath f = AppPath
{ _pathPath :: Prepath f,
2022-09-14 17:16:15 +03:00
_pathIsInput :: Bool
}
deriving stock (Data, Eq)
2022-09-14 17:16:15 +03:00
2022-12-20 15:05:40 +03:00
makeLenses ''AppPath
2022-09-14 17:16:15 +03:00
2022-12-20 15:05:40 +03:00
instance Show (AppPath f) where
show = Prelude.show . (^. pathPath)
2022-09-14 17:16:15 +03:00
2022-12-20 15:05:40 +03:00
parseInputJuvixFile :: Parser (AppPath File)
2022-09-14 17:16:15 +03:00
parseInputJuvixFile = do
_pathPath <-
argument
somePreFileOpt
2022-09-14 17:16:15 +03:00
( metavar "JUVIX_FILE"
<> help "Path to a .juvix file"
<> completer juvixCompleter
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = True, ..}
2022-09-14 17:16:15 +03:00
2022-12-20 15:05:40 +03:00
parseInputJuvixCoreFile :: Parser (AppPath File)
parseInputJuvixCoreFile = do
_pathPath <-
argument
somePreFileOpt
( metavar "JUVIX_CORE_FILE"
<> help "Path to a .jvc file"
<> completer juvixCoreCompleter
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = True, ..}
Add Geb Backend Evaluator with some extra subcommands (#1808) This PR introduces an evaluator for the Geb STLC interface/fragment and other related commands, including a REPL to interact with his backend. - https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp We have included a REPL and support for commands such as read and eval here. Check out: ``` juvix dev geb --help ``` - [x] Add Geb evaluator with the two basic eval strategies. - [x] Add quasi quoter: return morphisms from typed geb values. - [x] Add type/object inference for morphisms. - [x] All combined: morphisms-eval-to-morphisms - [x] Parse and pretty printer Geb values (without quoting them) - [x] Parse files containing Geb terms: - [x] Saved in a .lisp file according to anoma/geb example (typed object). - [x] Store in a .geb file simple as simple lisp expression. - [x] Add related commands to the CLI for `dev geb`: - [x] Subcommand: eval - [x] Subcommand: read - [x] Subcommand: infer - [x] Subcommand: repl - [x] Subcommand: check - [x] Minor changes `hom` by `!->` in the Geb prettyprinter - [x] Add tests for: - [x] New subcommand (smoke tests) - [x] Eval Issues to solve after merging this PR: - Add location to Geb ast for proper error location. - Add tests for all related subcommands, e.g. check, and infer. - Check compilation from Core to Geb: (run inferObject with the type provided by the core node). - [x] Update the vs code-plugin to load Geb repl and eval. (https://github.com/anoma/vscode-juvix/commit/31994c8684e9b44a62d58ac13304b9e04503410c)
2023-02-22 17:27:40 +03:00
parseInputJuvixGebFile :: Parser (AppPath File)
parseInputJuvixGebFile = do
_pathPath <-
argument
somePreFileOpt
Add Geb Backend Evaluator with some extra subcommands (#1808) This PR introduces an evaluator for the Geb STLC interface/fragment and other related commands, including a REPL to interact with his backend. - https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp We have included a REPL and support for commands such as read and eval here. Check out: ``` juvix dev geb --help ``` - [x] Add Geb evaluator with the two basic eval strategies. - [x] Add quasi quoter: return morphisms from typed geb values. - [x] Add type/object inference for morphisms. - [x] All combined: morphisms-eval-to-morphisms - [x] Parse and pretty printer Geb values (without quoting them) - [x] Parse files containing Geb terms: - [x] Saved in a .lisp file according to anoma/geb example (typed object). - [x] Store in a .geb file simple as simple lisp expression. - [x] Add related commands to the CLI for `dev geb`: - [x] Subcommand: eval - [x] Subcommand: read - [x] Subcommand: infer - [x] Subcommand: repl - [x] Subcommand: check - [x] Minor changes `hom` by `!->` in the Geb prettyprinter - [x] Add tests for: - [x] New subcommand (smoke tests) - [x] Eval Issues to solve after merging this PR: - Add location to Geb ast for proper error location. - Add tests for all related subcommands, e.g. check, and infer. - Check compilation from Core to Geb: (run inferObject with the type provided by the core node). - [x] Update the vs code-plugin to load Geb repl and eval. (https://github.com/anoma/vscode-juvix/commit/31994c8684e9b44a62d58ac13304b9e04503410c)
2023-02-22 17:27:40 +03:00
( metavar "JUVIX_GEB_FILE"
<> help "Path to a .geb or custom .lisp file"
<> completer juvixGebCompleter
<> completer juvixGebLispCompleter
)
pure AppPath {_pathIsInput = True, ..}
2022-12-20 15:05:40 +03:00
parseInputJuvixAsmFile :: Parser (AppPath File)
2022-09-29 18:44:55 +03:00
parseInputJuvixAsmFile = do
_pathPath <-
argument
somePreFileOpt
2022-09-29 18:44:55 +03:00
( metavar "JUVIX_ASM_FILE"
<> help "Path to a .jva file"
<> completer juvixAsmCompleter
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = True, ..}
2022-09-29 18:44:55 +03:00
2022-12-20 15:05:40 +03:00
parseInputCFile :: Parser (AppPath File)
2022-11-03 11:38:09 +03:00
parseInputCFile = do
_pathPath <-
argument
somePreFileOpt
2022-11-03 11:38:09 +03:00
( metavar "C_FILE"
<> help "Path to a .c file"
<> completer juvixCCompleter
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = True, ..}
2022-11-03 11:38:09 +03:00
parseGenericInputFile :: Parser (AppPath File)
parseGenericInputFile = do
_pathPath <-
argument
somePreFileOpt
( metavar "INPUT_FILE"
<> help "Path to input file"
<> action "file"
)
pure AppPath {_pathIsInput = True, ..}
2022-12-20 15:05:40 +03:00
parseGenericOutputFile :: Parser (AppPath File)
2022-09-14 17:16:15 +03:00
parseGenericOutputFile = do
_pathPath <-
option
somePreFileOpt
2022-09-14 17:16:15 +03:00
( long "output"
<> short 'o'
<> metavar "OUTPUT_FILE"
<> help "Path to output file"
<> action "file"
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = False, ..}
2022-09-14 17:16:15 +03:00
parseGenericOutputDir :: Mod OptionFields (Prepath Dir) -> Parser (AppPath Dir)
2022-09-14 17:16:15 +03:00
parseGenericOutputDir m = do
_pathPath <-
option
somePreDirOpt
2022-09-14 17:16:15 +03:00
( long "output-dir"
<> metavar "OUTPUT_DIR"
<> help "Path to output directory"
<> action "directory"
<> m
)
2022-12-20 15:05:40 +03:00
pure AppPath {_pathIsInput = False, ..}
somePreDirOpt :: ReadM (Prepath Dir)
somePreDirOpt = mkPrepath <$> str
somePreFileOpt :: ReadM (Prepath File)
somePreFileOpt = mkPrepath <$> str
2022-12-20 15:05:40 +03:00
someFileOpt :: ReadM (SomeBase File)
someFileOpt = eitherReader aux
where
aux :: String -> Either String (SomeBase File)
aux s = maybe (Left $ s <> " is not a file path") Right (parseSomeFile s)
someDirOpt :: ReadM (SomeBase Dir)
someDirOpt = eitherReader aux
where
aux :: String -> Either String (SomeBase Dir)
aux s = maybe (Left $ s <> " is not a directory path") Right (parseSomeDir s)
2022-09-14 17:16:15 +03:00
naturalNumberOpt :: ReadM Word
naturalNumberOpt = eitherReader aux
where
aux :: String -> Either String Word
aux s = maybe (Left $ s <> " is not a nonnegative number") Right (readMaybe s :: Maybe Word)
extCompleter :: String -> Completer
extCompleter ext = mkCompleter $ \word -> do
let cmd = unwords ["compgen", "-o", "plusdirs", "-f", "-X", "!*." <> ext, "--", requote word]
2022-09-14 17:16:15 +03:00
result <- GHC.try @GHC.SomeException $ readProcess "bash" ["-c", cmd] ""
return . lines . fromRight [] $ result
juvixCompleter :: Completer
juvixCompleter = extCompleter "juvix"
juvixCoreCompleter :: Completer
juvixCoreCompleter = extCompleter "jvc"
Add Geb Backend Evaluator with some extra subcommands (#1808) This PR introduces an evaluator for the Geb STLC interface/fragment and other related commands, including a REPL to interact with his backend. - https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp We have included a REPL and support for commands such as read and eval here. Check out: ``` juvix dev geb --help ``` - [x] Add Geb evaluator with the two basic eval strategies. - [x] Add quasi quoter: return morphisms from typed geb values. - [x] Add type/object inference for morphisms. - [x] All combined: morphisms-eval-to-morphisms - [x] Parse and pretty printer Geb values (without quoting them) - [x] Parse files containing Geb terms: - [x] Saved in a .lisp file according to anoma/geb example (typed object). - [x] Store in a .geb file simple as simple lisp expression. - [x] Add related commands to the CLI for `dev geb`: - [x] Subcommand: eval - [x] Subcommand: read - [x] Subcommand: infer - [x] Subcommand: repl - [x] Subcommand: check - [x] Minor changes `hom` by `!->` in the Geb prettyprinter - [x] Add tests for: - [x] New subcommand (smoke tests) - [x] Eval Issues to solve after merging this PR: - Add location to Geb ast for proper error location. - Add tests for all related subcommands, e.g. check, and infer. - Check compilation from Core to Geb: (run inferObject with the type provided by the core node). - [x] Update the vs code-plugin to load Geb repl and eval. (https://github.com/anoma/vscode-juvix/commit/31994c8684e9b44a62d58ac13304b9e04503410c)
2023-02-22 17:27:40 +03:00
juvixGebLispCompleter :: Completer
juvixGebLispCompleter = extCompleter "lisp"
juvixGebCompleter :: Completer
juvixGebCompleter = extCompleter "geb"
2022-09-29 18:44:55 +03:00
juvixAsmCompleter :: Completer
juvixAsmCompleter = extCompleter "jva"
2022-11-03 11:38:09 +03:00
juvixCCompleter :: Completer
juvixCCompleter = extCompleter "c"
2022-09-14 17:16:15 +03:00
requote :: String -> String
requote s =
let -- Bash doesn't appear to allow "mixed" escaping
-- in bash completions. So we don't have to really
-- worry about people swapping between strong and
-- weak quotes.
unescaped =
case s of
-- It's already strongly quoted, so we
-- can use it mostly as is, but we must
-- ensure it's closed off at the end and
-- there's no single quotes in the
-- middle which might confuse bash.
('\'' : rs) -> unescapeN rs
-- We're weakly quoted.
('"' : rs) -> unescapeD rs
-- We're not quoted at all.
-- We need to unescape some characters like
-- spaces and quotation marks.
elsewise -> unescapeU elsewise
in strong unescaped
where
strong :: String -> String
strong ss = '\'' : foldr go "'" ss
where
-- If there's a single quote inside the
-- command: exit from the strong quote and
-- emit it the quote escaped, then resume.
go '\'' t = "'\\''" ++ t
go h t = h : t
-- Unescape a strongly quoted string
-- We have two recursive functions, as we
-- can enter and exit the strong escaping.
unescapeN = goX
where
goX ('\'' : xs) = goN xs
goX (x : xs) = x : goX xs
goX [] = []
goN ('\\' : '\'' : xs) = '\'' : goN xs
goN ('\'' : xs) = goX xs
goN (x : xs) = x : goN xs
goN [] = []
-- Unescape an unquoted string
unescapeU = goX
where
goX [] = []
goX ('\\' : x : xs) = x : goX xs
goX (x : xs) = x : goX xs
-- Unescape a weakly quoted string
unescapeD = goX
where
-- Reached an escape character
goX ('\\' : x : xs)
-- If it's true escapable, strip the
-- slashes, as we're going to strong
-- escape instead.
| x `elem` ("$`\"\\\n" :: String) = x : goX xs
| otherwise = '\\' : x : goX xs
-- We've ended quoted section, so we
-- don't recurse on goX, it's done.
goX ('"' : xs) =
xs
-- Not done, but not a special character
-- just continue the fold.
goX (x : xs) =
x : goX xs
goX [] =
[]
optDeBruijn :: Parser Bool
optDeBruijn =
switch
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
optIdentIds :: Parser Bool
optIdentIds =
switch
( long "show-ident-ids"
<> help "Show identifier IDs"
)
optArgsNum :: Parser Bool
optArgsNum =
switch
( long "show-args-num"
<> help "Show identifier arguments number"
)
optNoDisambiguate :: Parser Bool
optNoDisambiguate =
switch
( long "no-disambiguate"
<> help "Don't disambiguate the names of bound variables"
)
optTransformationIds :: Parser [TransformationId]
optTransformationIds =
option
(eitherReader parseTransf)
( long "transforms"
<> short 't'
<> value []
<> metavar "[Transform]"
<> completer (mkCompleter (return . completionsString))
<> help "hint: use autocomplete"
)
where
parseTransf :: String -> Either String [TransformationId]
parseTransf = mapLeft unpack . parseTransformations . pack