From fd301806c6a43fb09a3773e13af7baf85a26b239 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 21 Dec 2023 13:31:53 -0800
Subject: [PATCH] Add sections to the language syntax

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Parser.elm | 49 +++++++++++++++++++++++++++++++++++------
 src/Bergamot/Rules.elm  | 14 +++++++++---
 src/Main.elm            |  2 +-
 3 files changed, 54 insertions(+), 11 deletions(-)

diff --git a/src/Bergamot/Parser.elm b/src/Bergamot/Parser.elm
index 9b7982f..5bdbead 100644
--- a/src/Bergamot/Parser.elm
+++ b/src/Bergamot/Parser.elm
@@ -1,11 +1,14 @@
 module Bergamot.Parser exposing (..)
 
 import Bergamot.Syntax exposing (Term(..), Metavariable(..))
-import Bergamot.Rules exposing (Rule, RuleEnv)
+import Bergamot.Rules exposing (Rule, Section, RuleEnv)
 import Bergamot.Utils exposing (decodeStr)
 
 import Parser exposing (Parser, Trailing(..), (|.), (|=))
-import Set
+import Set exposing (Set)
+
+reserved : Set String
+reserved = Set.fromList ["section"]
 
 intLit : Parser Int
 intLit = Parser.int
@@ -35,7 +38,7 @@ name : Parser String
 name = Parser.variable
     { start = \c -> Char.isAlpha c || c == '_'
     , inner = \c -> Char.isAlphaNum c || c == '_'
-    , reserved = Set.empty
+    , reserved = reserved
     }
 
 variable : Parser Metavariable
@@ -44,7 +47,7 @@ variable =
     |= Parser.variable
         { start = \c -> c == '?'
         , inner = \c -> Char.isAlphaNum c || c == '_'
-        , reserved = Set.empty
+        , reserved = reserved
         }
 
 term : Parser (Term Metavariable)
@@ -97,16 +100,48 @@ rule =
             , item = term
             , trailing = Forbidden
             }
+        |. Parser.spaces |. Parser.symbol ";"
+
+rules : Parser (List Rule)
+rules = Parser.sequence
+    { start = ""
+    , separator = ""
+    , end = ""
+    , spaces = Parser.spaces
+    , item = rule
+    , trailing = Optional
+    }
+
+sectionExp : Parser Section
+sectionExp =
+    Parser.succeed (\n rs -> { name = n, rules = rs })
+    |. Parser.symbol "section" |. Parser.spaces
+    |= strLit |. Parser.spaces
+    |. Parser.symbol "{" |. Parser.spaces
+    |= rules
+    |. Parser.symbol "}" |. Parser.spaces
+
+sectionImp : Parser Section
+sectionImp =
+    (\rs ->
+        Parser.oneOf
+            [ rule |> Parser.map (\r -> Parser.Loop <| r :: rs)
+            , case rs of
+                [] -> Parser.problem "empty implicit sections not allowed."
+                _ -> Parser.succeed (Parser.Done <| List.reverse rs)
+            ])
+    |> Parser.loop []
+    |> Parser.map (\rs -> { name = "", rules = rs })
 
 program : Parser RuleEnv
 program =
-    Parser.succeed (\rs -> { rules = rs })
+    Parser.succeed (\ss -> { sections = ss })
     |= Parser.sequence
         { start = ""
-        , separator = ";"
+        , separator = ""
         , end = ""
         , spaces = Parser.spaces
-        , item = rule
+        , item = Parser.oneOf [sectionExp, sectionImp]
         , trailing = Mandatory
         }
     |. Parser.end
diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index b31f13b..ab00fe9 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -12,6 +12,11 @@ type alias Rule =
     , premises : List (Term Metavariable)
     }
 
+type alias Section =
+    { name : String
+    , rules : List Rule
+    }
+
 type ProofTree = MkProofTree
     { name : String
     , conclusion : Term UnificationVar
@@ -19,7 +24,7 @@ type ProofTree = MkProofTree
     }
 
 type alias RuleEnv =
-    { rules : List Rule
+    { sections : List Section
     }
 
 type alias ProveState =
@@ -71,6 +76,9 @@ yield p env ps = Search.yield (p env ps)
 getEnv : Prover RuleEnv
 getEnv env ps = Search.pure (env, ps)
 
+getRules : Prover (List Rule)
+getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps)
+
 getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)
 
@@ -164,8 +172,8 @@ 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))
+        |> andThen (\() -> getRules)
+        |> andThen (List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp)))
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
diff --git a/src/Main.elm b/src/Main.elm
index 0a91968..0b83c1a 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -87,7 +87,7 @@ viewRules : String -> String -> Html Msg
 viewRules renderProgs 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
+            (Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) (List.concatMap .rules prog.sections)
             _ -> []
 
 proofGoal : EditMode -> String -> Maybe (Term Metavariable)