visual-lambda: predecessors

Author: bntre

config.cfg

@@ -8,15 +8,18 @@ eatingsec=2.0
 bold_lambda=1
 
 # Main window size
-windowsize=800x600
-#windowsize=1280x960
+#windowsize=800x600
+windowsize=1280x960
 
 # Menu font size
-fontsize=11
+#fontsize=11
 #fontsize=15
+fontsize=13
 
 # Library file
 library=library.txt
 
 # Default Workspace
-workspace=library_demo.xml
+#workspace=library_demo.xml
+#workspace=clear.xml
+workspace=predecessors.xml

lambdaparser.py

@@ -29,8 +29,8 @@ class Parser:
 
     def __init__( self ):
 
-        self.lib = Library()        # Create Library
-        self.lib.init( self )       # parser.lib reference must exist before initialization of Library
+        self.lib = Library( self )  # Create Library
+        self.lib.init()             # parser.lib reference must exist before initialization of Library
 
 
     def parse( self, str ):
@@ -81,11 +81,10 @@ def getExpression( self, struct, vars, func=None ):
                     expr = Variable( vars[ varname ] )
 
                 else:
-                    try:
-                        expr = self.lib[ varname ]          # Try to search in Library
-                    except:
+                    expr = self.lib.find_item( varname )
+                    if not expr:
                         expr = Variable()
-                        print("Warning: Free Variable '%s': %s" % (varname, expr))
+                        print("Warning: Free Variable '%s'" % varname)
 
 
             elif LET == vartype:            # Variable of Let-Expression
@@ -166,10 +165,10 @@ def poplevel( type ):
             elif 'let' == t:
                 level = addlevel( LET, level )
 
-                var = tokens.next()
+                var = next(tokens)
                 level.append( ( var, LET ) )
 
-                be = tokens.next()
+                be = next(tokens)
                 if not( '=' == be or 'be' == be ):
                     debug('parse', "Error: 'let %s' without '=' (got %s)" % (var, be) )
 

library.py

@@ -1,4 +1,6 @@
-
+r"""
+The Parser owns (and initializes) the Library object.
+"""
 
 from    debug       import  *
 
@@ -9,86 +11,81 @@
 import  config
 
 
+def strip( expr ):
+    return expr.strip(' \t\n\r')
 
-class Library:
-
-    def __init__( self ):
-        
-        self.dict = {}
-        
-        self.numbers = True     # Simulate numbers in library
-        
-        
-    
-    def __setitem__( self, key, value ):
-        self.dict[ key ] = isinstance( value, let.Expression )  \
-                               and value  \
-                               or  self.parser.parse( value )
 
-    def __getitem__( self, key ):
+class Library:
 
-        if key in self.dict:
-            #return copy.deepcopy( self.dict[ key ] )
-            debug( 4, 'library. asked', key, self.dict[ key ] )
-            return self.dict[ key ].copy( ({},{}) )
+    def __init__( self, parser ):
+        self.parser = parser
 
-        elif self.numbers and key.isdigit():
-            return self.number( int( key ) )
+        self.globalItems = {}  # loaded from (e.g.) "library.txt" always available
+        self.localItems  = {}  # loaded from workspace; reset on workspace reload
 
+        self.generateNumbers = True     # Generate numbers by demand
+    
+    
+    def add_item( self, key, value, isGlobal = True ):
+        if not isinstance( value, let.Expression ):
+            value = self.parser.parse( value )
+        if isGlobal:
+            self.globalItems[ key ] = value
         else:
-            raise KeyError(key)
+            self.localItems[ key ] = value
 
-        
-    def __iter__( self ):
-        return self.dict.__iter__()
 
+    def reset_local_items( self ):
+        self.localItems  = {}
 
+
+    def add_line( self, line, isGlobal = True ):
+        line = strip(line)
+        if not line or line[0] == '#': return False
+        if '=' not in line: return False
+        key, value = tuple(map( strip, line.split('=', 1) ))
+        self.add_item( key, value, isGlobal )
 
