Merge pull request #48 from Larch-Team/assistance

Assistance

app/article.py

@@ -0,0 +1,91 @@
+from html.parser import HTMLParser
+import os
+from typing import NewType, Optional
+
+class _Parser(HTMLParser):
+    def __init__(self, *, convert_charrefs: bool = True) -> None:
+        super().__init__(convert_charrefs=convert_charrefs)
+        self.id_stack = []
+        self.index_stack = []
+        self.ranges = {}
+
+    def handle_starttag(self, tag: str, attrs: list[tuple[str, Optional[str]]]) -> None:
+        if not attrs:
+            self.id_stack.append(None)
+            self.index_stack.append(self.getpos())
+            return
+        keys, vals = zip(*attrs)
+        try:
+            index = keys.index('id')
+        except ValueError:
+            self.id_stack.append(None)
+        else:
+            self.id_stack.append(vals[index])
+        self.index_stack.append(self.getpos())
+
+    def handle_endtag(self, tag: str) -> None:
+        id_val = self.id_stack.pop()
+        index = self.index_stack.pop()
+        l, i = self.getpos()
+        if id_val:
+            self.ranges[id_val] = index, (l, i+len(tag)+3) # i (długość linii przed końcem) + len(tag) (długość tagu) + 3 ("</>")
+
+    def handle_startendtag(self, tag: str, attrs: list[tuple[str, Optional[str]]]) -> None:
+        if not attrs:
+            return
+        keys, vals = zip(*attrs)
+        try:
+            index = keys.index('id')
+        except ValueError:
+            return
+        l, i = self.getpos()
+        self.ranges[vals[index]] = (l, i), (l, i+len(self.get_starttag_text()))
+
+_Article = NewType('_Article', object)
+
+class Article(object):
+
+    @staticmethod
+    def read(directory: str, *files: str) -> dict[str, _Article]:
+        d = {}
+        files = list(files)
+        while files:
+            f_name = files.pop(0)
+            file = f'{directory}/{f_name}'
+            if os.path.isdir(file):
+                files.extend([f'{f_name}/{i}' for i in os.listdir()])
+            elif os.path.isfile(file) and f_name.endswith('.html'):
+                d[f_name[:-5]] = Article(file)
+            else:
+                FileNotFoundError("There is no file with this name in the given directory")
+        return d
+
+    def __init__(self, file: str) -> None:
+        super().__init__()
+        self.file = file
+        self.parts = self.read_parts()
+
+    def read_parts(self) -> dict[str, tuple[tuple[int, int], tuple[int, int]]]:
+        parser = _Parser()
+        with open(self.file, encoding='utf8') as f:
+            parser.feed(f.read())
+        return parser.ranges
+
+    def __getitem__(self, part: str) -> Optional[str]:
+        if not isinstance(part, str):
+            return None
+        start, end = self.parts[part]
+        start_line, start_pos = start
+        end_line, end_pos = end
+
+        with open(self.file, encoding='utf8') as f:
+            lines = f.readlines()[start_line-1:end_line]
+        lines[0] = lines[0][start_pos:]
+        lines[-1] = lines[-1][:end_pos]
+
+        return "".join(lines).strip('\n ')
+
+    def text(self) -> str:
+        with open(self.file) as f:
+            t = f.read()
+        return t

app/config/config.json

@@ -1 +1 @@
-{"chosen_plugins": {"UserInterface": "CLI", "Lexicon": "classic", "Formal": "analytic_freedom", "Output": "actual_tree"}}
+{"chosen_plugins": {"Assistant": "pan", "UserInterface": "CLI", "Lexicon": "classic", "Formal": "analytic_freedom", "Output": "actual_tree"}}

app/engine.py

@@ -6,8 +6,8 @@
 import typing as tp
 
 import pop_engine as pop
-from exceptions import EngineError
-from proof import BranchCentric
+from exceptions import EngineError, RaisedUserMistake
+from proof import BranchCentric, Proof
 from rule import ContextDef
 from sentence import Sentence
 from tree import ProofNode
@@ -38,16 +38,6 @@ def new(*args, **kwargs):
         return func(*args, **kwargs)
     return new
 
