{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE LambdaCase #-}

module Funcons.Operations.Types where

import Funcons.Operations.Booleans
import Funcons.Operations.Internal
import Data.Foldable (toList) 
import qualified Data.BitVector as BV
import qualified Data.Map as M
import qualified Data.Char as C
import qualified Data.Set as S
import qualified Data.MultiSet as MS
import qualified Data.Vector as V

library :: (HasValues t, Ord t) => Library t
library = libFromList [
    ("types", NullaryExpr types)
  , ("value-types", NullaryExpr value_types)
  , ("defined-values", NullaryExpr defined_values)
  , ("nothing", NullaryExpr nothing)
  , ("values", NullaryExpr values)
  , ("type-member", BinaryExpr type_member)
--  , ("is-value", UnaryExpr is_value)
--  , ("is-val", UnaryExpr is_value)
  , ("value-type", UnaryExpr value_type)
  , ("datatype-values", NullaryExpr datatype_values)
  , ("ground-values", NullaryExpr ground_values)
  ]

datatype_values_ :: HasValues t => [OpExpr t] -> OpExpr t
datatype_values_ = nullaryOp datatype_values
datatype_values :: HasValues t => OpExpr t
datatype_values = vNullaryOp "datatype-values" (Normal $ injectT ADTs)

ground_values_ :: HasValues t => [OpExpr t] -> OpExpr t
ground_values_ = nullaryOp ground_values
ground_values :: HasValues t => OpExpr t
ground_values = vNullaryOp "ground-values" (Normal $ injectT GroundValues)

types_ :: HasValues t => [OpExpr t] -> OpExpr t
types_ = nullaryOp types
types :: HasValues t => OpExpr t
types = NullaryOp "types" (Normal $ injectT Types)

value_types_ :: HasValues t => [OpExpr t] -> OpExpr t
value_types_ = nullaryOp types
value_types :: HasValues t => OpExpr t
value_types = NullaryOp "value-types" (Normal $ injectT Types)

defined_values_ :: HasValues t => [OpExpr t] -> OpExpr t
defined_values_ = nullaryOp defined_values
defined_values :: HasValues t => OpExpr t
defined_values = NullaryOp "defined-values" (Normal $ injectT DefinedValues)

nothing_ :: HasValues t => [OpExpr t] -> OpExpr t
nothing_ = nullaryOp nothing 
nothing :: HasValues t => OpExpr t
nothing = NullaryOp "nothing" (Normal $ injectT Nothings)

values_ :: HasValues t => [OpExpr t] -> OpExpr t
values_ = nullaryOp values
values :: HasValues t => OpExpr t
values = NullaryOp "values" (Normal $ injectT Values)


is_value_ :: HasValues t => [OpExpr t] -> OpExpr t
is_value_ = unaryOp is_value
is_value :: HasValues t => OpExpr t -> OpExpr t
is_value = UnaryOp "is-value" op
  where op _ = Normal $ inject (tobool True) 

value_type_ :: HasValues t => [OpExpr t] -> OpExpr t
value_type_ = unaryOp value_type
value_type :: HasValues t => OpExpr t -> OpExpr t
value_type = vUnaryOp "value-type" (Normal . injectT . tyOf)
 
tyOf :: HasValues t => Values t -> Types t
tyOf (ADTVal "true" [])         = ADT "booleans" []
tyOf (ADTVal "false" [])        = ADT "booleans" []
tyOf (Int _)                    = Integers
tyOf (Nat _)                    = Naturals
tyOf (ADTVal _ _)               = ADTs
tyOf (Ascii _)                  = AsciiCharacters
tyOf (Atom _)                   = Atoms
tyOf (Bit v)                    = Bits (BV.size v)
tyOf (Char _)                   = UnicodeCharacters 
tyOf (ComputationType (Type _)) = Types
tyOf (ComputationType _)        = ComputationTypes
tyOf (Float f)                  = IEEEFloats Binary32 
--tyOf (Type _)                   = Types 
tyOf (IEEE_Float_32 _)          = IEEEFloats Binary32 
tyOf (IEEE_Float_64 _)          = IEEEFloats Binary64 
tyOf (Rational _)               = Rationals
tyOf (Map m)                    = Maps Values Values -- TODO find "strongest common type"
tyOf (Set s)                    | null s = Sets Values
                                | otherwise = Sets (tyOf (S.findMax s))
tyOf (Multiset s)               | null s = Multisets Values
                                | otherwise = Multisets (tyOf (MS.findMax s)) 
tyOf (Vector v)                 | V.null v = Vectors Values
                                | otherwise = Vectors (tyOf (v V.! 0))
tyOf VAny                       = Values
tyOf (VMeta t)                  = ASTs

type_member_ :: HasValues t => [OpExpr t] -> OpExpr t
type_member_ = binaryOp type_member
-- | Type membership check for primitive types and
-- predefined composite types (non-ADTs).
type_member :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
type_member = vBinaryOp "type-member" op
  where op v mty = case mty of
         ComputationType (Type t) -> proceed v t
         ComputationType (ComputesType t) -> proceed v t
         ComputationType (ComputesFromType _ t) -> proceed v t
         _ -> SortErr "type-member(V,Ty) not applied to a value and a type"
 
        proceed v ty = case isInType v ty of
          Nothing -> DomErr "type-member applied to an ADT or a non-type"
          Just b  -> Normal $ inject (tobool b)

isInType :: HasValues t => Values t -> Types t -> Maybe Bool
isInType _ EmptyType = return False
isInType v Values = return True 
isInType n Nothings = return (isNoValue n) 
isInType v DefinedValues = return (isDefinedVal v)
isInType v GroundValues = return (isGround v)
isInType v (ADT "strings" []) = return (isString_ v)
isInType (ADTVal "list" vs') (ADT "lists" [ty']) 
  | Just ty <- projectT ty', Just vs <- sequence (map project vs') = 
  and <$> mapM (flip isInType ty) vs
