
  0 | module Text.WebIDL.Parser.Util
  1 | 
  2 | import public Data.Refined
  3 | import public Data.List.Elem
  4 | import public Text.Parse.Manual
  5 | import public Text.WebIDL.Types
  6 | import public Text.WebIDL.Lexer
  7 | 
  8 | export %inline
  9 | fromChar : Char -> IdlToken
 10 | fromChar c = Other $ Symb c
 11 | 
 12 | export %inline
 13 | fromString : (v : String) -> {auto 0 p : Holds IsKeyword v} -> IdlToken
 14 | fromString v = Key $ MkKeyword v p
 15 | 
 16 | public export
 17 | 0 AccRule : Bool -> Type -> Type
 18 | AccRule b a =
 19 |      (ts : List (Bounded IdlToken))
 20 |   -> (0 acc : SuffixAcc ts)
 21 |   -> Res b IdlToken ts IdlError a
 22 | 
 23 | public export
 24 | 0 Rule : Bool -> Type -> Type
 25 | Rule b a = (ts : List (Bounded IdlToken)) -> Res b IdlToken ts IdlError a
 26 | 
 27 | idlErr : Bounds -> IdlError -> Res b IdlToken ts IdlError a
 28 | idlErr b err = custom b err
 29 | 
 30 | public export
 31 | isOpen : IdlToken -> Bool
 32 | isOpen '(' = True
 33 | isOpen '[' = True
 34 | isOpen '{' = True
 35 | isOpen _   = False
 36 | 
 37 | public export
 38 | closes : IdlToken -> IdlToken -> Bool
 39 | ')' `closes` '(' = True
 40 | ']' `closes` '[' = True
 41 | '}' `closes` '{' = True
 42 | _   `closes` _   = False
 43 | 
 44 | public export
 45 | ident : Rule True Identifier
 46 | ident = terminal $ \case Ident i => Just i; _ => Nothing
 47 | 
 48 | public export %inline
 49 | inj :
 50 |       {0 a  : Type}
 51 |    -> {0 xs : List Type}
 52 |    -> Result0 b t ts e a
 53 |    -> {auto   p : Elem a xs}
 54 |    -> Result0 b t ts e (NS I xs)
 55 | inj r = map (\v => inject v) r
 56 |