
   0 | module Protocol.SExp
   1 | 
   2 | import Data.List1
   3 | import Data.String
   4 | 
   5 | %default total
   6 | 
   7 | public export
   8 | data SExp = SExpList (List SExp)
   9 |           | StringAtom String
  10 |           | BoolAtom Bool
  11 |           | IntegerAtom Integer
  12 |           | SymbolAtom String
  13 | 
  14 | escape : String -> String
  15 | escape = pack . concatMap escapeChar . unpack
  16 |   where
  17 |     escapeChar : Char -> List Char
  18 |     escapeChar '\\' = ['\\', '\\']
  19 |     escapeChar '"'  = ['\\', '\"']
  20 |     escapeChar c    = [c]
  21 | 
  22 | export
  23 | Show SExp where
  24 |   show (SExpList xs) = assert_total $ "(" ++ joinBy " " (map show xs) ++ ")"
  25 |   show (StringAtom str) = "\"" ++ escape str ++ "\""
  26 |   show (BoolAtom b) = ":" ++ show b
  27 |   show (IntegerAtom i) = show i
  28 |   show (SymbolAtom s) = ":" ++ s
  29 | 
  30 | public export
  31 | interface SExpable a where
  32 |   toSExp : a -> SExp
  33 | 
  34 | -- TODO: Merge these into 1 interface later
  35 | public export
  36 | interface FromSExpable a where
  37 |   fromSExp : SExp -> Maybe a
  38 | 
  39 | export
  40 | SExpable SExp where
  41 |   toSExp = id
  42 | 
  43 | export
  44 | SExpable Bool where
  45 |   toSExp = BoolAtom
  46 | 
  47 | export
  48 | FromSExpable Bool where
  49 |   fromSExp (BoolAtom b) = Just b
  50 |   fromSExp _ = Nothing
  51 | 
  52 | export
  53 | SExpable String where
  54 |   toSExp = StringAtom
  55 | 
  56 | export
  57 | FromSExpable String where
  58 |   fromSExp (StringAtom s) = Just s
  59 |   fromSExp _ = Nothing
  60 | 
  61 | export
  62 | SExpable Integer where
  63 |   toSExp = IntegerAtom
  64 | 
  65 | export
  66 | FromSExpable Integer where
  67 |   fromSExp (IntegerAtom a) = Just a
  68 |   fromSExp _ = Nothing
  69 | 
  70 | export
  71 | SExpable Int where
  72 |   toSExp = IntegerAtom . cast
  73 | 
  74 | export
  75 | FromSExpable Int where
  76 |   fromSExp a = do Just $ cast {from = Integer }$ !(fromSExp a)
  77 | 
  78 | export
  79 | SExpable Nat where
  80 |   toSExp = IntegerAtom . cast
  81 | 
  82 | export
  83 | FromSExpable Nat where
  84 |   fromSExp a = do Just $ cast {from = Integer }$ !(fromSExp a)
  85 | 
  86 | export
  87 | (SExpable a, SExpable b) => SExpable (a, b) where
  88 |   toSExp (x, y)
  89 |       = case toSExp y of
  90 |              SExpList xs => SExpList (toSExp x :: xs)
  91 |              y' => SExpList [toSExp x, y']
  92 | 
  93 | export
  94 | (FromSExpable a, FromSExpable b) => FromSExpable (a, b) where
  95 |   fromSExp (SExpList xs) = case xs of
  96 |     [x,y] => do pure $ (!(fromSExp x), !(fromSExp y))
  97 |     (x :: xs) => do pure $ (!(fromSExp x), !(fromSExp $ SExpList xs))
  98 |     _ => Nothing
  99 |   fromSExp _ = Nothing
 100 | 
 101 | export
 102 | SExpable a => SExpable (List a) where
 103 |   toSExp xs
 104 |       = SExpList (map toSExp xs)
 105 | 
 106 | export
 107 | FromSExpable a => FromSExpable (List a) where
 108 |   fromSExp (SExpList sexps) = traverse fromSExp sexps
 109 |   fromSExp _ = Nothing
 110 | 
 111 | export
 112 | SExpable a => SExpable (List1 a) where
 113 |   toSExp xs
 114 |       = SExpList (map toSExp (toList xs))
 115 | 
 116 | export
 117 | FromSExpable a => FromSExpable (List1 a) where
 118 |   fromSExp (SExpList (sexp :: sexps)) = traverse fromSExp (sexp ::: sexps)
 119 |   fromSExp _ = Nothing
 120 | 
 121 | export
 122 | SExpable a => SExpable (Maybe a) where
 123 |   toSExp Nothing = SExpList []
 124 |   toSExp (Just x) = toSExp x
 125 |