{-# 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)
]