{-# 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)
, ("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 (IEEE_Float_32 _) = IEEEFloats Binary32
tyOf (IEEE_Float_64 _) = IEEEFloats Binary64
tyOf (Rational _) = Rationals
tyOf (Map m) = Maps Values Values
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_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 _ _ = return False
isInTupleType :: HasValues t => [Values t] -> [Types t] -> Maybe Bool
isInTupleType vs ttparams = and <$> sequence (zipWith isInType vs ttparams)