Require Export Derivation.

Module Dec_Word.

  Import Base Lists Definitions Derivation Symbols.

  Section Hm.

    Context {Tt Vt: Type}.
    Context {Tt_eqdec: eq_dec Tt}.
    Context {Vt_eqdec: eq_dec Vt}.

    Definition item := prod (@symbol Tt Vt) (@phrase Tt Vt).
    Definition items G u : list item :=
      @product _ _ _ (@pair _ _) (@symbs _ _ G) (segms u).

  End Hm.

  Section Dec_Word.

    Context {Tt Vt: Type}.
    Context {Tt_eqdec: eq_dec Tt}.
    Context {Vt_eqdec: eq_dec Vt}.

    Variable G : @grammar Tt Vt.
    Variable u : @phrase Tt Vt.

    Definition step (M : list item) i :=
      match i with
          (s, v) ⇒ v = [s] ∨ match s with
                                 Vs A ⇒ ∃ M', M' <<= M ∧ R A (fsts M') el G ∧ v = concat (snds M')
                               | _ ⇒ False
                             end
      end.

    Fixpoint fsts_comb X Y (D : eq_dec X) (M : list (X × Y)) (v : list X) : (list (list (X × Y))) :=
      match v with
          [] ⇒ [ [] ]
        | s :: v ⇒
          let
            M' := @fsts_comb _ _ D M v
          in let
            S := @filter _ (fun e ⇒ match e with (s', _) ⇒ s = s' end) (filter_prod_dec _ _ _) M
          in
          @product _ _ _ (fun s M ⇒ s :: M) S M'
      end.

    Lemma fsts_comb_corr1 X Y (D : eq_dec X) (M : list (X × Y)) (v : list X) (l : list (X × Y)) :
      l el fsts_comb M v → fsts l = v ∧ l <<= M.

    Lemma fsts_comb_corr2 X Y (D : eq_dec X) (M : list (X × Y)) (v : list X) (l : list (X × Y)) :
      fsts l = v ∧ l <<= M → l el fsts_comb M v.

    Lemma fsts_comb_corr X Y (D : eq_dec X) (M : list (X × Y)) (v : list X) (l : list (X × Y)) :
      l el fsts_comb M v ↔ fsts l = v ∧ l <<= M.

    Global Instance step_dec' (M : list item) A v :
      dec (∃ M', M' <<= M ∧ R A (fsts M') el G ∧ v = concat (snds M')).

    Global Instance step_dec M i : dec (step M i).

    Definition DW := FCI.C (step := step) (items G u).

    Lemma items_refl s v :
      s el symbs G → (s, v) el items G v.

    Lemma derf_DW v w :
      (∀ s, s el v → s el symbs G) → segment u w → derf G v w → ∃ M, v = fsts M
                                                                     ∧ w = concat (snds M)
                                                                     ∧ M <<= DW.

    Hint Constructors derf.


    Lemma DW_derf' :
      inclp DW (fun i ⇒ match i with (s, v) ⇒ derf G [s] v end).


    Lemma DW_der_equiv' s v :
      s el symbs G → ((s,v) el DW ↔ derf G [s] v ∧ segment u v).

    Lemma DW_der_equiv A :
      Vs A el symbs G → (der G A u ↔ (Vs A, u) el DW).

  End Dec_Word.

  Section DecidabilityOfWordProblem.
    Context {Tt Vt: Type}.
    Context {Tt_eqdec: eq_dec Tt}.
    Context {Vt_eqdec: eq_dec Vt}.

    Global Instance der_dec G A u : dec (@der Tt Vt G A u).

    Global Instance lang_dec G A u : dec (@language Tt Vt G A u).

  End DecidabilityOfWordProblem.

End Dec_Word.