Minor tweaks to style and rule rendering

Add some styling (still very early stages)
Add an index.html file that includes the web component
2023-11-26 16:32:27 -08:00 · 2023-11-26 16:25:23 -08:00 · 2023-11-26 15:54:17 -08:00 · 2023-11-26 15:54:01 -08:00 · 2023-11-26 14:34:52 -08:00 · 2023-11-26 13:14:44 -08:00
8 changed files with 283 additions and 77 deletions
--- a/elm.json
+++ b/elm.json
@ -9,10 +9,10 @@
            "elm/browser": "1.0.2",
            "elm/core": "1.0.5",
            "elm/html": "1.0.0",
+            "elm/json": "1.1.3",
            "elm/parser": "1.1.0"
        },
        "indirect": {
-            "elm/json": "1.1.3",
            "elm/time": "1.0.0",
            "elm/url": "1.0.0",
            "elm/virtual-dom": "1.0.3"
--- a/index.html
+++ b/index.html
@ -0,0 +1,60 @@
+<!DOCTYPE HTML>
+<html>
+<head>
+  <meta charset="UTF-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1" />
+  <title>Main</title>
+  <script type="module" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.esm.js"></script>
+  <script nomodule="" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.js"></script>
+  <style>body { padding: 0; margin: 0; }</style>
+  <style>
+textarea {
+    display: block;
+    width: 100%;
+    height: 10em;
+    resize: none;
+}
+
+input[type="text"] {
+    width: 100%;
+}
+
+.rule-list {
+    display: flex;
+    flex-direction: row;
+    flex-wrap: wrap;
+    justify-content: center;
+}
+
+.rule-list katex-expression {
+    margin-left: .5em;
+    margin-right: .5em;
+    flex-grow: 1;
+    flex-basis: 0;
+}
+
+.elm-root {
+    max-width: 800px;
+    margin: auto;
+    padding: 1em;
+    border: 1px solid #c3c3c3;
+    border-radius: 0.5em;
+    margin-top: 1em;
+}
+
+.elm-root h2 {
+    margin-bottom: 0.5em;
+}
+  </style>
+</head>
+
+<body>
+    <div id="elm"></div>
+    <script src="index.js"></script>
+    <script>
+        var app = Elm.Main.init({
+          node: document.getElementById('elm')
+        });
+    </script>
+</body>
+</html>
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@ -0,0 +1,35 @@
+module Bergamot.Latex exposing (..)
+
+import Bergamot.Syntax exposing (..)
+import Bergamot.Rules exposing (..)
+
+termToLatex : (a -> String) -> Term a -> String
+termToLatex f t =
+    case t of
+        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
+        Call "intlit" [t1]   -> termToLatex f t1
+        Call "strlit" [t1]   -> termToLatex f t1
+        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
+        Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
+        Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
+        Call s [] -> "\\text{" ++ s ++ "}"
+        Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
+        Var x -> f x
+        IntLit i -> String.fromInt i
+        StringLit s -> "\"" ++ s ++ "\""
+
+metavariableToLatex : Metavariable -> String
+metavariableToLatex (MkMetavariable s) =
+    let
+        noQuestion = String.dropLeft 1 s
+    in
+        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
+
+ruleToLatex : Rule -> String
+ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
+
+unificationVarToLatex : UnificationVar -> String
+unificationVarToLatex (MkUnificationVar s) = s
+
+proofTreeToLatex : ProofTree -> String
+proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
--- a/src/Bergamot/Parser.elm
+++ b/src/Bergamot/Parser.elm
@ -1,6 +1,6 @@
 module Bergamot.Parser exposing (..)

-import Bergamot.Syntax exposing (Term(..), Metavariable)
+import Bergamot.Syntax exposing (Term(..), Metavariable(..))
 import Bergamot.Rules exposing (Rule, RuleEnv)

 import Parser exposing (Parser, Trailing(..), (|.), (|=))
@ -16,12 +16,14 @@ name = Parser.variable
    , reserved = Set.empty
    }

-variable : Parser String
-variable = Parser.variable
-    { start = \c -> c == '?'
-    , inner = \c -> Char.isAlphaNum c || c == '_'
-    , reserved = Set.empty
-    }
+variable : Parser Metavariable
+variable =
+    Parser.succeed MkMetavariable
+    |= Parser.variable
+        { start = \c -> c == '?'
+        , inner = \c -> Char.isAlphaNum c || c == '_'
+        , reserved = Set.empty
+        }

 term : Parser (Term Metavariable)
 term = Parser.lazy (\() -> Parser.oneOf
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@ -1,6 +1,6 @@
 module Bergamot.Rules exposing (..)

-import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState)
+import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
 import Bergamot.Search as Search exposing (Search)

 import Debug
