diff --git a/funcons-values.cabal b/funcons-values.cabal --- a/funcons-values.cabal +++ b/funcons-values.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: funcons-values -version: 0.1.0.5 +version: 0.1.0.7 synopsis: Library providing values and operations on values in a fixed universe. description: The PLanCompS project () has developed a component-based approach to formal semantics. @@ -42,6 +42,7 @@ ,Funcons.Operations.NonGroundValues ,Funcons.Operations.Multisets ,Funcons.Operations.Sets + ,Funcons.Operations.Graphs ,Funcons.Operations.Bits ,Funcons.Operations.Characters ,Funcons.Operations.Maps diff --git a/src/Funcons/Operations.hs b/src/Funcons/Operations.hs --- a/src/Funcons/Operations.hs +++ b/src/Funcons/Operations.hs @@ -15,6 +15,7 @@ module Funcons.Operations.Floats, module Funcons.Operations.Strings, -- module Funcons.Operations.Rationals, + module Funcons.Operations.Graphs, module Funcons.Operations.Sets, module Funcons.Operations.Multisets, module Funcons.Operations.Bits, @@ -49,9 +50,13 @@ import qualified Funcons.Operations.Strings (library) --import Funcons.Operations.Rationals hiding (library) --import qualified Funcons.Operations.Rationals (library) +import Funcons.Operations.Graphs hiding (library) +import qualified Funcons.Operations.Graphs (library) import Funcons.Operations.Sets hiding (library, sets) import qualified Funcons.Operations.Sets (library) +import Funcons.Operations.Multisets hiding (library, multisets) import qualified Funcons.Operations.Multisets (library) +import Funcons.Operations.Bits hiding (library) import qualified Funcons.Operations.Bits (library) import Funcons.Operations.Characters hiding (library) import qualified Funcons.Operations.Characters (library) @@ -74,6 +79,7 @@ , Funcons.Operations.Floats.library , Funcons.Operations.Strings.library -- , Funcons.Operations.Rationals.library + , Funcons.Operations.Graphs.library , Funcons.Operations.Sets.library , Funcons.Operations.Multisets.library , Funcons.Operations.Bits.library diff --git a/src/Funcons/Operations/Bits.hs b/src/Funcons/Operations/Bits.hs --- a/src/Funcons/Operations/Bits.hs +++ b/src/Funcons/Operations/Bits.hs @@ -1,9 +1,123 @@ +{-# LANGUAGE OverloadedStrings #-} module Funcons.Operations.Bits where -import Funcons.Operations.Booleans (tobool) +import Funcons.Operations.Booleans (tobool,frombool) import Funcons.Operations.Internal +import Control.Monad (join) +import qualified Data.BitVector as BV + library :: (HasValues t, Ord t) => Library t -library = libFromList [] - +library = libFromList [ + ("bit-vector-not", UnaryExpr bit_vector_not) + , ("bit-vector-and", BinaryExpr bit_vector_and) + , ("bit-vector-or", BinaryExpr bit_vector_or) + , ("bit-vector-xor", BinaryExpr bit_vector_xor) + , ("bit-vector-shift-left", BinaryExpr bit_vector_shift_left) + , ("bit-vector-logical-shift-right", BinaryExpr bit_vector_logical_shift_right) + , ("bit-vector-arithmetic-shift-right", BinaryExpr bit_vector_arithmetical_shift_right) + , ("integer-to-bit-vector", BinaryExpr integer_to_bit_vector) + , ("bit-vector-to-integer", UnaryExpr bit_vector_to_integer) + , ("bit-vector-to-natural", UnaryExpr bit_vector_to_natural) + ] + +bit_vector_not_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_not_ = unaryOp bit_vector_not +bit_vector_not :: HasValues t => OpExpr t -> OpExpr t +bit_vector_not = vUnaryOp "bit-vector-not" op + where op (ADTVal "bit-vector" vals) | Just bv <- apply_to_vec BV.not vals = + Normal $ inject $ ADTVal "bit-vector" bv + op _ = SortErr "bit-vector-not applied to a bit-vector" + +bit_vector_and_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_and_ = binaryOp bit_vector_and +bit_vector_and :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_and = vBinaryOp "bit-vector-and" op + where op (ADTVal "bit-vector" vals1) (ADTVal "bit-vector" vals2) = + case args_to_bools vals1 of + Just bv1 -> case apply_to_vec (\bv2 -> BV.and [BV.fromBits bv1,bv2]) vals2 of + Just bv2 -> Normal $ inject $ ADTVal "bit-vector" bv2 + Nothing -> SortErr "second argument of bit-vector-and not a bit-vector" + Nothing -> SortErr "first argument of bit-vector-and not a bit-vector" + op _ _ = SortErr "bit-vector-and not applied to two bit-vectors" + +bit_vector_or_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_or_ = binaryOp bit_vector_or +bit_vector_or :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_or = vBinaryOp "bit-vector-or" op + where op (ADTVal "bit-vector" vals1) (ADTVal "bit-vector" vals2) = + case args_to_bools vals1 of + Just bv1 -> case apply_to_vec (\bv2 -> BV.or [BV.fromBits bv1,bv2]) vals2 of + Just bv2 -> Normal $ inject $ ADTVal "bit-vector" bv2 + Nothing -> SortErr "second argument of bit-vector-or not a bit-vector" + Nothing -> SortErr "first argument of bit-vector-or not a bit-vector" + op _ _ = SortErr "bit-vector-or not applied to two bit-vectors" + +bit_vector_xor_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_xor_ = binaryOp bit_vector_xor +bit_vector_xor :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_xor = vBinaryOp "bit-vector-xor" (binary_bit_op "bit-vector-xor" BV.xor) + +bit_vector_shift_left_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_shift_left_ = binaryOp bit_vector_shift_left +bit_vector_shift_left :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_shift_left = vBinaryOp "bit-vector-shift-left" (bit_nat_op "bit-vector-shift-left" BV.shl) + +bit_vector_logical_shift_right_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_logical_shift_right_ = binaryOp bit_vector_logical_shift_right +bit_vector_logical_shift_right :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_logical_shift_right = vBinaryOp "bit-vector-logical-shift-right" (bit_nat_op "bit-vector-logical-shift-right" BV.shr) + +bit_vector_arithmetical_shift_right_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_arithmetical_shift_right_ = binaryOp bit_vector_arithmetical_shift_right +bit_vector_arithmetical_shift_right :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +bit_vector_arithmetical_shift_right = vBinaryOp "bit-vector-arithmetical-shift-right" (bit_nat_op "bit-vector-arithmetical-shift-right" BV.ashr) + +bit_vector_to_integer_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_to_integer_ = unaryOp bit_vector_to_integer +bit_vector_to_integer :: HasValues t => OpExpr t -> OpExpr t +bit_vector_to_integer = vUnaryOp "bit-vector-to-integer" op + where op (ADTVal "bit-vector" vals) | Just bits <- args_to_bools vals + = Normal $ inject $ Int $ BV.int (BV.fromBits bits) + op _ = SortErr "bit-vector-to-integer not applied to a bit-vector" + +bit_vector_to_natural_ :: HasValues t => [OpExpr t] -> OpExpr t +bit_vector_to_natural_ = unaryOp bit_vector_to_natural +bit_vector_to_natural :: HasValues t => OpExpr t -> OpExpr t +bit_vector_to_natural = vUnaryOp "bit-vector-to-natural" op + where op (ADTVal "bit-vector" vals) | Just bits <- args_to_bools vals + = Normal $ inject $ Nat $ BV.nat (BV.fromBits bits) + op _ = SortErr "bit-vector-to-natural not applied to a bit-vector" + +integer_to_bit_vector_ :: HasValues t => [OpExpr t] -> OpExpr t +integer_to_bit_vector_ = binaryOp integer_to_bit_vector +integer_to_bit_vector :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +integer_to_bit_vector = vBinaryOp "integer-to-bit-vector" op + where op mi mn | Int i <- upcastIntegers mi, Nat n <- upcastNaturals mn + = Normal $ inject $ ADTVal "bit-vector" $ map (inject . tobool) $ + BV.toBits (BV.bitVec (fromInteger n) (i `mod` (2 ^ n))) + op _ _ = SortErr "integer-to-bit-vector not applied to an integer and a natural" +--- lib + +apply_to_vec :: HasValues t => (BV.BV -> BV.BV) -> [t] -> Maybe [t] +apply_to_vec app = + fmap (map (inject . tobool) . BV.toBits . app . BV.fromBits) . args_to_bools + +args_to_bools :: HasValues t => [t] -> Maybe [Bool] +args_to_bools = sequence . map (join . fmap frombool . project) + +binary_bit_op fc app (ADTVal "bit-vector" vals1) (ADTVal "bit-vector" vals2) = + case args_to_bools vals1 of + Just bv1 -> case apply_to_vec (app (BV.fromBits bv1)) vals2 of + Just bv2 -> Normal $ inject $ ADTVal "bit-vector" bv2 + Nothing -> SortErr ("second argument of " ++ fc ++ " not a bit-vector") + Nothing -> SortErr ("first argument of " ++ fc ++ " not a bit-vector") +binary_bit_op fc _ _ _ = SortErr (fc ++ " not applied to two bit-vectors") + +bit_nat_op fc app (ADTVal "bit-vector" vals1) v2 | Nat n <- upcastNaturals v2 = + case apply_to_vec (flip app (fromInteger n)) vals1 of + Just bv2 -> Normal $ inject $ ADTVal "bit-vector" bv2 + Nothing -> SortErr ("first argument of " ++ fc ++ " not a bit-vector") +bit_nat_op fc _ _ _ = SortErr (fc ++ " not applied to a bit-vector and a natural") + diff --git a/src/Funcons/Operations/Characters.hs b/src/Funcons/Operations/Characters.hs --- a/src/Funcons/Operations/Characters.hs +++ b/src/Funcons/Operations/Characters.hs @@ -3,16 +3,26 @@ import Funcons.Operations.Booleans (tobool) import Funcons.Operations.Internal +import Funcons.Operations.Integers +import Funcons.Operations.Bits -import Data.Char (ord,chr) +import Data.Char (ord,chr,isAscii) library :: (HasValues t, Ord t) => Library t library = libFromList [ ("ascii-characters", NullaryExpr ascii_characters) , ("ascii-character", UnaryExpr ascii_character) - , ("unicode", UnaryExpr unicode) - , ("unicode-character-code", UnaryExpr unicode_character_code) + , ("unicode-character", UnaryExpr unicode_character) + , ("unicode-point", UnaryExpr unicode_point) , ("characters", NullaryExpr characters) + , ("unicode-characters", NullaryExpr unicode_characters) + , ("iso-latin-1-characters", NullaryExpr iso_latin_characters) + , ("latin-1-chars", NullaryExpr iso_latin_characters) + , ("basic-plane-multilingual-characters", NullaryExpr bmp_characters) + , ("bmp-chars", NullaryExpr bmp_characters) + , ("unicode-chars", NullaryExpr unicode_characters) + , ("unicode-points", NullaryExpr unicode_points) + , ("basic-multilingual-plane-points", NullaryExpr bmp_points) ] characters_ :: HasValues t => [OpExpr t] -> OpExpr t @@ -20,34 +30,61 @@ characters :: HasValues t => OpExpr t characters = vNullaryOp "characters" (Normal $ injectT $ Characters) +unicode_characters_ :: HasValues t => [OpExpr t] -> OpExpr t +unicode_characters_ = nullaryOp unicode_characters +unicode_characters :: HasValues t => OpExpr t +unicode_characters = vNullaryOp "unicode-characters" (Normal $ injectT $ UnicodeCharacters) + +unicode_points_ :: HasValues t => [OpExpr t] -> OpExpr t +unicode_points_ = nullaryOp unicode_points +unicode_points :: HasValues t => OpExpr t +unicode_points = vNullaryOp "unicode-points" (Normal $ injectT (Intersection (IntegersFrom 0) (IntegersUpTo numUnicodeCodes))) + +bmp_points_ :: HasValues t => [OpExpr t] -> OpExpr t +bmp_points_ = nullaryOp bmp_points +bmp_points :: HasValues t => OpExpr t +bmp_points = vNullaryOp "basic-multilingual-plane-points" (Normal $ injectT (Intersection (IntegersFrom 0) (IntegersUpTo numBMPCodes))) + ascii_characters_ :: HasValues t => [OpExpr t] -> OpExpr t ascii_characters_ = nullaryOp ascii_characters ascii_characters :: HasValues t => OpExpr t ascii_characters = vNullaryOp "ascii-characters" (Normal $ injectT $ AsciiCharacters) +iso_latin_characters_ :: HasValues t => [OpExpr t] -> OpExpr t +iso_latin_characters_ = nullaryOp iso_latin_characters +iso_latin_characters :: HasValues t => OpExpr t +iso_latin_characters = vNullaryOp "iso-latin-1-characters" (Normal $ injectT $ ISOLatinCharacters) + +bmp_characters_ :: HasValues t => [OpExpr t] -> OpExpr t +bmp_characters_ = nullaryOp bmp_characters +bmp_characters :: HasValues t => OpExpr t +bmp_characters = vNullaryOp "basic-multilingual-plane-characters" (Normal $ injectT $ BMPCharacters) + ascii_character_ :: HasValues t => [OpExpr t] -> OpExpr t ascii_character_ = unaryOp ascii_character ascii_character :: HasValues t => OpExpr t -> OpExpr t ascii_character = vUnaryOp "ascii-character" op - where op v | isString_ v, [c] <- unString v - = Normal $ inject $ Ascii c + where op v | isString_ v, [c] <- unString v, isAscii c + = Normal $ inject $ downcast_unicode_characters c | otherwise = SortErr "ascii-character not applied to a string (of 1 ascii character long)" -unicode_ :: HasValues t => [OpExpr t] -> OpExpr t -unicode_ = unaryOp unicode -unicode :: HasValues t => OpExpr t -> OpExpr t -unicode = vUnaryOp "unicode" op - where op v | Int i <- upcastIntegers v, i < numUnicodeCodes = +unicode_character_ :: HasValues t => [OpExpr t] -> OpExpr t +unicode_character_ = unaryOp unicode_character +unicode_character :: HasValues t => OpExpr t -> OpExpr t +unicode_character = vUnaryOp "unicode-character" op + where op v | Int i <- upcastIntegers v, i < numUnicodeCodes, i >= 0 = Normal $ inject $ mk_unicode_characters (chr $ fromInteger i) - | otherwise = SortErr "unicode not applied to an integer in the range 0..(2^32)-1" + | otherwise = SortErr "unicode-character not applied to an integer in the right range" -numUnicodeCodes :: Integer -numUnicodeCodes = (2^32)-1 +numUnicodeCodes,numBMPCodes :: Integer +numUnicodeCodes = (2^21)-1 +numBMPCodes = (2^17)-1 -unicode_character_code_ :: HasValues t => [OpExpr t] -> OpExpr t -unicode_character_code_ = unaryOp unicode_character_code -unicode_character_code :: HasValues t => OpExpr t -> OpExpr t -unicode_character_code = vUnaryOp "unicode-character-code" op - where op v | Char c <- upcastUnicode v = + +unicode_point_ :: HasValues t => [OpExpr t] -> OpExpr t +unicode_point_ = unaryOp unicode_point +unicode_point :: HasValues t => OpExpr t -> OpExpr t +unicode_point = vUnaryOp "unicode-point" op + where op v | Just c <- upcastCharacter v = Normal $ inject $ mk_integers (toInteger $ ord c) - | otherwise = SortErr "unicode-character-code not applied to a unicode-character" + | otherwise = SortErr "unicode-point not applied to a unicode-character" diff --git a/src/Funcons/Operations/Graphs.hs b/src/Funcons/Operations/Graphs.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Graphs.hs @@ -0,0 +1,63 @@ +module Funcons.Operations.Graphs where + +import Funcons.Operations.Internal +import Funcons.Operations.Booleans (tobool) +import qualified Data.Map as M +import qualified Data.Set as S +import Data.List ((\\)) + +library :: (HasValues t, Ord t) => Library t +library = libFromList [ + ("is-cyclic", UnaryExpr is_cyclic) + , ("topological-sort", UnaryExpr topological_sort) + ] + +is_cyclic_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +is_cyclic_ = unaryOp is_cyclic +is_cyclic :: (Ord t, HasValues t) => OpExpr t -> OpExpr t +is_cyclic = vUnaryOp "is-cyclic" op + where op mm | Just m <- toGraph mm = Normal $ inject $ tobool (cyclic m) + op _ = SortErr "is-cyclic not applied to a graph" + +topological_sort_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +topological_sort_ = unaryOp topological_sort +topological_sort :: (Ord t, HasValues t) => OpExpr t -> OpExpr t +topological_sort = vUnaryOp "topological-sort" op + where op mm | Just m <- toGraph mm = Normal $ inject $ multi $ map inject $ fst (schedule m) + op _ = SortErr "topological-sort not applied to a graph" + +toGraph :: (Ord t) => Values t -> Maybe (Graph (Values t)) +toGraph (Map m) = M.foldrWithKey combine (Just M.empty) m + where combine k [Set s] mm = fmap (M.insert k s) mm + combine _ _ _ = Nothing +toGraph _ = Nothing + +-- small graph library +type Graph e = M.Map e (S.Set e) + +-- | Get the entry points of the graph +entries :: Eq e => Graph e -> [e] +entries m = M.keys m \\ withIncoming + where withIncoming = concatMap S.toList (M.elems m) + +-- | Delete a node from the graph +delete :: Ord e => e -> Graph e -> Graph e +delete n m = M.map (S.delete n) $ M.delete n m + +-- | Return all nodes in the graph such that if `a -> b` in the graph +-- then `a` occurs before `b` in the result +-- Also returns a graph which, if cyclic, contains all the cycles in the +-- original graph, corresponding to nodes not in the schedule. +schedule :: (Ord e) => Graph e -> ([e], Graph e) +schedule gr = schedule' gr (entries gr) [] + where schedule' gr [] uset = (uset, gr) + schedule' gr (e:es) uset = schedule' gr' (entries gr') uset' + where uset' = uset ++ [e] + gr' = delete e gr + +-- | Checks whether the given grammar contains cycles +cyclic :: (Ord e) => Graph e -> Bool +cyclic gr = not (is_empty (snd (schedule gr))) + +-- | Checks whether the given graph is empty +is_empty gr = M.null gr diff --git a/src/Funcons/Operations/Integers.hs b/src/Funcons/Operations/Integers.hs --- a/src/Funcons/Operations/Integers.hs +++ b/src/Funcons/Operations/Integers.hs @@ -6,6 +6,9 @@ import Funcons.Operations.Types import Funcons.Operations.Booleans (tobool) +import Data.Char +import Numeric + library :: HasValues t => Library t library = libFromList [ ("integers", NullaryExpr integers) @@ -35,6 +38,13 @@ , ("integer-list", BinaryExpr integer_list) , ("integer-absolute-value", UnaryExpr integer_absolute_value) , ("decimal-natural", UnaryExpr decimal_natural) + , ("decimal", UnaryExpr decimal_natural) + , ("hexadecimal-natural", UnaryExpr hexadecimal_natural) + , ("hexadecimal", UnaryExpr hexadecimal_natural) + , ("binary-natural", UnaryExpr binary_natural) + , ("binary", UnaryExpr binary_natural) + , ("octal-natural", UnaryExpr octal_natural) + , ("octal", UnaryExpr octal_natural) , ("natural-predecessor", UnaryExpr natural_predecessor) , ("nat-pred", UnaryExpr natural_predecessor) , ("natural-successor", UnaryExpr natural_successor) @@ -173,6 +183,36 @@ where op :: HasValues t => Values t -> Result t op s | isString_ s = Normal $ inject $ Nat (read (unString s)) | otherwise = SortErr "decimal-natural not applied to a string" + +binary_natural_ :: HasValues t => [OpExpr t] -> OpExpr t +binary_natural_ = unaryOp decimal_natural +binary_natural :: HasValues t => OpExpr t -> OpExpr t +binary_natural = vUnaryOp "binary-natural" op + where op :: HasValues t => Values t -> Result t + op s | isString_ s = case readInt 2 (`elem` ['0'..'1']) digitToInt (unString s) of + [(i,"")] -> Normal $ inject $ Nat i + _ -> SortErr "binary-natural not applied to a binary number" + | otherwise = SortErr "binary-natural not applied to a string" + +octal_natural_ :: HasValues t => [OpExpr t] -> OpExpr t +octal_natural_ = unaryOp decimal_natural +octal_natural :: HasValues t => OpExpr t -> OpExpr t +octal_natural = vUnaryOp "octal-natural" op + where op :: HasValues t => Values t -> Result t + op s | isString_ s = case readInt 8 (`elem` ['0'..'7']) digitToInt (unString s) of + [(i,"")] -> Normal $ inject $ Nat i + _ -> SortErr "octal-natural not applied to a octal number" + | otherwise = SortErr "octal-natural not applied to a string" + +hexadecimal_natural_ :: HasValues t => [OpExpr t] -> OpExpr t +hexadecimal_natural_ = unaryOp hexadecimal_natural +hexadecimal_natural :: HasValues t => OpExpr t -> OpExpr t +hexadecimal_natural = vUnaryOp "hexadecimal-natural" op + where op :: HasValues t => Values t -> Result t + op s | isString_ s = case readInt 16 (`elem` (['0'..'9'] ++ ['a'..'f'] ++ ['A'..'F'])) digitToInt (unString s) of + [(i,"")] -> Normal $ inject $ Nat i + _ -> SortErr "hexadecimal-natural not applied to a hexadecimal number" + | otherwise = SortErr "hexadecimal-natural not applied to a string" is_less_ :: HasValues t => [OpExpr t] -> OpExpr t is_less_ = binaryOp is_less diff --git a/src/Funcons/Operations/Multisets.hs b/src/Funcons/Operations/Multisets.hs --- a/src/Funcons/Operations/Multisets.hs +++ b/src/Funcons/Operations/Multisets.hs @@ -8,4 +8,62 @@ library :: (HasValues t, Ord t) => Library t library = libFromList [ + ("multisets", UnaryExpr Funcons.Operations.Multisets.multisets) + , ("multiset", NaryExpr multiset_) + , ("multiset-elements", UnaryExpr multiset_elements) + , ("multiset-occurrences", BinaryExpr multiset_occurrences) + , ("multiset-insert", BinaryExpr multiset_insert) + , ("multiset-delete", TernaryExpr multiset_delete) + , ("is-submultiset", BinaryExpr is_submultiset) ] + +multisets_ :: HasValues t => [OpExpr t] -> OpExpr t +multisets_ = unaryOp Funcons.Operations.Multisets.multisets +multisets :: HasValues t => OpExpr t -> OpExpr t +multisets = vUnaryOp "multisets" op + where op (ComputationType (Type t)) = + Normal $ injectT $ Funcons.Operations.Internal.multisets t + op _ = SortErr "multisets not applied to a type" + +multiset_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +multiset_ = vNaryOp "multiset" op + where op vs = Normal $ inject $ Multiset (MS.fromList vs) + +multiset_elements_ :: HasValues t => [OpExpr t] -> OpExpr t +multiset_elements_ = unaryOp multiset_elements +multiset_elements :: HasValues t => OpExpr t -> OpExpr t +multiset_elements = vUnaryOp "multiset-elements" op + where op (Multiset s) = Normal $ inject $ multi $ map inject $ MS.toList s + op _ = SortErr "multiset-elements not applied to a multiset" + +multiset_occurrences_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +multiset_occurrences_ = binaryOp multiset_occurrences +multiset_occurrences :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t +multiset_occurrences = vBinaryOp "multiset-occurrences" op + where op v (Multiset ms) = Normal $ inject $ Int count + where count = toInteger $ MS.occur v ms + op _ _ = SortErr "multiset-occurrences not applied to a value and a multiset" + +multiset_insert_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +multiset_insert_ = binaryOp multiset_insert +multiset_insert :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t +multiset_insert = vBinaryOp "multiset-insert" op + where op e (Multiset s) = Normal $ inject $ Multiset (e `MS.insert` s) + op _ _ = SortErr "second argument of multiset-insert is not a multiset" + +multiset_delete_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +multiset_delete_ = ternaryOp multiset_delete +multiset_delete :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t +multiset_delete = vTernaryOp "multiset-delete" op + where op (Multiset s) gv x | Nat n <- upcastNaturals x + = Normal $ inject $ Multiset (MS.deleteMany gv (fromInteger n) s) + op _ _ _ = SortErr "multiset-delete not applied to a multiset, a potential element, and a natural number" + +is_submultiset_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +is_submultiset_ = binaryOp is_submultiset +is_submultiset :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t +is_submultiset = vBinaryOp "is-submultiset" op + where op (Multiset s1) (Multiset s2) = Normal $ inject $ tobool (s1 `MS.isSubsetOf` s2) + op _ _ = SortErr "is-submultiset not applied to two multisets" + + diff --git a/src/Funcons/Operations/Sets.hs b/src/Funcons/Operations/Sets.hs --- a/src/Funcons/Operations/Sets.hs +++ b/src/Funcons/Operations/Sets.hs @@ -7,8 +7,6 @@ import qualified Data.Set as S -import System.IO.Unsafe (unsafePerformIO) - library :: (HasValues t, Ord t) => Library t library = libFromList [ ("set-empty", NullaryExpr set_empty) diff --git a/src/Funcons/Operations/Strings.hs b/src/Funcons/Operations/Strings.hs --- a/src/Funcons/Operations/Strings.hs +++ b/src/Funcons/Operations/Strings.hs @@ -26,8 +26,7 @@ stepTo_String s | isString_ s = Normal $ inject $ s stepTo_String (Rational r) = mk_string (show (fromRational r)) -stepTo_String (Ascii c) = mk_string ([c]) -stepTo_String (Char c) = mk_string ([c]) +stepTo_String v | Just c <- upcastCharacter v = mk_string ([c]) stepTo_String (Atom s) = mk_string s stepTo_String (Int i) = mk_string (show i) stepTo_String (Nat n) = mk_string (show n) diff --git a/src/Funcons/Operations/Types.hs b/src/Funcons/Operations/Types.hs --- a/src/Funcons/Operations/Types.hs +++ b/src/Funcons/Operations/Types.hs @@ -7,10 +7,6 @@ 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 @@ -86,13 +82,11 @@ tyOf :: HasValues t => Values t -> Types t tyOf (ADTVal "true" []) = ADT "booleans" [] tyOf (ADTVal "false" []) = ADT "booleans" [] +tyOf (ADTVal c [p]) | c == unicode_cons = UnicodeCharacters 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 @@ -139,11 +133,7 @@ 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 (Char _) AsciiCharacters = return True -isInType (Bit bv) (Bits n) = return (BV.size bv == n) +isInType v Characters | Just _ <- upcastCharacter v = return True isInType v (IntegersFrom n) | Int i <- upcastIntegers v = return (i >= n) isInType v (IntegersUpTo n) @@ -157,7 +147,10 @@ isInType v Integers | Int _ <- upcastIntegers v = return True isInType v Naturals | Nat _ <- upcastNaturals v = return True isInType v Rationals | Rational _ <- upcastRationals v = return True -isInType v UnicodeCharacters | Char _ <- upcastUnicode v = return True +isInType (ADTVal c [p]) UnicodeCharacters | c == unicode_cons = return True +isInType v AsciiCharacters = isInType v UnicodeCharacters -- requires interpreter to check whether character is in the character range +isInType v ISOLatinCharacters = isInType v UnicodeCharacters -- requires interpreter to check whether character is in the character range +isInType v BMPCharacters = isInType v UnicodeCharacters -- requires interpreter to check whether character is in the character range 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 diff --git a/src/Funcons/Operations/Values.hs b/src/Funcons/Operations/Values.hs --- a/src/Funcons/Operations/Values.hs +++ b/src/Funcons/Operations/Values.hs @@ -5,13 +5,12 @@ import qualified Data.Map as M import qualified Data.Vector as V import qualified Data.Set as S -import qualified Data.BitVector as BV import qualified Data.MultiSet as MS import qualified Data.Char as C import Data.Text (Text, pack, unpack) import Data.List (intercalate) -import Data.Maybe (fromJust) +import Data.Maybe (fromJust,isJust) import Data.String import Control.Monad (liftM2) @@ -26,10 +25,7 @@ -- such that there is a projection and injection between `t` and `Values t`, -- (see 'HasValues') data Values t = ADTVal Name [t] - | Ascii Char | Atom String - | Bit BV.BitVector - | Char Char | ComputationType (ComputationTypes t) | Float Double | IEEE_Float_32 Float @@ -46,6 +42,9 @@ | ValSeq [t] -- represents a multitude of values deriving (Eq,Ord,Show,Read) +ascii_cons = "ascii-character" +unicode_cons = "unicode-character" + tuple :: HasValues t => [Values t] -> Values t tuple = ADTVal "tuple" . map inject @@ -62,7 +61,7 @@ multi_ = multi . map inject instance HasValues t => IsString (Values t) where - fromString = ADTVal "list" . map (inject . Char) + fromString = ADTVal "list" . map (inject . mk_unicode_characters) type ValueMaps t = M.Map t [t] type ValueSets t = S.Set t @@ -85,8 +84,9 @@ | ADT Name [t] | AnnotatedType (Types t) SeqSortOp | AsciiCharacters + | ISOLatinCharacters + | BMPCharacters | Atoms - | Bits Int | IntegersFrom Integer -- value-dependent type | IntegersUpTo Integer | Characters @@ -145,10 +145,7 @@ vmap :: (Ord b) => (a -> b) -> Values a -> Values b vmap f v = case v of ADTVal nm ts -> ADTVal nm (map f ts) - Ascii a -> Ascii a Atom a -> Atom a - Bit b -> Bit b - Char c -> Char c ComputationType t -> ComputationType (fmap f t) Float f -> Float f IEEE_Float_32 f -> IEEE_Float_32 f @@ -172,10 +169,7 @@ (a -> m b) -> ([a] -> m [b]) -> Values a -> m (Values b) traverseVM f fs v = case v of ADTVal nm vs -> return . ADTVal nm =<< fs vs - Ascii a -> return $ Ascii a Atom a -> return $ Atom a - Bit b -> return $ Bit b - Char c -> return $ Char c ComputationType t -> return . ComputationType =<< traverseCTM f fs t Float f -> return $ Float f IEEE_Float_32 f -> return $ IEEE_Float_32 f @@ -203,9 +197,10 @@ ADTs -> return ADTs ADT nm ts -> return . ADT nm =<< fs ts AsciiCharacters -> return AsciiCharacters + ISOLatinCharacters -> return ISOLatinCharacters + BMPCharacters -> return BMPCharacters Atoms -> return Atoms AnnotatedType ty op -> AnnotatedType <$> traverseTM f fs ty <*> return op - Bits i -> return (Bits i) Characters -> return Characters ComputationTypes -> return ComputationTypes Complement t -> Complement <$> traverseTM f fs t @@ -256,18 +251,9 @@ | nm1 == nm2 -> Just $ comps vs1 vs2 (ADTVal _ _, _) -> Nothing (_, ADTVal _ _) -> Nothing - (Ascii x, Ascii u) | x == u -> Just (Just mempty) - (Ascii _, _) -> Nothing - (_, Ascii _) -> Nothing (Atom x, Atom y) | x == y -> Just (Just mempty) (Atom _, _) -> Nothing (_, Atom _) -> Nothing - (Bit x, Bit y) | x == y -> Just (Just mempty) - (_, Bit _) -> Nothing - (Bit _, _) -> Nothing - (Char x, Char y) | x == y -> Just (Just mempty) - (Char _, _) -> Nothing - (_, Char _) -> Nothing (ComputationType x ,ComputationType y) -> structCTMcompare comp comps x y (_, ComputationType x) -> Nothing @@ -327,12 +313,15 @@ (AsciiCharacters, AsciiCharacters) -> Just (Just mempty) (AsciiCharacters, _) -> Nothing (_, AsciiCharacters) -> Nothing + (ISOLatinCharacters, ISOLatinCharacters) -> Just (Just mempty) + (ISOLatinCharacters, _) -> Nothing + (_, ISOLatinCharacters) -> Nothing + (BMPCharacters, BMPCharacters) -> Just (Just mempty) + (BMPCharacters, _) -> Nothing + (_, BMPCharacters) -> Nothing (AnnotatedType t1 op1, AnnotatedType t2 op2) | op1 == op2 -> structTMcompare comp comps t1 t2 (AnnotatedType _ _, _) -> Nothing (_, AnnotatedType _ _) -> Nothing - (Bits x, Bits y) | x == y -> Just (Just mempty) - (Bits _, _) -> Nothing - (_, Bits _) -> Nothing (Characters, Characters) -> Just (Just mempty) (Characters, _) -> Nothing (_, Characters) -> Nothing @@ -385,9 +374,10 @@ ADT nm ts -> ADT nm (map f ts) ADTs -> ADTs AsciiCharacters -> AsciiCharacters + ISOLatinCharacters -> ISOLatinCharacters + BMPCharacters -> BMPCharacters Atoms -> Atoms AnnotatedType ty op -> AnnotatedType (fmap f ty) op - Bits n -> Bits n Complement t1 -> Complement (fmap f t1) ComputationTypes -> ComputationTypes IntegersFrom p -> IntegersFrom p @@ -416,9 +406,10 @@ ADT _ ts -> foldMap f ts ADTs -> mempty AsciiCharacters -> mempty + ISOLatinCharacters -> mempty + BMPCharacters -> mempty Atoms -> mempty AnnotatedType ty op -> foldMap f ty - Bits _ -> mempty Characters -> mempty Complement t1 -> foldMap f t1 ComputationTypes -> mempty @@ -441,9 +432,10 @@ ADTs -> pure ADTs ADT nm ts -> ADT nm <$> traverse f ts AsciiCharacters -> pure AsciiCharacters + ISOLatinCharacters -> pure ISOLatinCharacters + BMPCharacters -> pure BMPCharacters AnnotatedType ty op -> AnnotatedType <$> traverse f ty <*> pure op Atoms -> pure Atoms - Bits n -> pure $ Bits n Characters -> pure Characters Complement t -> Complement <$> traverse f t ComputationTypes -> pure ComputationTypes @@ -486,11 +478,10 @@ upcastNaturals (Int i) | i >= 0 = Nat i upcastNaturals v = v --- | Returns the /unicode/ representation of an assci value. --- Otherwise it returns the original value. -upcastUnicode :: Values t -> Values t -upcastUnicode (Ascii c) = Char c -upcastUnicode v = v +upcastCharacter :: HasValues t => Values t -> Maybe Char +upcastCharacter (ADTVal c [v]) + | Just (Int p) <- project v = Just (C.chr (fromInteger p)) +upcastCharacter v = Nothing castType :: HasValues t => Values t -> Maybe (Types t) castType (ComputationType (Type ty)) = Just ty @@ -506,14 +497,14 @@ mk_naturals :: Integer -> Values t mk_naturals = Nat -mk_unicode_characters :: Char -> Values t -mk_unicode_characters c | C.isAscii c = mk_ascii_characters c - | otherwise = Char c - --- TODO: haven't included `basic-characters` in the subtyping heirarchy yet. +mk_unicode_characters :: HasValues t => Char -> Values t +mk_unicode_characters = downcast_unicode_characters -mk_ascii_characters :: Char -> Values t -mk_ascii_characters = Ascii +-- | +-- Checks whetDoes not check whether the `unicode-point` of +downcast_unicode_characters :: HasValues t => Char -> Values t +downcast_unicode_characters c = + ADTVal unicode_cons [inject (Int (toInteger (C.ord c)))] --- Value specific @@ -525,10 +516,7 @@ isGround :: HasValues t => Values t -> Bool isGround (ADTVal _ mv) = all (maybe False isGround . project) mv -isGround (Ascii _) = True isGround (Atom _) = True -isGround (Bit _) = True -isGround (Char _) = True isGround (Float _) = True isGround (IEEE_Float_32 _) = True isGround (IEEE_Float_64 _) = True @@ -546,10 +534,6 @@ -- functions that check simple properties of funcons -- TODO: Some of these are used, and all are exported by Funcons.EDSL -- But are all of them still needed. E.g isId doesn't seem very useful now that ids are just strings. -isAscii ((Ascii _)) = True -isAscii _ = False -isChar ((Char _)) = True -isChar _ = False isNat ((Int _)) = True isNat _ = False isInt ((Int _)) = True @@ -560,7 +544,7 @@ isSet ((Set _)) = True isSet _ = False isString_ :: HasValues t => Values t -> Bool -isString_ (ADTVal "list" vs) = not (null vs) && all (maybe False (isChar . upcastUnicode)) (map project vs) +isString_ (ADTVal "list" vs) = not (null vs) && all (maybe False (isJust . upcastCharacter)) (map project vs) isString_ _ = False isType (ComputationType _) = True isType _ = False @@ -569,8 +553,8 @@ unString :: HasValues t => Values t -> String unString (ADTVal "list" vs) - | Just vs' <- sequence (map (fmap upcastUnicode . project) vs) - , all isChar vs' = map (\(Char c) -> c) vs' + | Just vs' <- sequence (map (fmap upcastCharacter . project) vs) + , all isJust vs' = map (\(Just c) -> c) vs' unString _ = error "unString" null__ :: Values t @@ -597,10 +581,6 @@ ppValues showT (ADTVal c []) = unpack c ppValues showT (ADTVal c vs) = unpack c ++ showArgs (map showT vs) ppValues showT (Atom c) = "atom("++ c ++")" -ppValues showT (Ascii c) = "`" ++ [c] ++ "`" -ppValues showT (Bit i) = "bits(" ++ show (BV.size i) - ++ ", " ++ show (BV.int i) ++ ")" -ppValues showT (Char c) = show c ppValues showT (Float f) = show f -- rationals ppValues showT (IEEE_Float_32 f) = show f @@ -633,8 +613,10 @@ ppTypes showT NullType = "null-type" ppTypes showT Atoms = "atoms" ppTypes showT AsciiCharacters = "ascii-characters" +ppTypes showT ISOLatinCharacters = "iso-latin-1-characters" +ppTypes showT BMPCharacters = "basic-multilingual-plane-characters" ppTypes showT Characters = "characters" -ppTypes showT (Intersection t1 t2) = "(" ++ ppTypes showT t1 ++ "^" ++ ppTypes showT t2 ++")" +ppTypes showT (Intersection t1 t2) = "(" ++ ppTypes showT t1 ++ "&" ++ ppTypes showT t2 ++")" ppTypes showT (IntegersFrom n) = "integers-from(" ++ show n ++ ")" ppTypes showT (IntegersUpTo n) = "integers-to(" ++ show n ++ ")" ppTypes showT EmptyType = "empty-type" @@ -644,7 +626,6 @@ ppTypes showT Types = "types" ppTypes showT ADTs = "algebraic-datatypes" ppTypes showT (ADT nm ts) = unpack nm ++ showArgs (map showT ts) -ppTypes showT (Bits n) = "bits(" ++ show n ++ ")" ppTypes showT (IEEEFloats format) = "ieee-floats(" ++ show format ++ ")" ppTypes showT Naturals = "naturals" ppTypes showT Rationals = "rationals"