src/Bergamot/Latex.elm

@@ -22,45 +22,51 @@ 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 quoteMetavariables r.premises
-        quotedConc = quoteMetavariables r.conclusion
+        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
+            , "}"
+            ]
     in
         renderTermViaRules env quotedConc
         |> Maybe.andThen (\conc ->
             sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
-            |> Maybe.map (\prems -> buildInferenceRuleFrac prems conc r.name))
+            |> Maybe.map (\prems -> buildStr conc prems))
 
-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))
+quoteMetavariable : Metavariable -> Term Void
+quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v]
 
-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)
+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) ++ "\"" ++ "}"
 
 metavariableToLatex : Metavariable -> String
 metavariableToLatex (MkMetavariable s) =
@@ -69,3 +75,12 @@ 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 "number"
-    , Parser.succeed TStr |. Parser.keyword "string"
+    [ Parser.succeed TInt |. Parser.keyword "tint"
+    , Parser.succeed TStr |. Parser.keyword "tstr"
     , 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 "number" []
-        TStr -> Syntax.Call "string" []
+        TInt -> Syntax.Call "tint" []
+        TStr -> Syntax.Call "tstr" []
         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,14 +1,11 @@
 module Bergamot.Parser exposing (..)
 
 import Bergamot.Syntax exposing (Term(..), Metavariable(..))
-import Bergamot.Rules exposing (Rule, Section, RuleEnv)
+import Bergamot.Rules exposing (Rule, RuleEnv)
 import Bergamot.Utils exposing (decodeStr)
 
 import Parser exposing (Parser, Trailing(..), (|.), (|=))
-import Set exposing (Set)
-
-reserved : Set String
-reserved = Set.fromList ["section"]
+import Set
 
 intLit : Parser Int
 intLit = Parser.int
@@ -38,7 +35,7 @@ name : Parser String
 name = Parser.variable
     { start = \c -> Char.isAlpha c || c == '_'
     , inner = \c -> Char.isAlphaNum c || c == '_'
-    , reserved = reserved
+    , reserved = Set.empty
     }
 
 variable : Parser Metavariable
@@ -47,7 +44,7 @@ variable =
     |= Parser.variable
         { start = \c -> c == '?'
         , inner = \c -> Char.isAlphaNum c || c == '_'
-        , reserved = reserved
+        , reserved = Set.empty
         }
 
 term : Parser (Term Metavariable)
@@ -100,48 +97,16 @@ 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 (\ss -> { sections = ss })
+    Parser.succeed (\rs -> { rules = rs })
     |= Parser.sequence
         { start = ""
-        , separator = ""
+        , separator = ";"
         , end = ""
         , spaces = Parser.spaces
-        , item = Parser.oneOf [sectionExp, sectionImp]
+        , item = rule
         , trailing = Mandatory
         }
     |. Parser.end

src/Bergamot/Rules.elm

@@ -12,11 +12,6 @@ type alias Rule =
     , premises : List (Term Metavariable)
     }
 
-type alias Section =
-    { name : String
-    , rules : List Rule
-    }
-
 type ProofTree = MkProofTree
     { name : String
     , conclusion : Term UnificationVar
@@ -24,7 +19,7 @@ type ProofTree = MkProofTree
     }
 
 type alias RuleEnv =
-    { sections : List Section
+    { rules : List Rule
     }
 
 type alias ProveState =
@@ -76,14 +71,11 @@ 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 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
+burn : Prover ()
+burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail
 
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
@@ -171,9 +163,9 @@ proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
     map (reify t) getUnificationState
     |> andThen (\tp ->
-        burn (
-            getRules
-            |> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp))))
+        burn
+        |> andThen (\() -> getEnv)
+        |> andThen (\env -> List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp) env.rules))
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
@@ -182,6 +174,6 @@ prove mt =
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =
-    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 30 }
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
     |> Search.one
     |> Maybe.map (Tuple.first << Tuple.first)

src/Main.elm

@@ -11,21 +11,18 @@ 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
 
@@ -50,7 +47,6 @@ type alias Model =
 type alias Flags = { renderRules: String, rules: String, query: String }
 type Msg
     = SetProgram String
-    | SetRenderProgram String
     | SetQuery String
     | SetTab Tab
     | SetEditMode EditMode
@@ -62,11 +58,10 @@ 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 -> Html Msg
-viewTab tab editor metaEditor rendered =
+viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
+viewTab tab editor rendered =
     case tab of
         Editor -> editor
-        MetaEditor -> metaEditor
         Rendered -> rendered
 
 viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
@@ -88,28 +83,18 @@ 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-section-list" ] <|
+    Html.div [ class "bergamot-rule-list" ] <|
         case (run program renderProgs, run program progs) of
-            (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
+            (Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) prog.rules
             _ -> []
 
 proofGoal : EditMode -> String -> Maybe (Term Metavariable)
 proofGoal mode querys =
     case mode of
         Query -> run term querys
-        Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
+        Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
 
 tryProve : EditMode -> String -> String -> Maybe ProofTree
 tryProve mode progs querys =
@@ -117,37 +102,29 @@ tryProve mode progs querys =
         (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
-viewProofTree : EditMode -> String -> String -> String -> Html Msg
-viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
+viewProofTree : EditMode -> String -> String -> Html Msg
+viewProofTree mode progs querys = viewSection "Proof Tree" <|
     Html.div [ class "bergamot-proof-tree" ] <|
-        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 -> []
+      case tryProve mode progs querys of
+          Just tree -> [ latex (proofTreeToLatex tree) ]
+          Nothing -> []
 
 
 view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
-    [ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")]
+    [ viewTabSelector m.tab [(Editor, "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)