funcons-values 0.1.0.5 → 0.1.0.7

raw patch · 11 files changed

+387/−97 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• funcons-values.cabal +2/−1
• src/Funcons/Operations.hs +6/−0
• src/Funcons/Operations/Bits.hs +117/−3
• src/Funcons/Operations/Characters.hs +56/−19
• src/Funcons/Operations/Graphs.hs +63/−0
• src/Funcons/Operations/Integers.hs +40/−0
• src/Funcons/Operations/Multisets.hs +58/−0
• src/Funcons/Operations/Sets.hs +0/−2
• src/Funcons/Operations/Strings.hs +1/−2
• src/Funcons/Operations/Types.hs +6/−13
• src/Funcons/Operations/Values.hs +38/−57

@@ -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 (<http://plancomps.org>) 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

@@ -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

@@ -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")+

@@ -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"

@@ -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

@@ -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

@@ -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"++

@@ -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)

@@ -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)

@@ -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

@@ -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"