From aac1c7f9613ed49aef91adcfe0066633e97e7944 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 25 Dec 2023 11:51:50 -0800
Subject: [PATCH] Rename some parser functions in ObjectLanguage.elm

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/ObjectLanguage.elm | 69 +++++++++++++++++----------------
 src/Main.elm                    |  4 +-
 2 files changed, 38 insertions(+), 35 deletions(-)

diff --git a/src/Bergamot/ObjectLanguage.elm b/src/Bergamot/ObjectLanguage.elm
index ca797b4..e17b060 100644
--- a/src/Bergamot/ObjectLanguage.elm
+++ b/src/Bergamot/ObjectLanguage.elm
@@ -22,16 +22,16 @@ type Expr
     | App Expr Expr
     | Ref String
 
-parseParenthed : Parser a -> Parser a
-parseParenthed val = Parser.succeed (\x -> x)
+parenthed : Parser a -> Parser a
+parenthed val = Parser.succeed (\x -> x)
     |. Parser.symbol "("
     |. Parser.spaces
     |= val
     |. Parser.spaces
     |. Parser.symbol ")"
 
-parsePair : Parser a -> Parser (a, a)
-parsePair elem = parseParenthed <|
+pair : Parser a -> Parser (a, a)
+pair elem = parenthed <|
     Parser.succeed Tuple.pair
     |= elem
     |. Parser.spaces
@@ -39,45 +39,48 @@ parsePair elem = parseParenthed <|
     |. Parser.spaces
     |= elem
 
-parseType : Parser Type
-parseType = Parser.lazy <| \() -> Parser.oneOf
+type_ : Parser Type
+type_ = Parser.lazy <| \() -> Parser.oneOf
     [ Parser.backtrackable <| Parser.succeed TArr
-        |= parseTypeBasic
+        |= typeBasic
         |. Parser.spaces
         |. Parser.symbol "->"
         |. Parser.spaces
-        |= parseType
-    , parseTypeBasic
+        |= type_
+    , typeBasic
     ]
 
-parseTypeBasic : Parser Type
-parseTypeBasic = Parser.lazy <| \() -> Parser.oneOf
+typeBasic : Parser Type
+typeBasic = Parser.lazy <| \() -> Parser.oneOf
     [ 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
+    , Parser.backtrackable <| Parser.map (\(a, b) -> TPair a b) <| pair type_
+    , parenthed type_
     ]
 
-parseVariable : Parser String
-parseVariable = Parser.variable
+variable : Parser String
+variable = Parser.variable
     { start = Char.isAlphaNum
     , inner = Char.isAlphaNum
     , reserved = Set.fromList ["fst", "snd", "let", "in"]
     }
 
-parseExpr : Parser Expr
-parseExpr = Parser.lazy <| \() -> Parser.oneOf
+expr : Parser Expr
+expr = Parser.lazy <| \() -> Parser.oneOf
     [ Parser.backtrackable <| Parser.succeed Plus
-        |= parseExprBasic
+        |= exprBasic
         |. Parser.spaces
         |. Parser.symbol "+"
         |. Parser.spaces
-        |= parseExpr
-    , parseExprApps
+        |= expr
+    , exprApps
     ]
 
-parseExprApps : Parser Expr
-parseExprApps =
+topLevelExpr : Parser Expr
+topLevelExpr = expr |. Parser.end
+
+exprApps : Parser Expr
+exprApps =
     let
         handle l =
             case l of
@@ -89,37 +92,37 @@ parseExprApps =
             , separator = " "
             , end = ""
             , spaces = Parser.succeed ()
-            , item = parseExprBasic
+            , item = exprBasic
             , trailing = Optional
             }
         |> Parser.andThen handle
 
-parseExprBasic : Parser Expr
-parseExprBasic = Parser.lazy <| \() -> Parser.oneOf
+exprBasic : Parser Expr
+exprBasic = Parser.lazy <| \() -> Parser.oneOf
     [ Parser.backtrackable (Parser.succeed IntLit |= Parser.int)
-    , Parser.backtrackable <| Parser.map (\(a, b) -> Pair a b) <| parsePair parseExpr
+    , Parser.backtrackable <| Parser.map (\(a, b) -> Pair a b) <| pair expr
     , Parser.succeed Fst
         |. Parser.keyword "fst"
         |. Parser.spaces
-        |= parseParenthed parseExpr
+        |= parenthed expr
     , Parser.succeed Snd
         |. Parser.keyword "snd"
         |. Parser.spaces
-        |= parseParenthed parseExpr
+        |= parenthed expr
     , Parser.succeed Abs
         |. Parser.symbol "\\"
         |. Parser.spaces
-        |= parseVariable
+        |= variable
         |. Parser.spaces
         |. Parser.symbol ":"
         |. Parser.spaces
-        |= parseType
+        |= type_
         |. Parser.spaces
         |. Parser.symbol "."
         |. Parser.spaces
-        |= parseExpr
-    , Parser.succeed Ref |= parseVariable
-    , parseParenthed parseExpr
+        |= expr
+    , Parser.succeed Ref |= variable
+    , parenthed expr
     ]
 
 typeToTerm : Type -> Syntax.Term Metavariable
diff --git a/src/Main.elm b/src/Main.elm
index 51b1135..c5ff95b 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -10,7 +10,7 @@ import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
-import Bergamot.ObjectLanguage exposing (..)
+import Bergamot.ObjectLanguage exposing (topLevelExpr, exprToTerm)
 import Bergamot.Utils exposing (..)
 import Json.Encode
 import Maybe
@@ -127,7 +127,7 @@ proofGoal editMode inputProgs querys =
     case editMode of
         Query -> run term querys
         Syntax ->
-            case (run program inputProgs, run parseExpr querys) of
+            case (run program inputProgs, run topLevelExpr querys) of
                 (Just inputProg, Just e) ->
                     let
                         inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] }