BidiInversion.agda

module BidiInversion where

open import Data.Bool hiding (_≟_ ; if_then_else_)
open import Data.Empty
open import Data.List hiding ([_])
open import Data.Nat hiding (_*_ ; _+_ ; _≟_ ; _>_ ; _<_)
open import Data.Product hiding (<_,_> ; swap ; map) renaming (_,_ to pr)
open import Data.String renaming (_++_ to _++s_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Unit hiding (_≟_)




_>>=_ : forall {A B : Set} -> List A -> (A -> List B) -> List B
[] >>= f = []
(x ∷ xs) >>= f = f x ++ (xs >>= f)


data Type : Set where
  Zero One Two : Type
  _*_ _+_ _=>_ : Type -> Type -> Type
  var : String -> Type
  Forall : String -> Type -> Type


[_/_]ty : Type -> String -> Type -> Type
[ S / a ]ty Zero = Zero
[ S / a ]ty One = One
[ S / a ]ty Two = Two
[ S / a ]ty (T1 * T2) = [ S / a ]ty T1 * [ S / a ]ty T2
[ S / a ]ty (T1 + T2) = [ S / a ]ty T1 + [ S / a ]ty T2
[ S / a ]ty (T1 => T2) = [ S / a ]ty T1 => [ S / a ]ty T2
[ S / a ]ty (var b) with a ≟ b
... | yes _ = S
... | no _ = var b
[ S / a ]ty (Forall b T) with a ≟ b
... | yes _ = Forall b T
... | no _ = Forall b ([ S / a ]ty T)


infix 10 _::_
data HJdg (T : Set) : Set where
  _::_ : String -> T -> HJdg T
  _::* : String -> HJdg T


infixl 9 _,_
data Ctx (T : Set) : Set where
  <> : Ctx T
  _,_ : Ctx T -> HJdg T -> Ctx T


mutual
  data SynTerm : Set where
    var : String -> SynTerm
    isa : ChkTerm -> Type -> SynTerm
  
    -- One
    <> : SynTerm
  
    -- Two
    true false : SynTerm
    
    -- S => T
    _$_ : SynTerm -> ChkTerm -> SynTerm

    -- Forall a T
    inst : SynTerm -> Type -> SynTerm
  
  
  data ChkTerm : Set where
    [_] : SynTerm -> ChkTerm
    
    -- Zero
    abort : SynTerm -> ChkTerm

    -- Two
    if_then_else_ : SynTerm -> ChkTerm -> ChkTerm -> ChkTerm

    -- S * T
    <_,_> : ChkTerm -> ChkTerm -> ChkTerm
    split_as_,_inn_ : SynTerm -> String -> String -> ChkTerm -> ChkTerm
    
    -- S + T
    left right : ChkTerm -> ChkTerm
    case_left_:->_right_:->_ : SynTerm -> String -> ChkTerm -> String -> ChkTerm -> ChkTerm

    -- S => T
    lam : String -> ChkTerm -> ChkTerm

    -- Forall a T
    abs : String -> ChkTerm -> ChkTerm


mutual
  [_/_]synsyn : SynTerm -> String -> SynTerm -> SynTerm
  [ M / x ]synsyn (var y) with x ≟ y
  ... | yes _ = M
  ... | no _ = var y
  [ M / x ]synsyn (isa N T) = isa ([ M / x ]synchk N) T
  [ M / x ]synsyn <> = <>
  [ M / x ]synsyn true = true
  [ M / x ]synsyn false = false
  [ M / x ]synsyn (N1 $ N2) = [ M / x ]synsyn N1 $ [ M / x ]synchk N2
  [ M / x ]synsyn (inst N T) = inst ([ M / x ]synsyn N) T
  
  [_/_]synchk : SynTerm -> String -> ChkTerm -> ChkTerm
  [ M / x ]synchk [ N ] = [ [ M / x ]synsyn N ]
  [ M / x ]synchk (abort N) = abort ([ M / x ]synsyn N)
  [ M / x ]synchk (if N1 then N2 else N3) = if [ M / x ]synsyn N1 then [ M / x ]synchk N2 else [ M / x ]synchk N3
  [ M / x ]synchk < N1 , N2 > = < [ M / x ]synchk N1 , [ M / x ]synchk N2 >
  [ M / x ]synchk (split N1 as y , z inn N2) with x ≟ y | x ≟ z
  ... | no _ | no _ = split [ M / x ]synsyn N1 as y , z inn [ M / x ]synchk N2
  ... | _ | _ = split [ M / x ]synsyn N1 as y , z inn N2
  [ M / x ]synchk (left N) = left ([ M / x ]synchk N)
  [ M / x ]synchk (right N) = right ([ M / x ]synchk N)
  [ M / x ]synchk (case N1 left y :-> N2 right z :-> N3) with x ≟ y | x ≟ z
  ... | yes _ | yes _ = case [ M / x ]synsyn N1 left y :-> N2 right z :-> N3
  ... | yes _ | no _ = case [ M / x ]synsyn N1 left y :-> N2 right z :-> [ M / x ]synchk N3
  ... | no _ | yes _ = case [ M / x ]synsyn N1 left y :-> [ M / x ]synchk N2 right z :-> N3
  ... | no _ | no _ = case [ M / x ]synsyn N1 left y :-> [ M / x ]synchk N2 right z :-> [ M / x ]synchk N3
  [ M / x ]synchk (lam y N) with x ≟ y
  ... | yes _ = lam y N
  ... | no _ = lam y ([ M / x ]synchk N)
  [ M / x ]synchk (abs a N) with x ≟ a
  ... | yes _ = abs a N
  ... | no _ = abs a ([ M / x ]synchk N)


infix 10 _>_ _<_
data Jdg (T : Set) : Set where
  _>_ : T -> ChkTerm -> Jdg T
  _<_ : SynTerm -> T -> Jdg T



data Var {Ty : Set} : Ctx Ty -> HJdg Ty -> Set where
  top : forall {G x T} -> Var (G , x :: T) (x :: T)
  pop-term : forall {G J x T} -> Var G J -> Var (G , x :: T) J
  pop-type : forall {G J a} -> Var G J -> Var (G , a ::*) J



Fresh : {Ty : Set} -> Ctx Ty -> String -> Set
Fresh <> x = ⊤
Fresh (G , y :: _) x with x ≟ y
... | yes _ = ⊥
... | no _ = Fresh G x
Fresh (G , y ::*) x with x ≟ y
... | yes _ = ⊥
... | no _ = Fresh G x


infix 8 _!-_
data _!-_ (G : Ctx Type) : Jdg Type -> Set where


  -- [ G !- M < T ]

  hyp : forall {x T} ->    Var G (x :: T)
                           --------------
                     ->    G !- var x < T
  
  isa : forall {M T} ->   G !- T > M
                          ----------------
                     ->   G !- isa M T < T
  
  one-intro : G !- <> < One
  
  two-intro-1 : G !- true < Two
  
  two-intro-2 : G !- false < Two

  pair-intro : forall {M S N T} ->   G !- S > M   ->    G !- T > N
                                     -----------------------------
                                ->   G !- S * T > < M , N >

  pair-elim : forall {M R S x y N T} ->   G !- M < R * S   ->   G , x :: R , y :: S !- T > N
                                          --------------------------------------------------
                                     ->   G !- T > split M as x , y inn N
  
  fun-elim : forall {M N S T} ->   G !- M < S => T   ->   G !- S > N
                                   ---------------------------------
                              ->   G !- M $ N < T

  -- [ G !- T > M ]
  
  dirchange : forall {M T} ->   G !- M < T
                                --------------
                           ->   G !- T > [ M ]
  
  zero-elim : forall {M T} ->   G !- M < Zero
                                ----------------
                           ->   G !- T > abort M

  two-elim : forall {M N P T} ->   G !- M < Two   ->   G !- T > N   ->   G !- T > P
                                   ------------------------------------------------
                              ->   G !- T > if M then N else P
  
  sum-intro-1 : forall {M S T} ->   G !- S > M
                                    -------------------
                               ->   G !- S + T > left M
  
  sum-intro-2 : forall {N S T} ->   G !- T > N
                                    --------------------
                               ->   G !- S + T > right N
  
  sum-elim : forall {M x N y P R S T} ->   {_ : Fresh G x}   ->   {_ : Fresh G y}   ->   G !- M < R + S   ->   G , x :: R !- T > N   ->   G , y :: S !- T > P
                                           ------------------------------------------------------------------------------------------------------------------
                                      ->   G !- T > case M left x :-> N right y :-> P
  
  fun-intro : forall {x M S T} ->   {_ : Fresh G x}   ->   G , x :: S !- T > M
                                    ------------------------------------------
                               ->   G !- S => T > lam x M
  
  forall-intro : forall {a M T} ->   {_ : Fresh G a}   ->   G , a ::* !- T > M
                                     -----------------------------------------
                                ->   G !- Forall a T > abs a M

  forall-elim : forall {a M T} ->   G !- M < Forall a T   ->   (S : Type)
                                    -------------------------------------
                               ->   G !- inst M S < [ S / a ]ty T

infix 8 _==>_

data _==>_ : Ctx Type -> Jdg Type -> Set where

  id : forall {G x T} ->   Var G (x :: T)
                           ---------------
                      ->   G ==> var x < T

  dirchange : forall {G M T} ->   G ==> M < T
                                 ---------------
                            ->   G ==> T > [ M ]
  
  isa : forall {G M T} ->   G ==> T > M
                            -----------------
                       ->   G ==> isa M T < T

  zero-L : forall {G x T} ->   Var G (x :: Zero)
                               -----------------------
                          ->   G ==> T > abort (var x)

  one-R : forall {G} ->   G ==> <> < One

  two-R-1 : forall {G} ->   G ==> true < Two

  two-R-2 : forall {G} ->   G ==> false < Two

  two-L : forall {G x M N T} ->   Var G (x :: Two)   ->   G ==> T > M   ->   G ==> T > N
                                  ------------------------------------------------------
                             ->   G ==> T > if var x then M else N

  pair-R : forall {G M S N T} ->   G ==> S > M   ->   G ==> T > N
                                   ------------------------------
                              ->   G ==> S * T > < M , N >
  
  pair-L : forall {G p R S x y M T} ->   Var G (p :: R * S)   ->   {fr : Fresh G x}   ->   {fr' : Fresh G y}   ->   G , x :: R , y :: S ==> T > M
                                         --------------------------------------------------------------------------------------------------------
                                    ->   G ==> T > split var p as x , y inn M
  
  sum-R-1 : forall {G M S T} ->   G ==> S > M
                                  --------------------
                             ->   G ==> S + T > left M

  sum-R-2 : forall {G N S T} ->   G ==> T > N
                                  ---------------------
                             ->   G ==> S + T > right N

  sum-L : forall {G x y z R S M N T} ->   Var G (x :: R + S)   ->   {fr : Fresh G y}   ->   {fr' : Fresh G z}   ->   G , y :: R ==> T > M   ->   G , z :: S ==> T > N
                                          ---------------------------------------------------------------------------------------------------------------------------
                                     ->   G ==> T > case var x left y :-> M right z :-> N

  fun-R : forall {G x M S T} ->   {fr : Fresh G x}   ->   G , x :: S ==> T > M
                                  --------------------------------------------
                             ->   G ==> S => T > lam x M

  fun-L : forall {G f S T M} ->   Var G (f :: S => T)   ->   G ==> S > M
                                  --------------------------------------
                             ->   G ==> var f $ M < T

  tyinit : forall {G x a} ->   G , x :: var a ==> var x < var a
  
  forall-R : forall {G a M T} ->   {_ : Fresh G a}   ->   G , a ::* ==> T > M
                                   ------------------------------------------
                              ->   G ==> Forall a T > abs a M

  forall-L : forall {G f a M T} ->   Var G (f :: Forall a T)   ->   (S : Type)
                                     -----------------------------------------
                                ->   G ==> inst M S < [ S / a ]ty T
  
  cut : forall {G } M {S} x N {T} ->   G ==> M < S   ->   G , x :: S ==> N < T
                                       ---------------------------------------
                                  ->   G ==> [ M / x ]synsyn N < T

swap : forall {S T : Type} ->   <> ==> (S + T) => (T + S) > lam "d" (case var "d" left "x" :-> right [ var "x" ] right "y" :-> left [ var "y" ])
swap = fun-R (sum-L top (sum-R-2 (dirchange (id top))) (sum-R-1 (dirchange (id top))))

idd : forall {S : Type} ->   <> ==> S => S > lam "x" [ var "x" ]
idd = fun-R (dirchange (id top))

idapp : forall {S : Type} ->   <> , "x" :: S ==> S > [ isa (lam "y" [ var "y" ]) (S => S) $ [ var "x" ] ]
idapp {S} = dirchange (cut (isa (lam "y" [ var "y" ]) (S => S)) "f" (var "f" $ [ var "x" ]) (isa (fun-R (dirchange (id top)))) (fun-L top (dirchange (id (pop-term top)))))




data RightSearchableType : Set where
  Zero : RightSearchableType
  _+_ : Type -> Type -> RightSearchableType
  var : String -> RightSearchableType
  
data LeftSearchableType : Set where
  _=>_ : Type -> Type -> LeftSearchableType
  var : String -> LeftSearchableType
  Forall : String -> Type -> LeftSearchableType
    
_\\_ : forall {T} -> Ctx T -> String -> Ctx T
<> \\ x = <>
(G , y :: T) \\ x with x ≟ y
... | yes _ = G \\ x
... | no _ = (G \\ x) , y :: T
(G , y ::*) \\ x with x ≟ y
... | yes _ = G \\ x
... | no _ = (G \\ x) , y ::*

infix 8 _,_==R=>_ _,_==L=>_

mutual
  data _,_==R=>_ : Ctx LeftSearchableType -> Ctx Type -> Jdg Type -> Set where

    dirchange : forall {G O M T} ->   G , O ==R=> M < T
                                      ---------------------
                                 ->   G , O ==R=> T > [ M ]

    isa : forall {G O M T} ->   G , O ==R=> T > M
                                -----------------------
                           ->   G , O ==R=> isa M T < T
    
    one-R : forall {G O} ->   G , O ==R=> <> < One
  
    two-R-1 : forall {G O} ->   G , O ==R=> true < Two
  
    two-R-2 : forall {G O} ->   G , O ==R=> false < Two
  
    pair-R : forall {G O M S N T} ->   G , O ==R=> S > M   ->   G , O  ==R=> T > N
                                       -------------------------------------------
                                  ->   G , O ==R=> S * T > < M , N >

    fun-R : forall {G O M S T} x ->   {fr : Fresh G x}   ->   G , (O , x :: S) ==R=> T > M
                                      ----------------------------------------------------
                                 ->   G , O ==R=> S => T > lam x M

    forall-R : forall {G O M T} a ->   {fr : Fresh G a}   ->   (G , a ::*) , O ==R=> T > M
                                       ---------------------------------------------------
                                  ->   G , O ==R=> Forall a T > abs a M

    init : forall {G O x a} ->   Var G (x :: var a)
                                 -------------------------
                            ->   G , O ==R=> var x < var a

    LR-P-syn : forall {G O M a} ->   ¬ (Σ String \ x -> Var G (x :: var a))   ->   G , O ==L=> M < var a
                                     -------------------------------------------------------------------
                                ->   G , O ==R=> M < var a

    LR-P-chk : forall {G O M a} ->   ¬ (Σ String \ x -> Var G (x :: var a))   ->   G , O ==L=> var a > M
                                     -------------------------------------------------------------------
                                ->   G , O ==R=> var a > M
    
    LR-zero-chk : forall {G O M} ->   G , O ==L=> Zero > M
                                      --------------------
                                 ->   G , O ==R=> Zero > M
    
    LR-zero-syn : forall {G O M} ->   G , O ==L=> M < Zero
                                      --------------------
                                 ->   G , O ==R=> M < Zero

    LR-sum-chk : forall {G O M S T} ->   G , O ==L=> S + T > M
                                         ---------------------
                                    ->   G , O ==R=> S + T > M

    LR-sum-syn : forall {G O M S T} ->   G , O ==L=> M < S + T
                                         ---------------------
                                    ->   G , O ==R=> M < S + T

  data _,_==L=>_ : Ctx LeftSearchableType -> Ctx Type -> Jdg RightSearchableType -> Set where
    
    zero-L : forall {G x O T} ->   G , (O , x :: Zero) ==L=> T > abort (var x)

    one-L : forall {G O x J} ->   G , O ==L=> J
                                  --------------------------
                             ->   G , (O , x :: One) ==L=> J

    two-L : forall {G O x M N T} ->   G , O ==L=> T > M   ->   G , O ==L=> T > N
                                      ------------------------------------------------------
                                 ->   G , (O , x :: Two) ==L=> T > if var x then M else N
    
    pair-L : forall {G O p x y R S M T} ->   G , (O , x :: R , y :: S) ==L=> T > M
                                             ---------------------------------------------------------
                                        ->   G , (O , p :: R * S) ==L=> T > split var p as x , y inn M

    sum-L : forall {G O x R S y M z N T} ->   G , (O , y :: R) ==L=> T > M   ->   G , (O , z :: S) ==L=> T > N
                                              --------------------------------------------------------------------
                                         ->   G , (O , x :: R + S) ==L=> T > case var x left y :-> M right z :-> N

    init-syn : forall {G O x a} ->   G , (O , x :: var a) ==L=> var x < var a
     
    init-chk : forall {G O x a} ->   G , (O , x :: var a) ==L=> var a > [ var x ]

    P-shift-syn : forall {G O x a M T} ->   {- ¬ var a ≡ T   -> -}  (G , x :: var a) , O ==L=> M < T
                                            ---------------------------------------------------
                                       ->   G , (O , x :: var a) ==L=> M < T

    P-shift-chk : forall {G O x a M T} ->   {- ¬ var a ≡ T   ->  -} (G , x :: var a) , O ==L=> T > M
                                            ---------------------------------------------------
                                       ->   G , (O , x :: var a) ==L=> T > M
    
    fun-shift : forall {G O x R S J} ->   (G , x :: R => S) , O ==L=> J
                                          -----------------------------
                                     ->   G , (O , x :: R => S) ==L=> J

    tyvar-shift : forall {G O a J} ->    (G , a ::*) , O ==L=> J
                                         -----------------------
                                   ->    G , (O , a ::*) ==L=> J

    forall-shift : forall {G O f a T J} ->   (G , f :: Forall a T) , O ==L=> J
                                             ---------------------------------
                                        ->   G , (O , f :: Forall a T) ==L=> J
    
    sum-R-1 : forall {G M S T} ->   G , <> ==R=> S > M
                                    ---------------------------
                               ->   G , <> ==L=> S + T > left M

    sum-R-2 : forall {G N S T} ->   G , <> ==R=> T > N
                                    ----------------------------
                               ->   G , <> ==L=> S + T > right N

    fun-L : forall {G S T M J} f x ->   Var G (f :: S => T)   ->   G , <> ==R=> S > M   ->   (G \\ f) , (<> , x :: T) ==L=> J
                                        -------------------------------------------------------------------------------------
                                   ->   G , <> ==L=> J

    forall-L : forall {G T x J} f a ->   Var G (f :: Forall a T)   ->   (S : Type)   ->   (G \\ f) , (<> , x :: [ S / a ]ty T) ==L=> J
                                         ---------------------------------------------------------------------------------------------
                                    ->   G , <> ==L=> J





data List1 (A : Set) : Set where
  singleton : A -> List1 A
  _∷_ : A -> List1 A -> List1 A

map1 : {A B : Set} -> (A -> B) -> List1 A -> List1 B
map1 f (singleton x) = singleton (f x)
map1 f (x ∷ xs) = f x ∷ map1 f xs

list1ToList : {A : Set} -> List1 A -> List A
list1ToList (singleton x) = x ∷ []
list1ToList (x ∷ xs) = x ∷ list1ToList xs

data Dec* (A : Set) : Set where
  yes : List1 A -> Dec* A
  no : ¬ A -> Dec* A


findVar : (G : Ctx LeftSearchableType) (a : String) -> Dec* (Σ String \ x -> Var G (x :: var a))
findVar <> a = no (\ { (pr x ()) })
findVar (G , x :: (S => T)) a with findVar G a
findVar (G , x :: (S => T)) a | yes ps = yes (map1 (\ { (pr y v) -> pr y (pop-term v) }) ps)
findVar (G , x :: (S => T)) a | no ¬p = no (\ { (pr y (pop-term v)) → ¬p (pr y v) })
findVar (G , x :: var b) a with a ≟ b
findVar (G , x :: var .a) a | yes refl with findVar G a
... | yes ps = yes (map1 (\ { (pr x v) -> pr x (pop-term v) }) ps)
... | no _ = yes (singleton (pr x top))
findVar (G , x :: var b) a | no ¬p with findVar G a
findVar (G , x :: var b) a | no ¬eq | yes ps = yes (map1 (\ { (pr y v) -> pr y (pop-term v) }) ps)
findVar (G , x :: var b) a | no ¬eq | no ¬p = no (helper G x a b ¬eq ¬p)
  where
    helper : forall (G : Ctx LeftSearchableType) x (a b : String) -> ¬ a ≡ b → ¬ (Σ String \ y -> Var G (y :: var a)) → ¬ (Σ String \ y -> Var (G , x :: var b) (y :: var a))
    helper G y a .a ¬eq ¬v (pr .y top) = ¬eq refl
    helper G x a b ¬eq ¬v (pr y (pop-term v)) = ¬v (pr y v)
findVar (G , x :: Forall b T) a with findVar G a
findVar (G , x :: Forall b T) a | yes ps = yes (map1 (\ { (pr y v) -> pr y (pop-term v) }) ps)
findVar (G , x :: Forall b T) a | no ¬p = no (\ { (pr y (pop-term v)) → ¬p (pr y v) })
findVar (G , (b ::*)) a with findVar G a
findVar (G , (b ::*)) a | yes ps = yes (map1 (\ { (pr x p) -> pr x (pop-type p) }) ps)
findVar (G , (b ::*)) a | no ¬p = no (\ { (pr x (pop-type p)) → ¬p (pr x p) })


findFunctions : (G : Ctx LeftSearchableType) -> List (Σ String \ f -> Σ Type \ S -> Σ Type \ T -> Var G (f :: S => T))
findFunctions <> = []
findFunctions (G , f :: S => T) = pr f (pr S (pr T top)) ∷ map (\ { (pr f' (pr S' (pr T' v))) → pr f' (pr S' (pr T' (pop-term v))) }) (findFunctions G)
findFunctions (G , f :: var a) = map (λ { (pr f (pr S (pr T v))) → pr f (pr S (pr T (pop-term v))) }) (findFunctions G)
findFunctions (G , f :: Forall a T) = map (λ { (pr f (pr S (pr T v))) → pr f (pr S (pr T (pop-term v))) }) (findFunctions G)
findFunctions (G , _ ::*) = map (λ { (pr f (pr S (pr T v))) → pr f (pr S (pr T (pop-type v))) }) (findFunctions G)


nameForType : Type -> String
nameForType Zero = "x"
nameForType One = "x"
nameForType Two = "b"
nameForType (_ * _) = "p"
nameForType (_ + _) = "d"
nameForType (_ => _) = "d"
nameForType (var _) = "x"
nameForType (Forall _ _) = "f"

{-# TERMINATING #-}
addPrimesAsNecessary : List String -> String -> String
addPrimesAsNecessary vs x with any (\v -> x == v) vs
addPrimesAsNecessary vs x | false = x
addPrimesAsNecessary vs x | true = addPrimesAsNecessary vs (x ++s "'")

freshVar : forall {A B} -> Ctx A -> Ctx B -> Type -> String
freshVar G O T = addPrimesAsNecessary (extractNames G ++ extractNames O) (nameForType T)
  where
    extractNames : forall {C} -> Ctx C -> List String
    extractNames <> = []
    extractNames (c , x :: _) = x ∷ extractNames c
    extractNames (c , x ::*) = x ∷ extractNames c
    

postulate freshIsFresh : forall {A B} (G : Ctx A) (O : Ctx B) (T : Type) -> Fresh G (freshVar G O T)
          freshTrustMe : forall {A} (G : Ctx A) x -> Fresh G x



mutual
  invertR-chk : ℕ -> (G : Ctx LeftSearchableType) (O : Ctx Type) (T : Type) -> List (Σ ChkTerm \ M -> G , O ==R=> T > M)
  invertR-chk 0 _ _ _ = []
  invertR-chk (suc n) G O Zero = invertL-chk n G O Zero >>= \ { (pr M p) ->
                                   pr M (LR-zero-chk p) ∷ []
                                 }
  invertR-chk (suc n) G O One = pr [ <> ] (dirchange one-R) ∷ []
  invertR-chk (suc n) G O Two = pr [ true ] (dirchange two-R-1) ∷ pr [ false ] (dirchange two-R-2) ∷ []
  invertR-chk (suc n) G O (S * T) = ms >>= \ { (pr M p) ->
                                    ns >>= \ { (pr N q) ->
                                      pr (< M , N >) (pair-R p q) ∷ []
                                    } }
    where ms = invertR-chk n G O S
          ns = invertR-chk n G O T
  invertR-chk (suc n) G O (S + T) = invertL-chk n G O (S + T) >>= \ { (pr M p) ->
                                      pr M (LR-sum-chk p) ∷ []
                                    }
  invertR-chk (suc n) G O (S => T) = invertR-chk n G (O , x :: S) T >>= \ { (pr M p) ->
                                       pr (lam x M) (fun-R x {fr = freshIsFresh G O S} p) ∷ []
                                     }
    where x = freshVar G O S
  invertR-chk (suc n) G O (var a) with findVar G a
  ... | yes ps = map (\ { (pr x v) -> pr [ var x ] (dirchange (init v)) }) (list1ToList ps)
  ... | no ¬v = invertL-chk n G O (var a) >>= \ { (pr M p) -> pr M (LR-P-chk ¬v p) ∷ [] }
  invertR-chk (suc n) G O (Forall a T) = invertR-chk n (G , a ::*) O T >>= \ { (pr M p) -> pr (abs a M) (forall-R a {fr = freshTrustMe G a} p) ∷ [] }

  invertL-chk : ℕ → (G : Ctx LeftSearchableType) (O : Ctx Type) (T : RightSearchableType) -> List (Σ ChkTerm \ M -> G , O ==L=> T > M)
  invertL-chk 0 _ _ _ = []
  invertL-chk (suc n) G <> Zero = findFunctions G >>= \ { (pr f (pr S (pr T v))) ->
                                  invertR-chk n G <> S >>= \ { (pr M p) ->
                                  invertL-chk n (G \\ f) (<> , freshVar {B = Type} (G \\ f) <> S :: T) Zero >>= \ { (pr N q) ->
                                    pr N (fun-L f (freshVar {B = Type} (G \\ f) <> S) v p q) ∷ []
                                  } } }
  invertL-chk (suc n) G <> (S + T) = (invertR-chk n G <> S >>= \ { (pr M p) -> pr (left M) (sum-R-1 p) ∷ [] }) ++
                                     (invertR-chk n G <> T >>= \ { (pr N q) -> pr (right N) (sum-R-2 q) ∷ [] })
  invertL-chk (suc n) G <> (var a) = []
  invertL-chk (suc n) G (O , x :: Zero) T = pr (abort (var x)) zero-L ∷ []
  invertL-chk (suc n) G (O , x :: One) T = invertL-chk n G O T >>= \ { (pr M p) -> pr M (one-L p) ∷ [] }
  invertL-chk (suc n) G (O , x :: Two) T = ts >>= \ { (pr M p) ->
                                           ts >>= \ { (pr N q) ->
                                             pr (if var x then M else N) (two-L p q) ∷ []
                                           } }
    where ts = invertL-chk n G O T
  invertL-chk (suc n) G (O , x :: (R * S)) T = invertL-chk n G (O , freshVar G (O , x :: R * S) R :: R , freshVar G ((O , x :: R * S) , freshVar G (O , x :: R * S) R :: R) S :: S) T >>= \ { (pr M p) ->
                                                 pr (split var x as freshVar G (O , x :: R * S) R , freshVar G ((O , x :: R * S) , freshVar G (O , x :: R * S) R :: R) S inn M) (pair-L p) ∷ []
                                               }
  invertL-chk (suc n) G (O , x :: (R + S)) T = ls >>= \ { (pr M p) ->
                                               rs >>= \ { (pr N q) ->
                                                 pr (case var x left (freshVar G O R) :-> M right (freshVar G O S) :-> N) (sum-L p q) ∷ []
                                               } }
    where ls = invertL-chk n G (O , freshVar G O R :: R) T
          rs = invertL-chk n G (O , freshVar G O S :: S) T
  invertL-chk (suc n) G (O , x :: (R => S)) T = invertL-chk n (G , x :: R => S) O T >>= \ { (pr M p) -> pr M (fun-shift p) ∷ [] }
  invertL-chk (suc n) G (O , x :: var a) Zero = invertL-chk n (G , x :: var a) O Zero >>= \ { (pr M p) -> pr M (P-shift-chk {-(λ ())-} p) ∷ [] }
  invertL-chk (suc n) G (O , x :: var a) (S + T) = invertL-chk n (G , x :: var a) O (S + T) >>= \ { (pr M p) -> pr M (P-shift-chk {-(λ ())-} p) ∷ [] }
  invertL-chk (suc n) G (O , x :: var a) (var b) with a ≟ b
  invertL-chk (suc n) G (O , x :: var a) (var .a) | yes refl = pr [ var x ] init-chk ∷ invertL-chk n (G , x :: var a) O (var a) >>= \ { (pr M p) -> pr M (P-shift-chk {-(uncong-var a b ¬eq)-} p) ∷ [] }
  ... | no ¬eq = invertL-chk n (G , x :: var a) O (var b) >>= \ { (pr M p) -> pr M (P-shift-chk {-(uncong-var a b ¬eq)-} p) ∷ [] }
    where
      uncong-var : (a b : String) -> ¬ (a ≡ b) → ¬ (_≡_ {A = RightSearchableType} (var a) (var b))
      uncong-var a .a f refl = f refl
  invertL-chk (suc n) G (O , a ::*) T = invertL-chk n (G , a ::*) O T >>= \ { (pr M p) -> pr M (tyvar-shift p) ∷ [] }
  invertL-chk (suc n) G (O , f :: Forall a S) T = invertL-chk n (G , f :: Forall a S) O T >>= (\ { (pr M p) -> pr M (forall-shift p) ∷ [] })





-- id : forall a. a -> a
-- id = /\a b -> \x -> x
ids : List (Σ ChkTerm \ M -> <> , <> ==R=> _ > M)
ids = invertR-chk 4 <> <> (Forall "a" (var "a" => var "a"))

-- swap : forall a b. a * b -> b * a
-- swap = /\a b -> \p -> (split p as (x,y) in y, split p as (x,y) in x)
swaps : List (Σ ChkTerm \ M -> <> , <> ==R=> _ > M)
swaps = invertR-chk 8 <> <> (Forall "a" (Forall "b" ((var "a" * var "b") => (var "b" * var "a"))))

-- flip : forall a b. a + b -> b + a
-- flip = /\a b -> \d -> case d of left x -> right x ; right y -> left y
flips : List (Σ ChkTerm \ M -> <> , <> ==R=> _ > M)
flips = invertR-chk 8 <> <> (Forall "a" (Forall "b" ((var "a" + var "b") => (var "b" + var "a"))))

-- assoc : forall a b c. a * (b * c) -> (a * b) * c
-- assoc = /\a b c. \t -> ( ( split t as (x,p) in split p as (y,z) in x
--                          , split t as (x,p) in split p as (y,z) in y
--                          )
--                        , split t as (x,p) in split p as (y,z) in z
--                        )
assocs : List (Σ ChkTerm \ M -> <> , <> ==R=> _ > M)
assocs = invertR-chk 12 <> <> (Forall "a" (Forall "b" (Forall "c" ((var "a" * (var "b" * var "c")) => ((var "a" * var "b") * var "c")))))

-- distr : forall a b c. a * (b + c) -> (a * b) + (a * c)
-- distr = /\a b c. \p -> split p as (x,d) in case d of left y -> left (x,y) ; right z -> right (x,z)
distrs : List (Σ ChkTerm \ M -> <> , <> ==R=> _ > M)
distrs = invertR-chk 12 <> <> (Forall "a" (Forall "b" (Forall "c" ((var "a" * (var "b" + var "c")) => ((var "a" * var "b") + (var "a" * var "c"))))))