{-# 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 :: Library t library = [(OP, ValueOp t)] -> Library t forall t. [(OP, ValueOp t)] -> Library t libFromList [ (OP "lists", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t lists) , (OP "list-singleton", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t list_singleton) , (OP "list", NaryExpr t -> ValueOp t forall t. NaryExpr t -> ValueOp t NaryExpr NaryExpr t forall t. HasValues t => [OpExpr t] -> OpExpr t list_) , (OP "list-append", BinaryExpr t -> ValueOp t forall t. BinaryExpr t -> ValueOp t BinaryExpr BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t list_append) , (OP "list-concat", NaryExpr t -> ValueOp t forall t. NaryExpr t -> ValueOp t NaryExpr NaryExpr t forall t. HasValues t => [OpExpr t] -> OpExpr t list_concat) , (OP "nil", NullaryExpr t -> ValueOp t forall t. NullaryExpr t -> ValueOp t NullaryExpr NullaryExpr t forall t. HasValues t => OpExpr t nil) , (OP "cons", BinaryExpr t -> ValueOp t forall t. BinaryExpr t -> ValueOp t BinaryExpr BinaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t cons) , (OP "is-nil", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t is_nil) , (OP "head", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t headOp) , (OP "tail", UnaryExpr t -> ValueOp t forall t. UnaryExpr t -> ValueOp t UnaryExpr UnaryExpr t forall t. HasValues t => OpExpr t -> OpExpr t tailOp) ] lists_ :: HasValues t => [OpExpr t] -> OpExpr t lists_ :: [OpExpr t] -> OpExpr t lists_ = 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 lists lists :: HasValues t => OpExpr t -> OpExpr t lists :: OpExpr t -> OpExpr t lists = OP -> UnaryOp t -> OpExpr t -> OpExpr t forall t. OP -> UnaryOp t -> OpExpr t -> OpExpr t UnaryOp OP "lists" (UnaryOp t forall t. t -> Result t Normal UnaryOp t -> (t -> t) -> UnaryOp 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 "lists" ([t] -> Types t) -> (t -> [t]) -> t -> Types t forall b c a. (b -> c) -> (a -> b) -> a -> c . (t -> [t] -> [t] forall a. a -> [a] -> [a] :[])) list_singleton_ :: HasValues t => [OpExpr t] -> OpExpr t list_singleton_ :: [OpExpr t] -> OpExpr t list_singleton_ = 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 list_singleton list_singleton :: HasValues t => OpExpr t -> OpExpr t list_singleton :: OpExpr t -> OpExpr t list_singleton = OP -> UnaryVOp t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t vUnaryOp OP "list-singleton" (t -> Result t forall t. t -> Result t Normal (t -> Result t) -> (Values t -> t) -> UnaryVOp t forall b c a. (b -> c) -> (a -> b) -> a -> c . Values t -> t forall t. HasValues t => Values t -> t inject (Values t -> t) -> (Values t -> Values t) -> Values t -> t forall b c a. (b -> c) -> (a -> b) -> a -> c . [Values t] -> Values t forall t. HasValues t => [Values t] -> Values t list ([Values t] -> Values t) -> (Values t -> [Values t]) -> Values t -> Values t forall b c a. (b -> c) -> (a -> b) -> a -> c . (Values t -> [Values t] -> [Values t] forall a. a -> [a] -> [a] :[])) nil_ :: HasValues t => [OpExpr t] -> OpExpr t nil_ :: [OpExpr t] -> OpExpr t nil_ = OpExpr t -> [OpExpr t] -> OpExpr t forall t. NullaryExpr t -> [NullaryExpr t] -> NullaryExpr t nullaryOp OpExpr t forall t. HasValues t => OpExpr t nil nil :: HasValues t => OpExpr t nil :: OpExpr t nil = OP -> NullaryOp t -> OpExpr t forall t. OP -> NullaryOp t -> OpExpr t NullaryOp OP "nil" (t -> NullaryOp t forall t. t -> Result t Normal (t -> NullaryOp t) -> t -> NullaryOp 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 $ [Values t] -> Values t forall t. HasValues t => [Values t] -> Values t list []) is_nil_ :: HasValues t => [OpExpr t] -> OpExpr t is_nil_ :: [OpExpr t] -> OpExpr t is_nil_ = 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 is_nil is_nil :: HasValues t => OpExpr t -> OpExpr t is_nil :: OpExpr t -> OpExpr t is_nil = OP -> UnaryOp t -> OpExpr t -> OpExpr t forall t. OP -> UnaryOp t -> OpExpr t -> OpExpr t UnaryOp OP "is-nil" UnaryOp t forall t t. (HasValues t, HasValues t) => t -> Result t op where op :: t -> Result t op t xs | Just Values t lv <- t -> Maybe (Values t) forall t. HasValues t => t -> Maybe (Values t) project t xs = case Values t lv of ADTVal Name "list" [] -> 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 $ Values t forall t. HasValues t => Values t true_ Values t _ -> 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 $ Values t forall t. HasValues t => Values t false_ | Bool otherwise = OP -> Result t forall t. OP -> Result t ProjErr OP "is-nil" cons_ :: HasValues t =>[OpExpr t] -> OpExpr t cons_ :: [OpExpr t] -> OpExpr t cons_ = 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 cons cons :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t cons :: OpExpr t -> OpExpr t -> OpExpr t cons = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t vBinaryOp OP "cons" 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 Values t lv = case Values t lv of ADTVal Name "list" [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 (Values t -> t) -> Values t -> t forall a b. (a -> b) -> a -> b $ Name -> [t] -> Values t forall t. Name -> [t] -> Values t ADTVal Name "list" (Values t -> t forall t. HasValues t => Values t -> t inject Values t vt -> [t] -> [t] forall a. a -> [a] -> [a] :[t] xs) Values t _ -> OP -> Result t forall t. OP -> Result t SortErrOP "cons should be given a value and a list" list_ :: HasValues t => [OpExpr t] -> OpExpr t list_ :: [OpExpr t] -> OpExpr t list_ = OP -> NaryVOp t -> [OpExpr t] -> OpExpr t forall t. HasValues t => OP -> NaryVOp t -> [OpExpr t] -> OpExpr t vNaryOp OP "list" (t -> Result t forall t. t -> Result t Normal (t -> Result t) -> ([Values t] -> t) -> NaryVOp t forall b c a. (b -> c) -> (a -> b) -> a -> c . Values t -> t forall t. HasValues t => Values t -> t inject (Values t -> t) -> ([Values t] -> Values t) -> [Values t] -> t forall b c a. (b -> c) -> (a -> b) -> a -> c . [Values t] -> Values t forall t. HasValues t => [Values t] -> Values t list) list_append_ :: HasValues t => [OpExpr t] -> OpExpr t list_append_ :: [OpExpr t] -> OpExpr t list_append_ = 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 list_append list_append :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t list_append :: OpExpr t -> OpExpr t -> OpExpr t list_append = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t forall t. HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t vBinaryOp OP "list-append" BinaryVOp t forall t. HasValues t => Values t -> Values t -> Result t op where op :: Values t -> Values t -> Result t op (ADTVal Name "list" [t] l1) (ADTVal Name "list" [t] l2) = 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 $ Name -> [t] -> Values t forall t. Name -> [t] -> Values t ADTVal Name "list" ([t] l1 [t] -> [t] -> [t] forall a. [a] -> [a] -> [a] ++ [t] l2) op Values t _ Values t _ = OP -> Result t forall t. OP -> Result t SortErr OP "list-append not applied to two lists" isList :: Values t -> Bool isList (ADTVal Name "list" [t] l) = (Maybe (Values t) -> Bool) -> [Maybe (Values t)] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (Maybe (Values t) -> Bool forall a. Maybe a -> Bool isJust) ([Maybe (Values t)] -> Bool) -> [Maybe (Values t)] -> Bool forall a b. (a -> b) -> a -> b $ (t -> Maybe (Values t)) -> [t] -> [Maybe (Values t)] forall a b. (a -> b) -> [a] -> [b] map t -> Maybe (Values t) forall t. HasValues t => t -> Maybe (Values t) project [t] l isList Values t _ = Bool False toList :: Values t -> [Values t] toList (ADTVal Name "list" [t] l) = (t -> Values t) -> [t] -> [Values t] forall a b. (a -> b) -> [a] -> [b] map (Maybe (Values t) -> Values t forall a. HasCallStack => Maybe a -> a fromJust (Maybe (Values t) -> Values t) -> (t -> Maybe (Values t)) -> t -> Values t forall b c a. (b -> c) -> (a -> b) -> a -> c . t -> Maybe (Values t) forall t. HasValues t => t -> Maybe (Values t) project) [t] l toList Values t _ = OP -> [Values t] forall a. HasCallStack => OP -> a error OP "list-append 1" list_concat_ :: HasValues t => [OpExpr t] -> OpExpr t list_concat_ :: [OpExpr t] -> OpExpr t list_concat_ = [OpExpr t] -> OpExpr t forall t. HasValues t => [OpExpr t] -> OpExpr t list_concat list_concat :: HasValues t => [OpExpr t] -> OpExpr t list_concat :: [OpExpr t] -> OpExpr t list_concat = OP -> NaryVOp t -> [OpExpr t] -> OpExpr t forall t. HasValues t => OP -> NaryVOp t -> [OpExpr t] -> OpExpr t vNaryOp OP "list-concat" NaryVOp t forall (t :: * -> *) t. (Foldable t, HasValues t) => t (Values t) -> Result t op where op :: t (Values t) -> Result t op t (Values t) args | (Values t -> Bool) -> t (Values t) -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all Values t -> Bool forall t. HasValues t => Values t -> Bool isList t (Values t) args = 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 $ [Values t] -> Values t forall t. HasValues t => [Values t] -> Values t list ([Values t] -> Values t) -> [Values t] -> Values t forall a b. (a -> b) -> a -> b $ (Values t -> [Values t]) -> t (Values t) -> [Values t] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap Values t -> [Values t] forall t. HasValues t => Values t -> [Values t] toList t (Values t) args | Bool otherwise = OP -> Result t forall t. OP -> Result t SortErr OP "list-concat not applied to lists" head_, tail_ :: HasValues t => [OpExpr t] -> OpExpr t head_ :: [OpExpr t] -> OpExpr t 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 headOp tail_ :: [OpExpr t] -> OpExpr t 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 tailOp headOp,tailOp :: HasValues t => OpExpr t -> OpExpr t headOp :: OpExpr t -> OpExpr t headOp = 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 "list" []) = OP -> Result t forall t. OP -> Result t DomErr OP "head of empty list" op (ADTVal Name "list" (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 "head not applied to a list" tailOp :: OpExpr t -> OpExpr t tailOp = 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 "list" []) = OP -> Result t forall t. OP -> Result t DomErr OP "tail of empty list" op (ADTVal Name "list" (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 "list" [t] xs) op Values t _ = OP -> Result t forall t. OP -> Result t SortErr OP "tail not applied to a list"