isInType (ADTVal "true" []) (ADT "booleans" []) = return True
isInType (ADTVal "false" []) (ADT "booleans" []) = return True
isInType v (ADT "tuples" ttparams') 
  | Just ttparams <- sequence (map projectT ttparams') = case v of
    ADTVal "tuple" vs' | Just vs <- sequence (map project vs')
                            -> isInTupleType vs ttparams
    _                       -> isInTupleType [v] ttparams 
isInType v (ADT nm tys) = Nothing
isInType (ADTVal _ _) ADTs = return True
isInType (Atom _) Atoms = return True
isInType (Ascii _) Characters = return True
isInType (Char _) Characters = return True
isInType (Ascii _) AsciiCharacters = return True
isInType (Bit bv) (Bits n) = return (BV.size bv == n)
isInType v (IntegersFrom n) 
    | Int i <- upcastIntegers v = return (i >= n)
isInType v (IntegersUpTo n) 
    | Int i <- upcastIntegers v = return (i <= n)
isInType (ComputationType _) Types = return True
isInType (ComputationType (ComputesFromType _ _)) ComputationTypes = return True
isInType (ComputationType (ComputesType _)) ComputationTypes = return True
isInType (ComputationType (Type _)) ComputationTypes = return True
isInType (IEEE_Float_32 _) (IEEEFloats Binary32) = return True
isInType (IEEE_Float_64 _) (IEEEFloats Binary64) = return True
isInType v Integers | Int _ <- upcastIntegers v = return True
isInType (Map m) (Maps kt vt) = and <$> sequence [and <$> mapM (flip isInType kt) (M.keys m)
                                                 ,and <$> mapM (flip isInType vt) (M.elems m)]
isInType (Multiset ls) (Multisets ty) = and <$> mapM (flip isInType ty) (toList ls)
isInType v Naturals | Nat _ <- upcastNaturals v = return True
isInType v Rationals | Rational _ <- upcastRationals v = return True 
isInType (Set ls) (Sets ty) = and <$> mapM (flip isInType ty) (toList ls)
isInType v UnicodeCharacters | Char _ <- upcastUnicode v = return True
isInType v (Union ty1 ty2) = (||) <$> isInType v ty1 <*> isInType v ty2
isInType v (Complement ty) = not <$> isInType v ty
isInType v (Intersection ty1 ty2) = (&&) <$> isInType v ty1 <*> isInType v ty2
isInType (Vector ls) (Vectors ty) = and <$> mapM (flip isInType ty) (toList ls)
--isInType (VMeta _) ASTs = return True -- for meta-programming (see Funcons.MetaProgramming)
isInType _ _ = return False

isInTupleType :: HasValues t => [Values t] -> [Types t] -> Maybe Bool
isInTupleType vs ttparams = and <$> sequence (zipWith isInType vs ttparams)