Add support for editing the meta rules

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Latex.elm

@@ -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 ++ "}"

src/Bergamot/ObjectLanguage.elm

@@ -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 ]
 

src/Bergamot/Parser.elm

@@ -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

src/Bergamot/Rules.elm

@@ -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)

src/Main.elm

@@ -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)