@ -33,11 +33,26 @@ andThen f p env ps =
    p env ps
    |> Search.andThen (\(a, psp) -> (f a) env psp)

+join : Prover (Prover a) -> Prover a
+join p = andThen (\x -> x) p
+
+apply : Prover a -> Prover (a -> b) -> Prover b
+apply pa pf = pf |> andThen (\f -> map f pa)
+
 map : (a -> b) -> Prover a -> Prover b
 map f p env ps =
    p env ps
    |> Search.map (Tuple.mapFirst f)

+mapM : (a -> Prover b) -> List a -> Prover (List b)
+mapM f l =
+    case l of
+        x :: xs ->
+            pure (::)
+            |> apply (f x)
+            |> apply (mapM f xs)
+        [] -> pure []
+
 interleave : Prover a -> Prover a -> Prover a
 interleave p1 p2 env ps =
    Search.interleave (p1 env ps) (p2 env ps)
@ -51,34 +66,56 @@ fail env ps = Search.fail
 getEnv : Prover RuleEnv
 getEnv env ps = Search.pure (env, ps)

-rule : Term UnificationVar -> Rule -> Prover ProofTree
-rule t r env ps =
+getUnificationState : Prover UnificationState
+getUnificationState env ps = Search.pure (ps.unificationState, ps)
+
+liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
+liftInstantiation f a env ps =
    let
-        (conc, is) = instantiate r.conclusion ps.instantiationState
-        (prems, isp) = instantiateList r.premises is
+        (b, is) = f a ps.instantiationState
    in
