0 | module Text.Show.Value

  2 | import Data.List1

  3 | import Data.Vect

  4 | import Derive.Prelude

  5 | import Text.Parse.Manual

  6 | import Text.PrettyPrint.Bernardy

  8 | %language ElabReflection

 10 | %default total

 13 | public export

 14 | record VName where

 15 |   constructor MkName

 16 |   unName : String

 18 | public export %inline

 19 | Cast (SnocList Char) VName where

 20 |   cast = MkName . cast

 22 | %runElab derive "VName" [Show,Eq,Ord,FromString,Semigroup,Monoid]

 24 | public export

 25 | Interpolation VName where interpolate (MkName n) = n

 27 | public export

 28 | Pretty VName where

 29 |   prettyPrec _ = line . unName

 40 | public export

 41 | data Value : Type where

 42 |   Con       : VName -> List Value -> Value

 43 |   InfixCons : Value -> List (VName,Value) -> Value

 44 |   Rec       : VName -> List (VName,Value) -> Value

 45 |   Tuple     : Value -> Value -> List Value -> Value

 46 |   Lst       : List Value -> Value

 47 |   Neg       : Value -> Value

 48 |   Natural   : String -> Value

 49 |   Dbl       : String -> Value

 50 |   Chr       : String -> Value

 51 |   Str       : String -> Value

 53 | %runElab derive "Value" [Show, Eq]

 58 | public export

 59 | binOp : VName -> Value -> Value -> Value

 60 | binOp op pvx pvy =

 61 |    case pvy of

 62 |      InfixCons pv1 pairs@((op2, pv2) :: xs) =>

 63 |        if op2 == op

 64 |           then InfixCons pvx ((op,pvy) :: pairs)

 65 |           else InfixCons pvx [(op,pvy)]

 66 |      _ => InfixCons pvx [(op,pvy)]

 68 | hidden : (Bool,Value)

 69 | hidden = (True, Con "_" [])

 71 | toVal : Bool -> Lazy Value -> (Bool,Value)

 72 | toVal True  _ = hidden

 73 | toVal False v = (False, v)

 75 | 0 V,VN : Type

 76 | V  = Value

 77 | VN = VName

 79 | parameters (collapse : Bool) (hide : VName -> Bool)

 81 |   -- the `Bool` flag is set to `True`, if the wrapped value

 82 |   -- was hidden and corresponds to `Con "_" []`.

 83 |   val : V -> (Bool,V)

 85 |   ops : Bool -> SnocList (VN,V) -> V -> List (VN,V) -> (Bool,V)

 86 |   ops h sv v0 []            = toVal h $ InfixCons v0 (sv <>> [])

 87 |   ops h sv v0 ((n,v) :: vs) =

 88 |     let (h2,w) := val v in ops (h && h2) (sv :< (n,w)) v0 vs

 90 |   hrec : Bool -> SnocList (VN,V) -> VN -> List (VN,V) -> (Bool,V)

 91 |   hrec h sv nm [] = toVal h $ Rec nm (sv <>> [])

 92 |   hrec h sv nm ((n,v) :: vs) = case val v of

 93 |     (False, w) => hrec False (sv :< (n,w)) nm vs

 94 |     (True,_)   => hrec h sv n vs

 96 |   hcon : Bool -> SnocList V -> VN -> List V -> (Bool,V)

 97 |   hcon h sv n [] = toVal h $ Con n (sv <>> [])

 98 |   hcon h sv n (v :: vs) = let (h2,w) := val v in hcon (h && h2) (sv :< w) n vs

100 |   lst : Bool -> SnocList V -> List V -> (Bool,V)

101 |   lst h sv [] = toVal h $ Lst (sv <>> [])

102 |   lst h sv (v :: vs) = let (h2,w) := val v in lst (h && h2) (sv :< w) vs

104 |   val (Con x xs) =

105 |     if hide x then hidden else hcon (isCons xs && collapse) [<] x xs

107 |   val (InfixCons v ps) =

108 |     if any (hide . fst) ps then hidden

