diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/funcons-values.cabal b/funcons-values.cabal new file mode 100644 --- /dev/null +++ b/funcons-values.cabal @@ -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 +-- 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 + diff --git a/src/Funcons/Operations.hs b/src/Funcons/Operations.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations.hs @@ -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 diff --git a/src/Funcons/Operations/ADTs.hs b/src/Funcons/Operations/ADTs.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/ADTs.hs @@ -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" diff --git a/src/Funcons/Operations/Atoms.hs b/src/Funcons/Operations/Atoms.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Atoms.hs @@ -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" diff --git a/src/Funcons/Operations/Bits.hs b/src/Funcons/Operations/Bits.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Bits.hs @@ -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 [] + diff --git a/src/Funcons/Operations/Booleans.hs b/src/Funcons/Operations/Booleans.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Booleans.hs @@ -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) + + diff --git a/src/Funcons/Operations/Characters.hs b/src/Funcons/Operations/Characters.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Characters.hs @@ -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" diff --git a/src/Funcons/Operations/Eval.hs b/src/Funcons/Operations/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Eval.hs @@ -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) ++ ")" diff --git a/src/Funcons/Operations/Expr.hs b/src/Funcons/Operations/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Expr.hs @@ -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) +-} diff --git a/src/Funcons/Operations/Floats.hs b/src/Funcons/Operations/Floats.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Floats.hs @@ -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" + + diff --git a/src/Funcons/Operations/Integers.hs b/src/Funcons/Operations/Integers.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Integers.hs @@ -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" diff --git a/src/Funcons/Operations/Internal.hs b/src/Funcons/Operations/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Internal.hs @@ -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 diff --git a/src/Funcons/Operations/Libraries.hs b/src/Funcons/Operations/Libraries.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Libraries.hs @@ -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 + diff --git a/src/Funcons/Operations/Lists.hs b/src/Funcons/Operations/Lists.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Lists.hs @@ -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" diff --git a/src/Funcons/Operations/Maps.hs b/src/Funcons/Operations/Maps.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Maps.hs @@ -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" diff --git a/src/Funcons/Operations/Multisets.hs b/src/Funcons/Operations/Multisets.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Multisets.hs @@ -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 [ + ] diff --git a/src/Funcons/Operations/NonGroundValues.hs b/src/Funcons/Operations/NonGroundValues.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/NonGroundValues.hs @@ -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 +-} diff --git a/src/Funcons/Operations/Optionals.hs b/src/Funcons/Operations/Optionals.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Optionals.hs @@ -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__) + + diff --git a/src/Funcons/Operations/Sets.hs b/src/Funcons/Operations/Sets.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Sets.hs @@ -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" diff --git a/src/Funcons/Operations/Strings.hs b/src/Funcons/Operations/Strings.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Strings.hs @@ -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) diff --git a/src/Funcons/Operations/Tuples.hs b/src/Funcons/Operations/Tuples.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Tuples.hs @@ -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" diff --git a/src/Funcons/Operations/Types.hs b/src/Funcons/Operations/Types.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Types.hs @@ -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) diff --git a/src/Funcons/Operations/Values.hs b/src/Funcons/Operations/Values.hs new file mode 100644 --- /dev/null +++ b/src/Funcons/Operations/Values.hs @@ -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 +