From 8302fb08a7dcac1192aa6acd440752110f151c00 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 2 Jun 2019 15:38:39 +0100 Subject: [PATCH] Bring in more bits of IDE mode --- src/Idris/IDEMode/CaseSplit.idr | 178 ++++++++++++++++++++++++++ src/Idris/IDEMode/MakeClause.idr | 57 +++++++++ src/Idris/IDEMode/Parser.idr | 93 ++++++++++++++ src/Idris/IDEMode/TokenLine.idr | 50 ++++++++ src/TTImp/Interactive/CaseSplit.idr | 7 + src/TTImp/Interactive/GenerateDef.idr | 6 - yaffle.ipkg | 3 + 7 files changed, 388 insertions(+), 6 deletions(-) create mode 100644 src/Idris/IDEMode/CaseSplit.idr create mode 100644 src/Idris/IDEMode/MakeClause.idr create mode 100644 src/Idris/IDEMode/Parser.idr create mode 100644 src/Idris/IDEMode/TokenLine.idr diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr new file mode 100644 index 0000000..44b2af7 --- /dev/null +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -0,0 +1,178 @@ +module Idris.IDEMode.CaseSplit + +import Core.Context +import Core.Env +import Core.Metadata +import Core.TT +import Core.Value + +import TTImp.Interactive.CaseSplit +import TTImp.TTImp +import TTImp.Utils + +import Idris.IDEMode.TokenLine +import Idris.REPLOpts +import Idris.Resugar +import Idris.Syntax + +%default covering + +getLine : Nat -> List String -> Maybe String +getLine Z (l :: ls) = Just l +getLine (S k) (l :: ls) = getLine k ls +getLine _ [] = Nothing + +toStrUpdate : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + (Name, RawImp) -> Core (List (String, String)) +toStrUpdate (UN n, term) + = do clause <- pterm term + pure [(n, show (bracket clause))] + where + bracket : PTerm -> PTerm + bracket tm@(PRef _ _) = tm + bracket tm@(PList _ _) = tm + bracket tm@(PPair _ _ _) = tm + bracket tm@(PUnit _) = tm + bracket tm@(PComprehension _ _ _) = tm + bracket tm@(PPrimVal _ _) = tm + bracket tm = PBracketed emptyFC tm +toStrUpdate _ = pure [] -- can't replace non user names + +dump : SourcePart -> String +dump (Whitespace str) = str +dump (Name n) = n +dump (HoleName n) = "?" ++ n +dump LBrace = "{" +dump RBrace = "}" +dump Equal = "=" +dump (Other str) = str + +data UPD : Type where + +doUpdates : {auto u : Ref UPD (List String)} -> + Defs -> List (String, String) -> List SourcePart -> + Core (List SourcePart) +doUpdates defs ups [] = pure [] +doUpdates defs ups (LBrace :: xs) + = case dropSpace xs of + Name n :: RBrace :: rest => + pure (LBrace :: Name n :: + Whitespace " " :: Equal :: Whitespace " " :: + !(doUpdates defs ups (Name n :: RBrace :: rest))) + Name n :: Equal :: rest => + pure (LBrace :: Name n :: + Whitespace " " :: Equal :: Whitespace " " :: + !(doUpdates defs ups rest)) + _ => pure (LBrace :: !(doUpdates defs ups xs)) + where + dropSpace : List SourcePart -> List SourcePart + dropSpace [] = [] + dropSpace (RBrace :: xs) = RBrace :: xs + dropSpace (Whitespace _ :: xs) = dropSpace xs + dropSpace (x :: xs) = x :: dropSpace xs +doUpdates defs ups (Name n :: xs) + = case lookup n ups of + Nothing => pure (Name n :: !(doUpdates defs ups xs)) + Just up => pure (Other up :: !(doUpdates defs ups xs)) +doUpdates defs ups (HoleName n :: xs) + = do used <- get UPD + n' <- uniqueName defs used n + put UPD (n' :: used) + pure $ HoleName n' :: !(doUpdates defs ups xs) +doUpdates defs ups (x :: xs) + = pure $ x :: !(doUpdates defs ups xs) + +-- State here is a list of new hole names we generated (so as not to reuse any). +-- Update the token list with the string replacements for each match, and return +-- the newly generated strings. +updateAll : {auto u : Ref UPD (List String)} -> + Defs -> List SourcePart -> List (List (String, String)) -> + Core (List String) +updateAll defs l [] = pure [] +updateAll defs l (rs :: rss) + = do l' <- doUpdates defs rs l + rss' <- updateAll defs l rss + pure (concat (map dump l') :: rss') + +-- Turn the replacements we got from 'getSplits' into a list of actual string +-- replacements +getReplaces : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + List (Name, RawImp) -> Core (List (String, String)) +getReplaces updates + = do strups <- traverse toStrUpdate updates + pure (concat strups) + +showImpossible : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + RawImp -> Core String +showImpossible lhs + = do clause <- pterm lhs + pure (show clause ++ " impossible") + +-- Given a list of updates and a line and column, find the relevant line in +-- the source file and return the lines to replace it with +export +updateCase : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto o : Ref ROpts REPLOpts} -> + List ClauseUpdate -> Int -> Int -> + Core (List String) +updateCase splits line col + = do opts <- get ROpts + case mainfile opts of + Nothing => throw (InternalError "No file loaded") + Just f => + do Right file <- coreLift $ readFile f + | Left err => throw (FileErr f err) + let thisline = getLine (cast line) (lines file) + case thisline of + Nothing => throw (InternalError "File too short!") + Just l => + do let valid = mapMaybe getValid splits + let bad = mapMaybe getBad splits + if isNil valid + then traverse showImpossible bad + else do rs <- traverse getReplaces valid + let stok = tokens l + defs <- get Ctxt + u <- newRef UPD (the (List String) []) + updateAll defs stok rs + where + getValid : ClauseUpdate -> Maybe (List (Name, RawImp)) + getValid (Valid _ ups) = Just ups + getValid _ = Nothing + + getBad : ClauseUpdate -> Maybe RawImp + getBad (Impossible lhs) = Just lhs + getBad _ = Nothing + +fnName : Bool -> Name -> String +fnName lhs (UN n) + = if any (not . identChar) (unpack n) + then if lhs then "(" ++ n ++ ")" + else "op" + else n +fnName lhs (NS _ n) = fnName lhs n +fnName lhs (DN s _) = s +fnName lhs n = show n + + +export +getClause : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + Int -> Name -> Core (Maybe String) +getClause l n + = do defs <- get Ctxt + Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p) + | Nothing => pure Nothing + n <- getFullName nidx + argns <- getEnvArgNames defs envlen !(nf defs [] ty) + pure (Just (indent loc ++ fnName True n ++ concat (map (" " ++) argns) ++ + " = ?" ++ fnName False n ++ "_rhs")) + where + indent : FC -> String + indent fc = pack (replicate (cast (snd (startPos fc))) ' ') diff --git a/src/Idris/IDEMode/MakeClause.idr b/src/Idris/IDEMode/MakeClause.idr new file mode 100644 index 0000000..c989b9f --- /dev/null +++ b/src/Idris/IDEMode/MakeClause.idr @@ -0,0 +1,57 @@ +module Idris.IDEMode.MakeClause + +import Core.Name +import Parser.Lexer + +-- Implement make-with and make-case from the IDE mode + +isLit : String -> (Bool, String) +isLit str + = assert_total $ + if length str > 0 && strHead str == '>' + then (True, strTail str) + else (False, str) + +showRHSName : Name -> String +showRHSName n + = let fn = show (dropNS n) in + if any (flip elem (unpack opChars)) (unpack fn) + then "op" + else fn + +export +makeWith : Name -> String -> String +makeWith n srcline + = let (lit, src) = isLit srcline + isrc : (Nat, String) = + case span isSpace src of + (spc, rest) => (length spc, rest) + indent = fst isrc + src = snd isrc + lhs = pack (readLHS 0 (unpack src)) in + mkWithArg lit indent lhs ++ "\n" ++ + mkWithPat lit indent lhs ++ "\n" + where + readLHS : (brackets : Nat) -> List Char -> List Char + readLHS Z ('=' :: rest) = [] + readLHS n ('(' :: rest) = '(' :: readLHS (S n) rest + readLHS n ('{' :: rest) = '{' :: readLHS (S n) rest + readLHS n (')' :: rest) = ')' :: readLHS (pred n) rest + readLHS n ('}' :: rest) = '}' :: readLHS (pred n) rest + readLHS n (x :: rest) = x :: readLHS n rest + readLHS n [] = [] + + pref : Bool -> Nat -> String + pref l ind + = (if l then ">" else "") ++ + pack (replicate ind ' ') + + mkWithArg : Bool -> Nat -> String -> String + mkWithArg lit indent lhs + = pref lit indent ++ lhs ++ "with (_)" + + mkWithPat : Bool -> Nat -> String -> String + mkWithPat lit indent lhs + = pref lit (indent + 2) ++ lhs ++ "| with_pat = ?" ++ + showRHSName n ++ "_rhs" + diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr new file mode 100644 index 0000000..e1ea0fc --- /dev/null +++ b/src/Idris/IDEMode/Parser.idr @@ -0,0 +1,93 @@ +module Idris.IDEMode.Parser + +import Idris.IDEMode.Commands + +import Text.Parser +import Parser.Lexer +import Parser.Support +import Text.Lexer + +-- Slightly different lexer than the source language because we are more free +-- as to what can be identifiers, and fewer tokens are supported. But otherwise, +-- we can reuse the standard stuff + +%hide Lexer.symbols + +symbols : List String +symbols = ["(", ":", ")"] + +ident : Lexer +ident = pred startIdent <+> many (pred validIdent) + where + startIdent : Char -> Bool + startIdent '_' = True + startIdent x = isAlpha x + + validIdent : Char -> Bool + validIdent '_' = True + validIdent '-' = True + validIdent '\'' = True + validIdent x = isAlphaNum x + +ideTokens : TokenMap Token +ideTokens = + map (\x => (exact x, Symbol)) symbols ++ + [(digits, \x => Literal (cast x)), + (stringLit, \x => StrLit (stripQuotes x)), + (ident, Ident), + (space, Comment)] + where + stripQuotes : String -> String + -- ASSUMPTION! Only total because we know we're getting quoted strings. + stripQuotes = assert_total (strTail . reverse . strTail . reverse) + +idelex : String -> Either (Int, Int, String) (List (TokenData Token)) +idelex str + = case lex ideTokens str of + -- Add the EndInput token so that we'll have a line and column + -- number to read when storing spans in the file + (tok, (l, c, "")) => Right (filter notComment tok ++ + [MkToken l c EndInput]) + (_, fail) => Left fail + where + notComment : TokenData Token -> Bool + notComment t = case tok t of + Comment _ => False + _ => True + +sexp : Rule SExp +sexp + = do symbol ":"; exactIdent "True" + pure (BoolAtom True) + <|> do symbol ":"; exactIdent "False" + pure (BoolAtom False) + <|> do i <- intLit + pure (IntegerAtom i) + <|> do str <- strLit + pure (StringAtom str) + <|> do symbol ":"; x <- unqualifiedName + pure (SymbolAtom x) + <|> do symbol "(" + xs <- many sexp + symbol ")" + pure (SExpList xs) + +ideParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty +ideParser str p + = case idelex str of + Left err => Left $ LexFail err + Right toks => + case parse p toks of + Left (Error err []) => + Left $ ParseFail err Nothing [] + Left (Error err (t :: ts)) => + Left $ ParseFail err (Just (line t, col t)) + (map tok (t :: ts)) + Right (val, _) => Right val + +export +parseSExp : String -> Either ParseError SExp +parseSExp inp + = ideParser inp (do c <- sexp; eoi; pure c) + + diff --git a/src/Idris/IDEMode/TokenLine.idr b/src/Idris/IDEMode/TokenLine.idr new file mode 100644 index 0000000..33d9cfa --- /dev/null +++ b/src/Idris/IDEMode/TokenLine.idr @@ -0,0 +1,50 @@ +module Idris.IDEMode.TokenLine + +-- Tokenise a source line for easier processing + +import Text.Lexer + +public export +data SourcePart + = Whitespace String + | Name String + | HoleName String + | LBrace + | RBrace + | Equal + | Other String + +ident : Lexer +ident = pred startIdent <+> many (pred validIdent) + where + startIdent : Char -> Bool + startIdent '_' = True + startIdent x = isAlpha x + + validIdent : Char -> Bool + validIdent '_' = True + validIdent '\'' = True + validIdent x = isAlphaNum x + +holeIdent : Lexer +holeIdent = is '?' <+> ident + +srcTokens : TokenMap SourcePart +srcTokens = + [(ident, Name), + (holeIdent, \x => HoleName (assert_total (strTail x))), + (space, Whitespace), + (is '{', const LBrace), + (is '}', const RBrace), + (is '=', const Equal), + (any, Other)] + +export +tokens : String -> List SourcePart +tokens str + = case lex srcTokens str of + -- Add the EndInput token so that we'll have a line and column + -- number to read when storing spans in the file + (srctoks, (l, c, rest)) => + map tok srctoks ++ (if rest == "" then [] else [Other rest]) + diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 847ea03..5778107 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -149,6 +149,13 @@ getArgNames defs allvars env (NBind fc x (Pi _ p ty) sc) pure $ ns ++ !(getArgNames defs (map UN ns ++ allvars) env sc') getArgNames defs allvars env val = pure [] +export +getEnvArgNames : Defs -> Nat -> NF [] -> Core (List String) +getEnvArgNames defs Z sc = getArgNames defs [] [] sc +getEnvArgNames defs (S k) (NBind fc n _ sc) + = getEnvArgNames defs k !(sc defs (toClosure defaultOpts [] (Erased fc))) +getEnvArgNames defs n ty = pure [] + expandCon : {auto c : Ref Ctxt Defs} -> FC -> List Name -> Name -> Core RawImp expandCon fc usedvars con diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 8542911..fcafb3a 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -32,12 +32,6 @@ fnName lhs (NS _ n) = fnName lhs n fnName lhs (DN s _) = s fnName lhs n = show n -getEnvArgNames : Defs -> Nat -> NF [] -> Core (List String) -getEnvArgNames defs Z sc = getArgNames defs [] [] sc -getEnvArgNames defs (S k) (NBind fc n _ sc) - = getEnvArgNames defs k !(sc defs (toClosure defaultOpts [] (Erased fc))) -getEnvArgNames defs n ty = pure [] - expandClause : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> diff --git a/yaffle.ipkg b/yaffle.ipkg index 2afe335..18baba3 100644 --- a/yaffle.ipkg +++ b/yaffle.ipkg @@ -34,7 +34,10 @@ modules = Idris.Desugar, Idris.Error, + Idris.IDEMode.CaseSplit, Idris.IDEMode.Commands, + Idris.IDEMode.Parser, + Idris.IDEMode.TokenLine, Idris.Parser, Idris.REPLCommon, Idris.REPLOpts,