Require Export Base Lists.

Module Definitions.

  Import Base Lists.

  Section Defs.

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

    Inductive ter : Type :=
    | T : Tt → ter.

    Inductive var : Type :=
    | V : Vt → var.

    Inductive symbol : Type :=
    | Ts : ter → symbol
    | Vs : var → symbol.

    Definition phrase := list symbol.

    Inductive rule : Type :=
    | R : var → phrase → rule.

    Definition grammar := list rule.

  End Defs.

  Section DecidabilityInstances.

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

    Global Instance ter_eq_dec : eq_dec (@ter Tt).

    Global Instance var_eq_dec : eq_dec (@var Vt).

    Global Instance rule_eq_dec : eq_dec (@rule Tt Vt).

    Global Instance symbol_eq_dec : eq_dec (@symbol Tt Vt).

    Global Instance exists_rule_dec G p {D : ∀ A u, dec (p A u)} : dec (∃ A u, @R Tt Vt A u el G ∧ p A u).

    Global Instance exists_phrase_dec G A p : (∀ x, dec (p x)) → dec (∃ u , @R Tt Vt A u el G ∧ p u).

    Global Instance symbol_ter_dec : ∀ s, dec (∃ a, s = @Ts Tt Vt a).

    Global Instance phrase_var_dec u : dec (∃ A, u = [@Vs Tt Vt A]).

    Global Instance phrase_char_dec u : dec (∃ a, u = [@Ts Tt Vt a]).

    Global Instance filter_rule_dec (p : @phrase Tt Vt → Prop) {D : ∀ u, dec (p u)} : ∀ r, (dec ((fun r ⇒ match r with R A u ⇒ p u end) r)).

  End DecidabilityInstances.

End Definitions.