Something went wrong. Try again.
Newt - a dependent typed programming language
This is a mirror of the main github repository. newt.cloakedarrow.com
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788module Lib.ReplParserimport Preludeimport Lib.Parser.Implimport Lib.Parserimport Lib.Tokenimport Lib.Commonimport Data.List1data ReplCommand = Load String | OutputJS String | Verbose (Maybe Int) | GetDoc String | BrowseCmd QName | HelpCmdkw : String → Parser Stringkw s = satisfy (\t => t.val.text == s) "Expected \{show s}"replString : Parser StringreplString = do token StartQuote s <- token StringKind token EndQuote pure sreplInt : Parser IntreplInt = do t <- token Number pure $ stringToInt treplQN : Parser QNamereplQN = do ident <- uident rest <- many $ token Projection let name = joinBy "" (ident :: rest) let (ns,nm) = unsnoc $ splitBy1 name '.' pure $ QN (joinBy "." ns) nmdata ArgType = ArgNone | ArgString | ArgIdent | ArgOptInt | ArgQName0 argCon : ArgType → UargCon ArgNone = ReplCommandargCon ArgOptInt = Maybe Int → ReplCommandargCon ArgIdent = String → ReplCommandargCon ArgString = String → ReplCommandargCon ArgQName = QName → ReplCommanddata CmdDesc : U where MkCmd : String → String → (arg : ArgType) → argCon arg → CmdDesccommands : List CmdDesccommands = MkCmd ":h" "Show this help" ArgNone HelpCmd :: MkCmd ":help" "Show this help" ArgNone HelpCmd :: MkCmd ":l" "load file" ArgString Load :: MkCmd ":load" "load file" ArgString Load :: MkCmd ":o" "write javascript file" ArgString OutputJS :: MkCmd ":out" "write javascript file" ArgString OutputJS :: MkCmd ":v" "change verbosity" ArgOptInt Verbose :: MkCmd ":d" "document function" ArgIdent GetDoc :: MkCmd ":doc" "document function" ArgIdent GetDoc :: MkCmd ":b" "browse namespace" ArgQName BrowseCmd -- type at point -- solve hole -- search by prefix (for autocomplete - ideally include types at point, but we'd need recovery) -- Ideally we could auto-import too -- case split :: NilparseCommand : Parser ReplCommandparseCommand = do key <- ident let (Just cmd) = lookup key commands | _ => fail "Unknown command" the (Parser ReplCommand) $ case cmd of MkCmd _ _ ArgNone cstr => pure cstr MkCmd _ _ ArgOptInt cstr => cstr <$> optional replInt MkCmd _ _ ArgIdent cstr => cstr <$> (ident <|> uident) MkCmd _ _ ArgString cstr => cstr <$> replString MkCmd _ _ ArgQName cstr => cstr <$> replQN where lookup : String → List CmdDesc → Maybe CmdDesc lookup key (cmd@(MkCmd nm _ _ _) :: rest) = if key == nm then Just cmd else lookup key rest lookup key Nil = Nothing