funcons-values (empty) → 0.1.0.0

raw patch · 25 files changed

+2456/−0 lines, 25 filesdep +basedep +bvdep +containerssetup-changed

Dependencies added: base, bv, containers, multiset, random-strings, text, vector

Files

• LICENSE +20/−0
• Setup.hs +2/−0
• funcons-values.cabal +54/−0
• src/Funcons/Operations.hs +93/−0
• src/Funcons/Operations/ADTs.hs +59/−0
• src/Funcons/Operations/Atoms.hs +40/−0
• src/Funcons/Operations/Bits.hs +9/−0
• src/Funcons/Operations/Booleans.hs +50/−0
• src/Funcons/Operations/Characters.hs +53/−0
• src/Funcons/Operations/Eval.hs +33/−0
• src/Funcons/Operations/Expr.hs +165/−0
• src/Funcons/Operations/Floats.hs +238/−0
• src/Funcons/Operations/Integers.hs +185/−0
• src/Funcons/Operations/Internal.hs +10/−0
• src/Funcons/Operations/Libraries.hs +18/−0
• src/Funcons/Operations/Lists.hs +89/−0
• src/Funcons/Operations/Maps.hs +142/−0
• src/Funcons/Operations/Multisets.hs +11/−0
• src/Funcons/Operations/NonGroundValues.hs +31/−0
• src/Funcons/Operations/Optionals.hs +37/−0
• src/Funcons/Operations/Sets.hs +129/−0
• src/Funcons/Operations/Strings.hs +37/−0
• src/Funcons/Operations/Tuples.hs +45/−0
• src/Funcons/Operations/Types.hs +171/−0
• src/Funcons/Operations/Values.hs +735/−0

@@ -0,0 +1,20 @@+Copyright (c) 2016 L. Thomas van Binsbergen and Neil Sculthorpe++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,54 @@+-- Initial funcons-values.cabal generated by cabal init.  For further+-- documentation, see http://haskell.org/cabal/users-guide/++name:                funcons-values+version:             0.1.0.0+synopsis:            Library providing values and operations on values.+-- description:+homepage:            http://plancomps.org+license:             MIT+license-file:        LICENSE+author:              L. Thomas van Binsbergen and Neil Sculthorpe+maintainer:          L. Thomas van Binsbergen <ltvanbinsbergen@acm.org>+-- copyright:+category:            Compilers/Interpreters+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++library+  exposed-modules:     Funcons.Operations+  other-modules:       Funcons.Operations.Eval+                      ,Funcons.Operations.Libraries+                      ,Funcons.Operations.Expr+                      ,Funcons.Operations.Values+                      ,Funcons.Operations.Types+                      ,Funcons.Operations.Atoms+                      ,Funcons.Operations.ADTs+                      ,Funcons.Operations.Booleans+                      ,Funcons.Operations.Optionals+--                      ,Funcons.Operations.Rationals+                      ,Funcons.Operations.Integers+                      ,Funcons.Operations.Floats+                      ,Funcons.Operations.Strings+                      ,Funcons.Operations.Lists+                      ,Funcons.Operations.Tuples+                      ,Funcons.Operations.NonGroundValues+                      ,Funcons.Operations.Multisets +                      ,Funcons.Operations.Sets +                      ,Funcons.Operations.Bits +                      ,Funcons.Operations.Characters+                      ,Funcons.Operations.Maps+                      ,Funcons.Operations.Internal+  other-extensions:    InstanceSigs, OverloadedStrings+  build-depends:       base >=4.8 && <5+                      ,containers >=0.5 && <0.6+                      ,vector >=0.12+                      ,bv >=0.5+                      ,multiset >=0.3 && <0.4+                      ,text >=1.2 && <1.3+                      ,random-strings+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -fwarn-incomplete-patterns -fwarn-monomorphism-restriction -fwarn-unused-imports+

@@ -0,0 +1,93 @@++module Funcons.Operations (+  module Funcons.Operations.Atoms,+  module Funcons.Operations.ADTs,+  module Funcons.Operations.Expr,+  module Funcons.Operations.Values,+  module Funcons.Operations.Eval,+  module Funcons.Operations.Lists,+  module Funcons.Operations.Tuples,+  module Funcons.Operations.Booleans,+  module Funcons.Operations.Optionals,+  module Funcons.Operations.Types,+  module Funcons.Operations.NonGroundValues,+  module Funcons.Operations.Integers,+  module Funcons.Operations.Floats,+  module Funcons.Operations.Strings,+--  module Funcons.Operations.Rationals,+  module Funcons.Operations.Sets,+  module Funcons.Operations.Multisets,+  module Funcons.Operations.Bits,+  module Funcons.Operations.Characters,+  module Funcons.Operations.Maps,+  libApp, Funcons.Operations.library, Library+  ) where++import Funcons.Operations.Expr +import Funcons.Operations.Libraries +import Funcons.Operations.Values hiding (showArgs, isGround, set_)+import Funcons.Operations.Eval hiding (showArgs)+import Funcons.Operations.Atoms hiding (library)+import qualified Funcons.Operations.Atoms (library)+import Funcons.Operations.Booleans hiding (library)+import qualified Funcons.Operations.Booleans (library)+import Funcons.Operations.Optionals hiding (library)+import qualified Funcons.Operations.Optionals (library)+import Funcons.Operations.Lists hiding (library)+import qualified Funcons.Operations.Lists (library)+import Funcons.Operations.Tuples hiding (library)+import qualified Funcons.Operations.Tuples (library)+import Funcons.Operations.Types hiding (library)+import qualified Funcons.Operations.Types (library)+import Funcons.Operations.NonGroundValues hiding (library, isGround)+import qualified Funcons.Operations.NonGroundValues (library)+import Funcons.Operations.Integers hiding (isInt, unInt, library)+import qualified Funcons.Operations.Integers (library)+import Funcons.Operations.Floats hiding (isInt, unInt, library)+import qualified Funcons.Operations.Floats (library)+import Funcons.Operations.Strings hiding (library)+import qualified Funcons.Operations.Strings (library)+--import Funcons.Operations.Rationals hiding (library)+--import qualified Funcons.Operations.Rationals (library)+import Funcons.Operations.Sets hiding (library)+import qualified Funcons.Operations.Sets (library)+import qualified Funcons.Operations.Multisets (library)+import qualified Funcons.Operations.Bits (library)+import Funcons.Operations.Characters hiding (library)+import qualified Funcons.Operations.Characters (library)+import Funcons.Operations.Maps hiding (library)+import qualified Funcons.Operations.Maps (library)+import Funcons.Operations.ADTs hiding (library)+import qualified Funcons.Operations.ADTs++library :: (HasValues t, Ord t) => Library t+library = libUnite [+    Funcons.Operations.Atoms.library+  , Funcons.Operations.ADTs.library+  , Funcons.Operations.Booleans.library+  , Funcons.Operations.Optionals.library+  , Funcons.Operations.Lists.library+  , Funcons.Operations.Tuples.library+  , Funcons.Operations.Types.library+  , Funcons.Operations.NonGroundValues.library+  , Funcons.Operations.Integers.library+  , Funcons.Operations.Floats.library+  , Funcons.Operations.Strings.library+--  , Funcons.Operations.Rationals.library+  , Funcons.Operations.Sets.library+  , Funcons.Operations.Multisets.library+  , Funcons.Operations.Bits.library+  , Funcons.Operations.Characters.library+  , Funcons.Operations.Maps.library+  ]++libApp :: (HasValues t, Ord t) => OP -> [OpExpr t] -> Maybe (OpExpr t)+libApp op args = do +  valop <- libLookup op Funcons.Operations.library+  case (args, valop) of+    ([], NullaryExpr op)      -> Just op+    ([x], UnaryExpr op)       -> Just (op x)+    ([x,y], BinaryExpr op)    -> Just (op x y)+    ([x,y,z], TernaryExpr op) -> Just (op x y z)+    (_, NaryExpr op)          -> Just (op args)+    _                         -> Nothing

@@ -0,0 +1,59 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.ADTs where++import Funcons.Operations.Internal++import Data.Maybe (fromJust, isJust)+import Data.Text (pack, unpack)+import Data.String(fromString)++library :: HasValues t => Ord t => Library t+library = libFromList [+    ("adts", NullaryExpr adts)+  , ("adt-construct", NaryExpr adt_construct_)+  , ("adt-type", NaryExpr adt_type_construct_)+  , ("adt-type-construct", NaryExpr adt_type_construct_)+  , ("adt-constructor", UnaryExpr adt_constructor)+  , ("adt-fields", UnaryExpr adt_fields)+  ]++adts_ :: HasValues t => [OpExpr t] -> OpExpr t+adts_ = nullaryOp adts+adts :: HasValues t => OpExpr t+adts = NullaryOp "adts" (Normal $ injectT ADTs)++adt_construct_ :: HasValues t => [OpExpr t] -> OpExpr t+adt_construct_ = NaryOp "adt-construct" op+  where op :: HasValues t => [t] -> Result t+        op (x : vs) = case project x of+          Just v -> +            if isString_ v +              then Normal $ inject $ ADTVal (pack (unString v)) vs+              else SortErr "adt-construct: first argument not a string"+          _      -> ProjErr "adt-construct"+        op _  = SortErr "adt-construct: insufficient arguments"++adt_type_construct_ :: HasValues t => [OpExpr t] -> OpExpr t+adt_type_construct_ = vNaryOp "adt-type-construct" op+  where op (s : vs) +          | isString_ s =   +              if all isType vs +                then Normal $ injectT $ ADT (pack (unString s))+                              (map (injectT . fromJust . castType) vs)  +                else SortErr "adt-type-construct: last arguments not types" +        op _  = SortErr "adt-construct: first argument not a string"++adt_constructor_ :: HasValues t => [OpExpr t] -> OpExpr t+adt_constructor_ = unaryOp adt_constructor+adt_constructor :: HasValues t => OpExpr t -> OpExpr t+adt_constructor = vUnaryOp "adt-constructor" op+  where op (ADTVal cons _) = Normal $ inject $ fromString (unpack cons)+        op _ = SortErr "adt-constructor: argument not an adt value"++adt_fields_ :: HasValues t => [OpExpr t] -> OpExpr t+adt_fields_ = unaryOp adt_fields+adt_fields :: HasValues t => OpExpr t -> OpExpr t+adt_fields = vUnaryOp "adt-fields" op+  where op (ADTVal _ fs) = Normal $ inject $ ADTVal "list" fs +        op _ = SortErr "adt-fields: argument not an adt value"

@@ -0,0 +1,40 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Atoms where++import Funcons.Operations.Internal++library :: (HasValues t, Eq t) => Library t+library = libFromList [+    ("atoms", NullaryExpr atoms)+  , ("next-atom", UnaryExpr next_atom)+  , ("atom-seed", NullaryExpr atom_seed)+  , ("atom", UnaryExpr atom)+  ]++atom_seed_ :: HasValues t => [OpExpr t] -> OpExpr t+atom_seed_ = nullaryOp atom_seed +atom_seed :: HasValues t => OpExpr t+atom_seed = vNullaryOp "atom-seed" (Normal $ inject $ Atom "0")++next_atom_ :: HasValues t => [OpExpr t] -> OpExpr t+next_atom_ = unaryOp next_atom+next_atom :: HasValues t => OpExpr t -> OpExpr t+next_atom = vUnaryOp "next-atom" op+  where op (Atom a) = Normal $ inject $ Atom (show (i+1))+          where i::Int+                i = read a+        op _ = SortErr "next-atom not applied to an atom"++atoms_ :: HasValues t => [OpExpr t] -> OpExpr t+atoms_ = nullaryOp atoms+atoms :: HasValues t => OpExpr t+atoms = vNullaryOp "atoms" (Normal $ injectT Atoms)++atom_ :: HasValues t => [OpExpr t] -> OpExpr t+atom_ = unaryOp atom++atom :: HasValues t => OpExpr t -> OpExpr t+atom = vUnaryOp "atom" op+  where op v | isString_ v = Normal $ inject $ Atom (unString v)+             | otherwise   = SortErr "atom not applied to a string"  

