0 | module Yaffle.REPL

  2 | import Core.AutoSearch

  3 | import Core.Env

  4 | import Core.Metadata

  5 | import Core.Termination

  6 | import Core.Unify

  8 | import Idris.REPL.Opts

  9 | import Idris.Syntax

 11 | import TTImp.Elab

 12 | import TTImp.Elab.Check

 13 | import TTImp.Interactive.ExprSearch

 14 | import TTImp.Interactive.GenerateDef

 15 | import TTImp.Parser

 16 | import TTImp.ProcessDecls

 17 | import TTImp.TTImp

 18 | import TTImp.Unelab

 20 | import Parser.Source

 22 | %default covering

 24 | showInfo : (Name, Int, GlobalDef) -> Core ()

 25 | showInfo (n, _, d)

 26 |     = coreLift_ $ putStrLn (show n ++ " ==>\n" ++

 27 |                    "\t" ++ show (definition d) ++ "\n" ++

 28 |                    "\t" ++ show (sizeChange d) ++ "\n")

 31 | process : {auto c : Ref Ctxt Defs} ->

 32 |           {auto m : Ref MD Metadata} ->

 33 |           {auto u : Ref UST UState} ->

 34 |           {auto s : Ref Syn SyntaxInfo} ->

 35 |           {auto o : Ref ROpts REPLOpts} ->

 36 |           ImpREPL -> Core Bool

 37 | process (Eval ttimp)

 38 |     = do (tm, _) <- elabTerm 0 InExpr [] (MkNested []) Env.empty ttimp Nothing

 39 |          defs <- get Ctxt

 40 |          tmnf <- normalise defs Env.empty tm

 41 |          coreLift_ (printLn !(unelab Env.empty tmnf))

 42 |          pure True

 43 | process (Check (IVar _ n))

 44 |     = do defs <- get Ctxt

 45 |          ns <- lookupTyName n (gamma defs)

 46 |          traverse_ printName ns

 47 |          pure True

 48 |   where

 49 |     printName : (Name, Int, ClosedTerm) -> Core ()

 50 |     printName (n, _, tyh)

 51 |         = do defs <- get Ctxt

 52 |              ty <- normaliseHoles defs Env.empty tyh

 53 |              coreLift_ $ putStrLn $ show n ++ " : " ++

 54 |                                     show !(unelab Env.empty ty)

 55 | process (Check ttimp)

 56 |     = do (tm, gty) <- elabTerm 0 InExpr [] (MkNested []) Env.empty ttimp Nothing

 57 |          defs <- get Ctxt

 58 |          tyh <- getTerm gty

 59 |          ty <- normaliseHoles defs Env.empty tyh

 60 |          coreLift_ (printLn !(unelab Env.empty ty))

 61 |          pure True

 62 | process (ProofSearch n_in)

 63 |     = do defs <- get Ctxt

 64 |          [(n, i, ty)] <- lookupTyName n_in (gamma defs)

 65 |               | ns => ambiguousName (justFC defaultFC) n_in (map fst ns)

 66 |          def <- search (justFC defaultFC) top False 1000 n ty Env.empty

 67 |          defs <- get Ctxt

 68 |          defnf <- normaliseHoles defs Env.empty def

 69 |          coreLift_ (printLn !(toFullNames defnf))

 70 |          pure True

 71 | process (ExprSearch n_in)

 72 |     = do defs <- get Ctxt

 73 |          [(n, i, ty)] <- lookupTyName n_in (gamma defs)

 74 |               | ns => ambiguousName (justFC defaultFC) n_in (map fst ns)

 75 |          results <- exprSearchN (justFC defaultFC) 1 n []

 76 |          traverse_ (coreLift . printLn) results

 77 |          pure True

 78 | process (GenerateDef line name)

 79 |     = do defs <- get Ctxt

 80 |          Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p)

 81 |               | Nothing => do coreLift_ (putStrLn ("Can't find declaration for " ++ show name))

 82 |                               pure True

 83 |          case !(lookupDefExact n' (gamma defs)) of

 84 |               Just None =>

 85 |                   catch

 86 |                     (do ((fc, cs) :: _) <- logTime 0 "Generation" $

 87 |                                 makeDefN (\p, n => onLine line p) 1 n'

 88 |                            | _ => coreLift_ (putStrLn "Failed")

 89 |                         coreLift_ $ putStrLn (show cs))

 90 |                     (\err => coreLift_ $ putStrLn $ "Can't find a definition for " ++ show n')

 91 |               Just _ => coreLift_ $ putStrLn "Already defined"

 92 |               Nothing => coreLift_ $ putStrLn $ "Can't find declaration for " ++ show name

 93 |          pure True

 94 | process (Missing n_in)

 95 |     = do defs <- get Ctxt

 96 |          case !(lookupCtxtName n_in (gamma defs)) of

 97 |               [] => undefinedName emptyFC n_in

 98 |               ts => do traverse_ (\fn =>

 99 |                           do tot <- getTotality emptyFC fn

100 |                              case isCovering tot of

101 |                                   MissingCases cs =>

102 |                                      coreLift_ (putStrLn (show fn ++ ":\n" ++

103 |                                                  showSep "\n" (map show cs)))

104 |                                   NonCoveringCall ns =>

105 |                                      coreLift_ (putStrLn

106 |                                          (show fn ++ ": Calls non covering function"

107 |                                            ++ case ns of

108 |                                                    [fn] => " " ++ show fn

109 |                                                    _ => "s: " ++ showSep ", " (map show ns)))

110 |                                   _ => coreLift_ $ putStrLn (show fn ++ ": All cases covered"))

111 |                         (map fst ts)

112 |                        pure True

113 | process (CheckTotal n)

114 |     = do defs <- get Ctxt

115 |          case !(lookupCtxtName n (gamma defs)) of

116 |               [] => undefinedName emptyFC n

117 |               ts => do traverse_ (\fn =>

118 |                           do ignore $ checkTotal emptyFC fn

119 |                              tot <- getTotality emptyFC fn

120 |                              coreLift_ (putStrLn (show fn ++ " is " ++ show tot)))

121 |                                (map fst ts)

122 |                        pure True

123 | process (DebugInfo n)

124 |     = do defs <- get Ctxt

125 |          traverse_ showInfo !(lookupCtxtName n (gamma defs))

126 |          pure True

127 | process Quit

128 |     = do coreLift_ $ putStrLn "Bye for now!"

129 |          pure False

131 | processCatch : {auto c : Ref Ctxt Defs} ->

132 |                {auto m : Ref MD Metadata} ->

133 |                {auto u : Ref UST UState} ->

134 |                {auto s : Ref Syn SyntaxInfo} ->

135 |                {auto o : Ref ROpts REPLOpts} ->

136 |                ImpREPL -> Core Bool

137 | processCatch cmd

138 |     = catch (process cmd)

139 |             (\err => do coreLift_ (putStrLn (show err))

140 |                         pure True)

143 | repl : {auto c : Ref Ctxt Defs} ->

144 |        {auto m : Ref MD Metadata} ->

145 |        {auto u : Ref UST UState} ->

146 |        {auto s : Ref Syn SyntaxInfo} ->

147 |        {auto o : Ref ROpts REPLOpts} ->

148 |        Core ()

150 |     = do coreLift_ (putStr "Yaffle> ")

151 |          inp <- coreLift getLine

152 |          case runParser (Virtual Interactive) Nothing inp command of

153 |               Left err => do coreLift_ (printLn err)

154 |                              repl

155 |               Right (_, _, cmd) => when !(processCatch cmd) repl