-    def init( self, parser ):
-    
-        self.parser = parser
-        
-        def getDefs( lines, spaces ):
-
-            def strip( s ):
-                return s.strip( spaces )
-            
-            while lines:
-                line = strip( lines.pop(0) )
-                
-                while  lines  and  lines[0]  and  lines[0][0] in spaces:
-                    next = strip( lines.pop(0) )
-                    if next: line += ' ' + next
-                
-                if line and not '#'==line[0]:
-                    yield list(map( strip, line.split('=',1) ))
-            
 
-
+    def init( self ):
         # Read library from txt
-        txt = config.get( 'library', 'library.txt' )
+        libraryFile = config.get( 'library', 'library.txt' )
         try:
-            f = open( txt )
+            f = open( libraryFile, 'r' )
         except IOError:
-            print("Warning: no library found", txt)
+            print("Warning: can't open library file", libraryFile)
+            return
         else:
             lines = f.readlines()
             f.close()
 
-            for d in getDefs( lines, ' \t\n\r' ):
-                self[ d[0] ] = d[1]       # Add synonym to Library
+            for line in lines:
+                self.add_line( line, isGlobal = True )
 
-            
 
-    def number( self, n ):
+    def find_item( self, key ):
+        value = self.localItems.get( key ) or  \
+                self.globalItems.get( key )
+        if value:
+            debug( 4, 'library. asked', key, value )
+            return value.copy( ({},{}) )
+
+        elif self.generateNumbers and key.isdigit():
+            return self.generate_number( int( key ) )
+
+        else:
+            return None
+    
+    
+    def generate_number( self, n ):
         "Generates Number Expression"
 
         lf = let.Abstraction( expr= None )
         lx = let.Abstraction( expr= None )
 
         x = let.Variable( lx )
 
-        for _ in range( n ):            
+        for _ in range( n ):
             f = let.Variable( lf )
             x = let.Application( func= f, arg= x )
 

main.py

@@ -23,7 +23,6 @@
 from    window      import  Window
 
 import  let
-import  lambdaparser
 import  refnames
 
 from    figure      import  Ring,Bubble,Group,Figure
@@ -140,8 +139,13 @@ def __init__( self, caption ):
         windowSize = tuple(map(int, config.get( 'windowsize', '600x450' ).split("x")))
 
         Window.__init__( self, caption, windowSize )
+        
+        if not config.IS_WEB_PLATFORM:
+            favicon = pygame.image.load('favicon.png')
+            pygame.display.set_icon(favicon)
+        
 
-        self.items = []
+        self.items = []  # FieldItem-s
 
 
         # Load default workspace
@@ -155,7 +159,6 @@ def __init__( self, caption ):
         self.expandMatrix = TransformMatrix()
         self.expandMatrix.setExpand( Figure.expandCoef )
 
-        self.viewMatrix = None
         self.viewMatrix = self.defaultView( self.size, 35 )
         self.viewMovePos = None            # Start position of dragging the View
         self.viewMatrixSaved = None  #!!! temporal ?
@@ -811,7 +814,15 @@ def handleEvent( self, event ):
                 for procMod,proc in procs:
                     if procMod == eventMods or procMod & eventMods:
                         proc()
+        
+        
+        elif VIDEORESIZE == event.type:
+            # mainly handled in Window class; here we additionally centrize the view
+            if self.size != event.size:
+                shift = (Vector2(event.size) - Vector2(self.size)) / 2
+                self.moveView( shift.x, shift.y )
 
+        
         # User events
 
         if ENDURINGEVENT == event.type:
@@ -1007,16 +1018,20 @@ def onClearWorkspace( self, _ ):
                 self.invalidate()
 
         def onSaveWorkspaceName( self, workspaceName ):
+            if not workspaceName: return
             xmlData = saving.save( self, pretty = True )
             if xmlData:
                 key = "workspace_%s" % workspaceName
                 localstorage.save_value(key, xmlData)
 
         def onLoadWorkspaceName( self, workspaceName ):
