Use 'gas' instead of yields to limit recursion

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

index.html

@@ -44,6 +44,8 @@ input[type="text"] {
 
 .elm-root h2 {
     margin-bottom: 0.5em;
+    font-family: sans-serif;
+    font-weight: normal;
 }
   </style>
 </head>
@@ -53,7 +55,8 @@ input[type="text"] {
     <script src="index.js"></script>
     <script>
         var app = Elm.Main.init({
-          node: document.getElementById('elm')
+          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)" }
         });
     </script>
 </body>

src/Bergamot/Latex.elm

@@ -6,12 +6,20 @@ 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 "var" [t1]   -> termToLatex f t1
         Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
         Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
+        Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
+        Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
+        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
+        Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
+        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
+        Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
+        Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
+        Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3 
+        Call "empty" [] -> "\\varnothing"
         Call s [] -> "\\text{" ++ s ++ "}"
         Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
         Var x -> f x
@@ -23,7 +31,8 @@ metavariableToLatex (MkMetavariable s) =
     let
         noQuestion = String.dropLeft 1 s
     in
-        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
+        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
+        if String.startsWith "Gamma" 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 ++ "}"

src/Bergamot/Parser.elm

@@ -27,8 +27,7 @@ variable =
 
 term : Parser (Term Metavariable)
 term = Parser.lazy (\() -> Parser.oneOf
-    [ Parser.succeed IntLit |= intLit
-    , Parser.backtrackable <|
+    [ Parser.backtrackable <|
       Parser.succeed Call
         |= name
         |= Parser.sequence
@@ -39,9 +38,12 @@ term = Parser.lazy (\() -> Parser.oneOf
             , item = term
             , trailing = Forbidden
             }
-    , Parser.succeed (\n -> Call n [])
+    , Parser.backtrackable <|
+      Parser.succeed (\n -> Call n [])
         |= name
-    , Parser.succeed Var |= variable
+    , Parser.backtrackable <|
+      Parser.succeed Var |= variable
+    , Parser.succeed IntLit |= intLit
     ])
 
 rule : Parser Rule

src/Bergamot/Rules.elm

@@ -24,6 +24,7 @@ type alias RuleEnv =
 type alias ProveState =
     { unificationState : UnificationState
     , instantiationState : InstantiationState
+    , gas: Int
     }
 
 type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
@@ -31,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
@@ -72,6 +73,9 @@ getEnv env ps = Search.pure (env, ps)
 getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)
 
+burn : Prover ()
+burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
+
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
     let
@@ -112,7 +116,8 @@ provePremises = mapM proveTerm
 
 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
-    getEnv
+    burn
+    |> andThen (\() -> getEnv)
     |> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
 
 prove : Term Metavariable -> Prover ProofTree
@@ -122,6 +127,6 @@ prove mt =
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =
-    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState }
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
     |> Search.one
     |> Maybe.map (Tuple.first << Tuple.first)

src/Bergamot/Search.elm

@@ -46,14 +46,7 @@ interleave s1 s2 () =
 
 one : Search a -> Maybe (a, Search a)
 one s =
-    let
-        go n sp =
-            if n > 0
-            then
-                case sp () of
-                    Empty -> Nothing
-                    Found a spp -> Just (a, spp)
-                    Yield spp -> go (n - 1) spp
-            else Nothing
-    in
-        go 10000 s
+    case s () of
+        Empty -> Nothing
+        Found a sp -> Just (a, sp)
+        Yield sp -> one sp

src/Main.elm

@@ -18,13 +18,13 @@ type alias Model =
     { program : String
     , query : String
     }
-type alias Flags = ()
+type alias Flags = { rules: String, query: String }
 type Msg
     = SetProgram String
     | SetQuery String
 
 init : Flags -> (Model, Cmd Msg)
-init () = ({ program = "", query = "type(?e, tint)" }, Cmd.none)
+init fs = ({ program = fs.rules, query = fs.query }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -56,7 +56,7 @@ viewProofTree progs querys = viewSection "Proof Tree" <|
 
 view : Model -> Html Msg
 view m = Html.div [ class "elm-root" ]
-    [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
+    [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]
     , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
     , viewRules m.program
     , viewProofTree m.program m.query