-- GSoC 2015 - Haskell bindings for OpenCog.
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE AutoDeriveTypeable        #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE StandaloneDeriving        #-}

-- | This Module defines the main data types for Haskell bindings.
module OpenCog.AtomSpace.Types (
    TruthVal (..)
  , AtomName (..)
  , Atom (..)
  , AtomGen (..)
  , Gen (..)
  , appGen
  , getType
  ) where

import OpenCog.AtomSpace.Inheritance    (type (<~))
import OpenCog.AtomSpace.AtomType       (AtomType(..))
import Data.Typeable                    (Typeable,typeRep)
import Control.Monad                    (Functor,Monad)

-- | Atom name type.
type AtomName = String

-- | 'TruthVal' represent the different types of TruthValues.
data TruthVal = SimpleTV { tvMean       :: Double
                         , tvConfidence :: Double
                         }
              | CountTV  { tvMean       :: Double
                         , tvCount      :: Double
                         , tvConfidence :: Double
                         }
              | IndefTV  { tvMean       :: Double
                         , tvL          :: Double
                         , tvU          :: Double
                         , tvConfLevel  :: Double
                         , tvDiff       :: Double
                         }
              | FuzzyTV  { tvMean       :: Double
                         , tvConfidence :: Double
                         }
              | ProbTV   { tvMean       :: Double
                         , tvCount      :: Double
                         , tvConfidence :: Double
                         }
    deriving (Show,Eq)

-- | 'Gen' groups all the atoms that are children of the atom type a.
data Gen a where
    Gen :: (Typeable a,b <~ a) => Atom b -> Gen a

deriving instance Show (Gen a)

-- | 'appGen' evaluates a given function with the atom type instance
-- wrapped inside the 'Gen' type.
appGen :: (forall b. (Typeable a,b <~ a) => Atom b -> c) -> Gen a -> c
appGen f (Gen at) = f at

-- | 'AtomGen' is a general atom type hiding the type variables.
-- (necessary when working with many instances of different atoms,
-- for example, for lists of general atoms)
type AtomGen = Gen AtomT

