
   0 | -- SPDX-FileCopyrightText: 2022 The toml-idr developers
   1 | --
   2 | -- SPDX-License-Identifier: MPL-2.0
   3 | 
   4 | module Language.TOML.Processing
   5 | 
   6 | import Data.List.Elem
   7 | import Decidable.Equality
   8 | import Language.TOML.Value
   9 | 
  10 | export infixr 2 `And`
  11 | 
  12 | mutual
  13 |     public export
  14 |     data ValueTy
  15 |         = TString
  16 |         | TInteger
  17 |         | TFloat
  18 |         | TBoolean
  19 |         | TEnum (List String)
  20 |         | TArray ValueTy
  21 |         | TTable TableTy
  22 | 
  23 |     public export
  24 |     record FieldTy where
  25 |         constructor MkFieldTy
  26 |         name : String
  27 |         optional : Bool
  28 |         ty : ValueTy
  29 | 
  30 |     public export
  31 |     data TableTy : Type where
  32 |         Emp : TableTy
  33 |         Ext : (ft : FieldTy) -> (FieldOf ft -> TableTy) -> TableTy
  34 | 
  35 |     public export
  36 |     And : FieldTy -> TableTy -> TableTy
  37 |     And x y = Ext x (const y)
  38 | 
  39 |     public export
  40 |     ValueOf : ValueTy -> Type
  41 |     ValueOf TString    = String
  42 |     ValueOf TInteger   = Integer
  43 |     ValueOf TFloat     = Double
  44 |     ValueOf TBoolean   = Bool
  45 |     ValueOf (TEnum names) = (name ** Elem name names)
  46 |     ValueOf (TArray t) = List (ValueOf t)
  47 |     ValueOf (TTable x) = TableOf x
  48 | 
  49 |     public export
  50 |     FieldOf : FieldTy -> Type
  51 |     FieldOf x = (if x.optional then Maybe else id) (ValueOf x.ty)
  52 | 
  53 |     public export
  54 |     data TableOf : TableTy -> Type where
  55 |         Nil : TableOf Emp
  56 |         (::) : (x : FieldOf ft) -> TableOf (f x) -> TableOf (Ext ft f)
  57 | 
  58 | 
  59 | mutual
  60 |     public export
  61 |     data ValueError
  62 |         = ExpectedType ValueTy
  63 |         | InsideArray ValueError
  64 |         | InsideTable TableError
  65 |         | BadEnumVal String
  66 | 
  67 |     public export
  68 |     data TableError
  69 |         = FieldError String ValueError
  70 |         | ExpectedField String
  71 |         | UnexpectedFields (List String)
  72 | 
  73 | 
  74 | mutual
  75 |     public export
  76 |     processTable : (ty : TableTy) -> Table -> Either TableError (TableOf ty)
  77 |     processTable Emp x with (keys x)
  78 |       _ | [] = Right []
  79 |       _ | ks = Left $ UnexpectedFields ks
  80 |     processTable (Ext (MkFieldTy name optional ty) fields) x with (lookup name x)
  81 |       _ | Nothing = case optional of
  82 |                          True => Right $ Nothing :: !(processTable (fields Nothing) x)
  83 |                          False => Left $ ExpectedField name
  84 |       _ | Just val = do
  85 |               val' <- bimap (FieldError name) id $ processValue ty val
  86 |               let val'' = case optional of
  87 |                                True => Just val'
  88 |                                False => val'
  89 |               fields' <- processTable (fields val'') (delete name x)
  90 |               Right (val'' :: fields')
  91 | 
  92 |     public export
  93 |     processValue : (ty : ValueTy) -> Value -> Either ValueError (ValueOf ty)
  94 |     processValue (TEnum xs) (VString x) with (isElem x xs)
  95 |       _ | Yes el = Right (x ** el)
  96 |       _ | No nel = Left $ BadEnumVal x
  97 |     processValue TString    (VString x)  = Right x
  98 |     processValue TInteger   (VInteger x) = Right x
  99 |     processValue TFloat     (VFloat x)   = Right x
 100 |     processValue TBoolean   (VBoolean x) = Right x
 101 |     processValue (TArray t) (VArray xs)  = traverse (bimap InsideArray id . processValue t) xs
 102 |     processValue (TTable t) (VTable x)   = bimap InsideTable id $ processTable t x
 103 |     processValue t          v            = Left $ ExpectedType t
 104 |