Add a mode for entering the object language to parse

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

src/Bergamot/ObjectLanguage.elm

@@ -1,5 +1,7 @@
 module Bergamot.ObjectLanguage exposing (..)
 
+import Bergamot.Syntax as Syntax exposing (Metavariable)
+
 import Parser exposing (Parser, Trailing(..), (|.), (|=))
 import Set
 
@@ -119,3 +121,24 @@ parseExprBasic = Parser.lazy <| \() -> Parser.oneOf
     , Parser.succeed Ref |= parseVariable
     , parseParenthed parseExpr
     ]
+
+typeToTerm : Type -> Syntax.Term Metavariable
+typeToTerm t =
+    case t of
+        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 ]
+
+exprToTerm : Expr -> Syntax.Term Metavariable
+exprToTerm e =
+    case e of
+        IntLit i -> Syntax.Call "intlit" [Syntax.IntLit i]
+        StrLit s -> Syntax.Call "strlit" [Syntax.StringLit s]
+        Plus e1 e2 -> Syntax.Call "plus" [exprToTerm e1, exprToTerm e2]
+        Pair e1 e2 -> Syntax.Call "pair" [exprToTerm e1, exprToTerm e2]
+        Fst ep -> Syntax.Call "fst" [exprToTerm ep]
+        Snd ep -> Syntax.Call "snd" [exprToTerm ep]
+        Abs s t ep -> Syntax.Call "abs" [Syntax.Call s [], typeToTerm t, exprToTerm ep]
+        App e1 e2 -> Syntax.Call "app" [exprToTerm e1, exprToTerm e2]
+        Ref x -> Syntax.Call "var" [Syntax.Call x []]

src/Main.elm

@@ -13,7 +13,6 @@ import Bergamot.ObjectLanguage exposing (..)
 import Json.Encode
 import Maybe
 import Tuple
-import Debug
 
 type Tab
     = Editor
@@ -26,19 +25,32 @@ tabEq t1 t2 =
         (Rendered, Rendered) -> True
         _ -> False
 
+type EditMode
+    = Query
+    | Syntax
+
+modeEq : EditMode -> EditMode -> Bool
+modeEq m1 m2 =
+    case (m1, m2) of
+        (Query, Query) -> True
+        (Syntax, Syntax) -> True
+        _ -> False
+
 type alias Model =
     { program : String
     , query : String
-    , tab: Tab
+    , tab : Tab
+    , editMode : EditMode
     }
 type alias Flags = { rules: String, query: String }
 type Msg
     = SetProgram String
     | SetQuery String
     | SetTab Tab
+    | SetEditMode EditMode
 
 init : Flags -> (Model, Cmd Msg)
-init fs = ({ program = fs.rules, query = fs.query, tab = Editor }, Cmd.none)
+init fs = ({ program = fs.rules, query = fs.query, tab = Editor, editMode = Syntax }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -50,13 +62,20 @@ viewTab tab editor rendered =
         Editor -> editor
         Rendered -> rendered
 
+viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
+viewSelector eq mkMsg mode modeNames =
+    Html.div [ class "bergamot-selector" ] <|
+        List.map (\(modep, name) ->
+            Html.button
+                [ classList [("active", eq mode modep)]
+                , onClick (mkMsg modep)
+                ] [ Html.text name ]) modeNames
+
 viewTabSelector : Tab -> List (Tab, String) -> Html Msg
-viewTabSelector tab tabNames = Html.div [ class "bergamot-tab-selector" ] <|
-    List.map (\(tabp, name) ->
-        Html.button
-            [ classList [("active", tabEq tab tabp)]
-            , onClick (SetTab tabp)
-            ] [ Html.text name ]) tabNames
+viewTabSelector = viewSelector tabEq SetTab
+
+viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
+viewEditModeSelector = viewSelector modeEq SetEditMode
 
 viewRule : Rule -> Html Msg
 viewRule = latex << ruleToLatex
@@ -68,16 +87,22 @@ viewRules progs = viewSection "Rendered Rules" <|
             Just prog -> List.map viewRule prog.rules
             Nothing -> []
 
-tryProve : String -> String -> Maybe ProofTree
-tryProve progs querys =
-    case (run program progs, run term querys) of
+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
+
+tryProve : EditMode -> String -> String -> Maybe ProofTree
+tryProve mode progs querys =
+    case (run program progs, proofGoal mode querys) of
         (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
-viewProofTree : String -> String -> Html Msg
-viewProofTree 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 progs querys of
+      case tryProve mode progs querys of
           Just tree -> [ latex (proofTreeToLatex tree) ]
           Nothing -> []
 
@@ -85,12 +110,12 @@ viewProofTree progs querys = viewSection "Proof Tree" <|
 view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
     [ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
+    , viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
     , viewTab m.tab
         (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
         (viewRules m.program)
     , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
-    , Html.text (Debug.toString <| run parseExpr m.query)
-    , viewProofTree m.program m.query
+    , viewProofTree m.editMode m.program m.query
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
@@ -99,6 +124,7 @@ update msg m =
         SetProgram prog -> ({ m | program = prog }, Cmd.none)
         SetQuery query -> ({ m | query = query }, Cmd.none)
         SetTab tab -> ({ m | tab = tab }, Cmd.none)
+        SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
 
 subscriptions : Model -> Sub Msg
 subscriptions _ = Sub.none