Lambda_Calcul/lambda_calcul.py

#!/usr/bin/python3
# -*- coding: utf-8 -*-

__author__ = 'Éric W'
__date_creation__ = 'Fri Jan 22 17:18:09 2021'
__doc__ = """
:mod:`lambda_calcul` module
:author: {:s} 
:creation date: {:s}
:last revision:

Module pour travailler avec le λ-calcul

""".format(__author__, __date_creation__)

from sly import Lexer, Parser


##################################################
# Partie Analyse Syntaxique
##################################################

class LambdaSyntaxError(Exception):
    def __init__(self, msg):
        self.message = msg

class Lambda_lexer(Lexer):
    tokens = {VAR, LPAR, RPAR, LAMBDA, POINT}
    VAR = r'[a-zA-Z][a-zA-Z0-9]*'
    LPAR = r'\('
    RPAR = r'\)'
    LAMBDA = r'\!|λ'
    POINT = r'\.'
    ignore = ' \t'
    
    @_(r'\n+')
    def ignore_newline(self, t):
        self.lineno += len(t.value)
        
    def error(self, t):
        raise LambdaSyntaxError('Caractère illégal : {:s} at position {:d}'.format(t.value[0],
                                                                                   t.index))
        self.index += 1

lexer = Lambda_lexer()

class Lambda_parser(Parser):
    tokens = Lambda_lexer.tokens
    
    @_('VAR')
    def term(self, p):
        return Lambda_terme(0, p[0])
    
    @_('LAMBDA VAR POINT term')
    def term(self, p):
        return Lambda_terme(1, p[1], p.term)
    
    @_('LPAR term term RPAR')
    def term(self, p):
        return Lambda_terme(2, p.term0, p.term1)

parser = Lambda_parser()

##################################################
# Une classe pour représenter les λ-termes
##################################################

def _autre_variable(var, variables):
    '''
    renvoie var concaténé avec le premier numéro de sorte que le résultat  ne soit pas dans variables
    fonction utile pour les substitutions de termes
    '''
    n = 0
    while var + '{:d}'.format(n) in variables:
        n += 1
    return var + '{:d}'.format(n)

class Lambda_termeError(Exception):
    def __init__(self, msg):
        self.message = msg
        
class Lambda_terme():
    def __init__(self, categorie, *args):
        if categorie not in (0, 1, 2):
            raise Lambda_termeError('categorie non valide')
        if categorie == 0: 
            if len(args) != 1 or not isinstance(args[0], str):
                raise Lambda_termeError('mauvaise construction pour une variable')
        elif categorie == 1:
            if (len(args) != 2 or
                not isinstance(args[0], str) or
                not isinstance(args[1], Lambda_terme)):
                raise Lambda_termeError('mauvaise construction pour une abstraction')
        else:
            if (len(args) != 2 or
                not isinstance(args[0], Lambda_terme) or
                not isinstance(args[1], Lambda_terme)):
                raise Lambda_termeError('mauvaise construction pour une application')
        self._content = (categorie,) + tuple(args)
        
    @staticmethod
    def cree(descr):
        return parser.parse(lexer.tokenize(descr))
    
    def est_variable(self):
        return self._content[0] == 0

    def est_abstraction(self):
        return self._content[0] == 1

    def est_application(self):
        return self._content[0] == 2

    def applique(self, terme):
        if not isinstance(terme, Lambda_terme):
            raise Lambda_termeError('Application impossible')
        return Lambda_terme(2, self, terme)
    
    def abstrait(self, var):
        if not isinstance(var, str):
            raise Lambda_termeError("Variable d'Abstraction invalide")
        return Lambda_terme(1, var, self)
    
    def est_redex(self):
        return self.est_application() and self._content[1].est_abstraction()
    
    def est_forme_normale(self):
        if self.est_variable():
            return True
        elif self.est_abstraction():
            return self._content[2].est_forme_normale()
        else:
            return (not self._content[1].est_abstraction() and
                    all(self._content[k].est_forme_normale() for k in (1, 2)))
        
    def variables_libres(self):
        if self.est_variable():
            return {self._content[1]}
        elif self.est_application():
            var_libres = self._content[2].variables_libres()
            return var_libres.union(self._content[1].variables_libres())
        else:
            var_libres = self._content[2].variables_libres()
            var_libres.discard(self._content[1])
            return var_libres
    
    def subs(self, var, terme):
        if not isinstance(var, str):
            raise Lambda_termeError('subst possible uniquement pour les variables')
        if not isinstance(terme, Lambda_terme):
            raise Lambda_termeError('subst possible uniquement sur un lambda-terme')
        if self.est_variable():
            if var == self._content[1]:
                return terme
            else:
                return self
        elif self.est_application():
            return Lambda_terme(2,
                                self._content[1].subs(var, terme),
                                self._content[2].subs(var, terme))
        else:
            var_abstr = self._content[1]
            corps_abstr = self._content[2]
            var_libres_corps = corps_abstr.variables_libres()
            if var == var_abstr or var not in var_libres_corps:
                return self
            elif var_abstr not in terme.variables_libres():
                return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))
            else:
                nouvelle_var = _autre_variable(var_abstr, corps_abstr.variables_libres())
                return Lambda_terme(1, 
                                    nouvelle_var, 
                                    corps_abstr.subs(var_abstr,
                                                     Lambda_terme(0,nouvelle_var)).subs(var, terme))

    def _reduit(self):
        if self.est_variable():
            return self, False
        elif self.est_abstraction():
            corps_reduit, est_reduit = self._content[2]._reduit()
            return (Lambda_terme(1,
                                 self._content[1],
                                 corps_reduit) if est_reduit else self,
                    est_reduit)
        else:
            termegauche = self._content[1]
            termedroit = self._content[2]
            if termegauche.est_abstraction():
                var_abstr = termegauche._content[1]
                corps = termegauche._content[2]
                return corps.subs(var_abstr, termedroit), True
            else:
                termegauche_reduit, est_reduit = termegauche._reduit()
                if est_reduit:
                    return Lambda_terme(2, termegauche_reduit, termedroit), est_reduit
                else:
                    termedroit_reduit, est_reduit = termedroit._reduit()
                    return (Lambda_terme(2,
                                         termegauche,
                                         termedroit_reduit) if est_reduit else self,
                            est_reduit)
                
    def reduit(self):
        return self._reduit()
            
    def __str__(self):
        if self.est_variable():
            return self._content[1]
        elif self.est_abstraction():
            return 'λ{:s}.{:s}'.format(self._content[1], str(self._content[2]))
        else:
            return '({:s} {:s})'.format(str(self._content[1]), str(self._content[2]))

        
if __name__ == '__main__':
    import doctest
    doctest.testmod(optionflags=doctest.NORMALIZE_WHITESPACE | doctest.ELLIPSIS, verbose=False)