Add sections to the language syntax
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
18d524a0d2
commit
fd301806c6
|
@ -1,11 +1,14 @@
|
|||
module Bergamot.Parser exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (Term(..), Metavariable(..))
|
||||
import Bergamot.Rules exposing (Rule, RuleEnv)
|
||||
import Bergamot.Rules exposing (Rule, Section, RuleEnv)
|
||||
import Bergamot.Utils exposing (decodeStr)
|
||||
|
||||
import Parser exposing (Parser, Trailing(..), (|.), (|=))
|
||||
import Set
|
||||
import Set exposing (Set)
|
||||
|
||||
reserved : Set String
|
||||
reserved = Set.fromList ["section"]
|
||||
|
||||
intLit : Parser Int
|
||||
intLit = Parser.int
|
||||
|
@ -35,7 +38,7 @@ name : Parser String
|
|||
name = Parser.variable
|
||||
{ start = \c -> Char.isAlpha c || c == '_'
|
||||
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||||
, reserved = Set.empty
|
||||
, reserved = reserved
|
||||
}
|
||||
|
||||
variable : Parser Metavariable
|
||||
|
@ -44,7 +47,7 @@ variable =
|
|||
|= Parser.variable
|
||||
{ start = \c -> c == '?'
|
||||
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||||
, reserved = Set.empty
|
||||
, reserved = reserved
|
||||
}
|
||||
|
||||
term : Parser (Term Metavariable)
|
||||
|
@ -97,16 +100,48 @@ rule =
|
|||
, item = term
|
||||
, trailing = Forbidden
|
||||
}
|
||||
|. Parser.spaces |. Parser.symbol ";"
|
||||
|
||||
rules : Parser (List Rule)
|
||||
rules = Parser.sequence
|
||||
{ start = ""
|
||||
, separator = ""
|
||||
, end = ""
|
||||
, spaces = Parser.spaces
|
||||
, item = rule
|
||||
, trailing = Optional
|
||||
}
|
||||
|
||||
sectionExp : Parser Section
|
||||
sectionExp =
|
||||
Parser.succeed (\n rs -> { name = n, rules = rs })
|
||||
|. Parser.symbol "section" |. Parser.spaces
|
||||
|= strLit |. Parser.spaces
|
||||
|. Parser.symbol "{" |. Parser.spaces
|
||||
|= rules
|
||||
|. Parser.symbol "}" |. Parser.spaces
|
||||
|
||||
sectionImp : Parser Section
|
||||
sectionImp =
|
||||
(\rs ->
|
||||
Parser.oneOf
|
||||
[ rule |> Parser.map (\r -> Parser.Loop <| r :: rs)
|
||||
, case rs of
|
||||
[] -> Parser.problem "empty implicit sections not allowed."
|
||||
_ -> Parser.succeed (Parser.Done <| List.reverse rs)
|
||||
])
|
||||
|> Parser.loop []
|
||||
|> Parser.map (\rs -> { name = "", rules = rs })
|
||||
|
||||
program : Parser RuleEnv
|
||||
program =
|
||||
Parser.succeed (\rs -> { rules = rs })
|
||||
Parser.succeed (\ss -> { sections = ss })
|
||||
|= Parser.sequence
|
||||
{ start = ""
|
||||
, separator = ";"
|
||||
, separator = ""
|
||||
, end = ""
|
||||
, spaces = Parser.spaces
|
||||
, item = rule
|
||||
, item = Parser.oneOf [sectionExp, sectionImp]
|
||||
, trailing = Mandatory
|
||||
}
|
||||
|. Parser.end
|
||||
|
|
|
@ -12,6 +12,11 @@ type alias Rule =
|
|||
, premises : List (Term Metavariable)
|
||||
}
|
||||
|
||||
type alias Section =
|
||||
{ name : String
|
||||
, rules : List Rule
|
||||
}
|
||||
|
||||
type ProofTree = MkProofTree
|
||||
{ name : String
|
||||
, conclusion : Term UnificationVar
|
||||
|
@ -19,7 +24,7 @@ type ProofTree = MkProofTree
|
|||
}
|
||||
|
||||
type alias RuleEnv =
|
||||
{ rules : List Rule
|
||||
{ sections : List Section
|
||||
}
|
||||
|
||||
type alias ProveState =
|
||||
|
@ -71,6 +76,9 @@ yield p env ps = Search.yield (p env ps)
|
|||
getEnv : Prover RuleEnv
|
||||
getEnv env ps = Search.pure (env, ps)
|
||||
|
||||
getRules : Prover (List Rule)
|
||||
getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps)
|
||||
|
||||
getUnificationState : Prover UnificationState
|
||||
getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
||||
|
||||
|
@ -164,8 +172,8 @@ proveTerm t =
|
|||
map (reify t) getUnificationState
|
||||
|> andThen (\tp ->
|
||||
burn
|
||||
|> andThen (\() -> getEnv)
|
||||
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp) env.rules))
|
||||
|> andThen (\() -> getRules)
|
||||
|> andThen (List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp)))
|
||||
|
||||
prove : Term Metavariable -> Prover ProofTree
|
||||
prove mt =
|
||||
|
|
|
@ -87,7 +87,7 @@ viewRules : String -> String -> Html Msg
|
|||
viewRules renderProgs progs = viewSection "Rendered Rules" <|
|
||||
Html.div [ class "bergamot-rule-list" ] <|
|
||||
case (run program renderProgs, run program progs) of
|
||||
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) prog.rules
|
||||
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) (List.concatMap .rules prog.sections)
|
||||
_ -> []
|
||||
|
||||
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
||||
|
|
Loading…
Reference in New Issue
Block a user