109 |     else let (b,w) := val v in ops (b && collapse) [<] w ps

111 |   val (Rec x xs) =

112 |     if hide x then hidden else hrec (isCons xs && collapse) [<] x xs

114 |   val (Lst xs) = lst (isCons xs && collapse) [<] xs

116 |   val (Neg v) = let (b,w) := val v in (b,w)

118 |   val (Tuple v1 v2 vs) =

119 |     let (b1,w1)     := val v1

120 |         (b2,w2)     := val v2

121 |         (b3,Lst ws) := lst (b1 && b2 && collapse) [<] vs | _ => hidden

122 |      in toVal b3 $ Tuple w1 w2 ws

124 |   val (Natural x) = (False,Natural x)

125 |   val (Dbl x)     = (False,Dbl x)

126 |   val (Chr x)     = (False,Chr x)

127 |   val (Str x)     = (False,Str x)

129 |   ||| Hide constructors matching the given predicate.

135 |   export

136 |   hideCon : Value -> Value

137 |   hideCon = snd . val

143 | public export

144 | data Token : Type where

145 |   Lit    : Value -> Token

146 |   Id     : VName -> Token

147 |   Op     : VName -> Token

148 |   Symbol : Char -> Token

149 |   EOI    : Token

151 | %runElab derive "Token" [Show,Eq]

154 | Interpolation Token where

155 |   interpolate (Lit x)    = case x of

156 |     Con y []    => interpolate y

157 |     Rec y []    => interpolate y

158 |     Lst []      => "[]"

159 |     Natural str => str

160 |     Dbl str     => str

161 |     Chr str     => str

162 |     Str str     => str

163 |     x           => show x

164 |   interpolate (Id str)   = interpolate str

165 |   interpolate (Op str)   = interpolate str

166 |   interpolate (Symbol c) = show c

167 |   interpolate EOI        = "end of input"

169 | public export

170 | data Err : Type where

171 |   ExpectedId : Err

173 | %runElab derive "Err" [Show,Eq]

176 | Interpolation Err where

177 |   interpolate ExpectedId = "Expected an identifier"

179 | public export

180 | 0 PSErr : Type

181 | PSErr = InnerError Err

183 | public export %inline

184 | fromChar : Char -> Token

185 | fromChar = Symbol

187 | isIdentStart : Char -> Bool

188 | isIdentStart '_' = True

189 | isIdentStart  x  = isAlpha x

191 | isIdentTrailing : Char -> Bool

192 | isIdentTrailing '\'' = True

193 | isIdentTrailing '_'  = True

194 | isIdentTrailing x    = isAlphaNum x || x > chr 160

196 | ident : AutoShift False

197 | ident ('.'::x::t) = if isIdentStart x then ident t else Succ ('.'::x::t)

198 | ident (x :: t)    = if isIdentTrailing x then ident t else Succ (x::t)

199 | ident []          = Succ []

201 | opChars : List Char

202 | opChars = unpack ":!#$%&*+./<=>?@\\^|-~"

204 | %inline isOp : Char -> Bool

205 | isOp c = c `elem` opChars

207 | toOp : SnocList Char -> Token

208 | toOp [<'='] = '='

209 | toOp sc     = Op $ cast sc

211 | sfx :

212 |      (SnocList Char -> Token)

213 |   -> ShiftRes True [<] ts

214 |   -> LexRes True ts e Token

215 | sfx = suffix

217 | %inline nat,dbl :

218 |      ShiftRes  True [<] ts

219 |   -> LexRes True ts e Token

220 | nat = suffix (Lit . Natural . cast)

222 | dbl = suffix $ \sc =>

223 |   if all isDigit sc then Lit (Natural $ cast sc) else Lit (Dbl $ cast sc)

225 | strLit : AutoShift True

226 | strLit ('\\' :: x :: xs) = strLit {b} xs

227 | strLit ('"' :: xs)       = Succ xs

228 | strLit (x :: xs)         = strLit {b} xs

229 | strLit []                = eoiAt sh

231 | charLit : AutoShift True

232 | charLit ('\\' :: x :: xs) = charLit {b} xs

