Compare commits
33 Commits
abd6a848f8
...
main
| Author | SHA1 | Date | |
|---|---|---|---|
| ceca48840e | |||
| 000d95ae5b | |||
| 2af1692bf4 | |||
| 0b4a1f2ebd | |||
| c77bb6f900 | |||
| e7d3e840b3 | |||
| a17ea205c7 | |||
| 2a0db676bc | |||
| a7b3efe56c | |||
| ec0b05ab51 | |||
| bfc21c2928 | |||
| d1fb4bfdc1 | |||
| b6569d8ca0 | |||
| 14b63fccc2 | |||
| 6a952f8a15 | |||
| cd9a048832 | |||
| f35a8d17e8 | |||
| 98562eca2d | |||
| 0b3469b49a | |||
| b828c73e43 | |||
| 4c12fee4aa | |||
| 29a95d2659 | |||
| 97fcae9c2c | |||
| c192193c57 | |||
| 287562619d | |||
| 7d07b2dee9 | |||
| 10d1edbc32 | |||
| aac1c7f961 | |||
| bc83f0ed53 | |||
| 12d823e944 | |||
| 9fd60b4013 | |||
| aa7fd44a6d | |||
| da470f5caa |
28
demorules.bergamot
Normal file
28
demorules.bergamot
Normal file
@@ -0,0 +1,28 @@
|
||||
section "" {
|
||||
TNumber @ type(?Gamma, lit(?n), number) <- num(?n);
|
||||
TString @ type(?Gamma, lit(?s), string) <- str(?s);
|
||||
TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);
|
||||
TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <-
|
||||
type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number);
|
||||
TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <-
|
||||
type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string);
|
||||
}
|
||||
section "" {
|
||||
TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <-
|
||||
type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);
|
||||
TFst @ type(?Gamma, fst(?e), ?tau_1) <-
|
||||
type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
|
||||
TSnd @ type(?Gamma, snd(?e), ?tau_2) <-
|
||||
type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
|
||||
}
|
||||
section "" {
|
||||
TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <-
|
||||
type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);
|
||||
TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <-
|
||||
type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);
|
||||
}
|
||||
|
||||
section "" {
|
||||
GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;
|
||||
GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);
|
||||
}
|
||||
4
elm.nix
4
elm.nix
@@ -29,7 +29,7 @@ let
|
||||
mkdir -p $out/share/doc
|
||||
${lib.concatStrings (map (module: ''
|
||||
echo "compiling ${elmfile module}"
|
||||
elm make ${elmfile module} --output $out/${module}.${extension} --docs $out/share/doc/${module}.json
|
||||
elm make ${elmfile module} --output $out/${module}.${extension} --docs $out/share/doc/${module}.json --optimize
|
||||
${lib.optionalString outputJavaScript ''
|
||||
echo "minifying ${elmfile module}"
|
||||
uglifyjs $out/${module}.${extension} --compress 'pure_funcs="F2,F3,F4,F5,F6,F7,F8,F9,A2,A3,A4,A5,A6,A7,A8,A9",pure_getters,keep_fargs=false,unsafe_comps,unsafe' \
|
||||
@@ -42,7 +42,7 @@ in mkDerivation {
|
||||
name = "bergamot-elm";
|
||||
srcs = ./elm-dependencies.nix;
|
||||
src = ./.;
|
||||
targets = ["Main"];
|
||||
targets = ["Main" "Bergamot.ObjectLanguage"];
|
||||
srcdir = "./src";
|
||||
outputJavaScript = true;
|
||||
}
|
||||
|
||||
14
flake.lock
generated
14
flake.lock
generated
@@ -5,11 +5,11 @@
|
||||
"systems": "systems"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694529238,
|
||||
"narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
|
||||
"lastModified": 1731533236,
|
||||
"narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
|
||||
"rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@@ -20,16 +20,16 @@
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1701068326,
|
||||
"narHash": "sha256-vmMceA+q6hG1yrjb+MP8T0YFDQIrW3bl45e7z24IEts=",
|
||||
"lastModified": 1766736597,
|
||||
"narHash": "sha256-BASnpCLodmgiVn0M1MU2Pqyoz0aHwar/0qLkp7CjvSQ=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "8cfef6986adfb599ba379ae53c9f5631ecd2fd9c",
|
||||
"rev": "f560ccec6b1116b22e6ed15f4c510997d99d5852",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-unstable",
|
||||
"ref": "nixos-25.11",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
{
|
||||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-25.11";
|
||||
flake-utils.url = "github:numtide/flake-utils";
|
||||
};
|
||||
outputs = { self, nixpkgs, flake-utils }:
|
||||
|
||||
39
index.html
39
index.html
@@ -53,11 +53,42 @@ input[type="text"] {
|
||||
<body>
|
||||
<div id="elm"></div>
|
||||
<script src="index.js"></script>
|
||||
<script src="language.js"></script>
|
||||
<script>
|
||||
var app = Elm.Main.init({
|
||||
node: document.getElementById('elm'),
|
||||
flags: { rules: "TInt @ type(?Gamma, intlit(?n), tint) <-;\nTString @ type(?Gamma, strlit(?s), tstr) <-;\nTVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);\nTPlusI @ type(?Gamma, plus(?e_1, ?e_2), tint) <- type(?Gamma, ?e_1, tint), type(?Gamma, ?e_2, tint);\nTPlusS @ type(?Gamma, plus(?e_1, ?e_2), tstr) <- type(?Gamma, ?e_1, tstr), type(?Gamma, ?e_2, tstr);\nTPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);\nTFst @ type(?Gamma, fst(?e), ?tau_1) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTSnd @ type(?Gamma, snd(?e), ?tau_2) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);\nTApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);\n\nGammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;\nGammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);", query: "type(empty, app(abs(x, tint, var(x)), intlit(1)), ?tau)" }
|
||||
});
|
||||
const objectLang = Elm.Bergamot.ObjectLanguage.init({});
|
||||
|
||||
(async () => {
|
||||
var rulesResponse = await fetch("./demorules.bergamot");
|
||||
var rules = await rulesResponse.text();
|
||||
var renderRulesResponse = await fetch("./renderrules.bergamot");
|
||||
var renderRules = await renderRulesResponse.text();
|
||||
console.log(rules);
|
||||
var app = Elm.Main.init({
|
||||
node: document.getElementById('elm'),
|
||||
flags: {
|
||||
inputModes: {
|
||||
"Language Term": { "custom": "langterm" },
|
||||
"Query": "query",
|
||||
},
|
||||
inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);",
|
||||
input: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)",
|
||||
renderRules: renderRules, rules: rules
|
||||
}
|
||||
});
|
||||
|
||||
objectLang.ports.parsedString.subscribe(({ string, term }) => {
|
||||
if (term !== null) {
|
||||
const query = `type(empty, ${term}, ?tau)`;
|
||||
app.ports.receiveConverted.send({ input: string, result: { query } });
|
||||
} else {
|
||||
app.ports.receiveConverted.send({ input: string, result: { error: "Unable to parse object language term" } });
|
||||
}
|
||||
});
|
||||
|
||||
app.ports.convertInput.subscribe(({ mode, input }) => {
|
||||
objectLang.ports.parseString.send(input);
|
||||
});
|
||||
})();
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
@@ -1,3 +1,23 @@
|
||||
PrecApp @ prec(app(?l, ?r), 100, left) <-;
|
||||
PrecPlus @ prec(plus(?l, ?r), 80, either) <-;
|
||||
PrecAbs @ prec(abs(?x, ?t, ?e), 0, right) <-;
|
||||
PrecArr @ prec(tarr(?l, ?r), 0, right) <-;
|
||||
|
||||
SelectHead @ select(cons([?t, ?v], ?rest), ?default, ?v) <- ?t;
|
||||
SelectTail @ select(cons([?t, ?v], ?rest), ?default, ?found) <- not(?t), select(?rest, ?default, ?found);
|
||||
SelectEmpty @ select(nil, ?default, ?default) <-;
|
||||
|
||||
ParenthAssocLeft @ parenthassoc(?a_i, left, right) <-;
|
||||
ParenthAssocRight @ parenthassoc(?a_i, right, left) <-;
|
||||
ParenthAssocNone @ parenthassoc(?a_i, none, ?pos) <-;
|
||||
ParenthAssocNeq @ parenthassoc(?a_i, ?a_o, ?pos) <- not(symeq(?a_i, ?a_o));
|
||||
|
||||
Parenth @ parenth(?inner, ?outer, ?pos, ?strin, ?strout) <-
|
||||
prec(?inner, ?p_i, ?a_i), prec(?outer, ?p_o, ?a_o),
|
||||
join(["(", ?strin, ")"], ?strinparen),
|
||||
select([ [less(?p_i, ?p_o), strinparen], [less(?p_o, ?p_i), ?strin], [ parenthassoc(?a_i, ?a_o, ?pos), ?strinparen ] ], ?strin, ?strout);
|
||||
ParenthFallback @ parenth(?inner, ?outer, ?pos, ?strin, ?strin) <-;
|
||||
|
||||
LatexListNil @ latexlist(nil, nil) <-;
|
||||
LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
|
||||
|
||||
@@ -8,21 +28,32 @@ IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
|
||||
NonEmpty @ nonempty(cons(?x, ?xs)) <-;
|
||||
|
||||
LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
|
||||
LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
|
||||
LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
|
||||
LatexMeta @ latex(metavariable(?l), ?l) <-;
|
||||
LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
|
||||
LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);
|
||||
LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l);
|
||||
LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l);
|
||||
LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " + ", ?l_2], ?l);
|
||||
LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
|
||||
LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l);
|
||||
LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
|
||||
latex(?e_1, ?l_1), latex(?e_2, ?l_2),
|
||||
parenth(?e_1, plus(?e_1, ?e_2), left, ?l_1, ?lp_1),
|
||||
parenth(?e_2, plus(?e_1, ?e_2), right, ?l_2, ?lp_2),
|
||||
join([?lp_1, " + ", ?lp_2], ?l);
|
||||
LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
|
||||
LatexAbs @ latex(abs(?x, ?t, ?e), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), latex(?x, ?l_x), join(["\\lambda ", ?l_x, " : ", ?l_t, " . ", ?l_e], ?l);
|
||||
LatexApp @ latex(app(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " \\enspace ", ?l_2], ?l);
|
||||
LatexApp @ latex(app(?e_1, ?e_2), ?l) <-
|
||||
latex(?e_1, ?l_1), latex(?e_2, ?l_2),
|
||||
parenth(?e_1, app(?e_1, ?e_2), left, ?l_1, ?lp_1),
|
||||
parenth(?e_2, app(?e_1, ?e_2), right, ?l_2, ?lp_2),
|
||||
join([?lp_1, " \\enspace ", ?lp_2], ?l);
|
||||
|
||||
LatexTInt @ latex(tint, "\\text{tint}") <-;
|
||||
LatexTStr @ latex(tstr, "\\text{tstr}") <-;
|
||||
LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join([?l_1, " \\to ", ?l_2], ?l);
|
||||
LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join([?l_1, " \\times ", ?l_2], ?l);
|
||||
LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <-
|
||||
latex(?t_1, ?l_1), latex(?t_2, ?l_2),
|
||||
parenth(?t_1, tarr(?t_1, ?t_2), left, ?l_1, ?lp_1),
|
||||
parenth(?t_2, tarr(?t_1, ?t_2), right, ?l_2, ?lp_2),
|
||||
join([?lp_1, " \\to ", ?lp_2], ?l);
|
||||
LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
|
||||
|
||||
LatexTypeEmpty @ latex(empty, "\\varnothing") <-;
|
||||
LatexTypeExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, " , ", ?l_b, " : ", ?l_c], ?l);
|
||||
@@ -30,3 +61,12 @@ LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t)
|
||||
|
||||
LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
|
||||
LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\vdash ", ?l_e, " : ", ?l_t], ?l);
|
||||
|
||||
LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\preceq ", ?l_t], ?l);
|
||||
|
||||
LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
|
||||
LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
|
||||
LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
|
||||
LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
|
||||
LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
|
||||
LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);
|
||||
|
||||
@@ -68,4 +68,5 @@ metavariableToLatex (MkMetavariable s) =
|
||||
noQuestion = String.dropLeft 1 s
|
||||
in
|
||||
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
|
||||
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
|
||||
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else
|
||||
if String.startsWith "rho" noQuestion then "\\" ++ noQuestion else noQuestion
|
||||
|
||||
@@ -1,8 +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
|
||||
@@ -13,6 +15,7 @@ type Type
|
||||
|
||||
type Expr
|
||||
= IntLit Int
|
||||
| FloatLit Float
|
||||
| StrLit String
|
||||
| Plus Expr Expr
|
||||
| Pair Expr Expr
|
||||
@@ -22,16 +25,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 +42,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,40 +95,48 @@ parseExprApps =
|
||||
, separator = " "
|
||||
, end = ""
|
||||
, spaces = Parser.succeed ()
|
||||
, item = parseExprBasic
|
||||
, item = exprBasic
|
||||
, 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
|
||||
exprBasic : Parser Expr
|
||||
exprBasic = Parser.lazy <| \() -> Parser.oneOf
|
||||
[ Parser.backtrackable <|
|
||||
Parser.number
|
||||
{ int = Just IntLit
|
||||
, hex = Nothing
|
||||
, octal = Nothing
|
||||
, binary = Nothing
|
||||
, float = Just FloatLit
|
||||
}
|
||||
, Parser.backtrackable (Parser.succeed StrLit |= strLit)
|
||||
, 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
|
||||
typeToTerm : Type -> Syntax.Term ()
|
||||
typeToTerm t =
|
||||
case t of
|
||||
TInt -> Syntax.Call "number" []
|
||||
@@ -130,11 +144,12 @@ 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 "intlit" [Syntax.IntLit i]
|
||||
StrLit s -> Syntax.Call "strlit" [Syntax.StringLit s]
|
||||
IntLit i -> Syntax.Call "lit" [Syntax.IntLit i]
|
||||
FloatLit f -> Syntax.Call "lit" [Syntax.FloatLit f]
|
||||
StrLit s -> Syntax.Call "lit" [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]
|
||||
@@ -142,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 }
|
||||
|
||||
@@ -8,10 +8,7 @@ import Parser exposing (Parser, Trailing(..), (|.), (|=))
|
||||
import Set exposing (Set)
|
||||
|
||||
reserved : Set String
|
||||
reserved = Set.fromList ["section"]
|
||||
|
||||
intLit : Parser Int
|
||||
intLit = Parser.int
|
||||
reserved = Set.fromList ["hidden", "section"]
|
||||
|
||||
strLit : Parser String
|
||||
strLit =
|
||||
@@ -78,10 +75,19 @@ term = Parser.lazy (\() -> Parser.oneOf
|
||||
|= name
|
||||
, Parser.backtrackable <|
|
||||
Parser.succeed Var |= variable
|
||||
, Parser.succeed IntLit |= intLit
|
||||
, Parser.number
|
||||
{ int = Just IntLit
|
||||
, hex = Nothing
|
||||
, octal = Nothing
|
||||
, binary = Nothing
|
||||
, float = Just FloatLit
|
||||
}
|
||||
, Parser.succeed StringLit |= strLit
|
||||
])
|
||||
|
||||
topLevelTerm : Parser (Term Metavariable)
|
||||
topLevelTerm = term |. Parser.end
|
||||
|
||||
rule : Parser Rule
|
||||
rule =
|
||||
let
|
||||
@@ -114,7 +120,13 @@ rules = Parser.sequence
|
||||
|
||||
sectionExp : Parser Section
|
||||
sectionExp =
|
||||
Parser.succeed (\n rs -> { name = n, rules = rs })
|
||||
Parser.succeed (\h n rs -> { hidden = h, name = n, rules = rs })
|
||||
|= Parser.oneOf
|
||||
[ Parser.succeed True
|
||||
|. Parser.symbol "hidden"
|
||||
|. Parser.spaces
|
||||
, Parser.succeed False
|
||||
]
|
||||
|. Parser.symbol "section" |. Parser.spaces
|
||||
|= strLit |. Parser.spaces
|
||||
|. Parser.symbol "{" |. Parser.spaces
|
||||
@@ -131,7 +143,7 @@ sectionImp =
|
||||
_ -> Parser.succeed (Parser.Done <| List.reverse rs)
|
||||
])
|
||||
|> Parser.loop []
|
||||
|> Parser.map (\rs -> { name = "", rules = rs })
|
||||
|> Parser.map (\rs -> { hidden = False, name = "", rules = rs })
|
||||
|
||||
program : Parser RuleEnv
|
||||
program =
|
||||
|
||||
@@ -15,6 +15,7 @@ type alias Rule =
|
||||
type alias Section =
|
||||
{ name : String
|
||||
, rules : List Rule
|
||||
, hidden: Bool
|
||||
}
|
||||
|
||||
type ProofTree = MkProofTree
|
||||
@@ -67,6 +68,9 @@ interleave p1 p2 env ps =
|
||||
pure : a -> Prover a
|
||||
pure a env ps = Search.pure (a, ps)
|
||||
|
||||
lazy : (() -> Prover a) -> Prover a
|
||||
lazy f env ps = Search.lazy ((\p -> p env ps) << f)
|
||||
|
||||
fail : Prover a
|
||||
fail env ps = Search.fail
|
||||
|
||||
@@ -85,6 +89,13 @@ getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
||||
burn : Prover a -> Prover a
|
||||
burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
|
||||
|
||||
try : Prover a -> Prover (Maybe a)
|
||||
try p env ps =
|
||||
p env { ps | gas = 30 }
|
||||
|> Search.one
|
||||
|> Maybe.map (Tuple.first << Tuple.first)
|
||||
|> (\mx -> Search.pure (mx, ps))
|
||||
|
||||
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
|
||||
liftInstantiation f a env ps =
|
||||
let
|
||||
@@ -129,47 +140,81 @@ collectStrings t =
|
||||
|
||||
builtinRules : Term UnificationVar -> Prover ProofTree
|
||||
builtinRules t =
|
||||
case t of
|
||||
Call "concat" [StringLit s1, StringLit s2, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (s1 ++ s2))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
|
||||
Call "join" [tp, Var output] ->
|
||||
collectStrings tp
|
||||
|> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
|
||||
Call "int" [IntLit i] ->
|
||||
MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "str" [StringLit s] ->
|
||||
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "sym" [Call s []] ->
|
||||
MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "call" [Call s ts, Var name, Var args] ->
|
||||
pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
|
||||
|> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
|
||||
|> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
|
||||
Call "tostring" [IntLit i, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (String.fromInt i))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
|
||||
Call "tostring" [Call s [], Var output] ->
|
||||
liftUnification unify (Var output) (StringLit <| encodeStr s)
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
|
||||
Call "escapestring" [StringLit s, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (encodeStr s))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
|
||||
Call "latexifystring" [StringLit s, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (encodeLatex s))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
|
||||
_ -> fail
|
||||
let
|
||||
suggest r v output =
|
||||
liftUnification unify (Var output) v
|
||||
|> map (\_ -> MkProofTree { name = r, conclusion = t, premises = [] })
|
||||
in
|
||||
case t of
|
||||
Call "concat" [StringLit s1, StringLit s2, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (s1 ++ s2))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
|
||||
Call "join" [tp, Var output] ->
|
||||
collectStrings tp
|
||||
|> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
|
||||
Call "int" [IntLit i] ->
|
||||
MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "int" [Var output] ->
|
||||
let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
|
||||
in rec 0
|
||||
Call "add" [IntLit i1, IntLit i2, Var output] ->
|
||||
suggest "BuiltinAdd" (IntLit (i1 + i2)) output
|
||||
Call "subtract" [IntLit i1, IntLit i2, Var output] ->
|
||||
suggest "BuiltinSubtract" (IntLit (i1 - i2)) output
|
||||
Call "float" [FloatLit f] ->
|
||||
MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "float" [Var output] ->
|
||||
let rec f = interleave (suggest "BuiltinFloat" (FloatLit f) output) (lazy <| \_ -> rec (f+1))
|
||||
in rec 0
|
||||
Call "num" [tp] ->
|
||||
interleave (builtinRules (Call "int" [tp])) (builtinRules (Call "float" [tp]))
|
||||
|> map (\prem -> MkProofTree { name = "BuiltinNum", conclusion = t, premises = [prem] })
|
||||
Call "str" [StringLit s] ->
|
||||
MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "str" [Var output] ->
|
||||
List.foldr (\s -> interleave (suggest "BuiltinStr" (StringLit s) output)) fail
|
||||
<| String.split "" "abcdefghijklmnopqrstuvwxyz"
|
||||
Call "sym" [Call s []] ->
|
||||
MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
|
||||
|> pure
|
||||
Call "call" [Call s ts, Var name, Var args] ->
|
||||
pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
|
||||
|> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
|
||||
|> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
|
||||
Call "tostring" [tp, Var output] ->
|
||||
let
|
||||
suggestStr s = suggest "BuiltinToString" (StringLit s) output
|
||||
in
|
||||
case tp of
|
||||
IntLit i -> suggestStr (String.fromInt i)
|
||||
FloatLit f -> suggestStr (String.fromFloat f)
|
||||
Call s [] -> suggestStr (encodeStr s)
|
||||
_ -> fail
|
||||
Call "escapestring" [StringLit s, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (encodeStr s))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
|
||||
Call "latexifystring" [StringLit s, Var output] ->
|
||||
liftUnification unify (Var output) (StringLit (encodeLatex s))
|
||||
|> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
|
||||
Call "not" [tp] ->
|
||||
try (proveTerm tp)
|
||||
|> andThen (\mp ->
|
||||
case mp of
|
||||
Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
|
||||
Just _ -> fail)
|
||||
_ -> fail
|
||||
|
||||
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
||||
provePremises = mapM proveTerm
|
||||
|
||||
proveTerm : Term UnificationVar -> Prover ProofTree
|
||||
proveTerm t =
|
||||
map (reify t) getUnificationState
|
||||
getUnificationState
|
||||
|> map (\us -> reify t us)
|
||||
|> andThen (\tp ->
|
||||
burn (
|
||||
getRules
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
module Bergamot.Search exposing (Search, map, apply, andThen, pure, fail, yield, interleave, one)
|
||||
module Bergamot.Search exposing (Search, map, apply, andThen, pure, lazy, fail, yield, interleave, one)
|
||||
|
||||
type SearchStep a
|
||||
= Empty
|
||||
@@ -31,6 +31,9 @@ andThen f sa () =
|
||||
pure : a -> Search a
|
||||
pure a () = Found a (\() -> Empty)
|
||||
|
||||
lazy : (() -> Search a) -> Search a
|
||||
lazy f () = f () ()
|
||||
|
||||
fail : Search a
|
||||
fail () = Empty
|
||||
|
||||
|
||||
@@ -1,5 +1,6 @@
|
||||
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
|
||||
, reify
|
||||
@@ -23,14 +24,25 @@ unUnificationVar (MkUnificationVar s) = s
|
||||
|
||||
type Term a
|
||||
= IntLit Int
|
||||
| FloatLit Float
|
||||
| StringLit String
|
||||
| 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
|
||||
IntLit i -> IntLit i
|
||||
FloatLit ft -> FloatLit ft
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (map f) ts)
|
||||
Var a -> Var (f a)
|
||||
@@ -39,6 +51,7 @@ andThen : (a -> Term b) -> Term a -> Term b
|
||||
andThen f t =
|
||||
case t of
|
||||
IntLit i -> IntLit i
|
||||
FloatLit ft -> FloatLit ft
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (andThen f) ts)
|
||||
Var a -> f a
|
||||
@@ -78,6 +91,7 @@ instantiate : Term Metavariable -> InstantiationState -> (Term UnificationVar, I
|
||||
instantiate mt is =
|
||||
case mt of
|
||||
IntLit i -> (IntLit i, is)
|
||||
FloatLit f -> (FloatLit f, is)
|
||||
StringLit s -> (StringLit s, is)
|
||||
Call n mts -> Tuple.mapFirst (Call n) (instantiateList mts is)
|
||||
Var mv -> Tuple.mapFirst Var (metavariable mv is)
|
||||
@@ -109,12 +123,21 @@ merge v1 v2 us =
|
||||
in
|
||||
case (ui1.term, ui2.term) of
|
||||
(Just t1, Just t2) ->
|
||||
unify t1 t2 us
|
||||
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
|
||||
if occurs ui1.equivalence us t2 || occurs ui2.equivalence us t1
|
||||
then Nothing
|
||||
else
|
||||
unify t1 t2 us
|
||||
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
|
||||
(Just t1, Nothing) ->
|
||||
Just (reconcile newEq (Just t1) us)
|
||||
if occurs ui2.equivalence us t1
|
||||
then Nothing
|
||||
else
|
||||
Just (reconcile newEq (Just t1) us)
|
||||
(Nothing, Just t2) ->
|
||||
Just (reconcile newEq (Just t2) us)
|
||||
if occurs ui1.equivalence us t2
|
||||
then Nothing
|
||||
else
|
||||
Just (reconcile newEq (Just t2) us)
|
||||
(Nothing, Nothing) ->
|
||||
Just (reconcile newEq Nothing us)
|
||||
(Just ui1, Nothing) -> Just (reconcile (Set.insert v2s ui1.equivalence) ui1.term us)
|
||||
@@ -128,13 +151,35 @@ set v t us =
|
||||
in
|
||||
case Dict.get vs us of
|
||||
Just ui ->
|
||||
case ui.term of
|
||||
Just tp ->
|
||||
unify t tp us
|
||||
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
|
||||
Nothing ->
|
||||
Just (t, reconcile ui.equivalence (Just t) us)
|
||||
Nothing -> Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
|
||||
if occurs ui.equivalence us t
|
||||
then Nothing
|
||||
else
|
||||
case ui.term of
|
||||
Just tp ->
|
||||
unify t tp us
|
||||
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
|
||||
Nothing ->
|
||||
Just (t, reconcile ui.equivalence (Just t) us)
|
||||
Nothing ->
|
||||
if occurs (Set.singleton vs) us t
|
||||
then Nothing
|
||||
else
|
||||
Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
|
||||
|
||||
occurs : Set String -> UnificationState -> Term UnificationVar -> Bool
|
||||
occurs vars us t =
|
||||
case t of
|
||||
IntLit _ -> False
|
||||
FloatLit _ -> False
|
||||
StringLit _ -> False
|
||||
Call n ts -> List.any (occurs vars us) ts
|
||||
Var (MkUnificationVar v) -> if Set.member v vars then True else
|
||||
case Dict.get v us of
|
||||
Just { term } ->
|
||||
case term of
|
||||
Just tp -> occurs vars us tp
|
||||
Nothing -> False
|
||||
_ -> False
|
||||
|
||||
unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
|
||||
unifyList l1 l2 us =
|
||||
@@ -149,6 +194,7 @@ unify : Term UnificationVar -> Term UnificationVar -> UnificationState -> Maybe
|
||||
unify t1 t2 us =
|
||||
case (t1, t2) of
|
||||
(IntLit i1, IntLit i2) -> if i1 == i2 then Just (t1, us) else Nothing
|
||||
(FloatLit f1, FloatLit f2) -> if f1 == f2 then Just (t1, us) else Nothing
|
||||
(StringLit s1, StringLit s2) -> if s1 == s2 then Just (t1, us) else Nothing
|
||||
(Call n1 ts1, Call n2 ts2) ->
|
||||
if n1 == n2
|
||||
@@ -165,6 +211,7 @@ reify : Term UnificationVar -> UnificationState -> Term UnificationVar
|
||||
reify t us =
|
||||
case t of
|
||||
IntLit i -> IntLit i
|
||||
FloatLit f -> FloatLit f
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (\tp -> reify tp us) ts)
|
||||
Var v ->
|
||||
|
||||
327
src/Main.elm
327
src/Main.elm
@@ -1,4 +1,4 @@
|
||||
module Main exposing (main)
|
||||
port module Main exposing (main)
|
||||
|
||||
import Browser
|
||||
import Html exposing (Html)
|
||||
@@ -10,9 +10,9 @@ import Bergamot.Search exposing (..)
|
||||
import Bergamot.Rules exposing (..)
|
||||
import Bergamot.Parser exposing (..)
|
||||
import Bergamot.Latex exposing (..)
|
||||
import Bergamot.ObjectLanguage exposing (..)
|
||||
import Bergamot.Utils exposing (..)
|
||||
import Json.Encode
|
||||
import Json.Decode exposing (string, field, list, oneOf, succeed, fail)
|
||||
import Maybe
|
||||
import Tuple
|
||||
|
||||
@@ -31,32 +31,117 @@ tabEq t1 t2 =
|
||||
|
||||
type EditMode
|
||||
= Query
|
||||
| Syntax
|
||||
| Custom String
|
||||
|
||||
modeEq : EditMode -> EditMode -> Bool
|
||||
modeEq m1 m2 =
|
||||
case (m1, m2) of
|
||||
(Query, Query) -> True
|
||||
(Syntax, Syntax) -> True
|
||||
type ResultMode
|
||||
= Conclusion
|
||||
| Tree
|
||||
|
||||
type DesugaringState
|
||||
= Requested
|
||||
| Succeeded String
|
||||
| Failed String
|
||||
|
||||
resultModeEq : ResultMode -> ResultMode -> Bool
|
||||
resultModeEq rm1 rm2 =
|
||||
case (rm1, rm2) of
|
||||
(Conclusion, Conclusion) -> True
|
||||
(Tree, Tree) -> True
|
||||
_ -> False
|
||||
|
||||
type alias Model =
|
||||
{ program : String
|
||||
-- ^ The Bergamot rules to execute a search against
|
||||
, renderProgram: String
|
||||
, query : String
|
||||
-- ^ The Bergamot render rules to apply when generating LaTeX
|
||||
, tab : Tab
|
||||
, editMode : EditMode
|
||||
-- ^ The current tab (editor, redner rule editor, rendered)
|
||||
, input : String
|
||||
-- ^ The string the user has in the input box
|
||||
, desugaredQuery : DesugaringState
|
||||
-- ^ The Bergamot query corresponding to input, if we're in custom mode.
|
||||
, inputModes : List (String, EditMode)
|
||||
-- ^ A List of input modes that can be used with the input box.
|
||||
, inputMode : Int
|
||||
-- ^ The index of the currently selected input mode.
|
||||
, resultMode : ResultMode
|
||||
-- ^ How the result should be displayed (judgement or proof tree)
|
||||
}
|
||||
type alias Flags =
|
||||
{ renderRules : String
|
||||
, rules : String
|
||||
, input : String
|
||||
, inputModes : Json.Decode.Value
|
||||
}
|
||||
type alias Flags = { renderRules: String, rules: String, query: String }
|
||||
type Msg
|
||||
= SetProgram String
|
||||
| SetRenderProgram String
|
||||
| SetQuery String
|
||||
| SetInput String
|
||||
| SetTab Tab
|
||||
| SetEditMode EditMode
|
||||
| SetInputMode Int
|
||||
| SetResultMode ResultMode
|
||||
| SetDesugaredQuery { input: String, result: Json.Decode.Value }
|
||||
|
||||
decodeRenderResult : Json.Decode.Value -> Result String String
|
||||
decodeRenderResult val =
|
||||
let
|
||||
succeedDecoder = field "query" string |> Json.Decode.map Ok
|
||||
failDecoder = field "error" string |> Json.Decode.map Err
|
||||
decoder = Json.Decode.oneOf [ succeedDecoder, failDecoder ]
|
||||
in
|
||||
case Json.Decode.decodeValue decoder val of
|
||||
Ok v -> v
|
||||
Err _ -> Err "Unable to convert input into query"
|
||||
|
||||
decodeInputModes : Json.Decode.Value -> List (String, EditMode)
|
||||
decodeInputModes val =
|
||||
let
|
||||
exactString s1 v =
|
||||
string
|
||||
|> Json.Decode.andThen (\s2 ->
|
||||
if s1 == s2
|
||||
then succeed v
|
||||
else Json.Decode.fail "did not match expected string")
|
||||
editModeDecoder = oneOf
|
||||
[ exactString "query" Query
|
||||
, field "custom" string |> Json.Decode.map Custom
|
||||
]
|
||||
decoder = Json.Decode.keyValuePairs editModeDecoder
|
||||
in
|
||||
case Json.Decode.decodeValue decoder val of
|
||||
Ok l -> l
|
||||
Err _ -> [("Query", Query)]
|
||||
|
||||
-- Convert the user-entered string 'input' using custom query mode 'mode'
|
||||
port convertInput : { mode : String, input : String } -> Cmd msg
|
||||
|
||||
-- Invoked when user code finishes converting 'input' into a Bergamot query
|
||||
port receiveConverted : ({ input : String, result : Json.Decode.Value } -> msg) -> Sub msg
|
||||
|
||||
requestDesugaring : Int -> List (String, EditMode) -> String -> Cmd Msg
|
||||
requestDesugaring inputMode inputModes input =
|
||||
case getEditMode inputMode inputModes of
|
||||
Ok (Custom modeType) ->
|
||||
convertInput { mode = modeType, input = input }
|
||||
_ -> Cmd.none
|
||||
|
||||
init : Flags -> (Model, Cmd Msg)
|
||||
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
|
||||
init fs =
|
||||
let
|
||||
inputModes = decodeInputModes fs.inputModes
|
||||
inputMode = 0
|
||||
in
|
||||
( { program = fs.rules
|
||||
, renderProgram = fs.renderRules
|
||||
, input = fs.input
|
||||
, desugaredQuery = Requested
|
||||
, tab = Rendered
|
||||
, inputModes = inputModes
|
||||
, inputMode = 0
|
||||
, resultMode = Conclusion
|
||||
}
|
||||
, requestDesugaring inputMode inputModes fs.input
|
||||
)
|
||||
|
||||
viewSection : String -> Html Msg -> Html Msg
|
||||
viewSection name content =
|
||||
@@ -69,20 +154,23 @@ viewTab tab editor metaEditor rendered =
|
||||
MetaEditor -> metaEditor
|
||||
Rendered -> rendered
|
||||
|
||||
viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
|
||||
viewSelector : (Int -> a -> b -> Bool) -> (Int -> a -> Msg) -> b -> List (a, String) -> Html Msg
|
||||
viewSelector eq mkMsg mode modeNames =
|
||||
Html.div [ class "bergamot-selector" ] <|
|
||||
List.map (\(modep, name) ->
|
||||
List.indexedMap (\idx (modep, name) ->
|
||||
Html.button
|
||||
[ classList [("active", eq mode modep)]
|
||||
, onClick (mkMsg modep)
|
||||
[ classList [("active", eq idx modep mode)]
|
||||
, onClick (mkMsg idx modep)
|
||||
] [ Html.text name ]) modeNames
|
||||
|
||||
viewTabSelector : Tab -> List (Tab, String) -> Html Msg
|
||||
viewTabSelector = viewSelector tabEq SetTab
|
||||
viewTabSelector = viewSelector (\_ -> tabEq) (\_ -> SetTab)
|
||||
|
||||
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
|
||||
viewEditModeSelector = viewSelector modeEq SetEditMode
|
||||
viewInputModeSelector : Int -> List (EditMode, String) -> Html Msg
|
||||
viewInputModeSelector = viewSelector (\i _ idx -> i == idx) (\idx _ -> SetInputMode idx)
|
||||
|
||||
viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
|
||||
viewResultModeSelector = viewSelector (\_ -> resultModeEq) (\_ -> SetResultMode)
|
||||
|
||||
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
|
||||
viewRule env r = renderRuleViaRules env r
|
||||
@@ -93,67 +181,180 @@ viewRuleSection env sec =
|
||||
List.map (viewRule env) sec.rules
|
||||
|> sequenceMaybes
|
||||
|> Maybe.map (\rs ->
|
||||
Html.div [ class "bergamot-rule-section" ]
|
||||
[ Html.div [ class "bergamot-rule-list" ] rs
|
||||
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
|
||||
])
|
||||
case sec.hidden of
|
||||
True -> Html.div [ class "bergamot-rule-section" ] []
|
||||
False ->
|
||||
Html.div [ class "bergamot-rule-section" ]
|
||||
[ Html.div [ class "bergamot-rule-list" ] rs
|
||||
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
|
||||
])
|
||||
|
||||
viewRules : String -> String -> Html Msg
|
||||
viewRules renderProgs progs = viewSection "Rendered Rules" <|
|
||||
viewRules renderProgs progs =
|
||||
Html.div [ class "bergamot-section-list" ] <|
|
||||
case (run program renderProgs, run program progs) of
|
||||
(Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
|
||||
case progAndRenderProg progs renderProgs of
|
||||
Ok (prog, renderProg) -> List.filterMap (viewRuleSection renderProg) prog.sections
|
||||
_ -> []
|
||||
|
||||
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
||||
proofGoal mode querys =
|
||||
case mode of
|
||||
Query -> run term querys
|
||||
Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
|
||||
type Error
|
||||
= BadQuery
|
||||
| NoConversionResults
|
||||
| BadInputProg
|
||||
| BadProg
|
||||
| BadRenderProg
|
||||
| FailedRender String
|
||||
| InvalidInputMode
|
||||
| Silent
|
||||
|
||||
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
|
||||
combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
|
||||
combineTwoResults f ra rb =
|
||||
case ra of
|
||||
Err _ -> Err Silent
|
||||
Ok a ->
|
||||
case rb of
|
||||
Err _ -> Err Silent
|
||||
Ok b -> f a b
|
||||
|
||||
viewProofTree : EditMode -> String -> String -> String -> Html Msg
|
||||
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
|
||||
Html.div [ class "bergamot-proof-tree" ] <|
|
||||
case tryProve mode progs querys of
|
||||
Just tree ->
|
||||
case run program renderProgs of
|
||||
Just renderProg ->
|
||||
List.map latex
|
||||
<| List.filterMap (renderTreeViaRules renderProg)
|
||||
<| [ tree ]
|
||||
Nothing -> []
|
||||
Nothing -> []
|
||||
errorToString : Error -> String
|
||||
errorToString err =
|
||||
case err of
|
||||
BadQuery -> "Unable to parse input query"
|
||||
NoConversionResults -> "Failed to convert object language term to proof goal"
|
||||
BadInputProg -> "Unable to parse conversion rules from object language to proof goals"
|
||||
BadProg -> "Unable to parse rules"
|
||||
BadRenderProg -> "Unable to parse rendering rules"
|
||||
FailedRender s -> s
|
||||
InvalidInputMode -> "Invalid edit mode specified"
|
||||
Silent -> ""
|
||||
|
||||
viewError : Error -> Html Msg
|
||||
viewError e = Html.div [ class "bergamot-error" ] [ Html.text <| errorToString e ]
|
||||
|
||||
viewIfError : Result Error a -> List (Html Msg)
|
||||
viewIfError r =
|
||||
case r of
|
||||
Err Silent -> []
|
||||
Err e -> [ viewError e ]
|
||||
_ -> []
|
||||
|
||||
viewOrError : Result Error (Html Msg) -> Html Msg
|
||||
viewOrError r =
|
||||
case r of
|
||||
Err Silent -> Html.div [] []
|
||||
Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
|
||||
Ok html -> html
|
||||
|
||||
getEditMode : Int -> List (String, EditMode) -> Result Error EditMode
|
||||
getEditMode i l =
|
||||
case l of
|
||||
[] -> Err InvalidInputMode
|
||||
((_, editMode) :: xs) ->
|
||||
if i == 0 then Ok editMode else getEditMode (i - 1) xs
|
||||
|
||||
proofGoal : EditMode -> String -> DesugaringState -> Result Error (Term Metavariable)
|
||||
proofGoal editMode input desugaredQuery =
|
||||
if input == ""
|
||||
then Err Silent
|
||||
else
|
||||
case editMode of
|
||||
Query ->
|
||||
case run topLevelTerm input of
|
||||
Nothing -> Err BadQuery
|
||||
Just query -> Ok query
|
||||
Custom _ ->
|
||||
case desugaredQuery of
|
||||
Requested -> Err Silent
|
||||
Succeeded querys ->
|
||||
case run topLevelTerm querys of
|
||||
Nothing -> Err BadQuery
|
||||
Just query -> Ok query
|
||||
Failed s -> Err (FailedRender s)
|
||||
|
||||
progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
|
||||
progAndRenderProg progs renderProgs =
|
||||
case (run program progs, run program renderProgs) of
|
||||
(Just prog, Just renderProg) -> Ok (prog, renderProg)
|
||||
(Nothing, _) -> Err BadProg
|
||||
(_, Nothing) -> Err BadRenderProg
|
||||
|
||||
renderProofTree : ResultMode -> ProofTree -> RuleEnv -> Result Error (Html Msg)
|
||||
renderProofTree resultMode (MkProofTree node) renderProg =
|
||||
let
|
||||
maybeLatexString =
|
||||
case resultMode of
|
||||
Conclusion -> renderTermViaRules renderProg (quoteVariables node.conclusion)
|
||||
Tree -> renderTreeViaRules renderProg (MkProofTree node)
|
||||
in
|
||||
List.filterMap (Maybe.map latex) [maybeLatexString]
|
||||
|> Html.div [ class "bergamot-proof-tree" ]
|
||||
|> Ok
|
||||
|
||||
|
||||
viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result Error (Html Msg)
|
||||
viewProofTree resultMode query (prog, renderProg) =
|
||||
case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
|
||||
Just proofTree -> renderProofTree resultMode proofTree renderProg
|
||||
Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ]
|
||||
[ Html.text "No applicable rules to prove input" ]
|
||||
|
||||
view : Model -> Html Msg
|
||||
view m = Html.div [ class "bergamot-root" ]
|
||||
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")]
|
||||
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
||||
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
|
||||
, viewProofTree m.editMode m.renderProgram m.program m.query
|
||||
, viewTab m.tab
|
||||
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
|
||||
(viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
|
||||
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
||||
]
|
||||
view m =
|
||||
let
|
||||
mode = getEditMode m.inputMode m.inputModes
|
||||
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
|
||||
Html.div [ class "bergamot-root" ]
|
||||
[ viewSection "Input" <| Html.div [] <|
|
||||
[ viewInputModeSelector m.inputMode <|
|
||||
List.map (\(a, b) -> (b, a)) m.inputModes
|
||||
, Html.input [ type_ "text", onInput SetInput, value m.input ] []
|
||||
] ++
|
||||
viewIfError termOrErr
|
||||
, viewSection "Result" <| Html.div[]
|
||||
[ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
|
||||
, viewOrError proofTreeOrErr
|
||||
]
|
||||
, viewSection "Rules" <| Html.div [] <|
|
||||
[ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
|
||||
, viewTab m.tab
|
||||
(Html.textarea [ onInput SetProgram, value m.program ] [ ])
|
||||
(Html.textarea [ onInput SetRenderProgram, value m.renderProgram ] [ ])
|
||||
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
||||
] ++
|
||||
viewIfError progsOrErr
|
||||
]
|
||||
|
||||
update : Msg -> Model -> (Model, Cmd Msg)
|
||||
update msg m =
|
||||
case msg of
|
||||
SetProgram prog -> ({ m | program = prog }, Cmd.none)
|
||||
SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
|
||||
SetQuery query -> ({ m | query = query }, Cmd.none)
|
||||
SetInput input ->
|
||||
( { m | input = input, desugaredQuery = Requested }
|
||||
, requestDesugaring m.inputMode m.inputModes input
|
||||
)
|
||||
SetTab tab -> ({ m | tab = tab }, Cmd.none)
|
||||
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
|
||||
SetInputMode mode ->
|
||||
( { m | inputMode = mode, desugaredQuery = Requested }
|
||||
, requestDesugaring mode m.inputModes m.input
|
||||
)
|
||||
SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
|
||||
SetDesugaredQuery data ->
|
||||
({ m | desugaredQuery =
|
||||
if m.input == data.input
|
||||
then
|
||||
case decodeRenderResult data.result of
|
||||
Ok q -> Succeeded q
|
||||
Err e -> Failed e
|
||||
else m.desugaredQuery
|
||||
}
|
||||
, Cmd.none
|
||||
)
|
||||
|
||||
subscriptions : Model -> Sub Msg
|
||||
subscriptions _ = Sub.none
|
||||
subscriptions _ = receiveConverted SetDesugaredQuery
|
||||
|
||||
main =
|
||||
Browser.element
|
||||
|
||||
Reference in New Issue
Block a user