0 | module Protocol.IDE.Command

  1 | import Protocol.SExp

  3 | %default total

  6 | public export

  7 | data DocMode = Overview | Full

  9 | public export

 10 | record Hints where

 11 |   constructor MkHints

 12 |   list : List String

 15 | SExpable Hints where

 16 |   toSExp hs = toSExp hs.list

 19 | FromSExpable Hints where

 20 |   fromSExp hs = MkHints <$> fromSExp hs

 22 | public export

 23 | data IDECommand

 24 |      = Interpret String

 25 |      | LoadFile String (Maybe Integer)

 26 |      | TypeOf String (Maybe (Integer, Integer))

 27 |      | NameAt String (Maybe (Integer, Integer))

 28 |      | CaseSplit Integer Integer String

 29 |      | AddClause Integer String

 30 |      -- deprecated: | AddProofClause

 31 |      | AddMissing Integer String

 32 |      | Intro Integer String -- line, hole name

 33 |      | Refine Integer String String -- line, hole name, expression

 34 |      | ExprSearch Integer String Hints Bool

 35 |      | ExprSearchNext

 36 |      | GenerateDef Integer String

 37 |      | GenerateDefNext

 38 |      | MakeLemma Integer String

 39 |      | MakeCase Integer String

 40 |      | MakeWith Integer String

 41 |      | DocsFor String (Maybe DocMode)

 42 |      | Directive String

 43 |      | Apropos String

 44 |      | Metavariables Integer

 45 |      | WhoCalls String

 46 |      | CallsWho String

 47 |      | BrowseNamespace String

 48 |      | NormaliseTerm     String -- TODO: implement a Binary lib

 49 |      | ShowTermImplicits String -- and implement Binary (Term)

 50 |      | HideTermImplicits String -- for these four defintions,

 51 |      | ElaborateTerm     String -- then change String to Term, as in idris1

 52 |      | PrintDefinition String

 53 |      | ReplCompletions String

 54 |      | EnableSyntax Bool

 55 |      | Version

 56 |      | GetOptions

 59 | getIDECommand : SExp -> Maybe IDECommand

 60 | getIDECommand (SExpList [SymbolAtom "interpret", StringAtom cmd])

 61 |     = Just $ Interpret cmd

 62 | getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname])

 63 |     = Just $ LoadFile fname Nothing

 64 | getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom l])

 65 |     = Just $ LoadFile fname (Just l)

 66 | getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n])

 67 |     = Just $ TypeOf n Nothing

 68 | getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n,

 69 |                          IntegerAtom l, IntegerAtom c])

 70 |     = Just $ TypeOf n (Just (l, c))

 71 | getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n])

 72 |     = Just $ NameAt n Nothing

 73 | getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n,

 74 |                          IntegerAtom l, IntegerAtom c])

 75 |     = Just $ NameAt n (Just (l, c))

 76 | getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c,

 77 |                          StringAtom n])

 78 |     = Just $ CaseSplit l c n

 79 | getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])

 80 |     = Just $ CaseSplit l 0 n

 81 | getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])

 82 |     = Just $ AddClause l n

 83 | getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])

 84 |     = Just $ AddMissing line n

 85 | getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])

 86 |     = Just $ ExprSearch l n (MkHints []) False

 87 | getIDECommand (SExpList [SymbolAtom "intro", IntegerAtom l, StringAtom h])

 88 |     = Just $ Intro l h

 89 | getIDECommand (SExpList [SymbolAtom "refine", IntegerAtom l, StringAtom h, StringAtom n])

 90 |     = Just $ Refine l h n

 91 | getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, hs])

 92 |     = (\hs' => ExprSearch l n hs' False) <$> fromSExp hs

 93 | getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, hs, SymbolAtom mode])

 94 |     = (\hs' => ExprSearch l n hs' (getMode mode)) <$> fromSExp hs

 95 |   where

 96 |     getMode : String -> Bool

 97 |     getMode m = m == "all"

 98 | getIDECommand (SymbolAtom "proof-search-next") = Just ExprSearchNext

 99 | getIDECommand (SExpList [SymbolAtom "generate-def", IntegerAtom l, StringAtom n])

100 |     = Just $ GenerateDef l n

101 | getIDECommand (SymbolAtom "generate-def-next") = Just GenerateDefNext

102 | getIDECommand (SExpList [SymbolAtom "make-lemma", IntegerAtom l, StringAtom n])

103 |     = Just $ MakeLemma l n

104 | getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])

105 |     = Just $ MakeCase l n

106 | getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])

107 |     = Just $ MakeWith l n

108 | getIDECommand (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))

109 |     = do -- Maybe monad

110 |          modeOpt <- case modeTail of

111 |                       []                      => Just Nothing

112 |                       [SymbolAtom "overview"] => Just $ Just Overview

113 |                       [SymbolAtom "full"    ] => Just $ Just Full

114 |                       _ => Nothing