+            if not workspaceName: return
             key = "workspace_%s" % workspaceName
             xmlData = localstorage.load_value(key)
             if xmlData and saving.load( self, xmlData ):
                 self.invalidate()
+            elif saving.load_from_file( self, workspaceName + ".xml" ):  # allow loading included workspaces
+                self.invalidate()
 
 
     if config.ALLOW_FILE_WRITING:

saving.py

@@ -4,6 +4,7 @@
 
 from    debug       import  *
 
+from    lambdaparser import parser
 from    figure      import  Figure
 from    fielditem   import  TextItem
 
@@ -56,25 +57,35 @@ def load( manipulator, xmlData ):
         print("Error. Can't parse workspace xml")
         return False
 
+    # Reset library local defines
+    parser.lib.reset_local_items()
+    
+    # Load items
     manipulator.items = []
     lastOrigin = Vector((0, 0))
     for item in dom.getElementsByTagName('item'):
 
+        # Define
+        if item.hasAttribute('define'):
+            parser.lib.add_line( item.getAttribute('define'), isGlobal = False )
+            continue
+        
+        # Figure or Text item
         i = None
         if item.hasAttribute('figure'):
             i = Figure( item.getAttribute('figure') )
         elif item.hasAttribute('text'):
             i = TextItem( item.getAttribute('text') )
-
-        pos = item.getAttribute('pos').split(',')
-        pos = tuple(map( float, pos ))
-        pos = lastOrigin + Vector(pos)
-        i.position.setTranspose( pos[0],pos[1], 1 )
-        i.refreshTransform()
-        manipulator.items.append( i )
-        
-        if item.hasAttribute('origin'):
-            lastOrigin = pos
+        if i:
+            pos = item.getAttribute('pos').split(',')
+            pos = tuple(map( float, pos ))
+            pos = lastOrigin + Vector(pos)
+            i.position.setTranspose( pos[0],pos[1], 1 )
+            i.refreshTransform()
+            manipulator.items.append( i )
+            
+            if item.hasAttribute('origin'):
+                lastOrigin = pos
 
     dom.unlink()
 

window.py

@@ -14,9 +14,12 @@ class Window:
     def __init__( self, caption, size ):
 
         pygame.init()
-        self.size = size     # tuple, size of window in pixels
-        pygame.display.set_mode( self.size, pygame.RESIZABLE )  
-        self.window = pygame.display.get_surface()  # main surface
+        
+        self.size   = None      # tuple, size of window in pixels
+        self.window = None      # main surface
+        self.surface = None     # Draw to other Surface, not self.window   !!! used?
+        
+        self.createWindow( size )
 
         self.caption = caption
         pygame.display.set_caption( caption )
@@ -27,8 +30,6 @@ def __init__( self, caption, size ):
         self.font = pygame.font.SysFont( 'lucidaconsole', fontsize )
         self.fontAntialias = config.IS_WEB_PLATFORM  #!!! fixing pygbag
 
-        self.surface = None     # Draw to other Surface, not self.window
-        
         # Invalidation
         self.paintEvent = pygame.event.Event( events.ONPAINTEVENT )
         self.paintEventSent = False
@@ -39,6 +40,11 @@ def __del__( self ):
         pygame.quit()
 
 
+    def createWindow( self, size ):
+        self.size = size
+        pygame.display.set_mode( self.size, pygame.RESIZABLE )
+        self.window = pygame.display.get_surface()
+
 
     def getSurface( self ):
         return  self.surface or self.window
@@ -109,8 +115,7 @@ def handleEvent( self, event ):
         "Process standart events"
         if pygame.VIDEORESIZE == event.type:
             if self.size != event.size:
-                self.size = event.size
-                self.window = pygame.display.set_mode( self.size, pygame.RESIZABLE )
+                self.createWindow( event.size )
                 self.invalidate()
 
         elif events.ONPAINTEVENT == event.type: