Bring in more bits of IDE mode

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))) ' ')

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"
+

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)
+
+

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])
+

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

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} ->

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,