@@ -0,0 +1,9 @@++module Funcons.Operations.Bits where++import Funcons.Operations.Booleans (tobool)+import Funcons.Operations.Internal++library :: (HasValues t, Ord t) => Library t+library = libFromList []+ 

@@ -0,0 +1,50 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Booleans where++import Funcons.Operations.Internal++library :: (HasValues t, Eq t) => Library t+library = libFromList [+    ("is-equal", BinaryExpr is_equal)+--  , ("booleans", NullaryExpr booleans_)+--  , ("and", BinaryExpr stepAnd)+  ]++tobool :: Bool -> Values t +tobool True   = ADTVal "true" []+tobool False  = ADTVal "false" [] ++frombool :: (Values t) -> Maybe Bool+frombool (ADTVal "true" []) = Just True+frombool (ADTVal "false" []) = Just False+frombool _ = Nothing+++{-+and_ :: HasValues t => [OpExpr t] -> OpExpr t +and_ = binaryOp stepAnd+stepAnd :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+stepAnd = vBinaryOp "and" op+  where op x y = case (frombool x, frombool y) of +          (Just b1, Just b2) -> Normal $ inject $ tobool (b1 && b2)+          _ -> SortErr "and not applied to two booleans"+-}+booleans_ :: HasValues t => OpExpr t+booleans_ = vNullaryOp "booleans" (Normal $ injectT $ ADT "booleans" [])++true_ :: HasValues t => Values t +true_ = tobool True++false_ :: HasValues t => Values t +false_ = tobool False +++is_equal_ :: (HasValues t, Eq t) => [OpExpr t] -> OpExpr t+is_equal_ = binaryOp is_equal+is_equal :: (HasValues t, Eq t) => OpExpr t -> OpExpr t -> OpExpr t+is_equal = BinaryOp "is-equal" op +  where op :: (Eq t, HasValues t) => t -> t -> Result t+        op x y = Normal $ inject $ tobool (x == y)++

@@ -0,0 +1,53 @@++module Funcons.Operations.Characters where++import Funcons.Operations.Booleans (tobool)+import Funcons.Operations.Internal++import Data.Char (ord,chr)++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)+  , ("characters", NullaryExpr characters)+  ]++characters_ :: HasValues t => [OpExpr t] -> OpExpr t+characters_ = nullaryOp characters+characters :: HasValues t => OpExpr t+characters = vNullaryOp "characters" (Normal $ injectT $ Characters)++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)++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, s <- unString v, length s == 1 +                = Normal $ inject $ Ascii $ head s+             | 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 = +                Normal $ inject $ mk_unicode_characters (chr $ fromInteger i)+             | otherwise = SortErr "unicode not applied to an integer in the range 0..(2^32)-1"++numUnicodeCodes :: Integer+numUnicodeCodes = (2^32)-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 = +                  Normal $ inject $ mk_integers (toInteger $ ord c)+             | otherwise = SortErr "unicode-character-code not applied to a unicode-character"

@@ -0,0 +1,33 @@++module Funcons.Operations.Eval where++import Funcons.Operations.Expr+import Funcons.Operations.Values hiding (showArgs)++import Control.Monad+import Data.List (intercalate)++data EvalResult t = Error         (OpExpr t) (Result t)+                  | Success       t+                  deriving (Show)++eval :: HasValues t => OpExpr t -> EvalResult t+eval expr = applyEval expr (applyExpr expr) ++applyEval :: OpExpr t -> Result t -> EvalResult t+applyEval expr (Normal v) = Success v+applyEval expr res = Error expr res + +instance (HasValues t, Show t) => Show (OpExpr t) where+  show (ValExpr v)            = ppValues show v+  show (TermExpr t)           = show t+  show (NullaryOp nm _)       = nm+  show (UnaryOp nm _ x)       = nm ++ showArgs [x]+  show (BinaryOp nm _ x y)    = nm ++ showArgs [x,y]+  show (TernaryOp nm _ x y z) = nm ++ showArgs [x,y,z]+  show (NaryOp nm _ xs)       = nm ++ showArgs xs+  show (InvalidOp nm _ xs)    = nm ++ showArgs xs+  show (RewritesTo nm _ xs)   = nm ++ showArgs xs++showArgs :: (HasValues t, Show t) => [OpExpr t] -> String+showArgs args = "(" ++ intercalate "," (map show args) ++ ")"