-
-def DealWithPOP(func):
-    """Converts all PluginErrors to EngineErrors for simpler handling in the UI socket"""
-    def new(*args, **kwargs):
-        try:
-            return func(*args, **kwargs)
-        except pop.PluginError as e:
-            raise EngineError(str(e))
-    return new
-
 # Input type handling
 
 TYPE_LEXICON = {
@@ -95,7 +85,7 @@ def __init__(self, session_ID: str, config_file: str):
         self.proof = None
         self.branch = ""
 
-        self.compileLexer()
+        self.compile_lexer()
 
 
     def __repr__(self):
@@ -148,7 +138,7 @@ def plug_switch(self, socket_or_old: str, new: str) -> None:
 
         # Deal with lexer
         if socket_name == 'Lexicon':
-            self.compileLexer()
+            self.compile_lexer()
 
     def plug_list(self, socket: str) -> list[str]:
         """Zwraca listę wszystkich pluginów dla danej nazwy.
@@ -183,7 +173,11 @@ def plug_gen(self, socket: str, name: str) -> None:
 
     # Lexer
 
-    def compileLexer(self) -> None:
+    def compile_lexer(self) -> None:
+        """
+        Kompiluje lexer na bazie pluginu Lexiconu
+        Raczej zbędne poza zastosowaniami technicznymi
+        """
         self.lexer = lexer.BuiltLexer(self.acc('Lexicon').get_lexicon(),
             use_language = self.acc('Formal').get_tags()
         ) 
@@ -208,8 +202,7 @@ def write_config(self):
 
 
     @EngineLog
-    @DealWithPOP
-    def new_proof(self, statement: str) -> None:
+    def new_proof(self, statement: str) -> tp.Union[None, list[str]]:
         """Parsuje zdanie, testuje poprawność i tworzy z nim dowód
 
         :param statement: Zdanie
@@ -221,16 +214,17 @@ def new_proof(self, statement: str) -> None:
         try:
             tokenized = self.lexer.tokenize(statement)
         except lexer.LrchLexerError as e:
-            raise EngineError(str(e))
+            raise [EngineError(str(e))]
         tokenized = Sentence(tokenized, self)
         problem = self.acc('Formal').check_syntax(tokenized)
         if problem:
-            logger.warning(f"{statement} is not a valid statement \n{problem}")
-            raise EngineError(problem)
+            logger.warning(f"{statement} is not a valid statement \n{problem.name}")
+            return self.acc('Assistant').mistake_syntax(problem)
         else:
             tokenized = self.acc('Formal').prepare_for_proving(tokenized)
 
             self.proof = BranchCentric(tokenized, self.config)
+            self.deal_closure('Green')
 
 
     @EngineLog
@@ -239,7 +233,6 @@ def reset_proof(self) -> None:
 
 
     @EngineLog
-    @DealWithPOP
     def deal_closure(self, branch_name: str) -> tp.Union[None, str]:
         """Wywołuje proces sprawdzenia zamykalności gałęzi oraz (jeśli można) zamyka ją; Zwraca informacje o podjętych akcjach"""
         # Tests
@@ -269,8 +262,7 @@ def context_info(self, rule: str):
 
 
     @EngineLog
-    @DealWithPOP
-    def use_rule(self, rule: str, context: dict[str, tp.Any]) -> tp.Union[None, tuple[str]]:
+    def use_rule(self, rule: str, context: dict[str, tp.Any]) -> tp.Union[None, list[str]]:
         """Uses a rule of the given name on the current branch of the proof.
         Context allows to give the Formal additional arguments 
         Use `self.acc('Formal').get_needed_context(rule)` to check for needed context
@@ -279,8 +271,8 @@ def use_rule(self, rule: str, context: dict[str, tp.Any]) -> tp.Union[None, tupl
         :type rule: str
         :param context: Arguments for rule usage
         :type context: dict[str, tp.Any]
-        :return: Names of new branches
-        :rtype: tp.Union[None, tuple[str]]
+        :return: Readable information about the proof state, None if everything's good
+        :rtype: tp.Union[None, list[str]]
         """
         # Tests
         if not self.proof:
@@ -294,11 +286,19 @@ def use_rule(self, rule: str, context: dict[str, tp.Any]) -> tp.Union[None, tupl
         if {i.variable for i in context_info} != set(context.keys()):
             raise EngineError("Wrong context")
 
-        return self.proof.use_rule(self.acc('Formal'), rule, context, None)
+        try:
+            self.proof.use_rule(rule, context, None)
+        except RaisedUserMistake as e:
+            if self.sockets['Assistant'].isplugged():
+                return self.acc('Assistant').mistake_userule(e) or [e.default]
+            else:
+                return [e.default]
+        return None
 
 
     @EngineLog
     def undo(self, actions_amount: int) -> tuple[str]:
+        """Wycofuje `actions_amount` operacji zwracając informacje o nich"""
         if not self.proof:
             raise EngineError(
                 "There is no proof started")
@@ -318,28 +318,59 @@ def undo(self, actions_amount: int) -> tuple[str]:
         return rules
 
 
-    def check(self) -> tuple[str]:
+    # Proof assist
+
+    def start_help(self) -> list[str]:
+        """Zwraca listę podpowiedzi do wyświetlenia użytkownikowi"""
+        return self.acc('Assistant').hint_start() or []
+
+
+    @EngineLog
+    def hint(self) -> list[str]:
+        """Zwraca listę podpowiedzi w formacie HTML"""
         if not self.proof:
             raise EngineError(
                 "There is no proof started")
-        return self.proof.check(self.acc('Formal').checker)
 
+        return self.acc('Assistant').hint_command(self.proof)
 
-    def solve(self) -> tuple[str]:
-        if not self.proof:
+
+    @EngineLog
+    def check(self, proof: Proof = None) -> list[str]:
+        """Sprawdza dowód i zwraca listę błędów w formacie HTML"""
+        proof = proof or self.proof 
+        if not proof:
+            raise EngineError("There is no proof started")
+        if not proof.nodes.is_closed():
+            raise EngineError("Nie możesz sprawdzić nieskończonego dowodu")
+
+        mistakes = proof.check()
+        l = []
+        for i in mistakes:
+            if v := self.acc('Assistant').mistake_check(i) is not None:
+                l.extend(v)
+            else:
+                l.append(i.default)
+        return l
+
+
+    @EngineLog
+    def solve(self, proof: Proof = None) -> tuple[str]:
+        """Dokańcza podany, lub aktualny dowód, zwraca informację o sukcesie procedury"""
+        proof = proof or self.proof
+        if not proof:
             raise EngineError(
                 "There is no proof started")
 
-        if self.acc('Formal').solver(self.proof):
-            return ("Udało się zakończyć dowód", f"Formuła {'nie '*(not self.proof.nodes.is_successful())}jest tautologią")
+        if self.acc('Formal').solver(proof):
+            return ("Udało się zakończyć dowód", f"Formuła {'nie '*(not proof.nodes.is_successful())}jest tautologią")
         else:
             return ("Nie udało się zakończyć dowodu",)
 
+
     # Proof navigation
 
-
-    @DealWithPOP
-    def getbranch_strings(self) -> list[list[str], str]:
+    def getbranch_strings(self) -> tuple[list[str], tp.Optional[str]]:
         """Zwraca gałąź oraz stan zamknięcia w formie czytelnej dla użytkownika"""
         try:
             branch, closed = self.proof.get_node().getbranch_sentences()
@@ -364,13 +395,11 @@ def getbranches(self):
         return self.proof.nodes.getbranchnames()
 
 
-    @DealWithPOP
     def getrules(self) -> dict[str, str]:
         """Zwraca nazwy reguł wraz z dokumentacją"""
         return self.acc('Formal').get_rules_docs()
 
 
-    @DealWithPOP
     def gettree(self) -> list[str]:
         """Zwraca całość drzewa jako listę ciągów znaków"""
         if not self.proof:
@@ -380,14 +409,14 @@ def gettree(self) -> list[str]:
         printed = self.proof.nodes.gettree()
         return self.acc('Output').write_tree(printed)
 
-
+    @EngineLog
     def next(self) -> None:
         """Przeskakuje do następnej otwartej gałęzi"""
         if not self.proof:
             raise EngineError("There is no proof started")
         return self.proof.next()
 
-
+    @EngineLog
     def jump(self, new: str) -> None:
         """Skacze do gałęzi o nazwie new, albo na prawego/lewego sąsiadu, jeżeli podamy "left/right"
 

app/exceptions.py

@@ -1,5 +1,6 @@
+from dataclasses import dataclass
 import logging
-from typing import Any, Callable
+from typing import Any, Callable, Union
 
 
 logger = logging.getLogger('engine')
@@ -11,6 +12,11 @@ def __init__(self, msg: str, *args, **kwargs):
         logger.error(msg)
         super().__init__(msg, *args, **kwargs)
 
+class LrchLexerError(Exception):
+    pass
+
+class SentenceError(Exception):
+    pass
 
 # pop_engine
 
@@ -52,4 +58,23 @@ class VersionError(PluginError):
 # Formal
 
 class FormalError(Exception):
+    pass
+
+
+@dataclass(init=True, repr=True, frozen=True)
+class UserMistake:
+    name: str
+    default: str
+    additional: Union[dict[str, Any], None] = None
+
+    def __eq__(self, o: object) -> bool:
+        if isinstance(o, UserMistake):
+            return self.name == o.name and self.additional == o.additional
+        else:
+            return False
+
+    def __str__(self) -> str:
+        return self.default
+
+class RaisedUserMistake(UserMistake, Exception):
     pass