Compare commits
No commits in common. "18d524a0d27c9cc66d8b5e8cf1fa79532e3e1313" and "bb18c8bd8cb9dedb749b6683f701a9a478f33960" have entirely different histories.
18d524a0d2
...
bb18c8bd8c
@ -1,32 +0,0 @@
|
||||
LatexListNil @ latexlist(nil, nil) <-;
|
||||
LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
|
||||
|
||||
IntercalateNil @ intercalate(?sep, nil, nil) <-;
|
||||
IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
|
||||
IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
|
||||
|
||||
NonEmpty @ nonempty(cons(?x, ?xs)) <-;
|
||||
|
||||
LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?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);
|
||||
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);
|
||||
|
||||
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);
|
||||
|
||||
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);
|
||||
LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\in ", ?l_G], ?l);
|
||||
|
||||
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);
|
||||
@ -1,49 +1,7 @@
|
||||
module Bergamot.Latex exposing (..)
|
||||
|
||||
import Bergamot.Syntax as Syntax exposing (..)
|
||||
import Bergamot.Rules as Rules exposing (..)
|
||||
import Bergamot.Utils exposing (..)
|
||||
|
||||
import Debug
|
||||
|
||||
type Void = Void Void
|
||||
|
||||
absurd : Void -> a
|
||||
absurd (Void v) = absurd v
|
||||
|
||||
renderTermViaRules : RuleEnv -> Term Void -> Maybe String
|
||||
renderTermViaRules env t =
|
||||
Call "latex" [Syntax.map absurd t, Var (MkMetavariable "s")]
|
||||
|> prove
|
||||
|> Rules.andThen reifyProofTree
|
||||
|> single env
|
||||
|> Maybe.andThen (\(MkProofTree node) ->
|
||||
case node.conclusion of
|
||||
Call "latex" [_, StringLit s] -> Just s
|
||||
_ -> Nothing)
|
||||
|
||||
renderRuleViaRules : RuleEnv -> Rule -> Maybe String
|
||||
renderRuleViaRules env r =
|
||||
let
|
||||
quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises
|
||||
quotedConc = Syntax.andThen quoteMetavariable r.conclusion
|
||||
buildStr conc prems = String.concat
|
||||
[ "\\cfrac{"
|
||||
, String.join "\\quad " prems
|
||||
, "}{"
|
||||
, conc
|
||||
, "}\\ \\texttt{"
|
||||
, r.name
|
||||
, "}"
|
||||
]
|
||||
in
|
||||
renderTermViaRules env quotedConc
|
||||
|> Maybe.andThen (\conc ->
|
||||
sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
|
||||
|> Maybe.map (\prems -> buildStr conc prems))
|
||||
|
||||
quoteMetavariable : Metavariable -> Term Void
|
||||
quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v]
|
||||
import Bergamot.Syntax exposing (..)
|
||||
import Bergamot.Rules exposing (..)
|
||||
|
||||
termToLatex : (a -> String) -> Term a -> String
|
||||
termToLatex f t =
|
||||
@ -66,7 +24,7 @@ termToLatex f t =
|
||||
Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
|
||||
Var x -> f x
|
||||
IntLit i -> String.fromInt i
|
||||
StringLit s -> "\\texttt{" ++ "\"" ++ encodeLatex (encodeStr s) ++ "\"" ++ "}"
|
||||
StringLit s -> "\"" ++ s ++ "\""
|
||||
|
||||
metavariableToLatex : Metavariable -> String
|
||||
metavariableToLatex (MkMetavariable s) =
|
||||
|
||||
@ -1,144 +0,0 @@
|
||||
module Bergamot.ObjectLanguage exposing (..)
|
||||
|
||||
import Bergamot.Syntax as Syntax exposing (Metavariable)
|
||||
|
||||
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
|
||||
]
|
||||
|
||||
typeToTerm : Type -> Syntax.Term Metavariable
|
||||
typeToTerm t =
|
||||
case t of
|
||||
TInt -> Syntax.Call "tint" []
|
||||
TStr -> Syntax.Call "tstr" []
|
||||
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 e =
|
||||
case e of
|
||||
IntLit i -> Syntax.Call "intlit" [Syntax.IntLit i]
|
||||
StrLit s -> Syntax.Call "strlit" [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]
|
||||
Snd ep -> Syntax.Call "snd" [exprToTerm ep]
|
||||
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 []]
|
||||
@ -2,7 +2,6 @@ module Bergamot.Parser exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (Term(..), Metavariable(..))
|
||||
import Bergamot.Rules exposing (Rule, RuleEnv)
|
||||
import Bergamot.Utils exposing (decodeStr)
|
||||
|
||||
import Parser exposing (Parser, Trailing(..), (|.), (|=))
|
||||
import Set
|
||||
@ -10,30 +9,9 @@ import Set
|
||||
intLit : Parser Int
|
||||
intLit = Parser.int
|
||||
|
||||
strLit : Parser String
|
||||
strLit =
|
||||
let
|
||||
char = Parser.map decodeStr <| Parser.getChompedString <|
|
||||
Parser.oneOf
|
||||
[ Parser.backtrackable <|
|
||||
Parser.chompIf (\c -> c == '\\')
|
||||
|. Parser.chompIf (\c -> True)
|
||||
, Parser.backtrackable <| Parser.chompIf (\c -> c /= '"')
|
||||
]
|
||||
in
|
||||
Parser.map (String.join "") <| Parser.sequence
|
||||
{ start = "\""
|
||||
, separator = ""
|
||||
, end = "\""
|
||||
, spaces = Parser.succeed ()
|
||||
, item = char
|
||||
, trailing = Optional
|
||||
}
|
||||
|
||||
|
||||
name : Parser String
|
||||
name = Parser.variable
|
||||
{ start = \c -> Char.isAlpha c || c == '_'
|
||||
{ start = \c -> Char.isAlphaNum c || c == '_'
|
||||
, inner = \c -> Char.isAlphaNum c || c == '_'
|
||||
, reserved = Set.empty
|
||||
}
|
||||
@ -60,23 +38,12 @@ term = Parser.lazy (\() -> Parser.oneOf
|
||||
, item = term
|
||||
, trailing = Forbidden
|
||||
}
|
||||
, Parser.backtrackable
|
||||
<| Parser.map (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []))
|
||||
<| Parser.sequence
|
||||
{ start = "["
|
||||
, separator = ","
|
||||
, end = "]"
|
||||
, spaces = Parser.spaces
|
||||
, item = term
|
||||
, trailing = Forbidden
|
||||
}
|
||||
, Parser.backtrackable <|
|
||||
Parser.succeed (\n -> Call n [])
|
||||
|= name
|
||||
, Parser.backtrackable <|
|
||||
Parser.succeed Var |= variable
|
||||
, Parser.succeed IntLit |= intLit
|
||||
, Parser.succeed StringLit |= strLit
|
||||
])
|
||||
|
||||
rule : Parser Rule
|
||||
|
||||
@ -1,8 +1,7 @@
|
||||
module Bergamot.Rules exposing (..)
|
||||
|
||||
import Bergamot.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
|
||||
import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
|
||||
import Bergamot.Search as Search exposing (Search)
|
||||
import Bergamot.Utils exposing (encodeStr, encodeLatex)
|
||||
|
||||
import Debug
|
||||
|
||||
@ -33,7 +32,7 @@ type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
|
||||
andThen : (a -> Prover b) -> Prover a -> Prover b
|
||||
andThen f p env ps =
|
||||
p env ps
|
||||
|> Search.andThen (\(a, psp) -> (f a) env psp)
|
||||
|> Search.andThen (\(a, psp) -> if psp.gas > 0 then (f a) env psp else Search.fail)
|
||||
|
||||
join : Prover (Prover a) -> Prover a
|
||||
join p = andThen (\x -> x) p
|
||||
@ -75,7 +74,7 @@ getUnificationState : Prover UnificationState
|
||||
getUnificationState env ps = Search.pure (ps.unificationState, ps)
|
||||
|
||||
burn : Prover ()
|
||||
burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail
|
||||
burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
|
||||
|
||||
liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
|
||||
liftInstantiation f a env ps =
|
||||
@ -105,71 +104,25 @@ reifyProofTree (MkProofTree node) =
|
||||
rule : Term UnificationVar -> Rule -> Prover ProofTree
|
||||
rule t r =
|
||||
withVars (pure Tuple.pair
|
||||
|> apply (liftInstantiation instantiate r.conclusion
|
||||
|> andThen (\conc -> liftUnification unify t conc))
|
||||
|> apply (liftInstantiation instantiate r.conclusion)
|
||||
|> apply (liftInstantiation instantiateList r.premises))
|
||||
|> andThen (\(conc, prems) ->
|
||||
provePremises prems)
|
||||
|> map (\trees -> MkProofTree { name = r.name, conclusion = t, premises = trees })
|
||||
|
||||
collectStrings : Term UnificationVar -> Prover (List String)
|
||||
collectStrings t =
|
||||
case t of
|
||||
Call "cons" [StringLit s, rest] -> map (\ss -> s :: ss) <| collectStrings rest
|
||||
Call "nil" [] -> pure []
|
||||
_ -> fail
|
||||
|
||||
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
|
||||
pure (\tp trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees })
|
||||
|> apply (liftUnification unify t conc)
|
||||
|> apply (provePremises prems))
|
||||
|
||||
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
||||
provePremises = mapM proveTerm
|
||||
|
||||
proveTerm : Term UnificationVar -> Prover ProofTree
|
||||
proveTerm t =
|
||||
map (reify t) getUnificationState
|
||||
|> andThen (\tp ->
|
||||
burn
|
||||
|> andThen (\() -> getEnv)
|
||||
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp) env.rules))
|
||||
burn
|
||||
|> andThen (\() -> getEnv)
|
||||
|> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
|
||||
|
||||
prove : Term Metavariable -> Prover ProofTree
|
||||
prove mt =
|
||||
withVars (liftInstantiation instantiate mt)
|
||||
liftInstantiation instantiate mt
|
||||
|> andThen proveTerm
|
||||
|
||||
single : RuleEnv -> Prover a -> Maybe a
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
module Bergamot.Syntax exposing
|
||||
( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
|
||||
( Term(..), Metavariable(..), UnificationVar(..)
|
||||
, instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
|
||||
, unify, unifyList, UnificationState, emptyUnificationState
|
||||
, reify
|
||||
@ -27,22 +27,6 @@ type Term a
|
||||
| Call Name (List (Term a))
|
||||
| Var a
|
||||
|
||||
map : (a -> b) -> Term a -> Term b
|
||||
map f t =
|
||||
case t of
|
||||
IntLit i -> IntLit i
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (map f) ts)
|
||||
Var a -> Var (f a)
|
||||
|
||||
andThen : (a -> Term b) -> Term a -> Term b
|
||||
andThen f t =
|
||||
case t of
|
||||
IntLit i -> IntLit i
|
||||
StringLit s -> StringLit s
|
||||
Call n ts -> Call n (List.map (andThen f) ts)
|
||||
Var a -> f a
|
||||
|
||||
type alias InstantiationState =
|
||||
{ counter : Int
|
||||
, vars : Dict String UnificationVar
|
||||
|
||||
@ -1,46 +0,0 @@
|
||||
module Bergamot.Utils exposing (..)
|
||||
|
||||
decodeStr : String -> String
|
||||
decodeStr str =
|
||||
let
|
||||
go l =
|
||||
case l of
|
||||
'\\' :: '"' :: rest -> '"' :: go rest
|
||||
'\\' :: c :: rest -> c :: go rest
|
||||
c :: rest -> c :: go rest
|
||||
[] -> []
|
||||
noQuotes = String.dropLeft 1 <| String.dropRight 1 <| str
|
||||
in
|
||||
String.fromList (go (String.toList str))
|
||||
|
||||
encodeStr : String -> String
|
||||
encodeStr s =
|
||||
let
|
||||
go l =
|
||||
case l of
|
||||
'\\' :: xs -> '\\' :: '\\' :: go xs
|
||||
'"' :: xs -> '\\' :: '"' :: go xs
|
||||
x :: xs -> x :: go xs
|
||||
[] -> []
|
||||
in
|
||||
String.fromList (go (String.toList s))
|
||||
|
||||
encodeLatex : String -> String
|
||||
encodeLatex s =
|
||||
let
|
||||
go l =
|
||||
case l of
|
||||
'\\' :: xs -> String.toList "\\textbackslash " ++ go xs
|
||||
'{' :: xs -> '\\' :: '{' :: go xs
|
||||
'}' :: xs -> '\\' :: '}' :: go xs
|
||||
x :: xs -> x :: go xs
|
||||
[] -> []
|
||||
in
|
||||
String.fromList (go (String.toList s))
|
||||
|
||||
sequenceMaybes : List (Maybe a) -> Maybe (List a)
|
||||
sequenceMaybes l =
|
||||
case l of
|
||||
[] -> Just []
|
||||
(Just x :: mxs) -> sequenceMaybes mxs |> Maybe.map (\xs -> x :: xs)
|
||||
_ -> Nothing
|
||||
103
src/Main.elm
103
src/Main.elm
@ -2,123 +2,64 @@ module Main exposing (main)
|
||||
|
||||
import Browser
|
||||
import Html exposing (Html)
|
||||
import Html.Events exposing (onInput, onClick)
|
||||
import Html.Attributes exposing (type_, class, classList, value)
|
||||
import Html.Lazy
|
||||
import Html.Events exposing (onInput)
|
||||
import Html.Attributes exposing (type_, class, value)
|
||||
import Bergamot.Syntax exposing (..)
|
||||
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
|
||||
|
||||
type Tab
|
||||
= Editor
|
||||
| Rendered
|
||||
|
||||
tabEq : Tab -> Tab -> Bool
|
||||
tabEq t1 t2 =
|
||||
case (t1, t2) of
|
||||
(Editor, Editor) -> True
|
||||
(Rendered, Rendered) -> True
|
||||
_ -> False
|
||||
|
||||
type EditMode
|
||||
= Query
|
||||
| Syntax
|
||||
|
||||
modeEq : EditMode -> EditMode -> Bool
|
||||
modeEq m1 m2 =
|
||||
case (m1, m2) of
|
||||
(Query, Query) -> True
|
||||
(Syntax, Syntax) -> True
|
||||
_ -> False
|
||||
import Debug
|
||||
|
||||
type alias Model =
|
||||
{ program : String
|
||||
, renderProgram: String
|
||||
, query : String
|
||||
, tab : Tab
|
||||
, editMode : EditMode
|
||||
}
|
||||
type alias Flags = { renderRules: String, rules: String, query: String }
|
||||
type alias Flags = { rules: String, query: String }
|
||||
type Msg
|
||||
= SetProgram String
|
||||
| SetQuery String
|
||||
| SetTab Tab
|
||||
| SetEditMode EditMode
|
||||
|
||||
init : Flags -> (Model, Cmd Msg)
|
||||
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
|
||||
init fs = ({ program = fs.rules, query = fs.query }, Cmd.none)
|
||||
|
||||
viewSection : String -> Html Msg -> Html Msg
|
||||
viewSection name content =
|
||||
Html.div [ class "bergamot-section" ] [ Html.em [ class "bergamot-section-heading" ] [ Html.text name ], content ]
|
||||
|
||||
viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
|
||||
viewTab tab editor rendered =
|
||||
case tab of
|
||||
Editor -> editor
|
||||
Rendered -> rendered
|
||||
viewRule : Rule -> Html Msg
|
||||
viewRule = latex << ruleToLatex
|
||||
|
||||
viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
|
||||
viewSelector eq mkMsg mode modeNames =
|
||||
Html.div [ class "bergamot-selector" ] <|
|
||||
List.map (\(modep, name) ->
|
||||
Html.button
|
||||
[ classList [("active", eq mode modep)]
|
||||
, onClick (mkMsg modep)
|
||||
] [ Html.text name ]) modeNames
|
||||
|
||||
viewTabSelector : Tab -> List (Tab, String) -> Html Msg
|
||||
viewTabSelector = viewSelector tabEq SetTab
|
||||
|
||||
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
|
||||
viewEditModeSelector = viewSelector modeEq SetEditMode
|
||||
|
||||
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
|
||||
viewRule env r = renderRuleViaRules env r
|
||||
|> Maybe.map latex
|
||||
|
||||
viewRules : String -> String -> Html Msg
|
||||
viewRules renderProgs progs = viewSection "Rendered Rules" <|
|
||||
viewRules : String -> Html Msg
|
||||
viewRules progs = viewSection "Rendered Rules" <|
|
||||
Html.div [ class "bergamot-rule-list" ] <|
|
||||
case (run program renderProgs, run program progs) of
|
||||
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) prog.rules
|
||||
_ -> []
|
||||
case run program progs of
|
||||
Just prog -> List.map viewRule prog.rules
|
||||
Nothing -> []
|
||||
|
||||
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
||||
proofGoal mode querys =
|
||||
case mode of
|
||||
Query -> run term querys
|
||||
Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
|
||||
|
||||
tryProve : EditMode -> String -> String -> Maybe ProofTree
|
||||
tryProve mode progs querys =
|
||||
case (run program progs, proofGoal mode querys) of
|
||||
tryProve : String -> String -> Maybe ProofTree
|
||||
tryProve progs querys =
|
||||
case (run program progs, run term querys) of
|
||||
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
|
||||
_ -> Nothing
|
||||
|
||||
viewProofTree : EditMode -> String -> String -> Html Msg
|
||||
viewProofTree mode progs querys = viewSection "Proof Tree" <|
|
||||
viewProofTree : String -> String -> Html Msg
|
||||
viewProofTree progs querys = viewSection "Proof Tree" <|
|
||||
Html.div [ class "bergamot-proof-tree" ] <|
|
||||
case tryProve mode progs querys of
|
||||
case tryProve progs querys of
|
||||
Just tree -> [ latex (proofTreeToLatex tree) ]
|
||||
Nothing -> []
|
||||
|
||||
|
||||
view : Model -> Html Msg
|
||||
view m = Html.div [ class "bergamot-root" ]
|
||||
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
|
||||
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
||||
, viewTab m.tab
|
||||
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
|
||||
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
||||
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]
|
||||
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
|
||||
, viewProofTree m.editMode m.program m.query
|
||||
, viewRules m.program
|
||||
, viewProofTree m.program m.query
|
||||
]
|
||||
|
||||
update : Msg -> Model -> (Model, Cmd Msg)
|
||||
@ -126,8 +67,6 @@ update msg m =
|
||||
case msg of
|
||||
SetProgram prog -> ({ m | program = prog }, Cmd.none)
|
||||
SetQuery query -> ({ m | query = query }, Cmd.none)
|
||||
SetTab tab -> ({ m | tab = tab }, Cmd.none)
|
||||
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
|
||||
|
||||
subscriptions : Model -> Sub Msg
|
||||
subscriptions _ = Sub.none
|
||||
|
||||
Loading…
Reference in New Issue
Block a user