0 | module Text.TOML.Internal.TStack
  1 |
  2 | import Data.Time.Time
  3 | import Data.SortedMap
  4 | import Derive.Prelude
  5 | import Text.ILex
  6 | import Text.TOML.Lexer
  7 | import Text.TOML.Types
  8 | import Syntax.T1
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Tree and Tables
 15 | --------------------------------------------------------------------------------
 16 |
 17 | public export
 18 | data Tag = New | Undef | Def | HDef
 19 |
 20 | %runElab derive "Tag" [Eq,Show,Ord]
 21 |
 22 | public export
 23 | data Tree : Type where
 24 |   TV : TomlValue -> Tree
 25 |   TT : Tag -> SortedMap String Tree -> Tree
 26 |   TA : SnocList (SortedMap String Tree) -> SortedMap String Tree -> Tree
 27 |
 28 | public export
 29 | 0 TreeTable : Type
 30 | TreeTable = SortedMap String Tree
 31 |
 32 | toVal : Tree -> TomlValue
 33 |
 34 | toArr : List TomlValue -> SnocList TreeTable -> TomlValue
 35 |
 36 | export
 37 | toTbl : TreeTable -> TomlTable
 38 | toTbl t = assert_total $ map toVal t
 39 |
 40 | toVal (TV v)    = v
 41 | toVal (TT x t)  = TTbl (toTbl t)
 42 | toVal (TA sx x) = toArr [TTbl $ toTbl x] sx
 43 |
 44 | toArr vs [<]     = TArr vs
 45 | toArr vs (st:<t) = toArr (TTbl (toTbl t) :: vs) st
 46 |
 47 | public export
 48 | data TView : Type -> Type where
 49 |   VR : TView t
 50 |   VT : TView t -> SortedMap String t -> Key -> Tag -> TView t
 51 |   VA : TView Tree -> TreeTable -> Key -> SnocList TreeTable -> TView Tree
 52 |
 53 | export
 54 | tagAsHDef : TView t -> TView t
 55 | tagAsHDef (VT v t k _) = VT v t k HDef
 56 | tagAsHDef v            = v
 57 |
 58 | keys : List Key -> TView t -> List Key
 59 | keys ks VR           = ks
 60 | keys ks (VT v _ k _) = keys (k::ks) v
 61 | keys ks (VA v _ k _) = keys (k::ks) v
 62 |
 63 | existsErr : (List Key -> TomlParseError) -> List Key -> TView t -> TErr
 64 | existsErr f add view =
 65 |  let ks := keys add view
 66 |   in B (Custom $ f ks) (foldMap bounds ks)
 67 |
 68 | export
 69 | exists : TomlValue -> List Key -> TView t -> TErr
 70 | exists (TArr _) = existsErr StaticArray
 71 | exists (TTbl _) = existsErr InlineTableExists
 72 | exists _        = existsErr ValueExists
 73 |
 74 | export
 75 | vexists : TView t -> TErr
 76 | vexists (VA v _ k _) = existsErr TableArray [k] v
 77 | vexists v            = existsErr TableExists [] v
 78 |
 79 | new : TView t -> List Key -> TView t
 80 | new v []        = v
 81 | new v (k :: ks) = new (VT v empty k New) ks
 82 |
 83 | export
 84 | view : TView Tree -> TreeTable -> List Key -> Either TErr (TView Tree,TreeTable)
 85 | view v t []      = Right (v,t)
 86 | view v t (k::ks) =
 87 |   case lookup k.key t of
 88 |     Nothing         => Right (new (VT v t k New) ks, empty)
 89 |     Just (TT tt t2) => view (VT v t k tt) t2 ks
 90 |     Just (TA st t2) => view (VA v t k st) t2 ks
 91 |     Just (TV val)   => Left $ exists val [k] v
 92 |
 93 | export
 94 | tview : TreeTable -> List Key -> Either TErr (TView Tree,TreeTable)
 95 | tview t ks =
 96 |   view VR t ks >>= \case
 97 |     (v@(VT _ _ _ x), t) => if x < Def then Right (v,t) else Left (vexists v)
 98 |     (v,t)               => Left (vexists v)
 99 |
100 | export
101 | reduceT : Tag -> TreeTable -> TView Tree -> TreeTable
102 | reduceT x t VR             = t
103 | reduceT x t (VT v t2 k y)  = reduceT x (insert k.key (TT (max x y) t) t2) v
104 | reduceT x t (VA v t2 k st) = reduceT x (insert k.key (TA st t) t2) v
105 |
106 | noHDef : TView a -> Either TErr ()
107 | noHDef VR              = Right ()
108 | noHDef v@(VT w _ _ x)  = if x < HDef then noHDef w else Left (vexists v)
109 | noHDef v@(VA {})       = Left (vexists v)
110 |
111 | export
112 | addVal : TreeTable -> SnocList Key -> TomlValue -> Either TErr TreeTable
113 | addVal t sk tv = do
114 |   (VT v t k New,_) <- view VR t (sk <>> []) | (v,_) => Left (vexists v)
115 |   noHDef v
116 |   Right $ reduceT Def (insert k.key (TV tv) t) v
117 |