# ------------------------------------------------*- coding: utf-8 -*-
# Fichier : parser_lambda_ply.py
# Type    : Python + ply (pip install ply)
# Contient: Parsing sans contrôle de lambda-termes et représentation
#           sous forme d'arbre syntaxique
# 
#  Représentation des arbres : liste dont le premier terme (str) est
#  la racine, les termes suivants les fils. 
# ----------------------------------------------------------------------
import re

# ----------------------------------------------------------------------
# Partie LEX
# ----------------------------------------------------------------------
# Mots-clés réservés. Stockés dans un dictionnaire pour la gestion des
# identificateurs
reserved = {
    'and' : 'Et',
    'or'  : 'Ou',
    'implies' : 'Imp',
    'not' : 'Non',
    'all' : 'Q_Uni',
    'some': 'Q_Exi',
    'lambda' : 'Lambda'
}

# Liste des catégories de tokens qui vont être reconnues par le lexer
tokens = ['Var', 'CteI', 'CteP'] + [v for v in reserved.values()]

# Liste des tokens qui vont être passés tel quels à la grammaire
literals = ['(',')', '.']

# Définition des tokens définissables par une regexp
t_Et = r'&|\^'
t_Ou = r'\+|v|\|'
t_Imp = r'[-][>]'
t_Non = r'-|!'

# Convention de notation:
# Les variables sont des lettres minuscules
#t_Var = r'[a-z]'
# Les constantes individuelles sont des mots (2 lettres min) commençant par une maj
#t_CteI = r'[A-Z][a-z]+'
# Les constantes de prédicat sont des mots (2 lettres min) en minuscule
#t_CteP = r'[a-z][a-z]+'
# Pour mieux gérer les conflits entre ces formes, on utilise une fonction spécifique
# Gestion des identificateurs et des mots-clé: cf. doc ply

def t_ID(t):
    r'[a-zA-Z][a-zA-Z]*'
    if t.value in reserved:
        t.type = reserved.get(t.value,'ID')
    elif re.match(r'[A-Z][a-z]+',t.value): 
        t.type = 'CteI'
    elif re.match(r'[a-z][a-z]+',t.value): 
        t.type = 'CteP'
    elif re.match(r'[a-z]',t.value): 
        t.type = 'Var'
    else: 
        pass
    return t

# Séparateurs pour PLY
t_ignore = " \t\n"

# fonction déclenchée en cas d'erreur du lexeur
def t_error(t):
    print("Erreur de lexeur (%c)" % t.value[0])
    t.lexer.skip(1) 

# Construction du lexeur
import ply.lex as lex
lex.lex()

# ----------------------------------------------------------------------
# Code utilitaire
# ----------------------------------------------------------------------
# str_tree: prend un arbre et renvoie une string correspondant à la
# linéarisation de l'arbre (une formule, donc)
def str_tree(t):
    s = ""
    if len(t) == 1: s = s + str(t[0])
    else:
        tete = t[0]
        if tete == 'Conj':
            s = "(" + str_tree(t[1]) + " and " + str_tree(t[2]) + ")"
        elif tete == 'Disj':
            s = "(" + str_tree(t[1]) + " or " + str_tree(t[2]) + ")"
        elif tete == 'Impl':
            s = "(" + str_tree(t[1]) + " impl " + str_tree(t[2]) + ")"
        elif tete == 'Neg':
            s = "neg " + str_tree(t[1])
        elif tete == 'af':
            s = "(" + str_tree(t[1]) + ") " + str_tree(t[2])
        elif tete == 'Quant_u':
            s = "all " + str_tree(t[1]) + ". " +str_tree(t[2])
        elif tete == 'Quant_e':
            s = "some " + str_tree(t[1]) + ". " +str_tree(t[2])
        elif tete == 'Lambda':
            s = "lambda " + str_tree(t[1]) + ". " +str_tree(t[2])
        else: # t n'est pas censé être une liste
            s = str(t)
    return s


# ----------------------------------------------------------------------
# Partie YACC
# ----------------------------------------------------------------------
# Règle de grammaire pour permettre de parser une infinité d'expressions
def p_axiome(p):
    """S : cde S
         | """

# Une commande est une expression complète
def p_cde_expr(p):
    "cde : expr"
    print("Expression reconnue", str_tree(p[1]))


"""
    'term : Var
          | CteI'
    "af : '(' expr ')' term"
    'expr : CteP'
    "expr : af"
    "expr : Non expr"
    "expr : '(' expr Ou expr ')'"
    "expr : '(' expr Et expr ')'"
    "expr : '(' expr Imp expr ')'"
    "expr : Q_Uni Var '.' expr"
    "expr : Q_Exi Var '.' expr"
    "expr : Lambda Var '.' expr"
"""

def p_term(p):
    """term : Var
            | CteI"""
    p[0] = [p[1]]
    
def p_expr_pred(p):
    'expr : CteP'
    p[0] = p[1]

def p_appfonc(p):
   "af : '(' expr ')' term"
   p[0] = ['af', p[2], p[4]]

def p_expr_atomique(p):
    "expr : af"
    p[0] = p[1]

def p_expr_neg(p):
    "expr : Non expr"
    p[0] = ['Neg', p[2]]

def p_expr_ou(p):
    "expr : '(' expr Ou expr ')'"
    p[0] = ['Disj', p[2], p[4]]

def p_expr_et(p):
    "expr : '(' expr Et expr ')'"
    p[0] = ['Conj', p[2], p[4]]
    
def p_expr_imp(p):
    "expr : '(' expr Imp expr ')'"
    p[0] = ['Impl', p[2], p[4]]

def p_exp_quant_u(p):
    "expr : Q_Uni Var '.' expr"
    p[0] = ['Quant_u', p[2], p[4]]

def p_exp_quant_e(p):
    "expr : Q_Exi Var '.' expr"
    p[0] = ['Quant_e', p[2], p[4]]
    
def p_exp_lambda(p):
    "expr : Lambda Var '.' expr"
    p[0] = ['Lambda', p[2], p[4]]

def p_error(p):
   print("Erreur de syntaxe")

import ply.yacc as yacc
yacc.yacc()
# ----------------------------------------------------------------------
# Parser
# ----------------------------------------------------------------------
txt = """
(dog) Fido
((dog) Fido and (cat) Felix)
not (man) Fido
((dog) Fido | (cat) Felix)
((dog) Fido & (cat) Felix)
((dog) Fido ^ (cat) Felix)
((dog) Fido -> (cat) Felix)
all x. ((man) x -> (mortal) x)
all x. ((man) x -> some y. ((woman) y and ((love) x) y))
"""

# Le parser est lancé sur une variable de test
yacc.parse(txt)

# Boucle infinie pour tester de nouvelles expressions
while 1:
    try:
        s = input('ok> ')
    except EOFError:
        break
    if not s: continue
    yacc.parse(s)