RIS.closed_automaton: computing an automaton for the α-closure of an expression.

Set Implicit Arguments.

Require Import tools algebra language regexp automata systems.
Require Import aeq_facts alpha_regexp closed_languages binding_finite.

Section s.
  Context {atom : Set}{𝐀 : Atom atom}.
  Context {X : Set} {𝐗 : Alphabet 𝐀 X}.

  Notation Regexp := (@regexp letter).

  Definition bounded_stack A B n : list stack :=
    flat_map (lists_of_length (pairs A B)) (seq 0 (S n)).

  Definition state_space e A :=
    pairs (bounded_stack ⌊e⌋ A (2×sizeExpr e)) (stateSpace e).

  Definition transitions_from A (state : stack × Regexp) l :=
    match (state,l) with
    | (s,e,open a) ⇒ flat_map (fun f ⇒ map (fun b ⇒ ((s,e),open b,((a,b)::s,f))) A) (δA (open a) e)
    | (s,e,close a) ⇒ if (pairedb s a (image s a)) && (inb (image s a) A) then
                        map (fun f ⇒ ((s,e),close (image s a),(s⊖(a,image s a),f))) (δA (close a) e)
                      else []
    | (s,e,var x) ⇒
      match var_perm' ⌊x⌋ s with
      | None ⇒ []
      | Some p ⇒
        if inclb ⌊p∙x⌋ A
        then map (fun f ⇒ ((s,e),var (p∙x),(s,f))) (δA (var x) e)
        else []
      end
    end.

  Lemma transitions_from_spec A f s e l s1 s2 e1 e2 l' :
    (s,e)∈ state_space f A →
    ((s1,e1),l',(s2,e2)) ∈ transitions_from A (s,e) l ↔
    (s1 = s ∧ e1 = e ∧ ⌊l'⌋ ⊆ A ∧ e2 ∈ δA l e ∧ s ⊣ l | l' ↦ s2) .

  Definition closed_automaton (e : Regexp) (A : list atom) : NFA (stack×Regexp) letter :=
    (filter (fun st ⇒ (prj1 (fst st) =?= prj2 (fst st)) && ϵ (snd st) =?= e_un)(state_space e A),

     flat_map (fun st ⇒ flat_map (transitions_from A st) (Var e)) (state_space e A)).

  Lemma path_support u v s1 s2 : s1 ⊣ u | v ⤅ s2 → prj1 s2 ⊆ prj1 s1 ++ ⌊u⌋
                                                   ∧ prj2 s2 ⊆ prj2 s1 ++ ⌊v⌋.

  Lemma lang_close_automaton e A :
    is_binding_finite e →
    langNFA (closed_automaton e A) ([],e) ≃ restrict (cl_α ⟦e⟧) A.


End s.