@@ -0,0 +1,165 @@+{-# LANGUAGE InstanceSigs #-}++module Funcons.Operations.Expr where++import Funcons.Operations.Values+import Control.Monad (ap)++type OP = String++data Result t = SortErr     String -- sort mismatch+              | DomErr      String -- domain mismatch (in case of partial op)+              | ArityErr    String+              | ProjErr     String -- cannot project to a value+              | Normal      t +              deriving Show+ +type NullaryOp t  = Result t+type UnaryOp t    = t -> Result t+type BinaryOp t   = t -> t -> Result t+type TernaryOp t  = t -> t -> t -> Result t+type NaryOp t     = [t] -> Result t++type NullaryVOp t  = Result t+type UnaryVOp t    = Values t -> Result t+type BinaryVOp t   = Values t -> Values t -> Result t+type TernaryVOp t  = Values t -> Values t -> Values t -> Result t+type NaryVOp t     = [Values t] -> Result t++data OpExpr t  +      = ValExpr         (Values t)+      | TermExpr        t  +      | NullaryOp   OP  (NullaryOp t)                                    +      | UnaryOp     OP  (UnaryOp t)     (OpExpr t)                       +      | BinaryOp    OP  (BinaryOp t)    (OpExpr t) (OpExpr t)            +      | TernaryOp   OP  (TernaryOp t)   (OpExpr t) (OpExpr t) (OpExpr t) +      | NaryOp      OP  (NaryOp t)      [OpExpr t]  +      | InvalidOp   OP  String          [OpExpr t]+      | RewritesTo  OP  (OpExpr t)      [OpExpr t]++vNullaryOp :: OP -> NullaryVOp t -> OpExpr t+vNullaryOp nm op = NullaryOp nm op++vUnaryOp :: HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t+vUnaryOp nm op = UnaryOp nm op'+  where op' t = case project t of+                  Nothing -> ProjErr nm+                  Just v  -> op v++vBinaryOp :: HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t+vBinaryOp nm op = BinaryOp nm op'+  where op' x y = case (project x, project y) of+                  (Just v1,Just v2) -> op v1 v2 +                  _                 -> ProjErr nm++vTernaryOp :: HasValues t => OP -> TernaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t+vTernaryOp nm op = TernaryOp nm op'+  where op' x y z = case (project x, project y, project z) of+                  (Just v1,Just v2, Just v3)  -> op v1 v2 v3+                  _                           -> ProjErr nm++vNaryOp :: HasValues t => OP -> NaryVOp t -> [OpExpr t] -> OpExpr t+vNaryOp nm op = NaryOp nm op'+  where op' ts = case mapM project ts of+                  Just vs -> op vs+                  Nothing -> ProjErr nm++opName :: OpExpr t -> OP+opName (ValExpr _) = error "opName val"+opName (TermExpr _) = error "opName term"+opName (NullaryOp op _) = op+opName (UnaryOp op _ _) = op+opName (BinaryOp op _ _ _) = op+opName (TernaryOp op _ _ _ _) = op+opName (NaryOp op _ _) = op+opName (InvalidOp op _ _) = op+opName (RewritesTo op _ _) = op++data ValueOp t      = NullaryExpr (NullaryExpr t)+                    | UnaryExpr (UnaryExpr t)+                    | BinaryExpr (BinaryExpr t)+                    | TernaryExpr (TernaryExpr t)+                    | NaryExpr (NaryExpr t)++type NullaryExpr t  = OpExpr  t+type UnaryExpr t    = OpExpr t -> OpExpr  t+type BinaryExpr t   = OpExpr t -> OpExpr t -> OpExpr  t+type TernaryExpr t  = OpExpr t -> OpExpr t -> OpExpr t -> OpExpr  t+type NaryExpr t     = [OpExpr t] -> OpExpr t++nullaryOp :: NullaryExpr t ->  [OpExpr t] -> OpExpr t+nullaryOp f [] = f+nullaryOp f xs = arityErr 0 (opName f) xs++unaryOp :: UnaryExpr t ->  [OpExpr t] -> OpExpr t+unaryOp f [x] = f x+unaryOp f xs = arityErr 1 (opName (f undefined)) xs++binaryOp :: BinaryExpr t ->  [OpExpr t] -> OpExpr t+binaryOp f [x,y] = f x y+binaryOp f xs = arityErr 2 (opName (f undefined undefined)) xs++ternaryOp :: TernaryExpr t -> [OpExpr t] -> OpExpr t+ternaryOp f [x,y,z] = f x y z +ternaryOp f xs = arityErr 3 (opName (f undefined undefined undefined)) xs++arityErr :: Int -> OP -> [OpExpr t] -> OpExpr t+arityErr i op = InvalidOp op ("not applied to " ++ show i ++ " arguments")++applyExpr :: HasValues t => OpExpr t -> Result t+applyExpr expr = case expr of+  ValExpr v                     -> Normal (inject v)+  TermExpr t                    -> Normal t+  InvalidOp _ err _             -> ArityErr err+  NullaryOp _ f                 -> f+  UnaryOp _ f x                 -> f =<< applyExpr x+  BinaryOp _ f x y              -> do   xv <- applyExpr x +                                        yv <- applyExpr y+                                        f xv yv+  TernaryOp _ f x y z           -> do   xv <- applyExpr x+                                        yv <- applyExpr y+                                        zv <- applyExpr z+                                        f xv yv zv+  NaryOp _ f xs                 -> f =<< mapM applyExpr xs+  RewritesTo _ e1 _             -> applyExpr e1++instance Functor Result where+  fmap f (SortErr err)  = SortErr err+  fmap f (ProjErr err)  = ProjErr err+  fmap f (DomErr err)   = DomErr err+  fmap f (ArityErr err) = ArityErr err+  fmap f (Normal v)     = Normal (f v)++instance Applicative Result where+  pure = Normal+  (<*>) = ap++instance Monad Result where+  return = Normal+  p >>= q = case p of+    SortErr err   -> SortErr err+    ProjErr err   -> ProjErr err+    DomErr err    -> DomErr err+    ArityErr err  -> ArityErr err+    Normal f      -> q f ++-- helper / smart constructors+{-+nullaryOp :: OP -> Result t -> OpExpr t+nullaryOp = NullaryOp++unaryOp :: IsOperand o => OP -> o t -> UnaryOp t -> OpExpr t+unaryOp nm o res = UnaryOp nm (toOp o) res++binaryOp :: (IsOperand o1, IsOperand o2) => OP -> o1 t -> o2 t -> BinaryOp t -> OpExpr t+binaryOp nm x y res = BinaryOp nm (toOp x) (toOp y) res++ternaryOp :: IsOperand o => OP -> o t -> o t -> o t -> TernaryOp t -> OpExpr t+ternaryOp nm x y z op = TernaryOp nm (toOp x) (toOp y) (toOp z) op++naryOp :: IsOperand o => OP -> [o t] -> NaryOp t -> OpExpr t+naryOp nm xs op = NaryOp nm (map toOp xs) op++rewritesTo :: (IsOperand o1, IsOperand o2) => OP -> [o1 t] -> o2 t -> OpExpr t +rewritesTo nm xs op = RewritesTo nm (map toOp xs) (toOp op)+-}

@@ -0,0 +1,238 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Floats where++import Funcons.Operations.Internal hiding (isInt)+import Funcons.Operations.Types+import Funcons.Operations.Booleans (tobool)++library :: HasValues t => Library t+library = libFromList [+  ]++ieee_float_truncate_ :: HasValues t => [OpExpr t] -> OpExpr t+ieee_float_truncate_ = binaryOp ieee_float_truncate +ieee_float_truncate :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+ieee_float_truncate = vBinaryOp "ieee-float-truncate" op+  where op (IEEE_Float_64 f) (ADTVal "binary64" _) = Normal $ inject $ Int (truncate f)+        op _ _ = SortErr "ieee-float-truncate not applied to a float of the right format"++ieee_float_add_ :: HasValues t => [OpExpr t] -> OpExpr t+ieee_float_add_ = vNaryOp "ieee-float-add" op+  where op (format:vs) = ieee_float_op "ieee-float-add" (+) 0 format vs+        op [] = SortErr "ieee-float-add not applied to a format and a list of floats"++{-+ieee_float_multiply_ = ieee_float_multiply +ieee_float_multiply = applyFuncon "ieee-float-multiply"+ieee_float_multiply_op (format:vs) = ieee_float_op "ieee_float-multiply" ieee_float_multiply (*) 1 format vs+ieee_float_multiply_op [] = sortErr (ieee_float_multiply [listval []]) "ieee-float-multiply not applied to a format and a list of floats"++ieee_float_divide = applyFuncon "ieee-float-divide"+ieee_float_divide_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ IEEE_Float_64 $ (f1 / f2)+ieee_float_divide_op ft vx vy = sortErr (ieee_float_divide [FValue ft,FValue vx, FValue vy])+                         "ieee-float-divide not applied to a format and ieee-floats"++ieee_float_remainder = applyFuncon "ieee-float-remainder"+ieee_float_remainder_op format vx vy+    | isIEEEFormat format vx =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ IEEE_Float_64 $ (f1 `mod'` f2)+ieee_float_remainder_op ft vx vy = sortErr (ieee_float_remainder [FValue ft,FValue vx, FValue vy])+                         "ieee-float-remainder not applied to a format and ieee-floats"++ieee_float_negate = applyFuncon "ieee-float-negate"+ieee_float_negate_op format vx+    | isIEEEFormat format vx = let f1 = doubleFromIEEEFormat format vx+                               in rewriteTo $ FValue $ IEEE_Float_64 (-f1)+    | otherwise = sortErr (ieee_float_negate [FValue format,FValue vx]) "ieee-float-negate not applied to ieee-float"++ieee_float_subtract = applyFuncon "ieee-float-subtract"+ieee_float_subtract_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ IEEE_Float_64 $ (f1 - f2)+ieee_float_subtract_op ft vx vy = sortErr (ieee_float_subtract [FValue ft, FValue vx, FValue vy])+                         "ieee-float-subtract not applied to a format and ieee-floats"++ieee_float_float_power = applyFuncon "ieee-float-float-power"+ieee_float_power_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ IEEE_Float_64 $ (f1 ** f2)+ieee_float_power_op ft vx vy = sortErr (ieee_float_float_power [FValue ft, FValue vx, FValue vy])+                         "ieee-float-power not applied to a format and ieee-floats"++ieee_float_is_less = applyFuncon "ieee-float-is-less"+ieee_float_is_less_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ tobool (f1 < f2)+ieee_float_is_less_op ft vx vy = sortErr (ieee_float_is_less [FValue ft, FValue vx, FValue vy])+                         "ieee-float-is-less not applied to a format and ieee-floats"++ieee_float_is_greater = applyFuncon "ieee-float-is-greater"+ieee_float_is_greater_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ tobool (f1 > f2)+ieee_float_is_greater_op ft vx vy = sortErr (ieee_float_is_greater [FValue ft, FValue vx, FValue vy])+                         "ieee-float-is-greater not applied to a format and ieee-floats"++ieee_float_is_less_or_equal = applyFuncon "ieee-float-is-less-or-equal"+ieee_float_is_less_or_equal_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ tobool (f1 <= f2)+ieee_float_is_less_or_equal_op ft vx vy = sortErr (ieee_float_is_less_or_equal [FValue ft,FValue vx, FValue vy])+                         "ieee-float-is-less-or-equal not applied to a format and ieee-floats"++ieee_float_is_greater_or_equal = applyFuncon "ieee-float-is-greater-or-equal"+ieee_float_is_greater_or_equal_op format vx vy+    | isIEEEFormat format vx && isIEEEFormat format vy =+        let f1 = doubleFromIEEEFormat format vx+            f2 = doubleFromIEEEFormat format vy+        in rewriteTo $ FValue $ tobool (f1 >= f2)+ieee_float_is_greater_or_equal_op ft vx vy = sortErr (ieee_float_is_greater_or_equal [FValue ft,FValue vx, FValue vy])+                         "ieee-float-is-greater-or-equal not applied to a format and ieee-floats"+++signed_bits_maximum = applyFuncon "signed-bits-maximum"+stepSigned_Bits_Maximum [vn] | Nat n <- upcastNaturals vn+        = rewriteTo $ integer_subtract_ [integer_power_ [int_ 2, integer_subtract_ [int_ $ fromInteger n, int_ 1]],int_ 1]+stepSigned_Bits_Maximum vs = sortErr (signed_bits_maximum (fvalues vs)) "sort check"++signed_bits_minimum = applyFuncon "signed-bits-minimum"+stepSigned_Bits_Minimum [vn] | Nat n <- upcastNaturals vn+        = rewriteTo $ applyFuncon "integer-negate" [signed_bits_maximum [FValue vn]]+stepSigned_Bits_Minimum vs = sortErr (signed_bits_maximum (fvalues vs)) "sort check"++    -- TODO binary64 assumption (perhaps use config files)+ieee_float_acos = applyFuncon "ieee-float-acos"+stepIEEE_Float_Acos [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (acos f1)+stepIEEE_Float_Acos vn = sortErr (ieee_float_acos (fvalues vn)) "sort check"++ieee_float_asin = applyFuncon "ieee-float-asin"+stepIEEE_Float_Asin [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (asin f1)+stepIEEE_Float_Asin vn = sortErr (ieee_float_asin (fvalues vn)) "sort check"++ieee_float_atan = applyFuncon "ieee-float-atan"+stepIEEE_Float_Atan [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (atan f1)+stepIEEE_Float_Atan vn = sortErr (ieee_float_atan (fvalues vn)) "sort check"++ieee_float_atan2 = applyFuncon "ieee-float-atan2"+stepIEEE_Float_Atan2 [f,vx,vy] = let f1 = doubleFromIEEEFormat f vx+                                     f2 = doubleFromIEEEFormat f vy+                                 in rewriteTo $ FValue $ IEEE_Float_64 (atan2 f1 f2)+stepIEEE_Float_Atan2 vn = sortErr (ieee_float_atan2 (fvalues vn)) "sort check"++ieee_float_cos = applyFuncon "ieee-float-cos"+stepIEEE_Float_Cos [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (cos f1)+stepIEEE_Float_Cos vn = sortErr (ieee_float_cos (fvalues vn)) "sort check"++ieee_float_cosh = applyFuncon "ieee-float-cosh"+stepIEEE_Float_Cosh [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (cosh f1)+stepIEEE_Float_Cosh vn = sortErr (ieee_float_cosh (fvalues vn)) "sort check"++ieee_float_exp = applyFuncon "ieee-float-exp"+stepIEEE_Float_Exp [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (exp f1)+stepIEEE_Float_Exp vn = sortErr (ieee_float_exp (fvalues vn)) "sort check"++ieee_float_log = applyFuncon "ieee-float-log"+stepIEEE_Float_Log [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (log f1)+stepIEEE_Float_Log vn = sortErr (ieee_float_log (fvalues vn)) "sort check"++ieee_float_log10 = applyFuncon "ieee-float-log10"+stepIEEE_Float_Log10 [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (logBase 10 f1)+stepIEEE_Float_Log10 vn = sortErr (ieee_float_log10 (fvalues vn)) "sort check"++ieee_float_sin = applyFuncon "ieee-float-sin"+stepIEEE_Float_Sin [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (sin f1)+stepIEEE_Float_Sin vn = sortErr (ieee_float_sin (fvalues vn)) "sort check"++ieee_float_sinh = applyFuncon "ieee-float-sinh"+stepIEEE_Float_Sinh [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (sinh f1)+stepIEEE_Float_Sinh vn = sortErr (ieee_float_sinh (fvalues vn)) "sort check"++ieee_float_sqrt = applyFuncon "ieee-float-sqrt"+stepIEEE_Float_Sqrt [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (sqrt f1)+stepIEEE_Float_Sqrt vn = sortErr (ieee_float_sqrt (fvalues vn)) "sort check"++ieee_float_tan = applyFuncon "ieee-float-tan"+stepIEEE_Float_Tan [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (tan f1)+stepIEEE_Float_Tan vn = sortErr (ieee_float_tan (fvalues vn)) "sort check"++ieee_float_tanh = applyFuncon "ieee-float-tanh"+stepIEEE_Float_Tanh [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (tanh f1)+stepIEEE_Float_Tanh vn = sortErr (ieee_float_tanh (fvalues vn)) "sort check"++ieee_float_ceiling = applyFuncon "ieee-float-ceiling"+stepIEEE_Float_Ceiling [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ int_ (ceiling f1)+stepIEEE_Float_Ceiling vn = sortErr (ieee_float_ceiling (fvalues vn)) "sort check"++ieee_float_floor = applyFuncon "ieee-float-floor"+stepIEEE_Float_Floor [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ int_ (floor f1)+stepIEEE_Float_Floor vn = sortErr (ieee_float_floor (fvalues vn)) "sort check"++ieee_float_absolute_value = applyFuncon "ieee-float-absolute-value"+stepIEEE_Float_Absolute_Value [f,vx] = let f1 = doubleFromIEEEFormat f vx+                                     in rewriteTo $ FValue $ IEEE_Float_64 (Prelude.abs f1)+stepIEEE_Float_Absolute_Value vn = sortErr (ieee_float_absolute_value (fvalues vn)) "sort check"++stepIEEE_Float_Remainder [f,f1,f2] = ieee_float_remainder_op f f1 f2+stepIEEE_Float_Remainder vn = sortErr (ieee_float_remainder (fvalues vn)) "sort check"++stepIEEE_Float_Is_Less [f,f1,f2] = ieee_float_is_less_op f f1 f2+stepIEEE_Float_Is_Less vn = sortErr (ieee_float_is_less (fvalues vn)) "sort check"+stepIEEE_Float_Is_Greater [f,f1,f2] = ieee_float_is_greater_op f f1 f2+stepIEEE_Float_Is_Greater vn = sortErr (ieee_float_is_greater (fvalues vn)) "sort check"+stepIEEE_Float_Is_Less_Or_Equal [f,f1,f2] = ieee_float_is_less_or_equal_op f f1 f2+stepIEEE_Float_Is_Less_Or_Equal vn = sortErr (ieee_float_is_less_or_equal (fvalues vn)) "sort check"+stepIEEE_Float_Is_Greater_Or_Equal [f,f1,f2] = ieee_float_is_greater_or_equal_op f f1 f2+stepIEEE_Float_Is_Greater_Or_Equal vn = sortErr (ieee_float_is_greater_or_equal (fvalues vn)) "sort check"+-}++ieee_float_op :: HasValues t => String -> (Double -> Double -> Double) +                -> Double -> Values t -> [Values t] -> Result t +ieee_float_op str f b format vs+    | all (isIEEEFormat format) vs = Normal $ inject $ IEEE_Float_64+        $ foldr f b $ map (doubleFromIEEEFormat format) vs+    | otherwise = SortErr err+    where   err     = str ++ " not applied to ieee_floats"+++isIEEEFormat :: Values t -> Values t -> Bool+isIEEEFormat (ADTVal "binary32" _) (IEEE_Float_32 _) = True+isIEEEFormat (ADTVal "binary64" _) (IEEE_Float_64 _) = True+isIEEEFormat _ _ = False++doubleFromIEEEFormat :: Values t -> Values t -> Double+doubleFromIEEEFormat (ADTVal "binary64" _) (IEEE_Float_64 d) = d+doubleFromIEEEFormat _ _ = error "fromIEEEFormat"++

@@ -0,0 +1,185 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Integers where++import Funcons.Operations.Internal hiding (isInt)+import Funcons.Operations.Types+import Funcons.Operations.Booleans (tobool)++library :: HasValues t => Library t+library = libFromList [+    ("integers", NullaryExpr integers)+  , ("is-integer", UnaryExpr is_integer)+  , ("is-int", UnaryExpr is_integer)+  , ("integer-add", NaryExpr integer_add_)+  , ("integer-subtract", BinaryExpr integer_subtract)+  , ("integer-sub", BinaryExpr integer_subtract)+  , ("integer-modulo", BinaryExpr stepMod)+  , ("integer-mod", BinaryExpr stepMod)+  , ("integer-multiply", NaryExpr integer_multiply_)+  , ("int-mul", NaryExpr integer_multiply_)+  , ("integer-divide", BinaryExpr integer_divide)+  , ("int-div", BinaryExpr integer_divide)+  , ("integer-power", BinaryExpr integer_power)+  , ("int-pow", BinaryExpr integer_power)+-- integer-negate is now generated+--  ,   ("integer-negate", ValueOp stepInteger_Negate)+--  ,   ("int-neg", ValueOp stepInteger_Negate)+  , ("integer-list", BinaryExpr integer_list)+  , ("integer-absolute-value", UnaryExpr integer_absolute_value)+  , ("decimal-natural", UnaryExpr decimal_natural)+  , ("natural-predecessor", UnaryExpr natural_predecessor)+  , ("nat-pred", UnaryExpr natural_predecessor)+  , ("nat-successor", UnaryExpr natural_successor)+  , ("nat-succ", UnaryExpr natural_successor)+  , ("integer-is-less", BinaryExpr is_less)+  , ("is-less", BinaryExpr is_less)+  , ("is-less-or-equal", BinaryExpr is_less_or_equal)+  , ("integer-is-less-or-equal", BinaryExpr is_less_or_equal)+  , ("is-greater", BinaryExpr is_greater)+  , ("integer-is-greater", BinaryExpr is_greater)+  , ("is-greater-or-equal", BinaryExpr is_greater_or_equal)+  , ("integer-is-greater-or-equal", BinaryExpr is_greater_or_equal)+  ]++integer_modulo_, integer_mod_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_mod_ = binaryOp stepMod+integer_modulo_ = binaryOp stepMod++stepMod :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+stepMod = vBinaryOp "mod" op+  where op vx vy | (Int x, Int y)<- (upcastIntegers vx, upcastIntegers vy)+                 = Normal $ inject $ mk_integers $ x `mod` y+        op _ _ = SortErr "mod not applied to integers"++integers_ :: HasValues t => [OpExpr t] -> OpExpr t+integers_ = nullaryOp integers+integers :: HasValues t => OpExpr t+integers = vNullaryOp "integers" (Normal $ injectT Integers)++is_integer_ :: HasValues t => [OpExpr t] -> OpExpr t+is_integer_ = unaryOp is_integer+is_integer :: HasValues t => OpExpr t -> OpExpr t+is_integer x = RewritesTo "is-integer" (type_member x (ValExpr (ComputationType (Type Integers)))) [x]++isInt :: Values t -> Bool+isInt x | Int i <- upcastIntegers x = True +        | otherwise = False++unInt x | Int i <- upcastIntegers x = i+        | otherwise = error "unInt"++integer_add_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_add_ = vNaryOp "integer-add" op+  where op  xs | all isInt xs = Normal $ inject $ mk_integers $ sum (map unInt xs)+               | otherwise = SortErr "integer-add not applied to integers"++integer_multiply_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_multiply_ = vNaryOp "integer-multiply" op+  where op  xs | all isInt xs = Normal $ inject $ mk_integers $ product (map unInt xs)+               | otherwise = SortErr "integer-multiply not applied to integers"+++integer_subtract_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_subtract_ = binaryOp integer_subtract+integer_subtract :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+integer_subtract = vBinaryOp "integer-subtract" op+  where op vx vy | Int x <- upcastIntegers vx+                 , Int y <- upcastIntegers vy = Normal $ inject $ mk_integers $ (x - y)+        op _ _ = SortErr "integer-subtract not applied to integers"++integer_divide_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_divide_ = binaryOp integer_divide+integer_divide :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+integer_divide = vBinaryOp "integer-divide" op+  where op vx vy+          | (Int x,Int y) <- (upcastIntegers vx, upcastIntegers vy) = +              Normal $ inject $ mk_integers $ fromInteger (x `div` y)+          | otherwise = SortErr "integer-divide not applied to ints" ++integer_power_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_power_ = binaryOp integer_power  +integer_power :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+integer_power = vBinaryOp "integer-power" op+  where op vx vy+          | (Int x, Int y) <- (upcastIntegers vx, upcastIntegers vy) = +              Normal $ inject $ mk_integers $ fromInteger $(x ^ y)+          | otherwise = SortErr "integer-power not applied to two integers"++natural_predecessor_, nat_pred_ :: HasValues t => [OpExpr t] -> OpExpr t+natural_predecessor_ = unaryOp natural_predecessor +nat_pred_ = unaryOp natural_predecessor +natural_predecessor :: HasValues t => OpExpr t -> OpExpr t+natural_predecessor = vUnaryOp "natural-predecessor" op+  where op x | Nat n <- upcastNaturals x =+          if n == 0 then DomErr "no predecessor of 0"+                    else Normal $ inject $ Nat (n - 1) +             | otherwise = SortErr "natural-pred not applied to a natural number"++natural_successor_, nat_succ_ :: HasValues t => [OpExpr t] -> OpExpr t+natural_successor_ = nat_succ_+nat_succ_ = unaryOp natural_successor+natural_successor :: HasValues t => OpExpr t -> OpExpr t+natural_successor = vUnaryOp "natural-successor" op+  where op x | Nat n <- upcastNaturals x = Normal $ inject $ Nat (n + 1) +             | otherwise = SortErr "natural-succ not applied to a natural number"++integer_list_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_list_ = binaryOp integer_list+integer_list :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+integer_list = vBinaryOp "integer-list" op+ where op vi1 vi2+        | (Int i1, Int i2) <- (upcastIntegers vi1, upcastIntegers vi2)+                = Normal $ inject $ ADTVal "list" (map (inject . Int) [i1.. i2])+        | otherwise = SortErr "integer-list not applied to two integers"++integer_absolute_value_ :: HasValues t => [OpExpr t] -> OpExpr t+integer_absolute_value_ = unaryOp integer_absolute_value +integer_absolute_value :: HasValues t => OpExpr t -> OpExpr t+integer_absolute_value = vUnaryOp "integer-absolute-value" op+  where op v | Int  i <- upcastIntegers v = +                Normal $ inject $ Int (Prelude.abs i)+             | otherwise = SortErr "sort check: integer-absolute-value(I1)"++decimal_natural_ :: HasValues t => [OpExpr t] -> OpExpr t+decimal_natural_ = unaryOp decimal_natural +decimal_natural :: HasValues t => OpExpr t -> OpExpr t+decimal_natural = vUnaryOp "decimal-natural" op+  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"++is_less_ :: HasValues t => [OpExpr t] -> OpExpr t+is_less_ = binaryOp is_less+is_less :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+is_less = vBinaryOp "is-less" op+  where op vx vy+          | (Int x, Int y) <- (upcastIntegers vx, upcastIntegers vy)+              = Normal $ inject $ tobool (x < y)+          | otherwise = SortErr "is-less not applied to rationals"++is_less_or_equal_ :: HasValues t => [OpExpr t] -> OpExpr t+is_less_or_equal_ = binaryOp is_less_or_equal+is_less_or_equal ::  HasValues t => OpExpr t -> OpExpr t -> OpExpr t+is_less_or_equal = vBinaryOp "is-less-or-equal" op+ where op vx vy+         | (Int x, Int y) <- (upcastIntegers vx, upcastIntegers vy)+            = Normal $ inject $ tobool (x <= y) +         | otherwise = SortErr "is_less_or_equal not applied to two arguments"++is_greater_ :: HasValues t => [OpExpr t] -> OpExpr t+is_greater_ = binaryOp is_greater+is_greater :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+is_greater = vBinaryOp "is-greater" op+ where op vx vy+        | (Int x, Int y) <- (upcastIntegers vx, upcastIntegers vy)+            = Normal $ inject $ tobool (x > y) +        | otherwise = SortErr "is-greater not applied to two arguments"++is_greater_or_equal_ :: HasValues t => [OpExpr t] -> OpExpr t+is_greater_or_equal_ = binaryOp is_greater_or_equal +is_greater_or_equal :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+is_greater_or_equal = vBinaryOp "is-greater-or-equal" op+ where op vx vy | (Int x, Int y) <- (upcastIntegers vx, upcastIntegers vy)+                    = Normal $ inject $ tobool (x >= y) +                | otherwise = SortErr "is-greater-or-equal not applied to rationals"

@@ -0,0 +1,10 @@++module Funcons.Operations.Internal (+  module Funcons.Operations.Expr,+  module Funcons.Operations.Values,+  module Funcons.Operations.Libraries,+  ) where++import Funcons.Operations.Expr+import Funcons.Operations.Values+import Funcons.Operations.Libraries

@@ -0,0 +1,18 @@++module Funcons.Operations.Libraries where++import qualified Data.Map as M++import Funcons.Operations.Expr++type Library t = M.Map OP (ValueOp t)++libFromList :: [(OP, ValueOp t)] -> Library t+libFromList = M.fromList++libLookup :: OP -> Library t -> Maybe (ValueOp t)+libLookup = M.lookup++libUnite :: [Library t] -> Library t+libUnite = M.unions+

@@ -0,0 +1,89 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Lists where++import Funcons.Operations.Internal+import Funcons.Operations.Booleans++import Data.Maybe (isJust, fromJust)++library :: HasValues t => Library t+library = libFromList [+    ("lists", UnaryExpr lists)+  , ("list-singleton", UnaryExpr list_singleton)+  , ("list", NaryExpr list_)+  , ("list-append", BinaryExpr list_append)+  , ("list-concat", NaryExpr list_concat)+  , ("nil", NullaryExpr nil)+  , ("cons", BinaryExpr cons)+  , ("is-nil", UnaryExpr is_nil)+  , ("head", UnaryExpr headOp)+  , ("tail", UnaryExpr tailOp)+  ]++lists_ :: HasValues t => [OpExpr t] -> OpExpr t+lists_ = unaryOp lists+lists :: HasValues t => OpExpr t -> OpExpr t+lists = UnaryOp "lists" (Normal . injectT . ADT "lists" . (:[]))++list_singleton_ :: HasValues t => [OpExpr t] -> OpExpr t +list_singleton_ = unaryOp list_singleton+list_singleton :: HasValues t => OpExpr t -> OpExpr t+list_singleton = vUnaryOp "list-singleton" (Normal . inject . list . (:[]))++nil_ :: HasValues t => [OpExpr t] -> OpExpr t+nil_ = nullaryOp nil+nil :: HasValues t => OpExpr t+nil = NullaryOp "nil" (Normal $ inject $ list [])++is_nil_ :: HasValues t => [OpExpr t] -> OpExpr t+is_nil_ = unaryOp is_nil+is_nil :: HasValues t => OpExpr t -> OpExpr t+is_nil = UnaryOp "is-nil" op+  where op xs | Just lv <- project xs = case lv of +                  ADTVal "list" [] -> Normal $ inject $ true_ +                  _                -> Normal $ inject $ false_+              | otherwise = ProjErr "is-nil"++cons_ ::  HasValues t =>[OpExpr t] -> OpExpr t+cons_ = binaryOp cons+cons :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t +cons = vBinaryOp "cons" op+  where op v lv = case lv of+                    ADTVal "list" xs -> Normal $ inject $ ADTVal "list" (inject v:xs)+                    _ -> SortErr"cons should be given a value and a list"++list_ :: HasValues t => [OpExpr t] -> OpExpr t+list_ = vNaryOp "list" (Normal . inject . list)++list_append_ :: HasValues t => [OpExpr t] -> OpExpr t+list_append_ = binaryOp list_append+list_append :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+list_append = vBinaryOp "list-append" op+   where op (ADTVal "list" l1) (ADTVal "list" l2) = +            Normal $ inject $ ADTVal "list" (l1 ++ l2)+         op _ _ = SortErr "list-append not applied to two lists"+isList (ADTVal "list" l) = all (isJust) $ map project l +isList _                 = False+toList (ADTVal "list" l) = map (fromJust . project) l+toList _                 = error "list-append 1"+     +list_concat_ :: HasValues t => [OpExpr t] -> OpExpr t+list_concat_ = list_concat+list_concat :: HasValues t => [OpExpr t] -> OpExpr t+list_concat = vNaryOp "list-concat" op+   where op args | all isList args = Normal $ inject $ list $ concatMap toList args+                 | otherwise       = SortErr "list-concat not applied to lists"++head_, tail_ :: HasValues t => [OpExpr t] -> OpExpr t+head_ = unaryOp headOp+tail_ = unaryOp tailOp+headOp,tailOp :: HasValues t => OpExpr t -> OpExpr t+headOp = vUnaryOp "head" op+  where op (ADTVal "list" [])      = DomErr "head of empty list"+        op (ADTVal "list" (x:xs))  = Normal x+        op _                       = SortErr "head not applied to a list"+tailOp = vUnaryOp "tail" op+  where op (ADTVal "list" [])      = DomErr "tail of empty list"+        op (ADTVal "list" (x:xs))  = Normal $ inject (ADTVal "list" xs)+        op _                       = SortErr "tail not applied to a list"

@@ -0,0 +1,142 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Maps where++import Funcons.Operations.Booleans+import Funcons.Operations.Internal+import Funcons.Operations.Sets+import qualified Data.Map as M+import qualified Data.Set as S ++library :: (HasValues t, Ord t) => Library t+library = libFromList [+    ("map-empty", NullaryExpr map_empty)+  , ("map-singleton", BinaryExpr map_singleton)+  , ("is-map-empty", UnaryExpr is_map_empty)+  , ("map-insert", TernaryExpr map_insert)+  , ("map-lookup", BinaryExpr map_lookup)+  , ("lookup", BinaryExpr map_lookup)+  , ("map-domain", UnaryExpr domain)+  , ("domain", UnaryExpr domain)+  , ("map-delete", BinaryExpr map_delete)+  , ("is-in-domain", BinaryExpr is_in_domain)+  , ("map-unite", NaryExpr map_unite)+  , ("map-override", BinaryExpr map_override)+  , ("maps", BinaryExpr maps)+  , ("map", NaryExpr map_)+  , ("map-elements", UnaryExpr map_elements)+  , ("map-points", UnaryExpr map_points)+  ]++map_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+map_ = vNaryOp "map" (Normal . inject . Map . M.fromList . mkPairs)++mkPairs :: [a] -> [(a,a)]+mkPairs []        = []+mkPairs [x]       = []+mkPairs (x:y:ys)  = (x,y) : mkPairs ys++maps_ :: HasValues t => [OpExpr t] -> OpExpr t+maps_ = binaryOp maps+maps :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+maps = vBinaryOp "maps" op+  where op (ComputationType (Type t1)) (ComputationType (Type t2)) = Normal $ injectT (Maps t1 t2)+        op _ _ = SortErr "maps not applied to two types"++map_empty_ :: HasValues t => [OpExpr t] -> OpExpr t +map_empty_ = nullaryOp map_empty+map_empty :: HasValues t => OpExpr t +map_empty = NullaryOp "map-empty" (Normal $ inject (Map M.empty))++map_singleton_ :: (HasValues t,Ord t) => [OpExpr t] -> OpExpr t+map_singleton_ = binaryOp map_singleton+map_singleton :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t +map_singleton k v = RewritesTo "map-insert" (map_insert map_empty k v) [k,v]++is_map_empty_ :: HasValues t => [OpExpr t] -> OpExpr t+is_map_empty_ = unaryOp is_map_empty+is_map_empty :: HasValues t => OpExpr t -> OpExpr t +is_map_empty = vUnaryOp "is-map-empty" op +  where op (Map m)  = Normal $ inject $ tobool (null m)+        op _        = SortErr "is-map-empty(M) not applied to a map"++map_insert_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_insert_ = ternaryOp map_insert +map_insert :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t+map_insert = vTernaryOp "map-insert" op+  where op xv k v = case xv of +              Map m -> Normal $ inject $ Map (M.insert k v m)+              _     -> SortErr "map-insert(M,K,V) not applied to a map (first argument)"++map_lookup_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_lookup_ = binaryOp map_lookup+map_lookup :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t+map_lookup = vBinaryOp "map-lookup" op+  where op xv k = case xv of +                    Map m -> case M.lookup k m of +                        Nothing -> DomErr "key not in domain"+                        Just v  -> Normal $ inject v+                    _ -> SortErr "map-lookup(M,V) not applied to a map and a value"++map_delete_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_delete_ = binaryOp map_delete+map_delete :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t+map_delete = vBinaryOp "map-delete" op+  where op (Map m) (Set s) = Normal $ inject $ Map (foldr M.delete m s)+        op _ _ = SortErr "map-delete(M,S) not applied to a map and a set"++is_in_domain_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t +is_in_domain_ = binaryOp is_in_domain+is_in_domain :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t +is_in_domain x y = RewritesTo "is-in-domain" (is_in_set x (domain y)) [x,y] ++domain_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+domain_ = unaryOp domain+domain :: (HasValues t, Ord t) => OpExpr t -> OpExpr t+domain = vUnaryOp "domain" op+  where op (Map m)  = Normal $ inject $ Set $ S.fromList $ M.keys m+        op _        = SortErr "domain(M) not applied to a map"++map_override_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_override_ = binaryOp map_override+map_override :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t+map_override = vBinaryOp "map-override" op+  where op (Map m1) (Map m2) = Normal $ inject $ Map (M.union m1 m2)+        op _ _ = SortErr "map-override(M,M) not applied tOpExpr two maps"++map_unite_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_unite_ = map_unite +map_unite :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+map_unite = vNaryOp "map-unite" op+  where op args +          | all isMap args =+              let maps = map toMap args+                  domains = map (M.keysSet) maps+              in if all (null . uncurry S.intersection) (allDomainPairs domains)+                  then Normal $ inject $ Map $ M.unions maps+                  else DomErr "union with domain intersection"+          | otherwise     = SortErr "map-unite(M1,...,Mn) not applied to maps"+          where isMap (Map _) = True+                isMap _       = False+                toMap (Map m) = m+                toMap _       = error "map_unite"++allDomainPairs :: [a] -> [(a,a)] +allDomainPairs (x:xs) = [ (x,y)  | y <- xs ] ++ allDomainPairs xs+allDomainPairs [] = []++map_elements_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+map_elements_ = unaryOp map_elements+map_elements :: (Ord t, HasValues t) => OpExpr t -> OpExpr t+map_elements = vUnaryOp "map-elements" op+  where op (Map m) = Normal $ inject $ ADTVal "list" (map inject $ M.foldrWithKey combine [] m)+          where combine k v ls = k:v:ls+        op _ = SortErr "map-elements not applied to a map"++map_points_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+map_points_ = unaryOp map_points+map_points :: (Ord t, HasValues t) => OpExpr t -> OpExpr t+map_points = vUnaryOp "map-points" op+  where op (Map m) = Normal $ inject $ ADTVal "list" (map inject $ M.foldrWithKey combine [] m)+          where combine k v ls = ADTVal "tuple" [inject k, inject v]:ls+        op _ = SortErr "map-points not applied to a map"

@@ -0,0 +1,11 @@++module Funcons.Operations.Multisets where++import Funcons.Operations.Booleans+import Funcons.Operations.Internal++import qualified Data.MultiSet as MS++library :: (HasValues t, Ord t) => Library t+library = libFromList [+  ]

@@ -0,0 +1,31 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.NonGroundValues where++import Prelude hiding (non_grounded)+import Funcons.Operations.Internal++library :: (HasValues t, Eq t) => Library t+library = libFromList [+    ("non-grounded", UnaryExpr non_grounded)+  , ("non-grounded-values", NullaryExpr non_grounded_values)+  ]++non_grounded_ :: HasValues t => [OpExpr t] -> OpExpr t+non_grounded_ = unaryOp non_grounded +non_grounded :: HasValues t => OpExpr t -> OpExpr t+non_grounded = vUnaryOp "non-grounded" (Normal . inject . ADTVal "non-grounded" . (:[]) . inject) ++non_grounded_values_ :: HasValues t => [OpExpr t] -> OpExpr t+non_grounded_values_ = nullaryOp non_grounded_values +non_grounded_values :: HasValues t => OpExpr t+non_grounded_values = vNullaryOp "non-grounded-values" +  (Normal $ injectT $ ADT "non-grounded-values" [])++{-+-- This function differs from Funcons.Operations.Values.isGround+-- and assumes that non_grounded<> is the only non-ground value constructor+isGround :: Values t -> Bool+isGround (ADTVal "non-grounded" _) = False+isGround v = True+-}

@@ -0,0 +1,37 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Optionals where++import Funcons.Operations.Internal++library :: (HasValues t, Eq t) => Library t+library = libFromList [+    ("optionals", UnaryExpr optionals)+  , ("none", NullaryExpr none)+  , ("some", UnaryExpr some)+  ]++toOpt :: HasValues t => Maybe t -> Values t +toOpt (Just t)  = ADTVal "some" [t]+toOpt Nothing   = none__ ++optionals_ :: HasValues t => [OpExpr t] -> OpExpr t+optionals_ = unaryOp optionals+optionals :: HasValues t => OpExpr t -> OpExpr t+optionals = vUnaryOp "optionals" op+  where op (ComputationType t) = (Normal $ injectT $ ADT "optionals" [injectCT t])+        op _        = SortErr "optionals not applied to a type"++some__ :: HasValues t => t -> Values t +some__ = toOpt . Just+some_ :: HasValues t => [OpExpr t] -> OpExpr t+some_ = unaryOp some+some :: HasValues t => OpExpr t -> OpExpr t+some = vUnaryOp "some" (Normal . inject . some__ . inject)++none_ :: HasValues t => [OpExpr t] -> OpExpr t+none_ = nullaryOp none+none :: HasValues t => OpExpr t+none = vNullaryOp "none" (Normal $ inject $ none__)++

@@ -0,0 +1,129 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Sets where++import Funcons.Operations.Booleans+import Funcons.Operations.Internal hiding (set_)++import qualified Data.Set as S++import Test.RandomStrings (randomString', randomASCII)+import System.IO.Unsafe (unsafePerformIO)++library :: (HasValues t, Ord t) => Library t+library = libFromList [+    ("set-empty", NullaryExpr set_empty)+  , ("sets", UnaryExpr sets) +  , ("is-in-set", BinaryExpr is_in_set) +  , ("set", NaryExpr set_)+  , ("set-elements", UnaryExpr set_elements)+  , ("is-subset", BinaryExpr is_subset)+  , ("set-insert", BinaryExpr set_insert)+  , ("set-unite", NaryExpr set_unite_)+  , ("set-intersect", NaryExpr set_intersect_)+  , ("set-difference", NaryExpr set_difference_)+  , ("set-size", UnaryExpr set_size)+  , ("some-element", UnaryExpr some_element)+  , ("element-not-in", BinaryExpr element_not_in)+--  , ("is-set-empty", UnaryExpr is_set_empty)+  ]++sets_ :: HasValues t => [OpExpr t] -> OpExpr t+sets_ = unaryOp sets+sets :: HasValues t => OpExpr t -> OpExpr t+sets = vUnaryOp "sets" op+  where op (ComputationType (Type t)) = Normal $ injectT $ Sets t+        op _ = SortErr "sets not applied to a type" ++set_empty_ :: HasValues t => [OpExpr t] -> OpExpr t+set_empty_ = nullaryOp set_empty+set_empty :: HasValues t => OpExpr t+set_empty = NullaryOp "set-empty" (Normal $ inject (Set S.empty))++is_in_set_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t+is_in_set_ = binaryOp is_in_set+is_in_set :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t +is_in_set = BinaryOp "is-in-set" op +  where op e' s' +          | Just s <- project s', Just e <- project e' = case s of +            Set set -> Normal $ inject $ tobool (e `S.member` set)+            _       -> SortErr "is-in-set(V,S) not applied to a value and a set"+          | otherwise = ProjErr "is-in-set"++set_elements_ :: HasValues t => [OpExpr t] -> OpExpr t+set_elements_ = unaryOp set_elements+set_elements :: HasValues t => OpExpr t -> OpExpr t+set_elements = vUnaryOp "set-elements" op+ where op (Set s) = Normal $ inject $ ADTVal "list" (map inject $ S.toList s)+       op _ = SortErr "set-elements not applied to a set"++set_size_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_size_ = unaryOp set_size+set_size :: (Ord t, HasValues t) => OpExpr t -> OpExpr t+set_size = vUnaryOp "set-size" op+ where op (Set s) = Normal $ inject $ Nat (toInteger $ S.size s) +       op _ = SortErr "set-size not applied to a set"++set_intersect_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_intersect_ = vNaryOp "set-intersect" op+  where op [] = SortErr "set-intersect applied to an empty sequence of sets"+        op vs | all isSet_ vs = Normal $ inject $ +                                  Set (foldr1 S.intersection (map toSet vs))+              | otherwise = SortErr "set-intersect not applied to sets"+          where isSet_ (Set _) = True+                isSet_ _       = False+                toSet (Set s)  = s+                toSet _        = error "set-intersect toSet"++set_difference_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_difference_ = binaryOp set_difference+set_difference :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t+set_difference = vBinaryOp "set-difference" op+  where op (Set s1) (Set s2) = Normal $ inject $ Set (s1 `S.difference` s2)+        op _ _ = SortErr "set-difference not applied to two sets"++some_element_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+some_element_ = unaryOp some_element+some_element :: (HasValues t, Ord t) => OpExpr t -> OpExpr t+some_element = vUnaryOp "some-element" op+  where op (Set s) | not (S.null s) = Normal $ inject $ S.findMax s+        op _ = SortErr "some-element not applied to a non-empty set"++is_subset_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+is_subset_ = binaryOp is_subset+is_subset :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t+is_subset = vBinaryOp "is-subset" op+  where op (Set s1) (Set s2) = Normal $ inject $ tobool (s1 `S.isSubsetOf` s2)+        op _ _ = SortErr "is-subset not applied to two sets"++set_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_ = vNaryOp "set" op+  where op vs = Normal $ inject $ Set (S.fromList vs)++set_unite_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_unite_ = vNaryOp "set-unite" op+  where op vs | all isSet_ vs = Normal $ inject $ Set $ S.unions $ map unSet vs+              | otherwise = SortErr "set-unite not applied to sets"+          where isSet_ (Set s) = True+                isSet_ _       = False+                unSet (Set s) = s+                unSet _       = error "set-unite not applied to sets only"++set_insert_ :: (Ord t, HasValues t) => [OpExpr t] -> OpExpr t+set_insert_ = binaryOp set_insert+set_insert :: (HasValues t, Ord t) => OpExpr t -> OpExpr t -> OpExpr t+set_insert = vBinaryOp "set-insert" op+  where op e (Set s) = Normal $ inject $ Set (e `S.insert` s)+        op _ _ = SortErr "second argument of set-insert is not a set"++element_not_in_ :: (HasValues t, Ord t) => [OpExpr t] -> OpExpr t +element_not_in_ = binaryOp element_not_in+element_not_in :: (Ord t, HasValues t) => OpExpr t -> OpExpr t -> OpExpr t+element_not_in = vBinaryOp "element-not-in" op+  where op (ComputationType (Type ty)) (Set set) = case ty of +          Atoms -> Normal $ inject $ Atom (unsafePerformIO (getRnd >>= nextAtom))+          _     -> error "missing case for `element-not-in`"+          where nextAtom s | Atom s `S.member` set = getRnd >>= nextAtom+                           | otherwise             = return s  +                getRnd   = randomString' randomASCII 1 1 5+        op _ _ = SortErr "element-not-in not applied to a type and a set"

@@ -0,0 +1,37 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Strings where++import Funcons.Operations.Libraries+import Funcons.Operations.Internal+import Funcons.Operations.Types++library :: HasValues t => Library t+library = libFromList [+    ("is-string", UnaryExpr is_string)+  , ("strings", NullaryExpr (vNullaryOp "strings" (Normal $ injectT $ ADT "strings" [])))+  , ("to-string", UnaryExpr to_string)+  ]++is_string_ :: HasValues t => [OpExpr t] -> OpExpr t+is_string_ = unaryOp is_string+is_string x = RewritesTo "is-string" (type_member x (ValExpr (ComputationType (Type Strings)))) [x]++to_string_ :: HasValues t => [OpExpr t] -> OpExpr t+to_string_ = unaryOp to_string+to_string :: HasValues t => OpExpr t -> OpExpr t +to_string = vUnaryOp "to-string" stepTo_String++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 (Atom s)          = mk_string  s+stepTo_String (Int i)           = mk_string  (show i)+stepTo_String (Nat n)           = mk_string  (show n)+stepTo_String (Float f)         = mk_string  (show f)+stepTo_String (IEEE_Float_32 f) = mk_string  (show f)+stepTo_String (IEEE_Float_64 d) = mk_string  (show d)+stepTo_String v                 = DomErr ("to-string undefined on this type")++mk_string :: HasValues t => String -> Result t+mk_string = Normal . inject . ADTVal "list" . map (inject . Ascii)

@@ -0,0 +1,45 @@+{-# LANGUAGE OverloadedStrings #-}++module Funcons.Operations.Tuples where++import Funcons.Operations.Internal++library :: HasValues t => Library t+library = libFromList [+    ("tuples", NaryExpr tuples_)+  , ("tuple", NaryExpr tuple_)+  , ("tuple-index", BinaryExpr tuple_index)+  , ("empty-tuple", NullaryExpr  empty_tuple)+  , ("tuple-prepend", BinaryExpr tuple_prepend)+  ]++tuples_ :: HasValues t => [OpExpr t] -> OpExpr t+tuples_ = NaryOp "tuples" (Normal . injectT . ADT "tuples")++empty_tuple_, tuple_prepend_ :: HasValues t => [OpExpr t] -> OpExpr t+empty_tuple_ = nullaryOp empty_tuple+tuple_prepend_ = binaryOp tuple_prepend++empty_tuple :: HasValues t => OpExpr t+empty_tuple = vNullaryOp "empty-tuple" (Normal $ inject (tuple []))++tuple_prepend :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+tuple_prepend = vBinaryOp "tuple-prepend" op+  where op v (ADTVal "tuple" vs) = Normal $ inject (ADTVal "tuple" (inject v : vs))+        op _ _ = SortErr "tuple-prepend not applied to a value and a tuple"++tuple_ :: HasValues t => [OpExpr t] -> OpExpr t+tuple_ = vNaryOp "tuple" op+  where op ys = Normal $ inject (tuple ys)++tuple_index_ :: HasValues t => [OpExpr t] -> OpExpr t+tuple_index_ = binaryOp tuple_index+tuple_index :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t+tuple_index = vBinaryOp "tuple-index" op+  where op (ADTVal "tuple" ts) v +          | Nat n' <- upcastNaturals v, let n :: Int; n = fromInteger n'+            = case () of +               () | n >= 1 && n <= length ts -> Normal $ ts !! (n - 1)+               _ -> SortErr "tuple-index not in range"+          | otherwise = SortErr ("tuple-index not applied to a natural number: " ++ ppValues (const "_") v)+        op _ _ = SortErr "tuple-index not applied to a tuple"

@@ -0,0 +1,171 @@+{-# 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)

@@ -0,0 +1,735 @@+{-# LANGUAGE UndecidableInstances, OverloadedStrings, TupleSections, RankNTypes, FlexibleInstances, LambdaCase #-}++module Funcons.Operations.Values where++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.String++import Control.Monad (liftM2)+import Control.Arrow ((***))++type Name = Text+type MVar = String++-- | +-- This datatype provides a number of builtin value types.+-- The type `t` is expected to be a super-type of `Values t`,+-- such that there is a projection and injection between `t` and `Values t`,+-- (see 'HasValues')+-- Values forms a functor over the type `t` and provides a generic way of+-- comparing values (see `zipWithT`) for example to realise pattern matching +data Values t   = ADTVal Name [t]+                | Ascii Char +                | Atom String+                | Bit BV.BitVector+                | Char Char+                | ComputationType (ComputationTypes t)+                | Float Double +                | IEEE_Float_32 Float+                | IEEE_Float_64 Double+                | Int Integer+                | Map (ValueMaps (Values t))+                | Multiset (MS.MultiSet (Values t))+                | Nat Integer+                | Rational Rational+                | Set (ValueSets (Values t))+                | Vector (ValueVectors (Values t))+                | VMeta (TaggedSyntax t)+                | VAny -- used whenever funcon terms may have holes in them+                       -- currently only the case in "downwards" flowing signals+        deriving (Eq,Ord,Show,Read)++tuple :: HasValues t => [Values t] -> Values t+tuple = ADTVal "tuple" . map inject++list :: HasValues t => [Values t] -> Values t+list = ADTVal "list" . map inject++instance HasValues t => IsString (Values t) where+  fromString = ADTVal "list" . map (inject . Ascii)++data TaggedSyntax t = TagName Name [Values t]+                    | TagType (Types t) (Values t)+                  deriving (Eq, Ord, Show, Read)++type ValueMaps t      = M.Map t t +type ValueSets t      = S.Set t+type ValueVectors t   = V.Vector t++-- | Postfix operators for specifying sequences.+data SeqSortOp = StarOp | PlusOp | QuestionMarkOp+                deriving (Show, Eq, Ord, Read)+++-- | Computation type /S=>T/ reflects a type of term+-- whose given value is of type /S/ and result is of type /T/.+data ComputationTypes t = Type (Types t) -- | /=>T/+                        | ComputesType (Types t) -- | /S=>T/+                        | ComputesFromType (Types t) (Types t)+                        deriving (Ord,Eq,Show, Read)++-- | Representation of builtin types.+data Types t= ADTs+            | ADT Name [t]+            | AnnotatedType (Types t) SeqSortOp+            | AsciiCharacters+            | Atoms+            | Bits Int+            | IntegersFrom Integer -- value-dependent type+            | IntegersUpTo Integer+            | Characters+            | Complement (Types t)+            | ComputationTypes+            | EmptyType+            | GroundValues+            | IEEEFloats IEEEFormats+            | Integers+            | Intersection (Types t) (Types t)+            | Maps (Types t) (Types t)+            | Multisets (Types t)+            | Naturals+            | Nothings+            | Rationals+            | Sets (Types t)+            | Strings+            | Types+            | UnicodeCharacters+            | Union (Types t) (Types t)+            | DefinedValues +            | Values+            | Vectors (Types t)+            -- extension for meta-programming (see Funcons.MetaProgramming)+            | ASTs+              deriving (Ord,Eq,Show,Read)+++class HasValues t where+  project :: t -> Maybe (Values t)+  inject  :: Values t -> t+class HasComputationTypes t where+  projectCT :: t -> Maybe (ComputationTypes t)+  injectCT  :: ComputationTypes t -> t+class HasTypes t where+  projectT  :: t -> Maybe (Types t)+  injectT   :: Types t -> t+instance HasValues t => HasComputationTypes t where+  projectCT v = project v >>= \case+                ComputationType t -> Just t+                _      -> Nothing+                +  injectCT  = inject . ComputationType+instance HasComputationTypes t => HasTypes t where+  projectT ct = projectCT ct >>= \case +                  Type t -> Just t +                  _      -> Nothing+  injectT = injectCT . Type++data IEEEFormats = Binary32 | Binary64+        deriving (Enum,Show,Eq,Ord,Read)++-- Specialised version of 'fmap'+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+    IEEE_Float_64 f   -> IEEE_Float_64 f+    Int i             -> Int i+    Map m             -> Map $ M.fromList $ map (vmap f *** vmap f) $ M.assocs m+    Set s             -> Set $ S.map (vmap f) s+    Multiset ms       -> Multiset $ MS.map (vmap f) ms+    Nat n             -> Nat n+    Rational r        -> Rational r+    Vector v          -> Vector $ V.map (vmap f) v+    VMeta ts          -> VMeta $ vmapTS f ts+    VAny              -> VAny++vmapTS :: (Ord b) => (a -> b) -> TaggedSyntax a -> TaggedSyntax b+vmapTS f ts = case ts of+    TagName nm vs -> TagName nm (map (vmap f) vs)+    TagType t v   -> TagType (fmap f t) (vmap f v) +  +traverseV :: (Ord b, Monad m, HasValues a, HasValues b) => +  (a -> m b) -> Values a -> m (Values b)+traverseV f = traverseVM f (mapM f)++traverseVM :: (Ord b, Monad m, HasValues a, HasValues b) => +  (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+    IEEE_Float_64 f   -> return $ IEEE_Float_64 f+    Int i             -> return $ Int i+    Map m             -> do +        let (keys, vals) = unzip (M.assocs m)+        keys' <- map (fromJust . project) <$> fs (map inject keys)+        vals' <- map (fromJust . project) <$> fs (map inject vals)+        return (Map $ M.fromList $ zip keys' vals')+    Set s             -> return . Set . S.fromList . map (fromJust . project) =<< fs (map inject $ S.toList s)+    Multiset ms       -> return . Multiset . MS.fromList . map (fromJust . project) =<< fs (map inject $ MS.toList ms)+    Nat n             -> return $ Nat n+    Rational r        -> return $ Rational r+    Vector v          -> return . Vector . V.fromList . map (fromJust . project) =<< fs (map inject $ V.toList v)+    VMeta ts -> VMeta <$> traverseTSM f fs ts+    VAny -> return VAny++traverseT :: (Ord b, Monad m, HasValues a, HasValues b) => +  (a -> m b) -> Types a -> m (Types b)+traverseT f = traverseTM f (mapM f)+traverseTM :: (Ord b, Monad m, HasValues a, HasValues b) => +  (a -> m b) -> ([a] -> m [b]) -> Types a -> m (Types b)+traverseTM f fs t = case t of+  ADTs -> return ADTs+  ADT nm ts -> return . ADT nm =<< fs ts+  AsciiCharacters -> return AsciiCharacters+  Atoms ->  return Atoms+  AnnotatedType ty op -> AnnotatedType <$> traverseTM f fs ty <*> return op+  ASTs -> return ASTs+  Bits i -> return (Bits i)+  Characters -> return Characters+  ComputationTypes -> return ComputationTypes+  Complement t -> Complement <$> traverseTM f fs t  +  DefinedValues -> return DefinedValues+  GroundValues -> return GroundValues+  IntegersFrom f -> return (IntegersFrom f)+  IntegersUpTo f -> return (IntegersUpTo f)+  Intersection t1 t2 -> Intersection <$> traverseTM f fs t1 <*> traverseTM f fs t2+  Nothings -> return Nothings+  EmptyType -> return EmptyType+  IEEEFloats i -> return (IEEEFloats i)+  Integers -> return Integers+  Maps t1 t2 -> Maps <$> traverseTM f fs t1 <*> traverseTM f fs t2+  Multisets t -> Multisets <$> traverseTM f fs t+  Naturals -> return Naturals+  Rationals -> return Rationals+  Sets t -> Sets <$> traverseTM f fs t+  Strings -> return Strings+  Types -> return Types +  UnicodeCharacters -> return UnicodeCharacters+  Union t1 t2 -> Union <$> traverseTM f fs t1 <*> traverseTM f fs t2+  Values -> return Values+  Vectors t -> Vectors <$> traverseTM f fs t ++traverseTSM f fs t = case t of+  TagName nm vs -> TagName nm <$> traverse (traverseVM f fs) vs+  TagType ty v  -> TagType <$> traverseTM f fs ty <*> traverseVM f fs v++traverseCTM f fs t = case t of+  Type t -> Type <$> traverseTM f fs t+  ComputesType t -> ComputesType <$> traverseTM f fs t+  ComputesFromType ty ty2 -> ComputesFromType <$> traverseTM f fs ty+                                              <*> traverseTM f fs ty2++structVcompare :: (Monoid m, HasValues a, HasValues b) => +  (a -> b -> Maybe m) -> Values a -> Values b -> Maybe (Maybe m)+structVcompare comp = structVMcompare comp comps+  where comps xs ys | length xs == length ys = fmap mconcat $ sequence $ zipWith comp xs ys+                    | otherwise = Nothing++structCTMcompare :: (Monoid m, HasValues a, HasValues b) => +  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) ->+    ComputationTypes a -> ComputationTypes b -> (Maybe (Maybe m))+structCTMcompare comp comps va vb = case (va,vb) of+  (Type x, Type y)  -> structTMcompare comp comps x y +  (Type _,_)        -> Nothing+  (_, Type _)       -> Nothing+  (ComputesType x, ComputesType y)  -> structTMcompare comp comps x y +  (ComputesType _, _)               -> Nothing +  (_, ComputesType _)               -> Nothing+  (ComputesFromType x y, ComputesFromType x' y') -> +    liftM2 mappend (structTMcompare comp comps x x') (structTMcompare comp comps y y')++structVMcompare :: (Monoid m, HasValues b, HasValues a) => +  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) -> +    Values a -> Values b -> Maybe (Maybe m)+structVMcompare comp comps va vb = case (va, vb) of+  (ADTVal nm1 vs1, ADTVal nm2 vs2) +    | 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+  (ComputationType _, _)      -> Nothing+  (Float x, Float y) | x == y -> Just (Just mempty)+  (Float _, _)                -> Nothing+  (_, Float _)                -> Nothing+  (IEEE_Float_32 x, IEEE_Float_32 y) | x == y -> Nothing+  (IEEE_Float_32 _, _)                        -> Nothing+  (_, IEEE_Float_32 _)                        -> Nothing+  (IEEE_Float_64 x, IEEE_Float_64 y) | x == y -> Nothing+  (IEEE_Float_64 _, _)                        -> Nothing+  (_, IEEE_Float_64 _)                        -> Nothing+  (Int x, Int y) | x == y                     -> Just (Just mempty)+  (Int _, _)                                  -> Nothing+  (_, Int _)                                  -> Nothing+  (Map m1, Map m2) -> Just $ liftM2 mappend (comps (map inject (M.keys m1)) +                                                   (map inject (M.keys m2)))+                                            (comps (map inject (M.elems m1)) +                                                   (map inject (M.elems m2)))+  (Map _, _)      -> Nothing+  (_, Map _)      -> Nothing+  (Set x, Set y) -> Just $ comps (map inject $ S.toList x) (map inject $ S.toList y)  +  (Set _, _)      -> Nothing+  (_, Set _)      -> Nothing+  (Multiset x, Multiset y) -> Just $ comps (map inject $ MS.toList x) +                                           (map inject $ MS.toList y)+  (Multiset _, _)           -> Nothing+  (_, Multiset _)           -> Nothing+  (Nat x, Nat y)  | x == y  -> Just (Just mempty)+  (Nat _, _)                -> Nothing+  (_, Nat _)                -> Nothing+  (Rational x, Rational y) | x == y -> Just (Just mempty)+  (Rational _, _)                   -> Nothing+  (_, Rational _)                   -> Nothing+  (Vector x, Vector y) -> Just $ comps (map inject $ V.toList x) (map inject $ V.toList y)+  (VAny, VAny)  -> Just (Just mempty)+  (_, VAny)     -> Nothing+  (VAny, _)     -> Nothing+  (VMeta ts, VMeta ts') -> structTSMcompare comp comps ts ts' +  (VMeta _, _)  -> Nothing+  (_, VMeta _)  -> Nothing++structTSMcompare comp comps ts ts' = case (ts,ts') of+  (TagName nm vs, TagName nm' vs') | nm == nm' -> +    Just $ comps (map inject vs) (map inject vs')  +  (TagName _ _, _) -> Nothing+  (_, TagName _ _) -> Nothing+  (TagType ty v, TagType ty' v') -> +    liftM2 (liftM2 mappend) (structTMcompare comp comps ty ty')+                            (structVMcompare comp comps v v')++structTMcompare :: (Monoid m, HasValues a, HasValues b) => +  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) -> +    Types a -> Types b -> Maybe (Maybe m)+structTMcompare comp comps ta tb = case (ta, tb) of+  (ADTs, ADTs)                        -> Just (Just mempty)+  (ADTs, _)                           -> Nothing+  (_, ADTs)                           -> Nothing+  (ADT nm1 ts, ADT nm2 ts') | nm1 == nm2 -> Just $ comps ts ts'+  (ADT _ _, _)                        -> Nothing+  (_, ADT _ _)                        -> Nothing+  (Atoms, Atoms)                      -> Just (Just mempty)+  (Atoms, _)                          -> Nothing+  (_, Atoms)                          -> Nothing+  (AsciiCharacters, AsciiCharacters)  -> Just (Just mempty) +  (AsciiCharacters, _)                -> Nothing+  (_, AsciiCharacters)                -> Nothing+  (ASTs, ASTs)                        -> Just (Just mempty)+  (_, ASTs)                           -> Nothing+  (ASTs, _)                           -> 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+  (Complement x, Complement y)        -> structTMcompare comp comps x y+  (_, Complement _)                   -> Nothing+  (Complement _, _)                   -> Nothing+  (ComputationTypes, ComputationTypes)-> Just (Just mempty)+  (_, ComputationTypes)               -> Nothing+  (ComputationTypes, _)               -> Nothing+  (DefinedValues, DefinedValues)      -> Just (Just mempty)+  (_, DefinedValues)                  -> Nothing+  (DefinedValues, _)                  -> Nothing+  (GroundValues, GroundValues)        -> Just (Just mempty)+  (GroundValues, _)                   -> Nothing+  (_, GroundValues)                   -> Nothing+  (IntegersFrom mx, IntegersFrom mx') | mx == mx' -> Just (Just mempty)+  (IntegersFrom _, _)                 -> Nothing+  (_, IntegersFrom _)                 -> Nothing+  (IntegersUpTo mx, IntegersUpTo mx') | mx == mx' -> Just (Just mempty)+  (IntegersUpTo _, _)                   -> Nothing+  (_, IntegersUpTo _)                   -> Nothing+  (EmptyType, EmptyType)              -> Just (Just mempty)+  (_, EmptyType)                      -> Nothing+  (EmptyType, _)                      -> Nothing+  (IEEEFloats x, IEEEFloats y) | x ==y-> Just (Just mempty)+  (IEEEFloats _, _)                   -> Nothing+  (_, IEEEFloats _)                   -> Nothing+  (Maps k v, Maps k' v')              -> liftM2 mappend (structTMcompare comp comps k k') (structTMcompare comp comps v v')+  (Maps _ _, _)                       -> Nothing+  (_, Maps _ _)                       -> Nothing+  (Integers, Integers)                -> Just (Just mempty)+  (Integers, _)                       -> Nothing+  (_, Integers)                       -> Nothing+  (Intersection x y, Intersection x' y') -> liftM2 mappend (structTMcompare comp comps x x') (structTMcompare comp comps y y')+  (Intersection _ _, _)               -> Nothing+  (_, Intersection _ _)               -> Nothing+  (Multisets x, Multisets y)          -> structTMcompare comp comps x y+  (Multisets _, _)                    -> Nothing+  (_, Multisets _)                    -> Nothing+  (Naturals, Naturals)                -> Just (Just mempty)+  (_, Naturals)                       -> Nothing+  (Naturals, _)                       -> Nothing+  (Nothings, Nothings)                -> Just (Just mempty)+  (_, Nothings)                       -> Nothing+  (Nothings,_)                        -> Nothing+  (Rationals, Rationals)              -> Just (Just mempty)+  (Rationals, _)                      -> Nothing+  (_, Rationals)                      -> Nothing+  (Strings, Strings)                  -> Just (Just mempty) +  (_, Strings)                        -> Nothing+  (Strings, _)                        -> Nothing+  (Sets x, Sets y)                    -> structTMcompare comp comps x y+  (Sets _, _)                         -> Nothing+  (_, Sets _)                         -> Nothing+  (Types, Types)                      -> Just (Just mempty)+  (_, Types)                          -> Nothing+  (Types, _)                          -> Nothing+  (UnicodeCharacters, UnicodeCharacters)  -> Just (Just mempty)+  (UnicodeCharacters, _)                  -> Nothing+  (_, UnicodeCharacters)                  -> Nothing+  (Union u v, Union x y)                  -> liftM2 mappend (structTMcompare comp comps u x) (structTMcompare comp comps v y)+  (Union _ _, _)                          -> Nothing+  (_, Union _ _)                          -> Nothing+  (Values, Values)                        -> Just (Just mempty)+  (_, Values)                             -> Nothing+  (Values, _)                             -> Nothing+  (Vectors x, Vectors y)                  -> structTMcompare comp comps x y++instance Functor Types where+  fmap f t = case t of +    ADT nm ts           -> ADT nm (map f ts) +    ADTs                -> ADTs+    AsciiCharacters     -> AsciiCharacters+    Atoms               -> Atoms+    AnnotatedType ty op -> AnnotatedType (fmap f ty) op+    ASTs                -> ASTs+    Bits n              -> Bits n+    Complement t1       -> Complement (fmap f t1)+    ComputationTypes    -> ComputationTypes+    DefinedValues       -> DefinedValues  +    GroundValues        -> GroundValues+    IntegersFrom p      -> IntegersFrom p+    IntegersUpTo p      -> IntegersUpTo p+    Characters          -> Characters   +    EmptyType           -> EmptyType+    IEEEFloats b        -> IEEEFloats b+    Integers            -> Integers+    Intersection t1 t2  -> Intersection (fmap f t1) (fmap f t2)+    Maps k v            -> Maps (fmap f k) (fmap f v) +    Multisets t         -> Multisets (fmap f t)+    Naturals            -> Naturals+    Nothings            -> Nothings+    Rationals           -> Rationals+    Sets t              -> Sets (fmap f t)+    Strings             -> Strings+    Types               -> Types+    UnicodeCharacters   -> UnicodeCharacters+    Union t1 t2         -> Union (fmap f t1) (fmap f t2)+    Values              -> Values +    Vectors t           -> Vectors (fmap f t)++instance Functor ComputationTypes where+  fmap f t = case t of+    Type t -> Type $ fmap f t+    ComputesType t -> ComputesType $ fmap f t+    ComputesFromType t1 t2 -> ComputesFromType (fmap f t1) (fmap f t2)++instance Foldable Types where+  foldMap f fa = case fa of +    ADT _ ts            -> foldMap f ts+    ADTs                -> mempty+    AsciiCharacters     -> mempty+    Atoms               -> mempty+    ASTs                -> mempty+    AnnotatedType ty op -> foldMap f ty+    Bits _              -> mempty+    Characters          -> mempty+    Complement t1       -> foldMap f t1+    ComputationTypes    -> mempty+    DefinedValues       -> mempty+    GroundValues        -> mempty+    IntegersUpTo q      -> mempty+    IntegersFrom q      -> mempty+    Intersection t1 t2  -> foldMap f t1 `mappend` foldMap f t2+    EmptyType           -> mempty+    IEEEFloats b        -> mempty +    Integers            -> mempty+    Maps k v            -> foldMap f k `mappend` foldMap f v+    Multisets t         -> foldMap f t+    Naturals            -> mempty +    Nothings            -> mempty+    Rationals           -> mempty+    Sets t              -> foldMap f t+    Strings             -> mempty+    Types               -> mempty +    UnicodeCharacters   -> mempty +    Union t1 t2         -> foldMap f t1 `mappend` foldMap f t2+    Values              -> mempty +    Vectors t           -> foldMap f t++instance Traversable Types where+  traverse f ta = case ta of +    ADTs                -> pure ADTs+    ADT nm ts           -> ADT nm <$> traverse f ts+    AsciiCharacters     -> pure AsciiCharacters+    AnnotatedType ty op -> AnnotatedType <$> traverse f ty <*> pure op+    Atoms               -> pure Atoms+    ASTs                -> pure ASTs+    Bits n              -> pure $ Bits n+    Characters          -> pure Characters+    Complement t        -> Complement <$> traverse f t+    ComputationTypes    -> pure ComputationTypes+    DefinedValues       -> pure DefinedValues+    GroundValues        -> pure GroundValues +    IntegersFrom n      -> pure $ IntegersFrom n+    IntegersUpTo n        -> pure $ IntegersUpTo n+    EmptyType           -> pure EmptyType+    IEEEFloats b        -> pure $ IEEEFloats b+    Integers            -> pure Integers+    Intersection t1 t2  -> Intersection <$> traverse f t1 <*> traverse f t2+    Maps k v            -> Maps <$> traverse f k <*> traverse f v+    Multisets t         -> Multisets <$> traverse f t+    Naturals            -> pure Naturals+    Nothings            -> pure Nothings+    Rationals           -> pure Rationals+    Sets t              -> Sets <$> traverse f t+    Strings             -> pure Strings+    Types               -> pure Types+    UnicodeCharacters   -> pure UnicodeCharacters+    Union t1 t2         -> Union <$> traverse f t1 <*> traverse f t2+    Values              -> pure Values +    Vectors t           -> Vectors <$> traverse f t++downcastValueType :: Values t -> Types t+downcastValueType (ComputationType (Type t)) = t+downcastValueType (ComputationType (ComputesType t)) = t+downcastValueType (ComputationType (ComputesFromType _ t)) = t+downcastValueType _ = error "valueType: not a type"++-- | Returns the /rational/ representation of a value if it is a subtype.+-- Otherwise it returns the original value.+upcastRationals :: Values t -> Values t+upcastRationals (Nat n) = Rational (toRational n)+upcastRationals (Int i) = Rational (toRational i)+upcastRationals v       = v++-- | Returns the /integer/ representation of a value if it is a subtype.+-- Otherwise it returns the original value.+upcastIntegers :: Values t -> Values t+upcastIntegers (Nat n)  = Int n+upcastIntegers v        = v++-- | Returns the /natural/ representation of a value if it is a subtype.+-- Otherwise it returns the original value.+upcastNaturals :: Values t -> Values t+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++castType :: HasValues t => Values t -> Maybe (Types t)+castType (ComputationType (Type ty)) = Just ty+castType (ComputationType (ComputesType ty)) = Just ty+castType (ComputationType (ComputesFromType _ ty)) = Just ty+castType _            = Nothing++-- numbers+mk_integers :: Integer -> Values t+mk_integers i   | i >= 0    = mk_naturals i+                | otherwise = Int i++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_ascii_characters :: Char -> Values t+mk_ascii_characters = Ascii++--- Value specific++(===) :: (HasValues t, Eq t {- UNNECESSARY CONSTRAINT -}) => Values t -> Values t -> Bool+v1 === v2 = isGround v1 && isGround v2 && (v1 == v2)++(=/=) :: (HasValues t, Eq t {- UNNECESSARY CONSTRAINT -}) => Values t -> Values t -> Bool+v1 =/= v2 = isGround v1 && isGround v2 && (v1 /= v2)++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+isGround (Int _)                  = True+isGround (Map m)                  = all isGround (M.elems m)+isGround (Multiset ms)            = all isGround (MS.elems ms)+isGround (Nat _)                  = True+isGround (ComputationType _)      = True+isGround (Rational _)             = True+isGround (Set s)                  = all isGround (S.toList s)+isGround (Vector v)               = all isGround (V.toList v)+isGround (VMeta _)                = True+isGround VAny                     = False++-- 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+isInt _                             = False+isEnv f                             = isMap f+isMap ((Map _))                     = True+isMap _                             = False+isSet ((Set _))                     = True+isSet _                             = False+isString_ :: HasValues t => Values t -> Bool+isString_ (ADTVal "list" vs)        = not (null vs) && all (maybe False isAscii) (map project vs)+isString_ _                         = False+isType (ComputationType _)          = True+isType _                            = False+isVec ((Vector _))                  = True+isVec _                             = False++unString :: HasValues t => Values t -> String+unString (ADTVal "list" vs) +  | Just vs' <- sequence (map project vs), all isAscii vs' = map (\(Ascii c) -> c) vs'+unString _ = error "unString"++none__ :: Values t+none__ = ADTVal "none" []++isNoValue :: Values t -> Bool+isNoValue (ADTVal "none" _) = True+isNoValue _ = False++isDefinedVal :: Values t -> Bool+isDefinedVal f = not (isNoValue f)++set_ :: Ord t => [Values t] -> Values t+set_ = Set . S.fromList ++ppValues :: HasValues t => (t -> String) -> Values t -> String+ppValues showT v@(ADTVal "list" vs)+  | isString_ v = show (unString v)+  | otherwise   = "[" ++ showArgs_ (map showT vs) ++ "]"+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+ppValues showT (IEEE_Float_64 d) = show d+ppValues showT (Rational r)   = show r+ppValues showT (Int f)        = show f+ppValues showT (Nat f)        = show f+ppValues showT (Map m)        = if M.null m then "map-empty"+                               else "{" ++ key_values ++ "}"+ where key_values = intercalate ", " (map (\(k,v) -> ppValues showT k++" |-> "++ +                                                     ppValues showT v)$ M.toList m)+ppValues showT (Multiset s) = "{" ++ showArgs (map (ppValues showT) (MS.toList s)) ++ "}"+ppValues showT (Set s) =  "{" ++ showArgs (map (ppValues showT) (S.toList s)) ++ "}"+ppValues showT (Vector v) =  "vector" ++ showArgs (map (ppValues showT) (V.toList v))+ppValues showT (ComputationType ty) = ppComputationTypes showT ty+ppValues showT VAny = "_"+ppValues showT (VMeta ts) = ppTaggedSyntax showT ts++ppTaggedSyntax :: HasValues t => (t -> String) -> TaggedSyntax t -> String+ppTaggedSyntax showT (TagName nm vs) = "astv" ++ showArgs (unpack nm : map (ppValues showT) vs)+ppTaggedSyntax showT (TagType ty val) = "astv" ++ showArgs [ppTypes showT ty, ppValues showT val]++ppComputationTypes :: HasValues t => (t -> String) -> ComputationTypes t -> String+ppComputationTypes showT (Type t) = ppTypes showT t+ppComputationTypes showT (ComputesType ty) = "=>" ++ ppTypes showT ty+ppComputationTypes showT (ComputesFromType s t) = ppTypes showT s ++ "=>" ++ ppTypes showT t++ppTypes :: HasValues t => (t -> String) -> Types t -> String+ppTypes showT (AnnotatedType ty op)  = ppTypes showT ty ++ ppOp op+ppTypes showT (Complement ty)        = "~(" ++ ppTypes showT ty ++ ")"+ppTypes showT ComputationTypes       = "computation-types"+ppTypes showT GroundValues           = "ground-values"+ppTypes showT Nothings               = "nothing"+ppTypes showT DefinedValues          = "defined-values"+ppTypes showT ASTs                   = "asts"+ppTypes showT Atoms                  = "atoms"+ppTypes showT AsciiCharacters        = "ascii-characters"+ppTypes showT Characters             = "characters"+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"+ppTypes showT (UnicodeCharacters)    = "unicode-characters"+ppTypes showT (Integers)             = "integers"+ppTypes showT (Strings)              = "strings"+ppTypes showT (Values)               = "values"+ppTypes showT (Maps x y)             = "maps" ++ showArgs [ppTypes showT x, ppTypes showT y]+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 (Multisets ty)         = "multisets" ++ showArgs [ppTypes showT ty]+ppTypes showT Naturals               = "naturals"+ppTypes showT Rationals              = "rationals"+ppTypes showT (Sets ty)              = "sets(" ++ ppTypes showT ty ++ ")"+ppTypes showT (Vectors ty)           = "vectors(" ++ ppTypes showT ty ++ ")"+ppTypes showT (Union ty1 ty2)        = "(" ++ ppTypes showT ty1 ++ "|" ++ ppTypes showT ty2 ++")"++ppOp :: SeqSortOp -> String+ppOp StarOp = "*"+ppOp PlusOp = "+"+ppOp QuestionMarkOp = "?"++showArgs :: [String] -> String+showArgs args = "(" ++ showArgs_ args ++ ")"+showArgs_ :: [String] -> String+showArgs_ args = intercalate "," args +