diff --git a/src/Bergamot/ObjectLanguage.elm b/src/Bergamot/ObjectLanguage.elm new file mode 100644 index 0000000..db5d4fb --- /dev/null +++ b/src/Bergamot/ObjectLanguage.elm @@ -0,0 +1,121 @@ +module Bergamot.ObjectLanguage exposing (..) + +import Parser exposing (Parser, Trailing(..), (|.), (|=)) +import Set + +type Type + = TInt + | TStr + | TPair Type Type + | TArr Type Type + +type Expr + = IntLit Int + | StrLit String + | Plus Expr Expr + | Pair Expr Expr + | Fst Expr + | Snd Expr + | Abs String Type Expr + | App Expr Expr + | Ref String + +parseParenthed : Parser a -> Parser a +parseParenthed val = Parser.succeed (\x -> x) + |. Parser.symbol "(" + |. Parser.spaces + |= val + |. Parser.spaces + |. Parser.symbol ")" + +parsePair : Parser a -> Parser (a, a) +parsePair elem = parseParenthed <| + Parser.succeed Tuple.pair + |= elem + |. Parser.spaces + |. Parser.symbol "," + |. Parser.spaces + |= elem + +parseType : Parser Type +parseType = Parser.lazy <| \() -> Parser.oneOf + [ Parser.backtrackable <| Parser.succeed TArr + |= parseTypeBasic + |. Parser.spaces + |. Parser.symbol "->" + |. Parser.spaces + |= parseType + , parseTypeBasic + ] + +parseTypeBasic : Parser Type +parseTypeBasic = Parser.lazy <| \() -> Parser.oneOf + [ 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 + ] + +parseVariable : Parser String +parseVariable = Parser.variable + { start = Char.isAlphaNum + , inner = Char.isAlphaNum + , reserved = Set.fromList ["fst", "snd", "let", "in"] + } + +parseExpr : Parser Expr +parseExpr = Parser.lazy <| \() -> Parser.oneOf + [ Parser.backtrackable <| Parser.succeed Plus + |= parseExprBasic + |. Parser.spaces + |. Parser.symbol "+" + |. Parser.spaces + |= parseExpr + , parseExprApps + ] + +parseExprApps : Parser Expr +parseExprApps = + let + handle l = + case l of + [] -> Parser.problem "no applications found" + x :: xs -> Parser.succeed <| List.foldl (\a b -> App b a) x xs + in + Parser.sequence + { start = "" + , separator = " " + , end = "" + , spaces = Parser.succeed () + , item = parseExprBasic + , trailing = Optional + } + |> Parser.andThen handle + +parseExprBasic : Parser Expr +parseExprBasic = Parser.lazy <| \() -> Parser.oneOf + [ Parser.backtrackable (Parser.succeed IntLit |= Parser.int) + , Parser.backtrackable <| Parser.map (\(a, b) -> Pair a b) <| parsePair parseExpr + , Parser.succeed Fst + |. Parser.keyword "fst" + |. Parser.spaces + |= parseParenthed parseExpr + , Parser.succeed Snd + |. Parser.keyword "snd" + |. Parser.spaces + |= parseParenthed parseExpr + , Parser.succeed Abs + |. Parser.symbol "\\" + |. Parser.spaces + |= parseVariable + |. Parser.spaces + |. Parser.symbol ":" + |. Parser.spaces + |= parseType + |. Parser.spaces + |. Parser.symbol "." + |. Parser.spaces + |= parseExpr + , Parser.succeed Ref |= parseVariable + , parseParenthed parseExpr + ] diff --git a/src/Main.elm b/src/Main.elm index 1c6d96f..068453d 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -9,6 +9,7 @@ import Bergamot.Search exposing (..) import Bergamot.Rules exposing (..) import Bergamot.Parser exposing (..) import Bergamot.Latex exposing (..) +import Bergamot.ObjectLanguage exposing (..) import Json.Encode import Maybe import Tuple @@ -88,6 +89,7 @@ view m = Html.div [ class "bergamot-root" ] (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 ]