-----------------------------------------------------------------------------
-- |
-- Module      :  Translation
-- Copyright   :  (c) Masahiro Sakai 2007-2009
-- License     :  BSD3-style (see LICENSE)
-- 
-- Maintainer:    masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable

{-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, ScopedTypeVariables #-}

module Translation (translate) where

import Expr
import P

-----------------------------------------------------------------------------
-- Exprも型付きにしたいなぁ

{-
data E    -- e
data S    -- s
data Prop -- t
-- 関数型はHaskellの -> をそのまま使う

-- 範疇から型への対応
type family Translate x
type instance Translate Sen = Prop
type instance Translate IV = E -> Prop
type instance Translate CN = E -> Prop
type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a)
type instance Translate (a :// b) = ((S -> Translate b) -> Translate a)
-}

-----------------------------------------------------------------------------

translate :: forall c. P c -> Expr
--- 1. αがgの定義域にあれば，α は，g(α) に翻訳される．
-- 最後に
--- 2. be → λp.λx. p{f^λy.[x = y]}.
---    ここで，変数pのタイプは<s, <<s, <e, t>>, t>>.
translate (B (IV :/ (Sen :/ IV)){- TV -} "be") =
    lambda "p" $ lambda "x" $ 
    FVar "p" <@>
    int (lambda "y" $ Op2 Id (FVar "x") (FVar "y"))
--- 3. necessarily → λp[□ext p]. ここで，p のタイプは<s, t>とする．
translate (B (Sen :/ Sen) "necessarily") = lambda "p" $ Op1 Box (ext (FVar "p"))
--- 4. j, m, b はタイプがe の定数記号，変数P のタイプは<s, <e, t>>とする．
translate (B (Sen :/ IV){- T -} x) = lambda "p" $ FVar "p" <@> Const x
--- 5. he_n → λP. P {x_n}．x_ はタイプe の変数．
translate (He n) = lambda "p" $ FVar "p" <@> FVar (xn n)

translate (F2 delta zeta) = trApp delta zeta -- T2
translate (F3 n zeta phi) = -- T3
    lambda (xn n) $ Op2 And (translate zeta :@ FVar (xn n)) (translate phi)
translate (F4 alpha delta) = trApp alpha delta -- T4
translate (F5 delta beta)  = trApp delta beta  -- T5
-- T6 (T5と同じなので省略)
translate (F16 delta phi)  = trApp delta phi   -- T7
translate (F17 delta beta) = trApp' delta beta -- T8
translate (F6 delta beta)  = trApp delta beta  -- T9
translate (F7 delta beta)  = trApp delta beta  -- T10
translate (F8 phi psi) =
  case f8 :: Cat c of
    Sen -> Op2 And (translate phi) (translate psi) -- T11a
    IV -> lambda "x" $ Op2 And (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12a
translate (F9 phi psi) =
  case f9 :: Cat c of
    Sen -> Op2 Or (translate phi) (translate psi) -- T11b
    IV -> lambda "x" $ Op2 Or (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12b
    Sen :/ IV -> lambda "P" $ Op2 Or (translate phi :@ FVar "P") (translate psi :@ FVar "P") -- T13
-- T14 (講義資料はx_nになるべきところがxになっている)
translate (F10 n alpha phi) =
  case f10 :: Cat c of
    Sen -> translate alpha :@ (int $ lambda (xn n) (translate phi)) -- T14
    CN -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T15
    IV -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T16
-- T17
translate (F11 alpha delta) = Op1 Not         $ trApp alpha delta
translate (F12 alpha delta) =           Op1 F $ trApp alpha delta
translate (F13 alpha delta) = Op1 Not $ Op1 F $ trApp alpha delta
translate (F14 alpha delta) =           Op1 H $ trApp alpha delta
translate (F15 alpha delta) = Op1 Not $ Op1 H $ trApp alpha delta
-- T18 (beの扱い以外はT9と同じ)
translate (B (IV :/ Adj) "be") =
    lambda "P" $ lambda "x" $ FVar "P" <@> FVar "x"
-- T19
translate (F19 delta) =
    lambda "x" $ exists "y" $
           translate delta :@
             int (lambda "P" (FVar "P" <@> FVar "y")) :@
             FVar "x"
translate (F20 delta beta) = trApp delta beta -- T20
translate (F21 delta beta) = trApp delta beta -- T21 (講義資料ではF20を誤って使っている)
-- T22
translate (F22 delta) =
    lambda "P" $ lambda "Q" $ lambda "x" $
    translate delta :@ FVar "Q" :@ FVar "P" :@ FVar "x"
translate (F23 alpha delta) = trApp alpha delta -- T23
translate (F24 alpha beta)  = trApp alpha beta  -- T24
-- 講義資料のByの解釈は誤り? (型が一致しない)
translate (B (IV :/ (IV :/ (Sen :/ IV)) :/ (Sen :/ IV)){- PP/T -} "by") = 
    lambda "P" $ lambda "R" $ lambda "x" $
        FVar "P" <@>
        (int $ lambda "y" $
         FVar "R" <@> int (lambda "Q" $ FVar "Q" <@> FVar "x") :@ FVar "y")
-- T25
translate (F25 delta) =
    lambda "x" $ exists "y" $ Op1 H $
        translate delta :@
        int (lambda "P" $ FVar "P" <@> FVar "x") :@
        (FVar "y")

-- Det
translate (B (Sen :/ IV :/ CN) s) =
    case s of
    "a"   ->
        lambda "p" $ lambda "q" $ exists "x" $
        Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")
    "the" ->
        lambda "p" $ lambda "q" $ exists "y" $ forall "x" $
        Op2 And
          (Op2 Equiv (FVar "p" <@> FVar "x") (Op2 Id (FVar "x") (FVar "y")))
          (FVar "q" <@> FVar "x")
    "every" ->
        lambda "p" $ lambda "q" $ forall "x" $
        Op2 Imply (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")
    "no" ->
        lambda "p" $ lambda "q" $ forall "x" $
        Op1 Not (Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x"))
    _ -> Const s

-- それ以外
translate (B _ x) = Const x

-- ユーティリティ
trApp :: P (b :/ a) -> P a -> Expr
trApp  f a = translate f :@ (int (translate a))
trApp' :: P (b :// a) -> P a -> Expr
trApp' f a = translate f :@ (int (translate a))

xn :: Int -> Name
xn n = "he_"++show n