-        case unify t conc ps.unificationState of
-            Nothing -> Search.fail
-            Just (tp, usp) ->
-                let
-                    psp = { ps | instantiationState = resetVars isp
-                               , unificationState = usp }
-                in
-                    provePremises prems env psp
-                    |> Search.map (Tuple.mapFirst (\trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees }))
+        Search.pure (b, { ps | instantiationState = is })
+
+liftUnification : (a -> a -> UnificationState -> Maybe (a, UnificationState)) -> a -> a -> Prover a
+liftUnification f a1 a2 env ps =
+    case f a1 a2 ps.unificationState of
+        Just (a, us) -> Search.pure (a, { ps | unificationState = us })
+        Nothing -> Search.fail
+
+withVars : Prover a -> Prover a
+withVars p env ps =
+    p env ps
+    |> Search.map (Tuple.mapSecond (\psp -> { psp | instantiationState = resetVars psp.instantiationState }))
+
+
+reifyProofTree : ProofTree -> Prover ProofTree
+reifyProofTree (MkProofTree node) =
+    pure (\t trees -> MkProofTree { node | conclusion = t, premises = trees })
+    |> apply (map (reify node.conclusion) getUnificationState)
+    |> apply (mapM reifyProofTree node.premises)
+
+rule : Term UnificationVar -> Rule -> Prover ProofTree
+rule t r =
+        withVars (pure Tuple.pair
+            |> apply (liftInstantiation instantiate r.conclusion)
+            |> apply (liftInstantiation instantiateList r.premises))
+        |> andThen (\(conc, prems) ->
+            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 l =
-    case l of
-        t :: ts ->
-            prove t
-            |> andThen (\tree -> map (\trees -> tree :: trees) (provePremises ts))
-        [] -> pure []
+provePremises = mapM proveTerm

-prove : Term UnificationVar -> Prover ProofTree
-prove t =
+proveTerm : Term UnificationVar -> Prover ProofTree
+proveTerm t =
    getEnv
-    |> andThen (List.foldl (\r -> interleave (rule t r)) fail << .rules)
+    |> andThen (\env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
+
+prove : Term Metavariable -> Prover ProofTree
+prove mt =
+    liftInstantiation instantiate mt
+    |> andThen proveTerm

 single : RuleEnv -> Prover a -> Maybe a
 single env p =
--- a/src/Bergamot/Search.elm
+++ b/src/Bergamot/Search.elm
@ -12,11 +12,11 @@ map f s () =
        Empty -> Empty
        Found a sp -> Found (f a) (map f sp)

-apply : Search (a -> b) -> Search a -> Search b
-apply sf sa () =
+apply : Search a -> Search (a -> b) -> Search b
+apply sa sf () =
    case sf () of
        Empty -> Empty
-        Found f sfp -> interleave (map f sa) (apply sfp sa) ()
+        Found f sfp -> interleave (map f sa) (apply sa sfp) ()

 andThen : (a -> Search b) -> Search a -> Search b
 andThen f sa () =
--- a/src/Bergamot/Syntax.elm
+++ b/src/Bergamot/Syntax.elm
@ -1,5 +1,5 @@
 module Bergamot.Syntax exposing
-    ( Term(..), Metavariable, UnificationVar
+    ( Term(..), Metavariable(..), UnificationVar(..)
    , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
    , unify, unifyList, UnificationState, emptyUnificationState
    , reify
@ -12,8 +12,14 @@ import Tuple
 import Debug

 type alias Name = String
-type alias Metavariable = String
-type alias UnificationVar = String
+type Metavariable = MkMetavariable String
+type UnificationVar = MkUnificationVar String
+
+unMetavariable : Metavariable -> String
+unMetavariable (MkMetavariable s) = s
+
+unUnificationVar : UnificationVar -> String
+unUnificationVar (MkUnificationVar s) = s

 type Term a
    = IntLit Int
@ -23,7 +29,7 @@ type Term a

 type alias InstantiationState =
    { counter : Int
-    , vars : Dict Metavariable UnificationVar
+    , vars : Dict String UnificationVar
    }

 emptyInstantiationState = { counter = 0, vars = Dict.empty }
@ -33,12 +39,15 @@ resetVars is = { is | vars = Dict.empty }

 metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState)
 metavariable mv is =
-    case Dict.get mv is.vars of
+    case Dict.get (unMetavariable mv) is.vars of
        Just v -> (v, is)
        Nothing ->
            let
-                v = "var" ++ (String.fromInt is.counter)
-                isp = { counter = is.counter + 1, vars = Dict.insert mv v is.vars }
+                v = MkUnificationVar ("var" ++ (String.fromInt is.counter))
+                isp =
+                    { counter = is.counter + 1
+                    , vars = Dict.insert (unMetavariable mv) v is.vars
+                    }
            in (v, isp)

 instantiateList : List (Term Metavariable) -> InstantiationState -> (List (Term UnificationVar), InstantiationState)
@ -58,51 +67,58 @@ instantiate mt is =
        Var mv -> Tuple.mapFirst Var (metavariable mv is)

 type alias UnificationInfo =
-    { equivalence : Set UnificationVar
+    { equivalence : Set String
    , term : Maybe (Term UnificationVar)
    }

-type alias UnificationState = Dict UnificationVar UnificationInfo
+type alias UnificationState = Dict String UnificationInfo

 emptyUnificationState = Dict.empty

-reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
+reconcile : Set String -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
 reconcile eq mt us =
    let newValue = { equivalence = eq, term = mt }
    in Set.foldl (\v -> Dict.insert v newValue) us eq

 merge : UnificationVar -> UnificationVar -> UnificationState -> Maybe UnificationState
 merge v1 v2 us =
-    case (Dict.get v1 us, Dict.get v2 us) of
-        (Just ui1, Just ui2) ->
-            let
-                newEq = Set.union ui1.equivalence ui2.equivalence
-            in
-                case (ui1.term, ui2.term) of
-                    (Just t1, Just t2) ->
-                        unify t1 t2 us
-                        |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
-                    (Just t1, Nothing) ->
-                        Just (reconcile newEq (Just t1) us)
-                    (Nothing, Just t2) ->
-                        Just (reconcile newEq (Just t2) us)
-                    (Nothing, Nothing) ->
-                        Just (reconcile newEq Nothing us)
-        (Just ui1, Nothing) -> Just (reconcile (Set.insert v2 ui1.equivalence) ui1.term us)
-        (Nothing, Just ui2) -> Just (reconcile (Set.insert v1 ui2.equivalence) ui2.term us)
-        (Nothing, Nothing) -> Just (reconcile (Set.fromList [v1,v2]) Nothing us)
+    let
+        v1s = unUnificationVar v1
+        v2s = unUnificationVar v2
+    in
+        case (Dict.get v1s us, Dict.get v2s us) of
+            (Just ui1, Just ui2) ->
+                let
+                    newEq = Set.union ui1.equivalence ui2.equivalence
+                in
+                    case (ui1.term, ui2.term) of
+                        (Just t1, Just t2) ->
+                            unify t1 t2 us
+                            |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
+                        (Just t1, Nothing) ->
+                            Just (reconcile newEq (Just t1) us)
+                        (Nothing, Just t2) ->
+                            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)
+            (Nothing, Just ui2) -> Just (reconcile (Set.insert v1s ui2.equivalence) ui2.term us)
+            (Nothing, Nothing) -> Just (reconcile (Set.fromList [v1s,v2s]) Nothing us)

 set : UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
 set v t us =
-    case Dict.get v 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 v { equivalence = Set.singleton v, term = Just t } us)
+    let
+        vs = unUnificationVar v
+    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)

 unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
 unifyList l1 l2 us =
@ -136,7 +152,7 @@ reify t us =
        StringLit s -> StringLit s
        Call n ts -> Call n (List.map (\tp -> reify tp us) ts)
        Var v ->
-            case Dict.get v us of
+            case Dict.get (unUnificationVar v) us of
                Just ui ->
                    case ui.term of
                        Just tp -> reify tp us
--- a/src/Main.elm
+++ b/src/Main.elm
@ -3,32 +3,70 @@ module Main exposing (main)
 import Browser
 import Html exposing (Html)
 import Html.Events exposing (onInput)
+import Html.Attributes exposing (type_, class)
 import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
+import Bergamot.Latex exposing (..)
+import Json.Encode
 import Maybe
 import Tuple
 import Debug

-type alias Model = { program : String }
+type alias Model =
+    { program : String
+    , query : String
+    }
 type alias Flags = ()
 type Msg
    = SetProgram String
+    | SetQuery String

 init : Flags -> (Model, Cmd Msg)
-init () = ({ program = "" }, Cmd.none)
+init () = ({ program = "", query = "" }, Cmd.none)
+
+viewSection : String -> Html Msg -> Html Msg
+viewSection name content =
+    Html.div [] [ Html.h2 [] [ Html.text name ], content ]
+
+viewRule : Rule -> Html Msg
+viewRule = latex << ruleToLatex
+
+viewRules : String -> Html Msg
+viewRules progs = viewSection "Rendered Rules" <|
+    Html.div [ class "rule-list" ] <|
+        case run program progs of
+            Just prog -> List.map viewRule prog.rules
+            Nothing -> []
+
+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 : String -> String -> Html Msg
+viewProofTree progs querys = viewSection "Proof Tree" <|
+    Html.div [ class "proof-tree" ] <|
+      case tryProve progs querys of
+          Just tree -> [ latex (proofTreeToLatex tree) ]
+          Nothing -> []
+

 view : Model -> Html Msg
-view m = Html.div []
-    [ Html.textarea [ onInput SetProgram ] []
-    , Html.p [] [ Html.text (Debug.toString (run program m.program)) ]
+view m = Html.div [ class "elm-root" ]
+    [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
+    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery ] []
+    , viewRules m.program
+    , viewProofTree m.program m.query
    ]

 update : Msg -> Model -> (Model, Cmd Msg)
 update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
+        SetQuery query -> ({ m | query = query }, Cmd.none)

 subscriptions : Model -> Sub Msg
 subscriptions _ = Sub.none
@ -40,3 +78,21 @@ main =
        , update = update
        , subscriptions = subscriptions
        }
