60 lines
1.5 KiB
Elm
60 lines
1.5 KiB
Elm
|
module Bergamot.Parser exposing (..)
|
||
|
|
|
||
|
|
import Bergamot.Syntax exposing (Term(..), Metavariable)
|
||
|
|
import Bergamot.Rules exposing (Rule)
|
||
|
|
|
||
|
|
import Parser exposing (Parser, Trailing(..), (|.), (|=))
|
||
|
|
import Set
|
||
|
|
|
||
|
|
intLit : Parser Int
|
||
|
|
intLit = Parser.int
|
||
|
|
|
||
|
|
name : Parser String
|
||
|
|
name = Parser.variable
|
||
|
|
{ start = \c -> Char.isAlphaNum c || c == '_'
|
||
|
|
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||
|
|
, reserved = Set.empty
|
||
|
|
}
|
||
|
|
|
||
|
|
variable : Parser String
|
||
|
|
variable = Parser.variable
|
||
|
|
{ start = \c -> c == '?'
|
||
|
|
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||
|
|
, reserved = Set.empty
|
||
|
|
}
|
||
|
|
|
||
|
|
term : Parser (Term Metavariable)
|
||
|
|
term = Parser.lazy (\() -> Parser.oneOf
|
||
|
|
[ Parser.succeed IntLit |= intLit
|
||
|
|
, Parser.succeed Call
|
||
|
|
|= name
|
||
|
|
|= Parser.sequence
|
||
|
|
{ start = "("
|
||
|
|
, separator = ","
|
||
|
|
, end = ")"
|
||
|
|
, spaces = Parser.spaces
|
||
|
|
, item = term
|
||
|
|
, trailing = Forbidden
|
||
|
|
}
|
||
|
|
, Parser.succeed Var |= variable
|
||
|
|
])
|
||
|
|
|
||
|
|
rule : Parser Rule
|
||
|
|
rule =
|
||
|
|
let
|
||
|
|
makeRule n c ps = { name = n, conclusion = c, premises = ps }
|
||
|
|
in
|
||
|
|
Parser.succeed makeRule
|
||
|
|
|= name
|
||
|
|
|. Parser.spaces |. Parser.symbol "@" |. Parser.spaces
|
||
|
|
|= term
|
||
|
|
|. Parser.spaces |. Parser.symbol "<-" |. Parser.spaces
|
||
|
|
|= Parser.sequence
|
||
|
|
{ start = ""
|
||
|
|
, separator = ","
|
||
|
|
, end = ""
|
||
|
|
, spaces = Parser.spaces
|
||
|
|
, item = term
|
||
|
|
, trailing = Forbidden
|
||
|
|
}
|