content: -----------------------------------------------------------------------------
  -- |
  -- Module      :  Statement
  -- Copyright   :  (c) Masahiro Sakai 2004,2009
  -- License     :  BSD-style
  -- 
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  portable
  --
  -----------------------------------------------------------------------------
  
  module Statement
      ( ConditionalEquation (..)
      , Equation (..)
      , eqs
      , ceq
      , feq
      , statements
      ) where
  
  import CDT
  import Exp
  import qualified FE
  import Data.List
  
  infix 4 :=:
  infixr 3 :=>
  
  data ConditionalEquation = [Equation] :=> Equation
  data Equation = Exp :=: Exp
  
  instance Show ConditionalEquation where
      show (premisses :=> body) =
          case premisses of
          [] -> show body
          _  -> intercalate " & " (map show premisses) ++ " => " ++ show body
  
  instance Show Equation where
      show (a :=: b) = show a ++ "=" ++ show b
  
  eqs :: CDT.CDT -> [ConditionalEquation]
  eqs obj = map f (CDT.nats obj)
      where f nat =
                case CDT.objectType obj of
                LeftObject ->
                    [] :=>
                    FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat
                    :=: (factArgs !! CDT.natIndex nat) `comp`
                        FE.fold g mkFunct (CDT.natDeclDom nat)
                RightObject ->
                    [] :=>
                    Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)
                    :=: FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
                        (factArgs !! CDT.natIndex nat)
            factArgs = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]
            g 0 = Fact obj factArgs
            g _ = Identity
  
  ceq :: CDT -> ConditionalEquation
  ceq obj = map f (CDT.nats obj) :=> (u :=: Fact obj args)
      where f nat =
                case CDT.objectType obj of
                LeftObject ->
                    FE.fold g mkFunct (CDT.natDeclCod nat) `comp` Nat nat
                    :=:
                    (args !! CDT.natIndex nat) `comp`
                      FE.fold g mkFunct (CDT.natDeclDom nat)
                RightObject ->
                    Nat nat `comp` FE.fold g mkFunct (CDT.natDeclDom nat)
                    :=:
                    FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
                    (args !! CDT.natIndex nat)
            args = map (\i -> Var ("f" ++ show i) []) [0 .. CDT.nNats obj - 1]
            u = Var "g" []
            g 0 = u
            g _ = Identity
  
  feq :: CDT -> ConditionalEquation
  feq obj = [] :=> Funct obj functArgs :=: Fact obj factArgs
      where functArgs = map f [0 .. CDT.functArity obj - 1]
                where f i = Var ("f" ++ show i) []
            factArgs  = map f (CDT.nats obj)
                where f nat = FE.fold g mkFunct (CDT.natDeclCod nat) `comp`
                              Nat nat `comp`
                              FE.fold g mkFunct (CDT.natDeclDom nat)
                      g 0 = Identity
                      g n = functArgs !! (n-1)
  
  statements :: CDT -> [ConditionalEquation]
  statements obj = eqs obj ++ [feq obj, ceq obj]
  
  -----------------------------------------------------------------------------
  
  mkFunct :: CDT -> [Exp] -> Exp
  mkFunct _ []     = Identity
  mkFunct obj args = Funct obj args
  