-- | 'Atom' is the main data type to represent the different types of atoms.
--
-- Here we impose type constraints in how atoms relate between them.
--
-- The @<~@ type operator means that the type on the left "inherits" from the
-- type on the right.
--
-- __DEFINING NEW ATOM TYPES:__
--
-- * If it is a node:
--
--    We add a new data constructor such as:
--
--    @ NewAtomTypeNode :: AtomName -> TruthVal -> Atom NewAtomTypeT  @
--
--    where NewAtomTypeT is a phantom type (automatically generated by temp. hask.).
--
-- * If it is a link:
--
--     * If it is of a fixed arity:
--
--         We impose the type constraints on each of the members of its outgoing set.
--
--         @ NewAtomTypeLink :: (a <~ t1,b <~ t2,c <~ t3) =>
--                   TruthVal -> Atom a -> Atom b -> Atom c -> AtomNewAtomTypeT  @
--
--     * If it is of unlimited arity:
--
--         We define it as a data constructor that takes a list of atoms as first argument.
--         All the members of its outgoing set will satisfy the same constraints.
--
--         For example suppose NewAtomTypeLink accepts nodes that are concepts:
--
--         @ NewAtomTypeLink :: TruthVal -> [Gen ConceptT] -> Atom NewAtomTypeT  @
--
-- Also, you have to modify the module Internal. Adding proper case clauses for
-- this new atom type to the functions "toRaw" and "fromRaw".
--
data Atom (a :: AtomType) where
    PredicateNode       :: AtomName -> TruthVal -> Atom PredicateT

    ConceptNode         :: AtomName -> TruthVal -> Atom ConceptT

    DefinedPredicateNode:: AtomName -> TruthVal -> Atom DefinedPredicateT

    AnchorNode          :: AtomName -> Atom AnchorT

    AndLink             :: TruthVal -> [AtomGen] -> Atom AndT
    OrLink              :: TruthVal -> [AtomGen] -> Atom OrT
    NotLink             :: (a <~ AtomT) =>
                           TruthVal -> Atom a -> Atom NotT
    ImplicationLink     :: (p1 <~ AtomT,p2 <~ AtomT) =>
                           TruthVal -> Atom p1 -> Atom p2 -> Atom ImplicationT

    EquivalenceLink     :: (p1 <~ AtomT,p2 <~ AtomT) =>
                           TruthVal -> Atom p1 -> Atom p2 -> Atom EquivalenceT
    EvaluationLink      :: (p <~ PredicateT,a <~ AtomT) =>
                           TruthVal -> Atom p -> Atom a -> Atom EvaluationT


    InheritanceLink     :: (c1 <~ AtomT,c2 <~ AtomT) =>
                           TruthVal -> Atom c1 -> Atom c2 -> Atom InheritanceT
    SimilarityLink      :: (c1 <~ AtomT,c2 <~ AtomT) =>
                           TruthVal -> Atom c1 -> Atom c2 -> Atom SimilarityT
    MemberLink          :: (a <~ AtomT,c <~ ConceptT) =>
                           TruthVal -> Atom a -> Atom c -> Atom MemberT
    SatisfyingSetLink   :: (p <~ AtomT) =>
                           Atom p -> Atom SatisfyingSetT

    NumberNode          :: Double -> Atom NumberT

    ListLink            :: [AtomGen] -> Atom ListT
    SetLink             :: [AtomGen] -> Atom SetT

    SchemaNode          :: AtomName -> Atom SchemaT
    GroundedSchemaNode  :: AtomName -> Atom GroundedSchemaT
    ExecutionLink       :: (s <~ SchemaT,i <~ AtomT,o <~ AtomT) =>
                           Atom s -> Atom i -> Atom o -> Atom ExecutionT

    VariableNode        :: AtomName -> Atom VariableT
    VariableList        :: [Gen VariableT] -> Atom VariableListT

    SatisfactionLink    :: (v <~ VariableListT,l <~ AtomT) =>
                           Atom v -> Atom l -> Atom SatisfactionT
    ForAllLink          :: (v <~ VariableListT,i <~ AtomT) =>
                           TruthVal -> Atom v -> Atom i -> Atom ForAllT
    ExistsLink          :: (v <~ VariableListT,i <~ AtomT) =>
                           TruthVal -> Atom v -> Atom i -> Atom ExistsT

    QuoteLink           :: (a <~ AtomT) =>
                           Atom a -> Atom QuoteT

    BindLink            :: (v <~ VariableListT,p <~ AtomT,q <~ AtomT) =>
                           Atom v -> Atom p -> Atom q -> Atom BindT
    ContextLink         :: (c <~ AtomT,e <~ AtomT) =>
                           TruthVal -> Atom c -> Atom e -> Atom ContextT
    LambdaLink          :: (v <~ VariableListT,a <~ AtomT) =>
                            Atom v -> Atom a -> Atom LambdaT
    SubsetLink          :: (a1 <~ AtomT, a2 <~ AtomT) =>
                            TruthVal -> Atom a1 -> Atom a2 -> Atom SubsetT
    EqualLink           :: (a1 <~ AtomT, a2 <~ AtomT) =>
                            Atom a1 -> Atom a2 -> Atom EqualT
    TrueLink            :: [AtomGen] -> Atom TrueT
    FalseLink           :: [AtomGen] -> Atom FalseT
    SequentialAndLink   :: [AtomGen] -> Atom SequentialAndT
    SequentialOrLink    :: [AtomGen] -> Atom SequentialOrT
    DefineLink          :: (a1 <~ AtomT, a2 <~ AtomT) =>
                            Atom a1 -> Atom a2 -> Atom DefineT

deriving instance Show (Atom a)
deriving instance Typeable Atom

-- TODO: improve this code, defining an instance of Data for Atom GADT
-- and use the Data type class interface to get the constructor.
getType :: (Typeable a) => Atom a -> String
getType = head . words . show