Merge pull request #51 from Larch-Team/saving-loading

Saving loading

.gitignore

@@ -132,6 +132,7 @@ dmypy.json
 .vscode
 app/appdata/crashes
 app/appdata/config
+app/appdata/saved_proofs
 app/core_temp
 app/larch.pyz
 app/appdata/manifest.json

app/appdata/plugins/UserInterface/CLI.py

@@ -10,7 +10,6 @@
 from math import log10
 from xml.sax.saxutils import escape
 from colors import COLORS, DEFAULT_COLOR
-
 import engine
 import prompt_toolkit as ptk
 
@@ -381,6 +380,12 @@ def do_undo(session: engine.Session, amount: int) -> str:
     except engine.EngineError as e:
         return str(e)
 
+def do_redo(session: engine.Session, amount: int) -> str:
+    """Redoes last [arg] undone actions"""
+    try:
+        session.redo(amount)
+    except engine.EngineError as e:
+        return str(e)
 
 def do_contra(session: engine.Session, branch: str) -> str:
     """Detects contradictions and handles them by closing their branches"""
@@ -449,6 +454,29 @@ def do_write(session: engine.Session, filename: str):
         return f"Proof saved as {filename}"
 
 
+def do_save(session: engine.Session, filename: str):
+    """Saves current state of proof if needed
+    
+    Arguments:
+        - filename [str]
+    """
+    try:
+        return session.save_proof(filename)
+    except engine.EngineError as e:
+        return e
+
+def do_load(session: engine.Session, filename: str):
+    """Loads a saved proof 
+    
+    Arguments:
+        - filename [str]
+    """
+    try:
+        return session.load_proof(filename)
+    except EngineError as e:
+        return e
+
+
 # Proof navigation
 
 
@@ -521,11 +549,14 @@ def do_access_colors(session: engine.Session, val: int) -> str:
     'write': {'comm': do_write, 'args': [str]},
     'use': {'comm': do_use, 'args': 'multiple_strings'},
     'undo': {'comm': do_undo, 'args': [int]},
+    # 'redo': {'comm': do_redo, 'args': [int]},
     'leave': {'comm': do_leave, 'args': []},
     'prove': {'comm': do_prove, 'args': 'multiple_strings'},
     'hint': {'comm': do_hint, 'args': []},
     'solve': {'comm': do_solve, 'args': []},
     'check': {'comm': do_check, 'args': []},
+    'save': {'comm': do_save, 'args': [str]},
+    'load': {'comm': do_load, 'args': [str]},
     # Program interaction
     'plugin switch': {'comm': do_plug_switch, 'args': [str, str]},
     'plugin get': {'comm': do_plug_get, 'args': [str, str]},

app/core/engine.py

@@ -4,6 +4,7 @@
 import json
 import logging
 import os
+import sys
 import typing as tp
 from manager import FileManager
 from misc import setup_iter
@@ -90,6 +91,8 @@ def __init__(self, session_ID: str, config_file: str):
         self.defined = {}
         self.proof = None
         self.branch = ""
+        self.undo_counter = 0
+        self.undone_rules = None
 
         self.compile_lexer()
 
