{-# LANGUAGE RecordWildCards, DisambiguateRecordFields #-}
import Prelude hiding (abs)
import DerivationTrees
import DerivationTrees.Basics
import DerivationTrees.CPTS


translateE :: [Binding] -> [Binding]
translateE = concatMap translateB

translateJ (Jug v t e) = Jug (translate v) (translate t $$ Many v) (translateE e)

translateB :: Binding -> [Binding]
translateB (V x :- a) = [(V ("\\subR " ++ x) :- (translate a $$ Many (var x))), Mult (V x :- a)]
translateB (Base (x)) = [Base ("\\trans " ++ x)]

translate :: Term -> Term
translate (Var x) = Var ("\\subR " ++ x) 
translate (Con x) = Con ("\\trans " ++ x) 
translate (Sor s) = (lam (Mult (V "A" :- Sor s)) ((Many $ var "A") --> Sor ('~':s)))

translate (App k f a) = App (k++"_m") (App (k++"_i") (translate f) (Many a)) (translate a)
translate (Lam k a b) = Lam (k++"_i") w $
                        Lam (k++"_m") w' $
                        translate b        
   where [w',w] = translateB a
translate (Sub t (V x :- a)) = Sub (Sub (translate t) w) w'
    where w  = Mult (V x :- a)
          w' = V ("\\subR " ++ x) :- translate a
translate t@(Pi k a@(V x :- _) b) 
   = lam (Mult (V "f" :- t)) $
     Pi (k++"_i") w $
     Pi (k++"_m") w' $
     (translate b $$ Many (App k (var "f") (var x)))
   where [w',w] = translateB a




pr0 = Pr ""

axiomJ = translateJ (Jug (Sor "s") (Sor "t") [])
       where a = V "A"
             a' = Many $ var "A"


axiomT = Co "~u" (Many (Sor "s") --> Sor "~t")
          (Ab "~u" 
              (pr0 ("s","~t")
                  (St "t" Ax)
                  (wk "t" Ax Ax))
              
              (pr0 ("t","~u")
                  Ax
                  Ax))          
          (delay CenterA 4 $ Ap (Mult (Unbound :- Sor "t")) 
              (Ab "~v" 
                  (pr0 ("t","~u")
                      (St "u" Ax)
                      (wk "u" Ax Ax))
                  (pr0 ("u","~v") Ax Ax))
                    
              Ax)

ind' = halt "ind'"
ind = halt "ind"
lem = halt "lem"
gamma = [Base "\\Gamma"]

startJ = translateJ $ Jug (Var "x") (Con "A") [V "x" :- Con "A" ,Base ("\\Gamma")]
startT = St "~s" (Ap (Mult (Unbound :- Con "A"))
                     (wk "s~" ind' lem)
                     (St "s" lem))

weakJ = translateJ $ Jug (Con "A") (Con "B") [V "x" :- Con "C" ,Base ("\\Gamma")]
weakT = wk "~s" 
           (wk "s" 
               ind
               lem)
           (Ap (Mult (Unbound :- Con "C"))
               (wk "s" ind' lem) 
               (St "s" lem))

protoPi = (Pi "k" (V "x" :- Con "A") (Con "B"))
protoLam = (Lam "k" (V "x" :- Con "A") (Con "b"))

prodJ = translateJ $ Jug protoPi (Sor "s_3") gamma
prodT = Co "~t_3" (Many protoPi --> Sor "~s_3") 
          (dL $ 
           Ab "~t_3"
             (dL $ Pr "k_i" ("s_1","~s_3") 
                 (wk "s_3" lem lem)
                 (dR $ Pr "k_m" ("~s_1","~s_2") 
                      (detach "1" 31 $ Ap (Mult (Unbound :- Con "A")) 
                          (dL $ wk "s_1" 
                              (wk "s_3"
                                 ind'
                                 lem)
                              lem)
                          (St "s_1" 
                             (named "(2)" $ wk "s_3"
                                             lem
                                             lem))
                          )
                      (wk "~s_1" 
                       (dL $ Ap (Mult (Unbound :- Con "B")) 
                          (wk "s_1" 
                              (wk "s_3"
                                 ind'
                                 lem)
                              lem)
                          (dR $ Ap (Mult (V "x" :- Con "A")) 
                              (dC $wk "s_1" 
                                      (St "s_3" 
                                          lem) 
                                      (halt "(2)")) 
                              (St "s_1" (halt "(2)")))
                          )
                       (halt "(1)"))
                 ))
             (pr0 ("s_3","~t_3") lem Ax)
          )
          (Ap (Mult (Unbound :- Sor "s_3")) 
              (dL $ Ab "~u_3" 
                  (pr0 ("s_3","~t_3")
                    (St "t_3" Ax)
                    (wk "t_3" Ax Ax))
                  (pr0 ("t_3", "~u_3") 
                   Ax
                   Ax))
              (halt "lem"))

{-
subst x a b = 

nf (App _ (Lam _ (Mult (V x :- _)) b) a) = subst x a b

-}




applJ = translateJ $ Jug (App "k" (Con "F") (Con "a")) (Sub (Con "B") (V "x" :- Con "a")) gamma
applT = (Ap (V "\\subR x" :- (translate (Con "A") $$ (Many $ Con "a"))) 
            (Ap (Mult (V "x" :- Con "A"))
                (dL $ Co "~s_B" (translate protoPi) 
                  (dL $ ind)
                  (Pr "k_i" ("s_A","~s_B") 
                      (lem)
                      (Pr "k_m" ("~s_A","~s_B") 
                          (dL $ named "(1)" $ wk "s_A"
                                  (Ap (Mult (Unbound :- Con "A")) (ind') (lem))
                                  lem)
                          (wk "~s_A" 
                              (Ap (Mult (Unbound :- Con "B")) 
                                      (wk "s_A" 
                                       (ind')
                                       (lem)) 
                                      (dC $ Ap (Mult (V "x" :- Con "A")) 
                                              (wk "s_A" lem lem) 
                                              (St "s_A" lem)))
                              (halt "(1)")
                          ))
                   ))
                lem) 
            ind)

abstJ = translateJ $ Jug protoLam protoPi gamma
abstT = Co "~s" (Pi "k_i" (Mult ((:-) (V "x") (Con "A"))) (Pi "k_m" ((:-) (V "\\subR x") (App "" (Con "\\trans A") (Many (Var "x")))) (App "" (Con "\\trans B") (Many $ Con "b"))))
           (dL $ Ab "~s"
             (dL $ Ab "~s"
                 (wk "~s_A" 
                     (wk "s_A" ind lem)
                     (halt "(1)"))
                 (dR $ named "(3)" $ 
                  Pr "k_m" ("~s_A","~s")
                     (named "(1)" $ Ap (Mult (Unbound :- Con "A"))
                         (wk "s_A" ind' lem)
                         (St "s_A" lem))
                     (dR $ wk "~s_A" 
                         (wk "s_A" 
                             (Ap (Mult (Unbound :- Con "B"))
                                 ind'
                                 lem) 
                             lem) 
                         (halt "(1)"))
                  )
                 )
             (Pr "k_i" ("s_A","~s") 
                     lem
                     (halt ("(3)"))))
           (detach "S" 51 $ Ap (Mult (V "f" :- protoPi))
               (dL $ Ab "~t"
                    (dL $ Pr "k_i" ("s_A","~s") 
                        (wk "s" lem lem) 
                        (dR $ Pr "k_m" ("~s_A","~s") 
                            (named "(2)" $ Wk 1 "s" 
                               (halt "(1)") 
                               (wk "s_A" lem lem))
                            (dR $ wk "~s_A" 
                               (dL $ Ap (Mult (Unbound :- Con "B")) 
                                   (wk "s_A" 
                                    (wk "~s"
                                      ind'
                                      lem)
                                    -- (wk "s" lem lem)
                                    (named "(4)" $ wk "s" lem lem)
                                   ) 
                                   (dR $ Ap (Mult (V "x" :- Con "A"))
                                       (dC $ wk "s_A" 
                                           (St "s" lem) 
                                           (halt "(4)")
                                       )
                                       (St "s_A" (halt "(4)"))
                                       ))
                               (halt "(2)"))))
                    (pr0 ("s","~t") lem 
                         (wk "s" Ax lem)))
               lem)

convJ = translateJ $ Jug (Con "A") (Con "B'") gamma
convT = Co "~s" (translate (Con "B") $$ (Many $ Con "A"))
          ind
          (Ap (Mult (Unbound :- Con "B'"))
               ind'
               lem)

main = writeFile "AbsProof.mp" $ unlines $ compile [Figure 0 (interp axiomT axiomJ),
                                 Figure 1 (interp startT startJ),
                                 Figure 2 (interp weakT weakJ),
                                 Figure 3 (interp prodT prodJ),
                                 Figure 4 (interp applT applJ),
                                 Figure 5 (interp abstT abstJ),
                                 Figure 6 (interp convT convJ)
                                ]