233 | charLit ('\'' :: xs)      = Succ xs

234 | charLit (x :: xs)         = charLit {b} xs

235 | charLit []                = eoiAt sh

237 | tok : Tok True e Token

238 | tok ('0' :: 'x' :: t) = nat $ takeWhile1 {b = True} isHexDigit t

239 | tok ('0' :: 'X' :: t) = nat $ takeWhile1 {b = True} isHexDigit t

240 | tok ('0' :: 'o' :: t) = nat $ takeWhile1 {b = True} isOctDigit t

241 | tok ('0' :: 'b' :: t) = nat $ takeWhile1 {b = True} isBinDigit t

242 | tok ('(' :: t)  = Succ '(' t

243 | tok (')' :: t)  = Succ ')' t

244 | tok ('{' :: t)  = Succ '{' t

245 | tok ('}' :: t)  = Succ '}' t

246 | tok ('[' :: t)  = Succ '[' t

247 | tok (']' :: t)  = Succ ']' t

248 | tok (',' :: t)  = Succ ',' t

249 | tok ('\'' :: t) = sfx (Lit . Chr . cast) $ charLit {b = True} t

250 | tok ('"'  :: t) = sfx (Lit . Str . cast) $ strLit {b = True} t

251 | tok (x :: t)  =

252 |   if      isOp x then sfx toOp $ takeWhile isOp t

253 |   else if isDigit x then dbl $ number [<] (x::t)

254 |   else if isIdentStart x then sfx (Id . cast) $ ident t

255 |   else unknown Same

256 | tok []         = eoiAt Same

258 | post :

259 |      List (Bounded Token)

260 |   -> SnocList (Bounded Token)

261 |   -> List (Bounded Token)

262 | post xs (sx :< B '(' c :< B (Op s) d :< B ')' e) = case sx of

263 |   sy :< B (Id n) a :< B (Op ".") b =>

264 |     post (B (Id $ MkName "\{n}.(\{s})") (a <+> b <+> c <+> d <+> e) :: xs) sy

265 |   _ => post (B (Id $ MkName "(\{s})") (c <+> d <+> e) :: xs) sx

266 | post xs (sx :< x) = post (x :: xs) sx

267 | post xs [<]       = xs

269 | go :

270 |      SnocList (Bounded Token)

271 |  -> (pos   : Position)

272 |  -> (cs    : List Char)

273 |  -> (0 acc : SuffixAcc cs)

274 |  -> Either (Bounded PSErr) (List (Bounded Token))

275 | go sx pos ('\n' :: xs) (SA r) = go sx (incLine pos) xs r

276 | go sx pos (x :: xs)    (SA r) =

277 |   if isSpace x

278 |      then go sx (incCol pos) xs r

279 |      else case tok (x::xs) of

280 |        Succ t xs' @{prf} =>

281 |          let pos2 := addCol (toNat prf) pos

282 |           in go (sx :< bounded t pos pos2) pos2 xs' r

283 |        Fail start errEnd r => Left $ boundedErr pos start errEnd r

284 | go sx pos [] _ = Right (post [B EOI $ oneChar pos] sx)

287 | tokens : String -> Either (Bounded PSErr) (List (Bounded Token))

288 | tokens s = go [<] begin (unpack s) suffixAcc

294 | toInfx : List (VName,Value) -> SnocList (VName,Value) -> Value -> Value

