0 | module Protocol.IDE.Result
  1 |
  2 | import Protocol.SExp
  3 |
  4 | import Protocol.IDE.Holes
  5 | import Protocol.IDE.FileContext
  6 |
  7 | import Data.List1
  8 | import Data.Maybe
  9 |
 10 | %default total
 11 |
 12 | public export
 13 | data OptionType = BOOL | STRING | ATOM
 14 |
 15 | public export
 16 | (.sem) : OptionType -> Type
 17 | BOOL   .sem = Bool
 18 | STRING .sem = String
 19 | ATOM   .sem = String
 20 |
 21 | %unbound_implicits off
 22 | public export
 23 | record REPLOption where
 24 |   constructor MkOption
 25 |   name : String
 26 |   type : OptionType
 27 |   val  : type.sem
 28 | %unbound_implicits on
 29 |
 30 | sexpOptionVal : {type : OptionType} -> type.sem -> SExp
 31 | sexpOptionVal {type = BOOL  } = toSExp
 32 | sexpOptionVal {type = STRING} = toSExp
 33 | sexpOptionVal {type = ATOM  } = toSExp
 34 |
 35 | export
 36 | SExpable REPLOption where
 37 |   toSExp opt@(MkOption {}) = SExpList
 38 |     [ SymbolAtom opt.name
 39 |     , sexpOptionVal opt.val
 40 |     ]
 41 |
 42 | export
 43 | FromSExpable REPLOption where
 44 |   fromSExp (SExpList
 45 |     [ SymbolAtom name
 46 |     , val
 47 |     ]) = do
 48 |     let Nothing = fromSExp val
 49 |       | Just val => Just $ MkOption {name, type = BOOL, val}
 50 |     let Nothing = fromSExp val
 51 |       | Just val => Just $ MkOption {name, type = STRING, val}
 52 |     val <- fromSExp val
 53 |     Just $ MkOption {name, type = ATOM, val}
 54 |   fromSExp _ = Nothing
 55 |
 56 | public export
 57 | record MetaVarLemma where
 58 |   constructor MkMetaVarLemma
 59 |   application, lemma : String
 60 |
 61 | export
 62 | SExpable MetaVarLemma where
 63 |   toSExp mvl = SExpList [ SymbolAtom "metavariable-lemma"
 64 |              , SExpList [ SymbolAtom "replace-metavariable", StringAtom mvl.application ]
 65 |              , SExpList [ SymbolAtom "definition-type", StringAtom mvl.lemma ]
 66 |              ]
 67 |
 68 | export
 69 | FromSExpable MetaVarLemma where
 70 |   fromSExp (SExpList [ SymbolAtom "metavariable-lemma"
 71 |             , SExpList [ SymbolAtom "replace-metavariable", StringAtom application ]
 72 |             , SExpList [ SymbolAtom "definition-type", StringAtom lemma ]
 73 |             ]) = Just $ MkMetaVarLemma {application, lemma}
 74 |   fromSExp _ = Nothing
 75 |
 76 | public export
 77 | record IdrisVersion where
 78 |   constructor MkIdrisVersion
 79 |   major, minor, patch : Nat
 80 |   tag : Maybe String
 81 |
 82 | export
 83 | SExpable IdrisVersion where
 84 |   toSExp version = SExpList
 85 |     [ SExpList (map toSExp [version.major, version.minor, version.patch])
 86 |     , SExpList [StringAtom $ fromMaybe "" version.tag]
 87 |     ]
 88 |
 89 | export
 90 | FromSExpable IdrisVersion where
 91 |   fromSExp (SExpList
 92 |     [ SExpList [majorSExp, minorSExp, patchSExp]
 93 |     , SExpList [StringAtom tagSExp]
 94 |     ]) = do pure $ MkIdrisVersion
 95 |               { major = !(fromSExp majorSExp)
 96 |               , minor = !(fromSExp minorSExp)
 97 |               , patch = !(fromSExp patchSExp)
 98 |               , tag = case tagSExp of
 99 |                   "" => Nothing
100 |                   str => Just str}
101 |   fromSExp _ = Nothing
102 |
103 | public export
104 | data Result =
105 |     AString String
106 |   | AUnit
107 |   | AVersion IdrisVersion
108 |   | AMetaVarLemma MetaVarLemma
109 |   | ANameLocList (List (String, FileContext))
110 |   | AHoleList (List HoleData)
111 |   | ACompletionList (List String) String
112 |   | ANameList (List String)
113 |   | AnOptionList (List REPLOption)
114 |   | AnIntroList (List1 String)
115 |
116 | export
117 | SExpable Result where
118 |   toSExp (AString s) = toSExp s
119 |   toSExp (AUnit    ) = toSExp (the (List Int) [])
120 |   toSExp (AVersion version) = toSExp version
121 |   toSExp (AMetaVarLemma mvl) = toSExp mvl
122 |   toSExp (ANameLocList fcs) = toSExp fcs
123 |   toSExp (AHoleList holes) = toSExp holes
124 |   toSExp (ANameList names) = SExpList (map StringAtom names)
125 |   toSExp (ACompletionList names str) = SExpList [SExpList (map StringAtom names), StringAtom str]
126 |   toSExp (AnOptionList opts) = toSExp opts
127 |   toSExp (AnIntroList iss) = toSExp iss
128 |
129 | -- This code is not efficient. Usually the client knows what kind of
130 | -- result to expect based on the request it issued.
131 | export
132 | FromSExpable Result where
133 |   fromSExp (SExpList []) = Just AUnit -- resolve ambiguity somewhat arbitrarily...
134 |   fromSExp sexp = do
135 |   let Nothing = fromSExp sexp
136 |     | Just str => pure $ AString str
137 |   let Nothing = fromSExp sexp
138 |     | Just version => pure $ AVersion version
139 |   let Nothing = fromSExp sexp
140 |     | Just mvl => pure $ AMetaVarLemma mvl
141 |   let Nothing = fromSExp sexp
142 |     | Just nll => pure $ ANameLocList nll
143 |   let Nothing = fromSExp sexp
144 |     | Just hl => pure $ AHoleList hl
145 |   let Nothing = fromSExp sexp
146 |     | Just nl => pure $ ANameList nl
147 |   let Nothing = fromSExp sexp
148 |     | Just nlr => pure $ uncurry ACompletionList nlr
149 |   let Nothing = fromSExp sexp
150 |     | Just optl => pure $ AnOptionList optl
151 |   let Nothing = fromSExp sexp
152 |     | Just optl => pure $ AnIntroList optl
153 |   Nothing
154 |