
   0 | module Text.TOML.Parser
   1 | 
   2 | import Data.List1
   3 | import Data.SortedMap
   4 | import Text.Parse.Manual
   5 | import Text.Parse.Syntax
   6 | import Text.TOML.Lexer
   7 | import Text.TOML.Types
   8 | 
   9 | %default total
  10 | 
  11 | public export
  12 | data ElemType : Type where
  13 |   Table : TableType -> ElemType
  14 |   Array : ArrayType -> ElemType
  15 | 
  16 | public export
  17 | 0 ParentType : ElemType -> Type
  18 | ParentType (Table _) = TomlTable
  19 | ParentType (Array _) = SnocList TomlValue
  20 | 
  21 | ||| Key together with the a value and its type encountered in a
  22 | ||| TOML tree.
  23 | public export
  24 | record PathElem where
  25 |   constructor PE
  26 |   tpe    : ElemType
  27 |   parent : ParentType tpe
  28 |   key    : KeyToken
  29 | 
  30 | public export
  31 | record TOMLView where
  32 |   constructor TV
  33 |   path : SnocList PathElem
  34 |   cur  : Maybe TomlValue
  35 | 
  36 | keyErr :
  37 |      SnocList PathElem
  38 |   -> (List KeyToken -> TomlParseError)
  39 |   -> Either (Bounded TomlErr) a
  40 | keyErr sx f =
  41 |   let ks := map key (sx <>> [])
  42 |    in Left (B (Custom $ f ks) $ concatMap bounds ks)
  43 | 
  44 | public export
  45 | pth :
  46 |      SnocList PathElem
  47 |   -> List KeyToken
  48 |   -> Maybe TomlValue
  49 |   -> Either (Bounded TomlErr) TOMLView 
  50 | pth sx []        m = Right $ TV sx m
  51 | pth sx (x :: xs) m = case m of
  52 |   Nothing                 => pth (sx :< PE (Table None) empty x) xs Nothing
  53 |   Just (TTbl Inline _)    => keyErr sx InlineTableExists
  54 |   Just (TTbl tag t)       => pth (sx :< PE (Table tag) t x) xs (lookup x.key t)
  55 |   Just (TArr Static _)    => keyErr sx StaticArray
  56 |   Just (TArr tag sv)     => case sv of
  57 |     [<] => pth (sx :< PE (Array tag) [<TTbl None empty] x) xs Nothing
  58 |     (_ :< TTbl Inline _)  => keyErr sx InlineTableExists
  59 |     (_ :< TTbl tg t)      => pth (sx :< PE (Array tag) sv x) xs (lookup x.key t)
  60 |     _                     => keyErr sx ValueExists
  61 |   Just v                  => keyErr sx ValueExists
  62 | 
  63 | %inline
  64 | path : List KeyToken -> (root : TomlValue) -> Either (Bounded TomlErr) TOMLView
  65 | path xs root = pth [<] xs (Just root)
  66 | 
  67 | ins : SnocList PathElem -> TomlValue -> TomlValue
  68 | ins [<]                      v = v
  69 | ins (sx :< PE (Table x) t  k) v = ins sx (TTbl x $ insert k.key v t)
  70 | ins (sx :< PE (Array x) sv k) v = case sv of
  71 |   sy :< TTbl tag t => ins sx (TArr x $ sy :< (TTbl tag $ insert k.key v t))
  72 |   _                => ins sx (TArr x sv)
  73 | 
  74 | append : SnocList PathElem -> SnocList TomlValue -> TomlValue -> TomlValue
  75 | append p sx = ins p . TArr OfTables . (sx :<)
  76 | 
  77 | public export
  78 | tableAt :
  79 |      List1 KeyToken
  80 |   -> (root : TomlValue)
  81 |   -> Either (Bounded TomlErr) (SnocList PathElem, TomlValue)
  82 | tableAt xs root = case path (forget xs) root of
  83 |   Left err => Left err
  84 |   Right (TV path Nothing)                => Right (path, TTbl Table empty)
  85 |   Right (TV path (Just $ TTbl None t))   => Right (path, TTbl Table t)
  86 |   Right (TV path (Just $ TTbl Inline t)) => keyErr path InlineTableExists
  87 |   Right (TV path (Just $ TTbl Table t))  => keyErr path TableExists
  88 |   Right (TV path (Just x))               => keyErr path ValueExists
  89 | 
  90 | public export
  91 | arrayAt :
  92 |      List1 KeyToken
  93 |   -> (root : TomlValue)
  94 |   -> Either (Bounded TomlErr) (SnocList PathElem, SnocList TomlValue)
  95 | arrayAt xs root = case path (forget xs) root of
  96 |   Left err => Left err
  97 |   Right (TV path Nothing)                   => Right (path, [<])
  98 |   Right (TV path (Just $ TTbl _ t))         => keyErr path TableExists
  99 |   Right (TV path (Just $ TArr Static t))    => keyErr path StaticArray
 100 |   Right (TV path (Just $ TArr OfTables sv)) => Right (path, sv)
 101 |   Right (TV path (Just x))                  => keyErr path ValueExists
 102 | 
 103 | public export
 104 | tryInsert :
 105 |      List1 KeyToken
 106 |   -> (val,root : TomlValue)
 107 |   -> Either (Bounded TomlErr) TomlValue
 108 | tryInsert x val root = case path (forget x) root of
 109 |   Left y                  => Left y
 110 |   Right (TV path Nothing) => Right $ ins path val
 111 |   Right (TV path _)       => keyErr path ValueExists
 112 | 
 113 | public export
 114 | data TomlItem : Type where
 115 |   TableName : List1 KeyToken -> TomlItem
 116 |   ArrayName : List1 KeyToken -> TomlItem
 117 |   KeyVal    : List1 KeyToken -> TomlValue -> TomlItem
 118 | 
 119 | toTable : TomlValue -> TomlItem -> AccumRes TomlValue (Bounded TomlErr)
 120 | toTable root (KeyVal k v) = either Error Cont $ tryInsert k v root
 121 | toTable _    _            = Done
 122 | 
 123 | assemble :
 124 |      (top   : TomlValue)
 125 |   -> (items : List TomlItem)
 126 |   -> (0 acc : SuffixAcc items)
 127 |   -> Either (Bounded TomlErr) TomlValue
 128 | assemble top (x :: xs) (SA r) = case x of
 129 |   KeyVal k v =>
 130 |    let Right t1    := tryInsert k v top | Left err => Left err
 131 |        Succ0 t2 ys := accumErr t1 id toTable xs | Fail0 err => Left err
 132 |     in assemble t2 ys r
 133 |   TableName k =>
 134 |    let Right (p,t) := tableAt k top | Left e => Left e
 135 |        Succ0 t2 ys := accumErr t (ins p) toTable xs | Fail0 e => Left e
 136 |     in assemble t2 ys r
 137 |   ArrayName k =>
 138 |    let Right (p,sv) := arrayAt k top | Left e => Left e
 139 |        t            := TTbl Table empty
 140 |        Succ0 t2 ys  := accumErr t (append p sv) toTable xs | Fail0 e => Left e
 141 |     in assemble t2 ys r
 142 | assemble top []        _      = Right top
 143 | 
 144 | --------------------------------------------------------------------------------
 145 | --          TomlValue and Table
 146 | --------------------------------------------------------------------------------
 147 | 
 148 | -- facilitates pattern matching on and creating of symbol
 149 | -- tokens such as '['. We don't want to export this, as it tends
 150 | -- to interfer with regular `String` literals.
 151 | %inline
 152 | fromString : String -> TomlToken
 153 | fromString = TSym
 154 | 
 155 | 0 AccRule : Bool -> Type -> Type
 156 | AccRule b = AccGrammar b TomlToken TomlParseError
 157 | 
 158 | 0 Rule : Bool -> Type -> Type
 159 | Rule b = Grammar b TomlToken TomlParseError
 160 | 
 161 | array : Bounds -> SnocList TomlValue -> AccRule True TomlValue
 162 | 
 163 | table : Bounds -> TomlValue -> AccRule True TomlValue
 164 | 
 165 | value : AccRule True TomlValue
 166 | value (B (TVal v) _ :: xs)       _      = Succ0 v xs
 167 | value (B "[" _ :: B "]" _ :: xs) _      = Succ0 (TArr Static [<]) xs
 168 | value (B "{" _ :: B "}" _ :: xs) _      = Succ0 (TTbl Inline empty) xs
 169 | value (B "[" b :: xs)            (SA r) = succT $ array b [<] xs r
 170 | value (B "{" b :: xs)            (SA r) = succT $ table b (TTbl None empty) xs r
 171 | value xs                         _      = fail xs
 172 | 
 173 | array b sx xs acc@(SA r) = case value xs acc of 
 174 |   Succ0 v (B "," _ :: B "]" _ :: ys) => Succ0 (TArr Static $ sx :< v) ys
 175 |   Succ0 v (B "," _ :: ys)            => succT $ array b (sx :< v) ys r
 176 |   Succ0 v (B "]" _ :: ys)            => Succ0 (TArr Static $ sx :< v) ys
 177 |   res                                => failInParen b "[" res
 178 | 
 179 | key : Rule True (List1 KeyToken)
 180 | key = terminal $ \case TKey x => Just x; _ => Nothing
 181 | 
 182 | keyVal : AccRule True (List1 KeyToken,TomlValue)
 183 | keyVal (B (TKey x) _ :: B "=" _ :: xs) (SA r) = (x,) <$> succT (value xs r)
 184 | keyVal (B (TKey _) _ :: x :: xs)       _      = expected x.bounds "=" "\{x.val}"
 185 | keyVal xs                              _      = fail xs
 186 | 
 187 | inline : TomlValue -> TomlValue
 188 | inline (TTbl _ y) = TTbl Inline y
 189 | inline v          = v
 190 | 
 191 | table b tbl xs acc@(SA r) = case keyVal xs acc of 
 192 |   Succ0 (bk,v) ys => case fromEither {b = True} ys $ tryInsert bk v tbl of
 193 |     Succ0 tbl1 (B "," _ :: ys)            => succT $ table b tbl1 ys r
 194 |     Succ0 tbl1 (B "}" _ :: ys)            => Succ0 (inline tbl1) ys
 195 |     res                                   => failInParen b "{" res
 196 |   res => failInParen b "{" res
 197 | 
 198 | item : Rule True TomlItem
 199 | item (B "[" b1 :: xs)  = TableName <$> succT (before key "]" xs)
 200 | item (B "[[" b1 :: xs) = ArrayName <$> succT (before key "]]" xs)
 201 | item ts                = uncurry KeyVal <$> acc keyVal ts
 202 | 
 203 | items :
 204 |      SnocList TomlItem
 205 |   -> (ts : List $ Bounded TomlToken)
 206 |   -> (0 acc : SuffixAcc ts)
 207 |   -> Either (Bounded TomlErr) (List TomlItem)
 208 | items sx []             _      = Right $ sx <>> []
 209 | items sx (B NL _ :: xs) (SA r) = items sx xs r
 210 | items sx xs             (SA r) = case item xs of
 211 |   Succ0 i (B NL _ :: xs) => items (sx :< i) xs r
 212 |   Succ0 i (x::xs)        => unexpected x
 213 |   Succ0 i []             => Right (sx <>> [i])
 214 |   Fail0 err              => Left err
 215 | 
 216 | export
 217 | parse : Origin -> String -> Either (ParseError TomlParseError) TomlValue
 218 | parse o s = mapFst (toParseError o s) $ do
 219 |   ts <- lexToml s
 220 |   ti <- items [<] ts suffixAcc
 221 |   assemble (TTbl Table empty) ti suffixAcc
 222 |