#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
@author: Sylvain Boulmé
         et avec des suggestions d'Antoiner Terrier (Ensimag 1AA 2025-2026) pour la version "typée"
"""

import sys
assert (sys.version >= "3.12")

#######
#
# On manipule deux types d'automates: 
#   - DetAutomata
#   - NonDetAutomata
#
# La différence entre les deux porte uniquement sur le type de transitions.
# On factorise cette différence avec des types génériques.

type GTrans[Target] = dict[str, dict[str, Target]]

type DetTrans = GTrans[str]
type NonDetTrans = GTrans[set[str]]

type GAutomata[TTrans] = tuple[
    set[str],  # États
    set[str],  # Alphabet
    str,       # État de départ
    TTrans,    # Transitions
    set[str],  # États acceptants / finaux
]

type DetAutomata = GAutomata[DetTrans]
type NonDetAutomata = GAutomata[NonDetTrans]

type Automata = DetAutomata | NonDetAutomata
type Trans = DetTrans | NonDetTrans

# Remarque:
#   si (Q, V, s, delta, F): Automata
#   on impose ici toujours que Q == { q for q in delta }
#   => c'est explicite dans la fonction "display_system" ci-dessous.

#######
#
# Encodage des automates déterministes (pas forcément complet)

# Exemple d'automate déterministe et complet
pair: DetAutomata = (
    {'s', 'q'},
    {'a', 'b'},
    's',
    { 's': { 'a': 'q', 'b': 's' },
      'q': { 'a': 's', 'b': 'q' }},
    { 's' }
)

# affiche l'équation de "q"
def display_eq(q: str, delta: Trans, F: set[str]) -> None:
    print("{0} = ".format(q), end="")
    tq = delta[q]
    rq = q in F
    if rq:
        print("ε" , end="")
    for a in sorted(tq):
        if rq: # <=> la somme n'est pas vide
            print(" + ", end="")
        else:
            rq = True
        print("{0}.{1}".format(a, tq[a]), end="")
    print("" if rq else "∅")

# affiche le système d'équations
def display_system(A: Automata) -> None:
    (Q, V, s, delta, F) = A
    assert (Q == { q for q in delta }) # verif cohérence
    display_eq(s, delta, F) # axiome d'abord !
    for q in sorted(Q):
        if q != s:
            display_eq(q, delta, F)

def display_named_system(A: str) -> None:
    print("==={}===".format(A))
    display_system(eval(A))
    print()

# calcul du complémentaire de A
def complement(A: DetAutomata) -> DetAutomata:
    # remarque ici l'automate doit être complet
    (Q, V, s, delta, F) = A
    return (Q, V, s, delta, Q - F)

def rename(A: DetAutomata) -> DetAutomata:
    (Q, V, s, delta, F) = A
    rs = 'r'+repr(0) # renommage de l'axiome
    acc = [s]        # liste (dans l'ordre) des anciens noms (renommés)
    ren = { s: rs }  # dict des anciens noms vers les nouveaux
    rdelta = dict()
    todo = 0  # prochain état renommé dont il faut générer l'équation
    while todo < len(acc):
        q = acc[todo]
        tq = delta[q]
        rtodo = ren[q]
        rdelta[rtodo] = dict()
        tr = rdelta[rtodo]
        for a in sorted(V):
            if not a in tq:
                continue # automate incomplet
            q0 = tq[a]
            if q0 in ren:
                rq0 = ren[q0]  # q0 déjà renommé
            else:
                rq0 = 'r'+repr(len(acc)) # nouveau nom pour q0
                acc.append(q0)
                ren[q0] = rq0  # renommage q0 effectué
            tr[a] = rq0 # renommage de la transition
        todo += 1  # prochaine équation à visiter
    rQ = set(ren[q] for q in acc)
    rF = set(ren[q] for q in acc if q in F)
    return (rQ, V, rs, rdelta, rF)

impair: DetAutomata = complement(pair)

A0: DetAutomata = (
    {'q1','q2','q3'},
    {'0','1'},
    'q2',
    { 'q1':{'0':'q3', '1':'q2'},
      'q2':{'0':'q3', '1':'q2'},
      'q3':{'0':'q2', '1':'q3'} },
    { 'q1','q3' }
)

A1: DetAutomata = (
    {'q1','q2','q3','q4'},
    {'1','0'},
    'q1',
    { 'q1':{'0':'q2', '1':'q1'},
      'q2':{'0':'q1', '1':'q2'},
      'q3':{'0':'q1', '1':'q4'},  
      'q4':{'0':'q4', '1':'q3'} },
    { 'q2', 'q4' }
)

display_named_system('A0')
display_named_system('A1')
display_named_system('rename(A0)')
assert (rename(A0)==rename(A1))
assert(rename(A0)==
       ({'r1', 'r0'},
        {'0', '1'},
        'r0',
        {'r0': {'0': 'r1', '1': 'r0'},
         'r1': {'0': 'r0', '1': 'r1'}},
        {'r1'}))

#######
#
# Encodage des automates non-déterministes (sans epsilon-transition)

# exemple d'automate non-déterministe
a_L3 = ({'s', 'q1', 'q2', 'q3'},
        {'0', '1'},
        's',
        { 's': { '0': { 's', 'q1'}, '1': {'s'} },
          'q1': { '0': { 'q2'}, '1': {'q2'} },
          'q2': { '0': { 'q3'}, '1': {'q3'} },
          'q3': {} },
        { 'q3' })
display_named_system('a_L3')  # l'affichage peut toujours être utilisé 

def accepte(A: Automata, w: str) -> bool:
    (Q, V, s, delta, F) = A
    xq = frozenset({s})
    for a in w:
        xq = frozenset(q0 for q in xq if a in delta[q] for q0 in delta[q][a])
    for q in xq:
        if q in F:
            return True
    return False

# cacul d'un automate déterministe et complet, et canonique pour le renommage
def determ(A: NonDetAutomata) -> DetAutomata:
    (Q, V, s, delta, F) = A
    TODO() # à remplacer

term_a: NonDetAutomata = (
    {'s', 'f'},
    {'a', 'b'},
    's',
    { 's': { 'a': { 's', 'f'}, 'b': {'s'} },
      'f': {} },
    { 'f' }
)

display_named_system('term_a')
assert (determ(term_a) == ({'r0', 'r1'}, {'b', 'a'}, 'r0', {'r0': {'a': 'r1', 'b': 'r0'}, 'r1': {'a': 'r1', 'b': 'r0'}}, {'r1'}))

assert (determ(a_L3) == ({'r1', 'r0', 'r3', 'r7', 'r2', 'r6', 'r5', 'r4'},
                           {'1', '0'},
                           'r0',
                           {'r0': {'0': 'r1', '1': 'r0'},
                            'r1': {'0': 'r2', '1': 'r3'},
                            'r2': {'0': 'r4', '1': 'r5'},
                            'r3': {'0': 'r6', '1': 'r7'},
                            'r4': {'0': 'r4', '1': 'r5'},
                            'r5': {'0': 'r6', '1': 'r7'},
                            'r6': {'0': 'r2', '1': 'r3'},
                            'r7': {'0': 'r1', '1': 'r0'}},
                           {'r4', 'r6', 'r7', 'r5'}) )
display_named_system('determ(a_L3)')

###############
# exos de derminisation de la feuille 04
Delta1: NonDetAutomata = (
    {'q1', 'q2', 'q3', 'q4', 'q5'},
    {'a', 'b', 'c'},
    'q1',
    { 'q1': { 'a': { 'q2', 'q5'}, 'b': {'q3'} },
      'q2': { 'a': { 'q2'}, 'b': {'q3'} }, 
      'q3': { },
      'q4': { 'a': {'q5'} },
      'q5': { 'b': {'q5'} }, },
    { 'q3', 'q5' }
)

display_named_system('Delta1')
assert (determ(Delta1) == ({'r0', 'r4', 'r2', 'r6', 'r3', 'r1', 'r5'},
                           {'c', 'a', 'b'},
                           'r0',
                           {'r0': {'a': 'r1', 'b': 'r2', 'c': 'r3'},
                            'r1': {'a': 'r4', 'b': 'r5', 'c': 'r3'},
                            'r2': {'a': 'r3', 'b': 'r3', 'c': 'r3'},
                            'r3': {'a': 'r3', 'b': 'r3', 'c': 'r3'},
                            'r4': {'a': 'r4', 'b': 'r2', 'c': 'r3'},
                            'r5': {'a': 'r3', 'b': 'r6', 'c': 'r3'},
                            'r6': {'a': 'r3', 'b': 'r6', 'c': 'r3'}},
                           {'r5', 'r1', 'r2', 'r6'}))
display_named_system('determ(Delta1)')
display_named_system("Delta1")

Delta2: NonDetAutomata = (
    {'q1', 'q2', 'q3', 'q4'},
    {'a', 'b', 'c'},
    'q1',
    { 'q1': { 'a': { 'q1', 'q2'}, 'c': {'q3'} },
      'q2': { 'b': { 'q1', 'q3', 'q4' } }, 
      'q3': { 'b': { 'q3', 'q4'} },
      'q4': { 'b': {'q4'} }, },
    { 'q2', 'q3', 'q4' }
)

display_named_system('Delta2')
assert (determ(Delta2) == ({'r0', 'r2', 'r3', 'r4', 'r1', 'r5'},
                           {'a', 'b', 'c'},
                           'r0',
                           {'r0': {'a': 'r1', 'b': 'r2', 'c': 'r3'},
                            'r1': {'a': 'r1', 'b': 'r4', 'c': 'r3'},
                            'r2': {'a': 'r2', 'b': 'r2', 'c': 'r2'},
                            'r3': {'a': 'r2', 'b': 'r5', 'c': 'r2'},
                            'r4': {'a': 'r1', 'b': 'r5', 'c': 'r3'},
                            'r5': {'a': 'r2', 'b': 'r5', 'c': 'r2'}},
                           {'r4', 'r1', 'r3', 'r5'}) )

Delta3: NonDetAutomata = (
    {'q1', 'q2', 'q3', 'q4', 'q5'},
    {'a', 'b'},
    'q1',
    { 'q1': { 'a': { 'q1', 'q2'}, 'b': {'q1'} },
      'q2': { 'b': {'q3'} },
      'q3': { 'a': { 'q3', 'q4'}, 'b': {'q3'} },
      'q4': { 'b': {'q5'} },
      'q5': { 'a': { 'q5' }, 'b': {'q5'} }, },
    { 'q5' }
)

display_named_system('Delta3')
assert (determ(Delta3) == ({'r0', 'r2', 'r3', 'r4', 'r1', 'r5'},
                           {'b', 'a'},
                           'r0',
                           {'r0': {'a': 'r1', 'b': 'r0'},
                            'r1': {'a': 'r1', 'b': 'r2'},
                            'r2': {'a': 'r3', 'b': 'r2'},
                            'r3': {'a': 'r3', 'b': 'r4'},
                            'r4': {'a': 'r5', 'b': 'r4'},
                            'r5': {'a': 'r5', 'b': 'r4'}}, {'r4', 'r5'}))

Delta4: NonDetAutomata = (
    { 'q1', 'q4' },
    { 'a', 'b', 'c' },
    'q1',
    { 'q1': { 'a': { 'q1', 'q4' }, 'b': { 'q1' } },
      'q4': { 'c': { 'q4' } } },
    { 'q4' }
)

display_named_system('Delta4')
assert (determ(Delta4) == ({'r3', 'r2', 'r0', 'r1'},
                          {'a', 'c', 'b'},
                          'r0', {'r0': {'a': 'r1', 'b': 'r0', 'c': 'r2'},
                                 'r1': {'a': 'r1', 'b': 'r0', 'c': 'r3'},
                                 'r2': {'a': 'r2', 'b': 'r2', 'c': 'r2'},
                                 'r3': {'a': 'r2', 'b': 'r2', 'c': 'r3'}},
                          {'r3', 'r1'}))


def lift(A: DetAutomata) -> NonDetAutomata:
    (Q, V, s, delta, F) = A
    ndelta = { q: { a: { delta[q][a] } for a in delta[q] } for q in delta }
    return (Q, V, s, ndelta, F) # retourne encodage "non-déterministe" de A


print("== Quelques vérifications finales ==")


A : DetAutomata # ici pour automates déterministes et complet
for A in (pair, impair, A0, A1):
    assert determ(lift(A)) == rename(A) 

NA: NonDetAutomata
for NA in (Delta1, Delta2, Delta3, Delta4):
    A = determ(NA)
    assert determ(lift(A)) == A  # idempotence

print("== DONE ! ==")