Compare commits

..

7 Commits

Author SHA1 Message Date
abd6a848f8 Add support for editing the meta rules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 16:57:46 -08:00
535c714b47 Remove yields and switch to depth-based gas.
This considerably speeds up forward inference, but we do get lost when
trying to prove more difficult things, or doing backwards search.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 16:47:56 -08:00
363e52ec5e Switch entirely to using rules to render rules.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 14:45:04 -08:00
84c79ddb50 Render sections in widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 14:06:37 -08:00
678e51f146 Allow implicit sections to have more than one rule
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 14:06:10 -08:00
401883c1da Update the object language parser to use 'number' and 'string'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 14:05:03 -08:00
fd301806c6 Add sections to the language syntax
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 13:31:53 -08:00
5 changed files with 127 additions and 76 deletions

View File

@ -22,51 +22,45 @@ renderTermViaRules env t =
Call "latex" [_, StringLit s] -> Just s
_ -> Nothing)
buildInferenceRuleFrac : List String -> String -> String -> String
buildInferenceRuleFrac prems conc name = String.concat
[ "\\cfrac{"
, String.join "\\quad " prems
, "}{"
, conc
, "}\\ \\texttt{"
, name
, "}"
]
renderRuleViaRules : RuleEnv -> Rule -> Maybe String
renderRuleViaRules env r =
let
quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises
quotedConc = Syntax.andThen quoteMetavariable r.conclusion
buildStr conc prems = String.concat
[ "\\cfrac{"
, String.join "\\quad " prems
, "}{"
, conc
, "}\\ \\texttt{"
, r.name
, "}"
]
quotedPrems = List.map quoteMetavariables r.premises
quotedConc = quoteMetavariables r.conclusion
in
renderTermViaRules env quotedConc
|> Maybe.andThen (\conc ->
sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
|> Maybe.map (\prems -> buildStr conc prems))
|> Maybe.map (\prems -> buildInferenceRuleFrac prems conc r.name))
quoteMetavariable : Metavariable -> Term Void
quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v]
renderTreeViaRules : RuleEnv -> ProofTree -> Maybe String
renderTreeViaRules env (MkProofTree node) =
renderTermViaRules env (quoteVariables node.conclusion)
|> Maybe.andThen (\conc ->
sequenceMaybes (List.map (renderTreeViaRules env) node.premises)
|> Maybe.map (\prems -> buildInferenceRuleFrac prems conc node.name))
termToLatex : (a -> String) -> Term a -> String
termToLatex f t =
case t of
Call "intlit" [t1] -> termToLatex f t1
Call "strlit" [t1] -> termToLatex f t1
Call "var" [t1] -> termToLatex f t1
Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3
Call "empty" [] -> "\\varnothing"
Call s [] -> "\\text{" ++ s ++ "}"
Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
Var x -> f x
IntLit i -> String.fromInt i
StringLit s -> "\\texttt{" ++ "\"" ++ encodeLatex (encodeStr s) ++ "\"" ++ "}"
quote : String -> (a -> String) -> Term a -> Term Void
quote s f =
let helper a = Call s [StringLit <| f a]
in Syntax.andThen helper
quoteMetavariables : Term Metavariable -> Term Void
quoteMetavariables = quote "metavariable" metavariableToLatex
quoteVariables : Term UnificationVar -> Term Void
quoteVariables = quote "variable" (\(MkUnificationVar v) -> v)
metavariableToLatex : Metavariable -> String
metavariableToLatex (MkMetavariable s) =
@ -75,12 +69,3 @@ metavariableToLatex (MkMetavariable s) =
in
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
ruleToLatex : Rule -> String
ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
unificationVarToLatex : UnificationVar -> String
unificationVarToLatex (MkUnificationVar s) = s
proofTreeToLatex : ProofTree -> String
proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"

View File

