From ec0b05ab5101b86cd1a69c365a96a11ee701572a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 7 Sep 2024 22:23:04 -0700 Subject: [PATCH] Make 'language term' just a custom mode Signed-off-by: Danila Fedorin --- elm.nix | 2 +- index.html | 16 +++++++++--- src/Bergamot/ObjectLanguage.elm | 44 +++++++++++++++++++++++++++++---- src/Bergamot/Syntax.elm | 11 ++++++++- src/Main.elm | 30 +++------------------- 5 files changed, 66 insertions(+), 37 deletions(-) diff --git a/elm.nix b/elm.nix index 6080626..5d8a462 100644 --- a/elm.nix +++ b/elm.nix @@ -42,7 +42,7 @@ in mkDerivation { name = "bergamot-elm"; srcs = ./elm-dependencies.nix; src = ./.; - targets = ["Main"]; + targets = ["Main" "Bergamot.ObjectLanguage"]; srcdir = "./src"; outputJavaScript = true; } diff --git a/index.html b/index.html index 3b36b77..919bac7 100644 --- a/index.html +++ b/index.html @@ -53,7 +53,10 @@ input[type="text"] {
+ diff --git a/src/Bergamot/ObjectLanguage.elm b/src/Bergamot/ObjectLanguage.elm index 4fd9d4f..fb6946a 100644 --- a/src/Bergamot/ObjectLanguage.elm +++ b/src/Bergamot/ObjectLanguage.elm @@ -1,9 +1,10 @@ -module Bergamot.ObjectLanguage exposing (..) +port module Bergamot.ObjectLanguage exposing (..) -import Bergamot.Syntax as Syntax exposing (Metavariable) +import Bergamot.Syntax as Syntax exposing (toString) import Bergamot.Parser exposing (strLit) -import Parser exposing (Parser, Trailing(..), (|.), (|=)) +import Platform exposing (worker) +import Parser exposing (Parser, Trailing(..), (|.), (|=), run) import Set type Type @@ -135,7 +136,7 @@ exprBasic = Parser.lazy <| \() -> Parser.oneOf , parenthed expr ] -typeToTerm : Type -> Syntax.Term Metavariable +typeToTerm : Type -> Syntax.Term () typeToTerm t = case t of TInt -> Syntax.Call "number" [] @@ -143,7 +144,7 @@ typeToTerm t = 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 : Expr -> Syntax.Term () exprToTerm e = case e of IntLit i -> Syntax.Call "lit" [Syntax.IntLit i] @@ -156,3 +157,36 @@ exprToTerm e = 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 []] + +-- Receives requests from JS code to apply the parser +port parseString : (String -> msg) -> Sub msg + +-- Used to send the result of parsing back to JS +port parsedString : { string : String, term : Maybe String } -> Cmd msg + +type Msg = ParseString String +type alias Model = () +type alias Flags = () + +init : Flags -> (Model, Cmd Msg) +init _ = ((), Cmd.none) + +update : Msg -> Model -> (Model, Cmd Msg) +update (ParseString s) _ = + case run topLevelExpr s of + Ok e -> + ( () + , parsedString + { string = s + , term = + exprToTerm e + |> toString (\_ -> "") + |> Just + } + ) + Err _ -> ((), parsedString { string = s, term = Nothing }) + +subscriptions : Model -> Sub Msg +subscriptions _ = parseString ParseString + +main = worker { init = init, update = update, subscriptions = subscriptions } diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm index 5b2edb0..b5ff463 100644 --- a/src/Bergamot/Syntax.elm +++ b/src/Bergamot/Syntax.elm @@ -1,5 +1,5 @@ module Bergamot.Syntax exposing - ( Term(..), map, andThen, Metavariable(..), UnificationVar(..) + ( Term(..), toString, map, andThen, Metavariable(..), UnificationVar(..) , unMetavariable, unUnificationVar , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars , unify, unifyList, UnificationState, emptyUnificationState @@ -29,6 +29,15 @@ type Term a | Call Name (List (Term a)) | Var a +toString : (a -> String) -> Term a -> String +toString fn t = + case t of + IntLit i -> String.fromInt i + FloatLit f -> String.fromFloat f + StringLit s -> "\"" ++ s ++ "\"" -- TODO: insufficient, need to escape + Call n ts -> n ++ "(" ++ String.join ", " (List.map (toString fn) ts) ++ ")" + Var a -> fn a + map : (a -> b) -> Term a -> Term b map f t = case t of diff --git a/src/Main.elm b/src/Main.elm index 57adbde..77c777d 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -10,7 +10,6 @@ import Bergamot.Search exposing (..) import Bergamot.Rules exposing (..) import Bergamot.Parser exposing (..) import Bergamot.Latex exposing (..) -import Bergamot.ObjectLanguage exposing (topLevelExpr, exprToTerm) import Bergamot.Utils exposing (..) import Json.Encode import Json.Decode exposing (string, field, list, oneOf, succeed, fail) @@ -32,7 +31,6 @@ tabEq t1 t2 = type EditMode = Query - | Syntax | Custom String type ResultMode @@ -51,8 +49,6 @@ type alias Model = -- ^ The Bergamot rules to execute a search against , renderProgram: String -- ^ The Bergamot render rules to apply when generating LaTeX - , inputProgram : String - -- ^ The Bergamot rules to apply to convert a Syntax term into a query , tab : Tab -- ^ The current tab (editor, redner rule editor, rendered) , input : String @@ -94,14 +90,13 @@ decodeInputModes val = else Json.Decode.fail "did not match expected string") editModeDecoder = oneOf [ exactString "query" Query - , exactString "syntax" Syntax , field "custom" string |> Json.Decode.map Custom ] decoder = Json.Decode.keyValuePairs editModeDecoder in case Json.Decode.decodeValue decoder val of Ok l -> l - Err _ -> [("Language Term", Syntax), ("Query", Query)] + Err _ -> [("Query", Query)] -- Convert the user-entered string 'input' using custom query mode 'mode' port convertInput : { mode : String, input : String } -> Cmd msg @@ -124,7 +119,6 @@ init fs = in ( { program = fs.rules , renderProgram = fs.renderRules - , inputProgram = fs.inputRules , input = fs.input , desugaredQuery = Nothing , tab = Rendered @@ -242,8 +236,8 @@ getEditMode i l = ((_, editMode) :: xs) -> if i == 0 then Ok editMode else getEditMode (i - 1) xs -proofGoal : EditMode -> String -> String -> Maybe String -> Result Error (Term Metavariable) -proofGoal editMode inputProgs input desugaredQuery = +proofGoal : EditMode -> String -> Maybe String -> Result Error (Term Metavariable) +proofGoal editMode input desugaredQuery = if input == "" then Err Silent else @@ -252,22 +246,6 @@ proofGoal editMode inputProgs input desugaredQuery = case run topLevelTerm input of Nothing -> Err BadQuery Just query -> Ok query - Syntax -> - case (run program inputProgs, run topLevelExpr input) of - (Just inputProg, Just e) -> - let - inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] } - fullProgram = { sections = { name = "", rules = [inputRule] } :: inputProg.sections } - query = Call "prompt" [Var (MkMetavariable "?p")] - in - case single fullProgram (prove query |> Bergamot.Rules.andThen reifyProofTree) of - Just (MkProofTree node) -> - case node.conclusion of - Call "prompt" [t] -> Ok <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t - _ -> Err NoConversionResults - _ -> Err NoConversionResults - (_, Nothing) -> Err BadObjectTerm - (Nothing, _) -> Err BadInputProg Custom _ -> case desugaredQuery of Just querys -> @@ -307,7 +285,7 @@ view : Model -> Html Msg view m = let mode = getEditMode m.inputMode m.inputModes - termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.inputProgram m.input m.desugaredQuery) + termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.input m.desugaredQuery) progsOrErr = progAndRenderProg m.program m.renderProgram proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr in