(** Utilisation des GADT pour typer fortement des mots,
  * parler de reconnaissance par un automate et d'inclusions
  * de langages reconnus par des automates. *)

(** Mots sur {a,b}, reflétés dans leur type. *)

type 'w a = TA of 'w
type 'w b = TB of 'w
type nil = TEmpty

type ab = nil b a
type aab = nil b a a

type _ word =
  | A : 'w word -> 'w a word
  | B : 'w word -> 'w b word
  | Empty : nil word

let aba = A (B (A Empty))
let ab : ab word = A (B Empty)
let aab : aab word = A ab

(** Un exemple d'automate:
  *
  * n -a-> m -a-> f
  *        m -b-> f
  * (f acceptant)
  *
  * h -(epsilon)-> e -b-> f
  *                e -a-> o
  * h -(epsilon)-> o -a-> e
  *
  * On s'intéressera à montrer que (le langage de) n est inclus
  * dans (celui de) m, puis que m est inclus dans h.
  *
  *)

(** Types pour representer les runs. *)

type 'w n = TN of 'w
type 'w m = TM of 'w
type 'w f = TF of 'w
type 'w h = TH of 'w
type 'w e = TE of 'w
type 'w o = TO of 'w

type nmf = nil f m n
type nmmf = nil f m m n

(** Le type ('w,'r) acc exprime que le run r accepte le mot w.
  * Ses habitants sont des "preuves" de cet énoncé. *)
type ('w,'r) acc =
  | NM : ('w,'r m) acc -> ('w a, 'r m n) acc
  | MM : ('w,'r m) acc -> ('w a, 'r m m) acc
  | MF : ('w,'r f) acc -> ('w b, 'r f m) acc
  | F  : (nil, nil f) acc
  | HE : ('w,'r e) acc -> ('w, 'r e h) acc
  | HO : ('w,'r o) acc -> ('w, 'r o h) acc
  | EO : ('w,'r o) acc -> ('w a, 'r o e) acc
  | OE : ('w,'r e) acc -> ('w a, 'r e o) acc
  | EF : ('w,'r f) acc -> ('w b, 'r f e) acc

(** Quelques exemples *)

let n_acc_ab : (ab,nmf) acc = NM (MF F)
let n_acc_aab : (aab,nmmf) acc = NM (MM (MF F))

(** Fonction qui "prouve" que n est inclus dans m. *)

type ('w) in_m = InM : ('w,'r m) acc -> 'w in_m
type ('w) in_n = InN : ('w,'r n) acc -> 'w in_n

let n_in_m : type w. w in_n -> w in_m = function
  | InN (NM a) -> InM (MM a)

(** Idem pour m et h.
  * Cela nécessite d'introduire un type auxiliaire un
  * peu plus complexe, ainsi qu'une fonction auxiliaire,
  * exprimant que m est contenu dans l'union de e et o. *)

type ('w) in_h = InH : ('w,'r h) acc -> 'w in_h
type ('w) in_e_or_o =
  | InE : ('w,'r e) acc -> 'w in_e_or_o
  | InO : ('w,'r o) acc -> 'w in_e_or_o

let rec m_in_h : type w. w in_m -> w in_h = fun x ->
  match m_in_e_or_o x with
    | InE a -> InH (HE a)
    | InO a -> InH (HO a)
and m_in_e_or_o : type w. w in_m -> w in_e_or_o = function
  | InM (MF a) -> InE (EF a)
  | InM (MM a) ->
      match m_in_e_or_o (InM a) with
        | InE a -> InO (OE a)
        | InO a -> InE (EO a)