@ -52,8 +52,8 @@ parseType = Parser.lazy <| \() -> Parser.oneOf
parseTypeBasic : Parser Type
parseTypeBasic = Parser.lazy <| \() -> Parser.oneOf
[ Parser.succeed TInt |. Parser.keyword "tint"
, Parser.succeed TStr |. Parser.keyword "tstr"
[ Parser.succeed TInt |. Parser.keyword "number"
, Parser.succeed TStr |. Parser.keyword "string"
, Parser.backtrackable <| Parser.map (\(a, b) -> TPair a b) <| parsePair parseType
, parseParenthed parseType
]
@ -125,8 +125,8 @@ parseExprBasic = Parser.lazy <| \() -> Parser.oneOf
typeToTerm : Type -> Syntax.Term Metavariable
typeToTerm t =
case t of
TInt -> Syntax.Call "tint" []
TStr -> Syntax.Call "tstr" []
TInt -> Syntax.Call "number" []
TStr -> Syntax.Call "string" []
TPair t1 t2 -> Syntax.Call "tpair" [ typeToTerm t1, typeToTerm t2 ]
TArr t1 t2 -> Syntax.Call "tarr" [ typeToTerm t1, typeToTerm t2 ]

View File

@ -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 ";" |. Parser.spaces
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

View File

@ -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,11 +76,14 @@ 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)
burn : Prover ()
burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail
burn : Prover a -> Prover a
burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
liftInstantiation f a env ps =
@ -163,9 +171,9 @@ proveTerm : Term UnificationVar -> Prover ProofTree
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))
burn (
getRules
|> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp))))
prove : Term Metavariable -> Prover ProofTree
prove mt =
@ -174,6 +182,6 @@ prove mt =
single : RuleEnv -> Prover a -> Maybe a
single env p =
p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 30 }
|> Search.one
|> Maybe.map (Tuple.first << Tuple.first)

View File

@ -11,18 +11,21 @@ import Bergamot.Rules exposing (..)
import Bergamot.Parser exposing (..)
import Bergamot.Latex exposing (..)
import Bergamot.ObjectLanguage exposing (..)
import Bergamot.Utils exposing (..)
import Json.Encode
import Maybe
import Tuple
type Tab
= Editor
| MetaEditor
| Rendered
tabEq : Tab -> Tab -> Bool
tabEq t1 t2 =
case (t1, t2) of
(Editor, Editor) -> True
(MetaEditor, MetaEditor) -> True
(Rendered, Rendered) -> True
_ -> False
@ -47,6 +50,7 @@ type alias Model =
type alias Flags = { renderRules: String, rules: String, query: String }
type Msg
= SetProgram String
| SetRenderProgram String
| SetQuery String
| SetTab Tab
| SetEditMode EditMode
@ -58,10 +62,11 @@ viewSection : String -> Html Msg -> Html Msg
viewSection name content =
Html.div [ class "bergamot-section" ] [ Html.em [ class "bergamot-section-heading" ] [ Html.text name ], content ]
viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
viewTab tab editor rendered =
viewTab : Tab -> Html Msg -> Html Msg -> Html Msg -> Html Msg
viewTab tab editor metaEditor rendered =
case tab of
Editor -> editor
MetaEditor -> metaEditor
Rendered -> rendered
viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
@ -83,18 +88,28 @@ viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
viewRule env r = renderRuleViaRules env r
|> Maybe.map latex
viewRuleSection : RuleEnv -> Section -> Maybe (Html Msg)
viewRuleSection env sec =
List.map (viewRule env) sec.rules
|> sequenceMaybes
|> Maybe.map (\rs ->
Html.div [ class "bergamot-rule-section" ]
[ Html.div [ class "bergamot-rule-list" ] rs
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
])
viewRules : String -> String -> Html Msg
viewRules renderProgs progs = viewSection "Rendered Rules" <|
Html.div [ class "bergamot-rule-list" ] <|
Html.div [ class "bergamot-section-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 (viewRuleSection renderProg) prog.sections
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal mode querys =
case mode of
Query -> run term querys
Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
tryProve : EditMode -> String -> String -> Maybe ProofTree
tryProve mode progs querys =
@ -102,29 +117,37 @@ tryProve mode progs querys =
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
viewProofTree : EditMode -> String -> String -> Html Msg
viewProofTree mode progs querys = viewSection "Proof Tree" <|
viewProofTree : EditMode -> String -> String -> String -> Html Msg
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
Html.div [ class "bergamot-proof-tree" ] <|
case tryProve mode progs querys of
Just tree -> [ latex (proofTreeToLatex tree) ]
Nothing -> []
case tryProve mode progs querys of
Just tree ->
case run program renderProgs of
Just renderProg ->
List.map latex
<| List.filterMap (renderTreeViaRules renderProg)
<| [ tree ]
Nothing -> []
Nothing -> []
view : Model -> Html Msg
view m = Html.div [ class "bergamot-root" ]
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")]
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewProofTree m.editMode m.renderProgram m.program m.query
, viewTab m.tab
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
(viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewProofTree m.editMode m.program m.query
]
update : Msg -> Model -> (Model, Cmd Msg)
update msg m =
case msg of
SetProgram prog -> ({ m | program = prog }, Cmd.none)
SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
SetQuery query -> ({ m | query = query }, Cmd.none)
SetTab tab -> ({ m | tab = tab }, Cmd.none)
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)