From Tealeaves.Examples Require Import Lambda.Confluence.
From Tealeaves.Backends Require Import LN DB.
From Tealeaves.Backends.Adapters Require Import LNtoDB DBtoLN Roundtrips.LNDB.

Import List.ListNotations.

Check LNtokey: lam LN -> key.
LNtokey : lam LN -> key
     : lam LN -> key
Check toLN: key -> lam nat -> option (lam LN).
toLN : key -> lam nat -> option (lam LN)
     : key -> lam nat -> option (lam LN)
Check toDB: key -> lam LN  -> option (lam nat).
toDB : key -> lam LN -> option (lam nat)
     : key -> lam LN -> option (lam nat)

Definition x: atom := 0.
Definition y: atom := 1.
Definition z: atom := 2.
Definition a: atom := 3.
Definition b: atom := 4.

Module de_bruijn.

  Example term1: lam nat := tvar 0.
  Example term2: lam nat := app (tvar 0) (tvar 1).
  Example term3: lam nat := abs (app (tvar 0) (tvar 1)).
  Example term4: lam nat := app (abs (app (tvar 1) (tvar 0))) (app (tvar 1) (tvar 0)).
  (* ^ term4 = example from JAR paper *)

  Example k: key := [x ; y].

  Compute toLN [] term1. (* None *)
= None
: option (lam LN)
  Compute toLN k term1. (* Some (tvar (Fr 0)) *)
= Some (tvar (Fr 0))
: option (lam LN)
  Compute map (toDB k) (toLN k term1).
= Some (Some (tvar 0))
: option (option (lam nat))

  Compute toLN k term2.
= Some (app (tvar (Fr 0)) (tvar (Fr 1)))
: option (lam LN)
  Compute map (toDB k) (toLN k term1).
= Some (Some (tvar 0))
: option (option (lam nat))

  Compute toLN k term3.
= Some (abs (app (tvar (Bd 0)) (tvar (Fr 0))))
: option (lam LN)
  Compute map (toDB k) (toLN k term3).
= Some (Some (abs (app (tvar 0) (tvar 1))))
: option (option (lam nat))

  Compute toLN k term4.
= Some
    (app (abs (app (tvar (Fr 0)) (tvar (Bd 0))))
       (app (tvar (Fr 1)) (tvar (Fr 0))))
: option (lam LN)
  Compute map (toDB k) (toLN k term4).
= Some
    (Some
       (app (abs (app (tvar 1) (tvar 0)))
          (app (tvar 1) (tvar 0))))
: option (option (lam nat))

End de_bruijn.

Module locally_nameless.

  Example term1: lam LN := app (tvar (Bd 0)) (tvar (Fr x)).
  Example term2: lam LN := abs (app (tvar (Bd 0)) (tvar (Fr x))).
  Example term3: lam LN := abs (app (tvar (Fr z)) (tvar (Fr x))).
  Example term4: lam LN :=
    abs (app
           (abs (abs (app
                        (tvar (Fr z))
                        (tvar (Fr x)))))
           (app
              (tvar (Fr y))
              (tvar (Fr a)))).

  Import List.ListNotations.

  Example k: key := [b; z; a; y; x].

  Compute toDB k term1.
= None
: option (lam nat)
  Compute map (toLN k) (toDB k term1).
= None
: option (option (lam LN))

  Compute toDB k term2.
= Some (abs (app (tvar 0) (tvar 5)))
: option (lam nat)
  Compute map (toLN k) (toDB k term2).
= Some
    (Some (abs (app (tvar (Bd 0)) (tvar (Fr 0)))))
: option (option (lam LN))

  Compute toDB k term3.
= Some (abs (app (tvar 2) (tvar 5)))
: option (lam nat)
  Compute map (toLN k) (toDB k term3).
= Some
    (Some (abs (app (tvar (Fr 2)) (tvar (Fr 0)))))
: option (option (lam LN))

  Compute toDB k term4.
= Some
    (abs
       (app (abs (abs (app (tvar 4) (tvar 7))))
          (app (tvar 4) (tvar 3))))
: option (lam nat)
  Compute map (toLN k) (toDB k term4).
= Some
    (Some
       (abs
          (app
             (abs
                (abs
                   (app (tvar (Fr 2))
                      (tvar (Fr 0)))))
             (app (tvar (Fr 1)) (tvar (Fr 3))))))
: option (option (lam LN))

  Goal map (toLN k) (toDB k term4) = Some (Some term4).
map (toLN k) (toDB k term4) = Some (Some term4)
    reflexivity.
  Qed.

End locally_nameless.