#!/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):
    ''' Grammaire décrivant les λ-termes
        term : VAR
             | LAMBDA VAR POINT term
             | LPAR term term RPAR
    '''
    tokens = Lambda_lexer.tokens
    

    @_('VAR')
    def term(self, p):
        return (0, p[0])
    
    @_('LAMBDA VAR POINT term')
    def term(self, p):
        return (1, p[1], p.term)
    
    @_('LPAR term term RPAR')
    def term(self, p):
        return (2, p.term0, p.term1)

    def error(self, p):
        if p:
            raise LambdaSyntaxError('{} inattendu en position {}'.format(p.type, p.index))
        else:
            raise LambdaSyntaxError('description inachevée')
        
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():
    '''
    Création de λ-terme

    >>> T1 = Lambda_terme('z')
    >>> print(T1)
    z
    >>> T2 = Lambda_terme('!x.(y x)')
    >>> print(T2)
    λx.(y x)
    >>> T3 = Lambda_terme('(!x.(y x) z)')
    >>> print(T3)
    (λx.(y x) z)

    Quelques prédicats
    >>> [(t.est_variable(), t.est_abstraction(), t.est_application()) for t in (T1, T2, T3)]
    [(True, False, False), (False, True, False), (False, False, True)] 

    Abstraction d'un terme
    >>> T4 = T3.abstrait('z')
    >>> print(T4)
    λz.(λx.(y x) z)

    Application d'un terme sur un autre
    >>> T5 = T4.applique(Lambda_terme('t'))
    >>> print(T5)
    (λz.(λx.(y x) z) t)

    Sous-termes d'un terme
    >>> for t in T5.sous_termes():
    ...     print(t)
    (λz.(λx.(y x) z) t)
    λz.(λx.(y x) z)
    (λx.(y x) z)
    λx.(y x)
    (y x)
    y
    x
    z
    t
    
    Autres prédicats
    >>> [(t.est_redex(), t.est_forme_normale()) for t in (T1, T2, T3, T4, T5)]
    [(False, True), (False, True), (True, False), (False, False), (True, False)]

    Calcul de forme normale

    >>> print(T5.forme_normale())
    (y t)
    >>> print(T5.forme_normale(verbose=True))
    (λz.(λx.(y x) z) t)
      1: ---> (λz.(λx.(y x) z) t)
      2: ---> (λx.(y x) t)
      3: ---> (y t)
    Forme normale calculée : (y t)
    (y t)
    >>> OMEGA = Lambda_terme('(!x.(x x) !x.(x x))')
    >>> print(OMEGA.forme_normale(verbose=True, nb_etapes_max=10))
    (λx.(x x) λx.(x x))
      1: ---> (λx.(x x) λx.(x x))
      2: ---> (λx.(x x) λx.(x x))
      3: ---> (λx.(x x) λx.(x x))
      4: ---> (λx.(x x) λx.(x x))
      5: ---> (λx.(x x) λx.(x x))
      6: ---> (λx.(x x) λx.(x x))
      7: ---> (λx.(x x) λx.(x x))
      8: ---> (λx.(x x) λx.(x x))
      9: ---> (λx.(x x) λx.(x x))
     10: ---> (λx.(x x) λx.(x x))
    Pas de forme normale atteinte après 10 étapes de réduction
    None
    '''
    def __init__(self, *args):
        nb_args = len(args)
        if nb_args not in (1, 2, 3):
            raise Lambda_termeError('Lambda_terme : Nbre arguments incorrect')
        if nb_args == 1:
            if not isinstance(args[0], str):
                raise Lambda_termeError('Lambda_terme : type argument incorrect')
            self._content = Lambda_terme._cree(parser.parse(lexer.tokenize(args[0])))
        else:
            categorie = args[0]
            if categorie not in (0, 1, 2):
                raise Lambda_termeError('categorie non valide')
            if categorie == 0: 
                if nb_args != 2 or not isinstance(args[1], str):
                    raise Lambda_termeError('mauvaise construction pour une variable')
                self._content = tuple(args)
            elif categorie == 1:
                if (nb_args != 3 or
                    not isinstance(args[1], str) or
                    not (isinstance(args[2], tuple) or isinstance(args[2], Lambda_terme))):
                    raise Lambda_termeError('mauvaise construction pour une abstraction')
                self._content = (1, args[1],
                                 Lambda_terme(*args[2]) if isinstance(args[2], tuple) else args[2])
            else:
                if (nb_args != 3 or
                    not (isinstance(args[1], tuple) or isinstance(args[1], Lambda_terme)) or
                    not (isinstance(args[2], tuple) or isinstance(args[2], Lambda_terme))):
                    raise Lambda_termeError('mauvaise construction pour une application')
                self._content = (2,
                                 Lambda_terme(*args[1]) if isinstance(args[1], tuple) else args[1],
                                 Lambda_terme(*args[2]) if isinstance(args[2], tuple) else args[2])

    @staticmethod
    def _cree(descr):
        if descr[0] == 0:
            return descr
        elif descr[0] == 1:
            return (1, descr[1], Lambda_terme(*descr[2]))
        else:
            return (2, Lambda_terme(*descr[1]), Lambda_terme(*descr[2]))
                    
    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 __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]))
    
    def __eq__(self, terme):
        if not isinstance(terme, Lambda_terme):
            raise Lambda_termeError('Comparaison impossible')
        if self.est_variable():
            return terme.est_variable() and self._content[1] == terme._content[1]
        elif self.est_application():
            return (terme.est_application() and 
                    self._content[1] == terme._content[1] and
                    self._content[2] == terme._content[2])
        else:
            return (terme.est_abstraction() and
                    self._content[2] == terme._content[2].subs(terme._content[1],
                                                               Lambda_terme(self._content[1])))
                    
    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 variables(self):
        if self.est_variable():
            return ({self._content[1]}, set())
        elif self.est_application():
            var_libres1, var_liees1 = self._content[1].variables()
            var_libres2, var_liees2 = self._content[2].variables()
            return (var_libres1.union(var_libres2),
                    var_liees1.union(var_liees2))
        else:
            var_libres, var_liees = self._content[2].variables()
            if self._content[1] in var_libres:
                var_libres.discard(self._content[1])
                var_liees.add(self._content[1])
            return (var_libres, var_liees)
        
    def sous_termes(self):
        if self.est_variable():
            ss_termes = []
        elif self.est_abstraction():
            ss_termes = self._content[2].sous_termes()
        else:
            ss_termes = self._content[1].sous_termes()
            ss_termes.extend(self._content[2].sous_termes())
        return [self] + ss_termes
    
    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 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()
            if var == var_abstr or var not in var_libres_corps:
                return self
            elif var_abstr not in terme.variables()[0]:
                return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))
            else:
                nouvelle_var = _autre_variable(var_abstr, var_libres_corps)
                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 forme_normale(self, nb_etapes_max=100, verbose=False):
        lambda_terme = self
        etape = 0
        forme_normale_atteinte = False
        if verbose: print(lambda_terme)
        while not forme_normale_atteinte and etape < nb_etapes_max:
            etape += 1
            terme_reduit, est_reduit = lambda_terme.reduit()
            if verbose: print('{:3d}: ---> {:s}'.format(etape, str(terme_reduit)))
            forme_normale_atteinte = terme_reduit.est_forme_normale()
            lambda_terme = terme_reduit
        if forme_normale_atteinte:
            if verbose: print('Forme normale calculée : {:s}'.format(str(terme_reduit)))
            return terme_reduit
        else:
            if verbose: print('Pas de forme normale atteinte après {:d} étapes de réduction'.format(etape))
            return None

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