Everything-I-Know-About-Types/bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Make 'language term' just a custom mode

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-09-07 22:23:04 -07:00
parent bfc21c2928
commit ec0b05ab51
5 changed files with 66 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
elm.nix
View File

@ -42,7 +42,7 @@ in mkDerivation {
name = "bergamot-elm";
srcs = ./elm-dependencies.nix;
src = ./.;
targets = ["Main"];
targets = ["Main" "Bergamot.ObjectLanguage"];
srcdir = "./src";
outputJavaScript = true;
}

16
index.html
View File

@ -53,7 +53,10 @@ input[type="text"] {
<body>
<div id="elm"></div>
<script src="index.js"></script>
<script src="language.js"></script>
<script>
const objectLang = Elm.Bergamot.ObjectLanguage.init({});
(async () => {
var rulesResponse = await fetch("./demorules.bergamot");
var rules = await rulesResponse.text();
@ -64,9 +67,8 @@ input[type="text"] {
node: document.getElementById('elm'),
flags: {
inputModes: {
"My Mode": { "custom": "mymode" },
"Language Term": { "custom": "langterm" },
"Query": "query",
"Language Term": "syntax",
},
inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);",
input: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)",
@ -74,9 +76,15 @@ input[type="text"] {
}
});
objectLang.ports.parsedString.subscribe(({ string, term }) => {
if (term !== null) {
const query = `type(empty, ${term}, ?tau)`;
app.ports.receiveConverted.send({ input: string, query });
}
});
app.ports.convertInput.subscribe(({ mode, input }) => {
console.log(input);
app.ports.receiveConverted.send({ input, query: `type(empty, lit(${input}), ?tau )` });
objectLang.ports.parseString.send(input);
});
})();
</script>

44
src/Bergamot/ObjectLanguage.elm
View File

@ -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 }

11
src/Bergamot/Syntax.elm
View File

@ -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

30
src/Main.elm
View File

@ -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