295 | toInfx xs (sx :< (n,v')) v = toInfx ((n,v) :: xs) sx v'

296 | toInfx [] [<] v = v

297 | toInfx ps [<] v = InfixCons v ps

299 | toTpl : List Value -> Value

300 | toTpl [] = Con "()" []

301 | toTpl (x :: []) = x

302 | toTpl (x :: (y :: xs)) = Tuple x y xs

304 | 0 Rule : Bool -> Type -> Type

305 | Rule b t =

306 |      (xs : List $ Bounded Token)

307 |   -> (0 acc : SuffixAcc xs)

308 |   -> Res b Token xs Err t

310 | list : Bounds -> SnocList Value -> Rule True Value

312 | tpl : Bounds -> SnocList Value -> Rule True Value

314 | rec : VName -> Bounds -> SnocList (VName,Value) -> Rule True Value

316 | infx : SnocList (VName,Value) -> Rule True Value

318 | args : VName -> SnocList Value -> Rule False Value

320 | value,single,applied : Rule True Value

322 | applied (B (Lit y) _ :: xs) _        = Succ0 y xs

323 | applied (B (Id y) _ :: xs) _         = Succ0 (Con y []) xs

324 | applied (B '[' _ :: B ']' _ :: xs) _ = Succ0 (Lst []) xs

325 | applied (B '[' b :: xs) (SA r)       = succT $ list b [<] xs r

326 | applied (B '(' _ :: B ')' _ :: xs) _ = Succ0 (Con "()" []) xs

327 | applied (B '(' b :: xs) (SA r)       = succT $ tpl b [<] xs r

328 | applied (x::xs) _                    = unexpected x

329 | applied [] _                         = eoi

331 | single (B (Op "-") _ :: xs) (SA r)                = succT $ map Neg (applied xs r)

332 | single (B (Id y) _ :: B '{' _ :: B '}' _ :: xs) _ = Succ0 (Rec y []) xs

333 | single (B (Id y) _ :: B '{' b :: xs) (SA r)       = succT $ rec y b [<] xs r

334 | single (B (Id y) _ :: xs) (SA r)                  = succT $ args y [<] xs r

335 | single xs sa                                      = applied xs sa

337 | value xs sa = infx [<] xs sa

339 | args n sv xs sa@(SA r) = case applied xs sa of

340 |   Succ0 v xs' => succF $ args n (sv :< v) xs' r

341 |   Fail0 _     => Succ0 (Con n $ sv <>> []) xs

343 | list b sv xs sa@(SA r) = case value xs sa of

344 |   Succ0 v (B ',' _ :: ys)  => succT $ list b (sv :< v) ys r

345 |   Succ0 v (B ']' _ :: ys)  => Succ0 (Lst $ sv <>> [v]) ys

346 |   res                      => failInParen b '[' res

348 | tpl b sv xs sa@(SA r) = case value xs sa of

349 |   Succ0 v (B ',' _ :: ys)  => succT $ tpl b (sv :< v) ys r

350 |   Succ0 v (B ')' _ :: ys)  => Succ0 (toTpl $ sv <>> [v]) ys

351 |   res                      => failInParen b '(' res

353 | infx sv xs sa@(SA r) = case single xs sa of

354 |   Succ0 v (B (Op n) _ :: ys) => succT $ infx (sv :< (n,v)) ys r

355 |   Succ0 v ys                 => Succ0 (toInfx [] sv v) ys

356 |   Fail0 err                  => Fail0 err

358 | rec n b sv (B (Id y) _ :: B '=' _ :: xs) (SA r) = case succT $ value xs r of

359 |   Succ0 v (B ',' _ :: ys) => succT $ rec n b (sv :< (y,v)) ys r

360 |   Succ0 v (B '}' _ :: ys) => Succ0 (Rec n $ sv <>> [(y,v)]) ys

361 |   res                     => failInParen b '{' res

362 | rec _ _ _ (B (Id _) _ ::x::xs) _ = expected x.bounds "=" "\{x.val}"

363 | rec _ _ _ (x::xs) _ = custom x.bounds ExpectedId

364 | rec _ _ _ [] _ = eoi

367 | parseValueE : String -> Either (ParseError Err) Value

368 | parseValueE str = case tokens str of

369 |   Left x   => Left $ toParseError Virtual str x

370 |   Right ts => case value ts suffixAcc of

371 |     Fail0 err           => Left $ toParseError Virtual str err

372 |     Succ0 res []        => Right res

373 |     Succ0 res [B EOI _] => Right res

374 |     Succ0 res (x :: xs) => leftErr Virtual str $ unexpected x

377 | parseValue : String -> Maybe Value

378 | parseValue = either (const Nothing) Just . parseValueE