{-# LANGUAGE OverloadedStrings #-} module Funcons.Operations.Tuples where import Funcons.Operations.Internal import Funcons.Operations.Booleans library :: HasValues t => Library t library :: Library t library = [(OP, ValueOp t)] -> Library t forall t. [(OP, ValueOp t)] -> Library t libFromList [ (OP "tuples", NaryExpr t -> ValueOp t forall t. NaryExpr t -> ValueOp t NaryExpr NaryExpr t forall t. HasValues t => [OpExpr t] -> OpExpr t tuples_) , (OP "tuple", NaryExpr t -> ValueOp t forall t. NaryExpr t -> ValueOp t NaryExpr NaryExpr t forall t. HasValues t => [OpExpr t] -> OpExpr t tuple_) , (OP "tuple-index", BinaryExpr t -> ValueOp t forall t. BinaryExpr t -> ValueOp t BinaryExpr BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_index) , (OP "empty-tuple", NullaryExpr t -> ValueOp t forall t. NullaryExpr t -> ValueOp t NullaryExpr NullaryExpr t forall t. HasValues t => OpExpr t empty_tuple) , (OP "tuple-prepend", BinaryExpr t -> ValueOp t forall t. BinaryExpr t -> ValueOp t BinaryExpr BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_prepend) , (OP "is-empty", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tuple_is_empty) , (OP "tuple-head", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tupleHeadOp) , (OP "tuple-tail", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tupleTailOp) ] tuples_ :: HasValues t => [OpExpr t] -> OpExpr t tuples_ :: [OpExpr t] -> OpExpr t tuples_ = OP -> NaryOp t -> [OpExpr t] -> OpExpr t forall t. OP -> NaryOp t -> [OpExpr t] -> OpExpr t NaryOp OP "tuples" (t -> Result t forall t. t -> Result t Normal (t -> Result t) -> ([t] -> t) -> NaryOp t forall b c a. (b -> c) -> (a -> b) -> a -> c . Types t -> t forall t. HasTypes t => Types t -> t injectT (Types t -> t) -> ([t] -> Types t) -> [t] -> t forall b c a. (b -> c) -> (a -> b) -> a -> c . Name -> [t] -> Types t forall t. Name -> [t] -> Types t ADT Name "tuples") tuple_is_empty_ :: HasValues t => [OpExpr t] -> OpExpr t tuple_is_empty_ :: [OpExpr t] -> OpExpr t tuple_is_empty_ = UnaryExpr t -> [OpExpr t] -> OpExpr t forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t unaryOp UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tuple_is_empty tuple_is_empty :: HasValues t => OpExpr t -> OpExpr t tuple_is_empty :: OpExpr t -> OpExpr t tuple_is_empty = OP -> UnaryVOp t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t vUnaryOp OP "is-empty" UnaryVOp t forall t a. HasValues t => Values a -> Result t op where op :: Values a -> Result t op (ADTVal Name "tuple" [a] vs) = t -> Result t forall t. t -> Result t Normal (t -> Result t) -> t -> Result t forall a b. (a -> b) -> a -> b $ Values t -> t forall t. HasValues t => Values t -> t inject (Values t -> t) -> Values t -> t forall a b. (a -> b) -> a -> b $ Bool -> Values t forall t. Bool -> Values t tobool ([a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [a] vs) op Values a _ = OP -> Result t forall t. OP -> Result t SortErr OP "is-empty not applied to a tuple" empty_tuple_, tuple_prepend_ :: HasValues t => [OpExpr t] -> OpExpr t empty_tuple_ :: [OpExpr t] -> OpExpr t empty_tuple_ = OpExpr t -> [OpExpr t] -> OpExpr t forall t. NullaryExpr t -> [NullaryExpr t] -> NullaryExpr t nullaryOp OpExpr t forall t. HasValues t => OpExpr t empty_tuple tuple_prepend_ :: [OpExpr t] -> OpExpr t tuple_prepend_ = BinaryExpr t -> [OpExpr t] -> OpExpr t forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t binaryOp BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_prepend empty_tuple :: HasValues t => OpExpr t empty_tuple :: OpExpr t empty_tuple = OP -> NullaryVOp t -> OpExpr t forall t. OP -> NullaryVOp t -> OpExpr t vNullaryOp OP "empty-tuple" (t -> NullaryVOp t forall t. t -> Result t Normal (t -> NullaryVOp t) -> t -> NullaryVOp t forall a b. (a -> b) -> a -> b $ Values t -> t forall t. HasValues t => Values t -> t inject ([Values t] -> Values t forall t. HasValues t => [Values t] -> Values t tuple [])) tuple_prepend :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_prepend :: OpExpr t -> OpExpr t -> OpExpr t tuple_prepend = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t vBinaryOp OP "tuple-prepend" BinaryVOp t forall t. HasValues t => Values t -> Values t -> Result t op where op :: Values t -> Values t -> Result t op Values t v (ADTVal Name "tuple" [t] vs) = t -> Result t forall t. t -> Result t Normal (t -> Result t) -> t -> Result t forall a b. (a -> b) -> a -> b $ Values t -> t forall t. HasValues t => Values t -> t inject (Name -> [t] -> Values t forall t. Name -> [t] -> Values t ADTVal Name "tuple" (Values t -> t forall t. HasValues t => Values t -> t inject Values t v t -> [t] -> [t] forall a. a -> [a] -> [a] : [t] vs)) op Values t _ Values t _ = OP -> Result t forall t. OP -> Result t SortErr OP "tuple-prepend not applied to a value and a tuple" tuple_ :: HasValues t => [OpExpr t] -> OpExpr t tuple_ :: [OpExpr t] -> OpExpr t tuple_ = OP -> NaryVOp t -> [OpExpr t] -> OpExpr t forall t. HasValues t => OP -> NaryVOp t -> [OpExpr t] -> OpExpr t vNaryOp OP "tuple" NaryVOp t forall t. HasValues t => [Values t] -> Result t op where op :: [Values t] -> Result t op [Values t] ys = t -> Result t forall t. t -> Result t Normal (t -> Result t) -> t -> Result t forall a b. (a -> b) -> a -> b $ Values t -> t forall t. HasValues t => Values t -> t inject ([Values t] -> Values t forall t. HasValues t => [Values t] -> Values t tuple [Values t] ys) tuple_index_ :: HasValues t => [OpExpr t] -> OpExpr t tuple_index_ :: [OpExpr t] -> OpExpr t tuple_index_ = BinaryExpr t -> [OpExpr t] -> OpExpr t forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t binaryOp BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_index tuple_index :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t tuple_index :: OpExpr t -> OpExpr t -> OpExpr t tuple_index = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t vBinaryOp OP "tuple-index" BinaryVOp t forall b t. HasValues b => Values t -> Values b -> Result t op where op :: Values t -> Values b -> Result t op (ADTVal Name "tuple" [t] ts) Values b v | Nat Integer n' <- Values b -> Values b forall t. Values t -> Values t upcastNaturals Values b v, let n :: Int; n :: Int n = Integer -> Int forall a. Num a => Integer -> a fromInteger Integer n' = case () of () | Int n Int -> Int -> Bool forall a. Ord a => a -> a -> Bool >= Int 1 Bool -> Bool -> Bool && Int n Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= [t] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [t] ts -> t -> Result t forall t. t -> Result t Normal (t -> Result t) -> t -> Result t forall a b. (a -> b) -> a -> b $ [t] ts [t] -> Int -> t forall a. [a] -> Int -> a !! (Int n Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) () _ -> OP -> Result t forall t. OP -> Result t SortErr OP "tuple-index not in range" | Bool otherwise = OP -> Result t forall t. OP -> Result t SortErr (OP "tuple-index not applied to a natural number: " OP -> OP -> OP forall a. [a] -> [a] -> [a] ++ (b -> OP) -> Values b -> OP forall t. HasValues t => (t -> OP) -> Values t -> OP ppValues (OP -> b -> OP forall a b. a -> b -> a const OP "_") Values b v) op Values t _ Values b _ = OP -> Result t forall t. OP -> Result t SortErr OP "tuple-index not applied to a tuple" tuple_head_, tuple_tail_ :: HasValues t => [OpExpr t] -> OpExpr t tuple_head_ :: [OpExpr t] -> OpExpr t tuple_head_ = UnaryExpr t -> [OpExpr t] -> OpExpr t forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t unaryOp UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tupleHeadOp tuple_tail_ :: [OpExpr t] -> OpExpr t tuple_tail_ = UnaryExpr t -> [OpExpr t] -> OpExpr t forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t unaryOp UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tupleTailOp tupleHeadOp,tupleTailOp :: HasValues t => OpExpr t -> OpExpr t tupleHeadOp :: OpExpr t -> OpExpr t tupleHeadOp = OP -> UnaryVOp t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t vUnaryOp OP "head" UnaryVOp t forall t. Values t -> Result t op where op :: Values t -> Result t op (ADTVal Name "tuple" []) = OP -> Result t forall t. OP -> Result t DomErr OP "tuple-head of empty tuple" op (ADTVal Name "tuple" (t x:[t] xs)) = t -> Result t forall t. t -> Result t Normal t x op Values t _ = OP -> Result t forall t. OP -> Result t SortErr OP "tuple-head not applied to a tuple" tupleTailOp :: OpExpr t -> OpExpr t tupleTailOp = OP -> UnaryVOp t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t vUnaryOp OP "tail" UnaryVOp t forall t. HasValues t => Values t -> Result t op where op :: Values t -> Result t op (ADTVal Name "tuple" []) = OP -> Result t forall t. OP -> Result t DomErr OP "tupletail of empty tuple" op (ADTVal Name "tuple" (t x:[t] xs)) = t -> Result t forall t. t -> Result t Normal (t -> Result t) -> t -> Result t forall a b. (a -> b) -> a -> b $ Values t -> t forall t. HasValues t => Values t -> t inject (Name -> [t] -> Values t forall t. Name -> [t] -> Values t ADTVal Name "tuple" [t] xs) op Values t _ = OP -> Result t forall t. OP -> Result t SortErr OP "tuple-tail not applied to a tuple"