@@ -393,7 +396,7 @@ def use_rule(self, rule: str, context: dict[str, tp.Any]) -> tp.Union[None, list
             raise EngineError("Wrong context")
 
         try:
-            self.proof.use_rule(rule, context, None)
+            self.proof.use_rule(rule, context, decisions=None)
         except RaisedUserMistake as e:
             if self.sockets['Assistant'].isplugged():
                 return self.acc('Assistant').mistake_userule(e) or [e.default]
@@ -410,9 +413,10 @@ def undo(self, actions_amount: int) -> tuple[str]:
         if len(self.proof.metadata['usedrules']) < actions_amount:
             raise EngineError("Nothing to undo")
 
-        rules = [self.proof.metadata['usedrules'].pop()
+        self.undo_counter += actions_amount
+        self.undone_rules = [self.proof.metadata['usedrules'].pop()
                  for _ in range(actions_amount)]
-        min_layer = min((r.layer for r in rules))
+        min_layer = min((r.layer for r in self.undone_rules))
         self.proof.nodes.pop(min_layer)
 
         # Poprawianie gałęzi
@@ -421,7 +425,70 @@ def undo(self, actions_amount: int) -> tuple[str]:
         else:
             self.proof.branch = self.proof.nodes.branch
 
-        return rules
+        return self.undone_rules
+
+    # @EngineLog -> '''nie dziala XD'''
+    # def redo(self, actions_amount: int):
+    #     if not self.proof:
+    #         raise EngineError('There is no proof started')
+    #     if self.undo_counter < actions_amount:
+    #         raise EngineError('Not enough actions to redo')
+    #     else:
+    #         for i in range(actions_amount):
+    #             self.proof.perform_usedrule(self.proof.metadata['usedrules'][-1-i])
+
+    @EngineLog
+    def save_proof(self, filename: str):
+        if not self.proof:
+            raise EngineError('There is no proof to save')
+
+        saved = False
+        used_rules = [{'layer': obj.layer, 'branch': obj.branch, 'rule': obj.rule, 'context': obj.context, 'decisions': obj.decisions, 'auto': obj.auto} for obj in self.proof.metadata['usedrules']]
+
+        state = {
+            'sentence': self.proof.sentence,
+            'used rules': used_rules,
+            'setup': self.config
+        }
+
+        if not os.path.isfile(f'./saved_proofs/{filename}'):
+            with open(f'saved_proofs/{filename}', 'w') as save_file:
+                json.dump(state, save_file)
+            return 'Proof saved successfully'
+        else:
+            raise EngineError('Plik o podanej nazwie juz istnieje')
+
+    @EngineLog
+    def load_proof(self, filename: str):
+        if self.proof != None:
+            raise EngineError('There is already a proof started. Save or finish it and leave the current proof to load a saved one.')
+        if not os.path.isfile(f'./saved_proofs/{filename}'):
+            raise EngineError('There is no such save file')
+
+        with open(f'saved_proofs/{filename}') as save_file:
+            state = json.load(save_file)
+            self.config = state['setup']
+
+            tokenized = Sentence(state['sentence'], self)
+            self.proof = BranchCentric(tokenized, self.config)
+            self.deal_closure(self.proof.nodes.getbranchnames()[0])
+            rules_to_perform = [
+                UsedRule(
+                    branch=rule['branch'],
+                    rule=rule['rule'],
+                    context=rule['context'],
+                    decisions=rule['decisions'],
+                    layer=rule['layer'],
+                    _proof=self.proof,
+                    auto=rule['auto'],
+                )
+                for rule in state['used rules']
+            ]
+
+            for rule in rules_to_perform:
+                self.proof.perform_usedrule(rule)
+            return('Proof loaded successfully')            
+
 
     # Proof assist
 

app/core/manager.py

@@ -86,8 +86,9 @@ def select_dir(self, larch_version: str):
                 __file__).removesuffix('manager.py')+'../appdata'
         else:
             self.directory = user_data_dir(appname='Larch', appauthor=False, version=larch_version)
-            self.prepare_dirs('plugins')
-            self.prepare_dirs('setups')
+        self.prepare_dirs('plugins')
+        self.prepare_dirs('setups')
+        self.prepare_dirs('saved_proofs')
 
         # if not os.path.isfile(f'{self.directory}/manifest.json'):
         #     with open(f'{self.directory}/manifest.json', 'w') as f:

app/core/proof.py

@@ -64,20 +64,20 @@ def deal_closure_func(self, func: Callable[[list[Sentence], History], Union[None
         else:
             return None, None
 
-    def use_rule(self, branch_name: str, rule: str, context: dict[str, Any], decisions: dict = None) -> None:
+    def use_rule(self, rule: str, context: dict[str, Any], branch_name: str, decisions: dict = None) -> None:
         """
         Wykorzystuje regułę dowodzenia systemu FormalSystem na określonej gałęzi z określonym kontekstem.
 
         :param FormalSystem: Socket FormalSystem, używany do przywołania use_rule
         :type FormalSystem: Socket
-        :param branch: nazwa gałęzi do zastosowania reguły
-        :type branch: str
         :param rule: Nazwa reguły
         :type rule: str
         :param context: Kontekst zastosowania reguły
         :type context: dict[str, Any]
         :param decisions: Zbiór podjętych decyzji, defaults to None
         :type decisions: dict, optional
+        :param branch: nazwa gałęzi do zastosowania reguły
+        :type branch: str
         :raises EngineError: [description]
         :return: Lista nowych gałęzi
         :rtype: tuple[str]
@@ -109,9 +109,9 @@ def use_rule(self, branch_name: str, rule: str, context: dict[str, Any], decisio
     def perform_usedrule(self, usedrule: UsedRule):
         """Wykonuje na dowodzie regułę na podstawie obiektu UsedRules"""
         self.use_rule(
-            branch_name=usedrule.branch,
             rule=usedrule.rule,
             context=usedrule.context,
+            branch_name=usedrule.branch,
             decisions=usedrule.decisions
         )
 
@@ -214,5 +214,7 @@ def next(self):
         else:
             raise EngineError("All branches are closed")
 
-    def use_rule(self, rule: str, context: dict[str, Any], decisions: dict):
-        return super().use_rule(self.branch, rule, context, decisions=decisions)
+    def use_rule(self, rule: str, context: dict[str, Any], branch_name: str = None, decisions: dict = None):
+        if branch_name:
+            self.jump(branch_name)
+        return super().use_rule(rule, context, self.branch, decisions=decisions)

tests/sessiontest.py

@@ -1,4 +1,5 @@
 import sys
+import os
 
 from multiprocessing import Pool
 sys.path.extend([os.path.abspath(i) for i in ['../app/appdata', '../app/core']])

tests/solvertest.py

@@ -1,7 +1,7 @@
 import os
 import sys
 import time
-
+# dodac check
 sys.path.extend([os.path.abspath(i) for i in ['../app/appdata', '../app/core']])
 from plugins.UserInterface import CLI as c