+
+-- Latex support:
+-- Based on https://stackoverflow.com/questions/75492820/embedding-mathematical-equations-in-an-elm-spa
+
+latex : String -> Html Msg
+latex expr =
+  Html.node "katex-expression"
+    [ Html.Attributes.attribute "expression" expr
+    , Html.Attributes.attribute "katex-options" (Json.Encode.encode 0 options)
+    ]
+    []
+
+
+options : Json.Encode.Value
+options =
+    Json.Encode.object
+        [ ( "displayMode", Json.Encode.bool True )
+        ]
Author	SHA1	Message	Date
Danila Fedorin	4deb7bc556	Minor tweaks to style and rule rendering	2023-11-26 16:32:27 -08:00
Danila Fedorin	33c3f87564	Add some styling (still very early stages)	2023-11-26 16:25:23 -08:00
Danila Fedorin	250dbb4ee8	Add an index.html file that includes the web component Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-11-26 15:54:17 -08:00
Danila Fedorin	acc769e799	Add LaTeX support for rendering rules	2023-11-26 15:54:01 -08:00
Danila Fedorin	7cc5d05e9c	Add a way to print the rules as LaTeX	2023-11-26 14:34:52 -08:00
Danila Fedorin	e123f24af0	Add support for reifying proof trees Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-11-26 13:14:44 -08:00
Danila Fedorin	a24fbad249	Make Metavariable and UnificationVar newtypes to help type safety Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-11-26 12:58:38 -08:00
Danila Fedorin	985be53367	Add an interactive 'can this query be satisfied' interface	2023-11-26 12:47:05 -08:00
Danila Fedorin	9f7b59c65d	Instantiate the query-to-be-proven as well Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-11-26 12:32:28 -08:00
Danila Fedorin	2f1cb79013	Clean up the search and proving code somewhat	2023-11-26 12:27:44 -08:00