
  0 | module Idris.IDEMode.MakeClause
  1 | 
  2 | import Core.Name
  3 | import Parser.Unlit
  4 | 
  5 | import Data.List
  6 | import Data.Nat
  7 | import Data.String
  8 | 
  9 | %default total
 10 | 
 11 | -- Implement make-with and make-case from the IDE mode
 12 | 
 13 | showRHSName : Name -> String
 14 | showRHSName n
 15 |     = let fn = show (dropNS n) in
 16 |           if any isOpChar (unpack fn)
 17 |              then "op"
 18 |              else fn
 19 | 
 20 | export
 21 | makeWith : Name -> String -> String
 22 | makeWith n srcline
 23 |     = let (markerM, src) = isLitLine srcline
 24 |           isrc : (Nat, String) =
 25 |              case span isSpace src of
 26 |                   (spc, rest) => (length spc, rest)
 27 |           indent = fst isrc
 28 |           src = snd isrc
 29 |           lhs = pack (readLHS 0 (unpack src)) in
 30 |           mkWithArg markerM indent lhs ++ "\n" ++
 31 |           mkWithPat markerM indent lhs
 32 |   where
 33 |     readLHS : (brackets : Nat) -> List Char -> List Char
 34 |     readLHS Z ('=' :: rest) = []
 35 |     readLHS n ('(' :: rest) = '(' :: readLHS (S n) rest
 36 |     readLHS n ('{' :: rest) = '{' :: readLHS (S n) rest
 37 |     readLHS n (')' :: rest) = ')' :: readLHS (pred n) rest
 38 |     readLHS n ('}' :: rest) = '}' :: readLHS (pred n) rest
 39 |     readLHS n (x :: rest) = x :: readLHS n rest
 40 |     readLHS n [] = []
 41 | 
 42 |     pref : Maybe String -> Nat -> String
 43 |     pref mark ind = relit mark $ pack (replicate ind ' ')
 44 | 
 45 |     mkWithArg : Maybe String -> Nat -> String -> String
 46 |     mkWithArg mark indent lhs
 47 |         = pref mark indent ++ lhs ++ "with (_)"
 48 | 
 49 |     mkWithPat : Maybe String -> Nat -> String -> String
 50 |     mkWithPat mark indent lhs
 51 |         = pref mark (indent + 2) ++ lhs ++ "| with_pat = ?" ++
 52 |               showRHSName n ++ "_rhs"
 53 | 
 54 | export
 55 | makeCase : Bool -> Name -> String -> String
 56 | makeCase brack n srcline
 57 |     = let capp = ("case _ of", "case_val => ?" ++ show n) in
 58 |           newLines capp
 59 |   where
 60 |     addBrackets : Bool -> String -> String
 61 |     addBrackets False str = str
 62 |     addBrackets True str = "(" ++ str ++ ")"
 63 | 
 64 |     addCase : Nat -> (String, String) -> String
 65 |     addCase n (c, pat)
 66 |         = addBrackets brack $ c ++ "\n" ++
 67 |               pack (replicate (n + (if brack then 6 else 5)) ' ') ++ pat
 68 | 
 69 |     replaceStr : Nat -> String -> (String, String) -> String -> String
 70 |     replaceStr indent rep new "" = ""
 71 |     replaceStr indent rep new str
 72 |         = if isPrefixOf rep str
 73 |              then addCase indent new ++ pack (drop (length rep) (unpack str))
 74 |              else assert_total $ strCons (prim__strHead str)
 75 |                           (replaceStr (1 + indent) rep new
 76 |                                       (prim__strTail str))
 77 | 
 78 |     newLines : (String, String) -> String
 79 |     newLines capp = replaceStr 0 ("?" ++ show n) capp srcline
 80 |