115 |          Just $ DocsFor n modeOpt

116 | getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])

117 |     = Just $ Apropos n

118 | getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])

119 |     = Just $ Directive n

120 | getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])

121 |     = Just $ Metavariables n

122 | getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])

123 |     = Just $ WhoCalls n

124 | getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])

125 |     = Just $ CallsWho n

126 | getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])

127 |     = Just $ BrowseNamespace ns

128 | getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])

129 |     = Just $ NormaliseTerm     tm

130 | getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])

131 |     = Just $ ShowTermImplicits tm

132 | getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])

133 |     = Just $ HideTermImplicits tm

134 | getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])

135 |     = Just $ ElaborateTerm     tm

136 | getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])

137 |     = Just $ PrintDefinition n

138 | getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n])

139 |     = Just $ ReplCompletions n

140 | getIDECommand (SExpList [SymbolAtom "enable-syntax", BoolAtom b])

141 |     = Just $ EnableSyntax b

142 | getIDECommand (SymbolAtom "version") = Just Version

143 | getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions

144 | getIDECommand _ = Nothing

147 | FromSExpable IDECommand where

148 |   fromSExp = getIDECommand

150 | putIDECommand : IDECommand -> SExp

151 | putIDECommand (Interpret cmd)                 = (SExpList [SymbolAtom "interpret", StringAtom cmd])

152 | putIDECommand (LoadFile fname Nothing)        = (SExpList [SymbolAtom "load-file", StringAtom fname])

153 | putIDECommand (LoadFile fname (Just line))    = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line])

154 | putIDECommand (TypeOf cmd Nothing)            = (SExpList [SymbolAtom "type-of", StringAtom cmd])

155 | putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])

156 | putIDECommand (NameAt cmd Nothing)            = (SExpList [SymbolAtom "name-at", StringAtom cmd])

157 | putIDECommand (NameAt cmd (Just (line, col))) = (SExpList [SymbolAtom "name-at", StringAtom cmd, IntegerAtom line, IntegerAtom col])

158 | putIDECommand (CaseSplit line col n)          = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])

159 | putIDECommand (AddClause line n)              = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])

160 | putIDECommand (AddMissing line n)             = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])

161 | putIDECommand (Intro line hole)               = (SExpList [SymbolAtom "intro", IntegerAtom line, StringAtom hole])

162 | putIDECommand (Refine line hole name)         = (SExpList [SymbolAtom "refine", IntegerAtom line, StringAtom hole, StringAtom name])

163 | putIDECommand (ExprSearch line n hints mode)  = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, toSExp hints, getMode mode])

164 |   where

165 |   getMode : Bool -> SExp

166 |   getMode True  = SymbolAtom "all"

167 |   getMode False = SymbolAtom "other"

168 | putIDECommand ExprSearchNext                  = SymbolAtom "proof-search-next"

169 | putIDECommand (GenerateDef line n)            = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n])

170 | putIDECommand GenerateDefNext                 = SymbolAtom "generate-def-next"

171 | putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])

172 | putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])

173 | putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])

174 | putIDECommand (DocsFor n modeOpt)             = let modeTail = case modeOpt of

175 |                                                                  Nothing       => []

176 |                                                                  Just Overview => [SymbolAtom "overview"]

177 |                                                                  Just Full     => [SymbolAtom "full"] in

178 |                                                 (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))

179 | putIDECommand (Apropos n)                     = (SExpList [SymbolAtom "apropos", StringAtom n])

180 | putIDECommand (Metavariables n)               = (SExpList [SymbolAtom "metavariables", IntegerAtom n])

181 | putIDECommand (WhoCalls n)                    = (SExpList [SymbolAtom "who-calls", StringAtom n])

182 | putIDECommand (CallsWho n)                    = (SExpList [SymbolAtom "calls-who", StringAtom n])

183 | putIDECommand (BrowseNamespace ns)            = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])

184 | putIDECommand (NormaliseTerm     tm)          = (SExpList [SymbolAtom "normalise-term", StringAtom tm])

185 | putIDECommand (ShowTermImplicits tm)          = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])

186 | putIDECommand (HideTermImplicits tm)          = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])

187 | putIDECommand (ElaborateTerm     tm)          = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])

188 | putIDECommand (PrintDefinition n)             = (SExpList [SymbolAtom "print-definition", StringAtom n])

189 | putIDECommand (ReplCompletions n)             = (SExpList [SymbolAtom "repl-completions", StringAtom n])

190 | putIDECommand (Directive n)             = (SExpList [SymbolAtom "directive", StringAtom n])

191 | putIDECommand (EnableSyntax b)                = (SExpList [SymbolAtom "enable-syntax", BoolAtom b])

192 | putIDECommand GetOptions                      = (SExpList [SymbolAtom "get-options"])

193 | putIDECommand Version                         = SymbolAtom "version"

196 | SExpable IDECommand where

197 |   toSExp = putIDECommand