( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Type0_Constraint Num (Type_Root_of_Expr root)
- , Type0_Lift Type_Fun (Type_of_Expr root)
+ , Type0_Lift Type_Integer (Type_of_Expr root)
+ , Type0_Unlift Type_Integer (Type_of_Expr root)
+ , Type0_Lift Type_Fun (Type_of_Expr root)
, Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Num root) root)
case ast of
AST "abs" asts -> from_ast1 asts (class_op1_from Expr.abs c) ex ast
AST "negate" asts -> from_ast1 asts (class_op1_from Expr.negate c) ex ast
+ AST "signum" asts -> from_ast1 asts (class_op1_from Expr.signum c) ex ast
AST "+" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 (Expr.+) c) (class_op2_from (Expr.+) c) ex ast
AST "-" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 (Expr.-) c) (class_op2_from (Expr.-) c) ex ast
AST "*" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 (Expr.*) c) (class_op2_from (Expr.*) c) ex ast
+ AST "fromInteger" asts -> from_ast1 asts fromInteger_from ex ast
_ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Integral
( Expr_From AST root
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Maybe root) root)
) => Expr_From AST (Expr_Maybe root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "maybe" asts -> from_ast3 asts maybe_from ex ast ctx k
- AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
- AST "just" asts -> from_ast1 asts just_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "maybe" asts -> from_ast3 asts maybe_from ex ast
+ AST "nothing" asts -> from_ast1 asts nothing_from ex ast
+ AST "just" asts -> from_ast1 asts just_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Eq
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Eq root) root)
) => Expr_From AST (Expr_Eq root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "==" asts -> from_ast012 asts Nothing (Just (eq_from1 (Expr.==))) (eq_from (Expr.==)) ex ast ctx k
- AST "/=" asts -> from_ast012 asts Nothing (Just (eq_from1 (Expr./=))) (eq_from (Expr./=)) ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "==" asts -> from_ast012 asts Nothing (Just (eq_from1 (Expr.==))) (eq_from (Expr.==)) ex ast
+ AST "/=" asts -> from_ast012 asts Nothing (Just (eq_from1 (Expr./=))) (eq_from (Expr./=)) ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Ord
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Ord root) root)
) => Expr_From AST (Expr_Ord root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
let c = (Proxy :: Proxy Ord) in
case ast of
- AST "compare" asts -> from_ast012 asts Nothing (Just compare_from1) compare_from ex ast ctx k
- AST "<" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.<)) (ord_from (Expr.<)) ex ast ctx k
- AST "<=" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.<=)) (ord_from (Expr.<=)) ex ast ctx k
- AST ">" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.>)) (ord_from (Expr.>)) ex ast ctx k
- AST ">=" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.>=)) (ord_from (Expr.>=)) ex ast ctx k
- AST "min" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 Expr.min c) (class_op2_from Expr.min c) ex ast ctx k
- AST "max" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 Expr.max c) (class_op2_from Expr.max c) ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "compare" asts -> from_ast012 asts Nothing (Just compare_from1) compare_from ex ast
+ AST "<" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.<)) (ord_from (Expr.<)) ex ast
+ AST "<=" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.<=)) (ord_from (Expr.<=)) ex ast
+ AST ">" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.>)) (ord_from (Expr.>)) ex ast
+ AST ">=" asts -> from_ast012 asts Nothing (Just $ ord_from1 (Expr.>=)) (ord_from (Expr.>=)) ex ast
+ AST "min" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 Expr.min c) (class_op2_from Expr.min c) ex ast
+ AST "max" asts -> from_ast012 asts Nothing (Just $ class_op2_from1 Expr.max c) (class_op2_from Expr.max c) ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_List
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_List root) root)
) => Expr_From AST (Expr_List root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "[]" asts -> from_ast1 asts list_empty_from ex ast ctx k
- AST ":" asts -> from_ast2 asts list_cons_from ex ast ctx k
- AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
- AST "list" asts ->
+ AST "[]" asts -> from_ast1 asts list_empty_from ex ast
+ AST ":" asts -> from_ast2 asts list_cons_from ex ast
+ AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast
+ AST "list" asts -> \ctx k ->
case asts of
ast_ty_a:asts' -> list_from ast_ty_a asts' ex ast ctx k
_ -> Left $ error_expr ex $
Error_Expr_Wrong_number_of_arguments ast 1
- AST "list_zipWith" asts -> from_ast3 asts list_zipWith_from ex ast ctx k
- AST "list_reverse" asts -> from_ast1 asts list_reverse_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "list_zipWith" asts -> from_ast3 asts list_zipWith_from ex ast
+ AST "list_reverse" asts -> from_ast1 asts list_reverse_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Map
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Map root) root)
) => Expr_From AST (Expr_Map root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
- AST "mapWithKey" asts -> from_ast2 asts mapWithKey_from ex ast ctx k
- AST "map_lookup" asts -> from_ast2 asts map_lookup_from ex ast ctx k
- AST "map_keys" asts -> from_ast1 asts map_keys_from ex ast ctx k
- AST "map_member" asts -> from_ast2 asts map_member_from ex ast ctx k
- AST "map_insert" asts -> from_ast3 asts map_insert_from ex ast ctx k
- AST "map_delete" asts -> from_ast2 asts map_delete_from ex ast ctx k
- AST "map_difference" asts -> from_ast2 asts map_difference_from ex ast ctx k
- AST "map_foldrWithKey" asts -> from_ast3 asts map_foldrWithKey_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast
+ AST "mapWithKey" asts -> from_ast2 asts mapWithKey_from ex ast
+ AST "map_lookup" asts -> from_ast2 asts map_lookup_from ex ast
+ AST "map_keys" asts -> from_ast1 asts map_keys_from ex ast
+ AST "map_member" asts -> from_ast2 asts map_member_from ex ast
+ AST "map_insert" asts -> from_ast3 asts map_insert_from ex ast
+ AST "map_delete" asts -> from_ast2 asts map_delete_from ex ast
+ AST "map_difference" asts -> from_ast2 asts map_difference_from ex ast
+ AST "map_foldrWithKey" asts -> from_ast3 asts map_foldrWithKey_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Functor
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Functor root) root)
) => Expr_From AST (Expr_Functor root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "fmap" asts -> from_ast2 asts fmap_from ex ast ctx k
- AST "<$>" asts -> from_ast2 asts fmap_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "fmap" asts -> from_ast2 asts fmap_from ex ast
+ AST "<$>" asts -> from_ast2 asts fmap_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_MonoFunctor
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Applicative root) root)
) => Expr_From AST (Expr_Applicative root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "pure" asts -> from_ast2 asts pure_from ex ast ctx k
- AST "<*>" asts -> from_ast2 asts ltstargt_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "pure" asts -> from_ast2 asts pure_from ex ast
+ AST "<*>" asts -> from_ast2 asts ltstargt_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Traversable
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
( Expr_From AST root
, Type0_Constraint Eq (Type_Root_of_Expr root)
, Type0_Constraint Monoid (Type_Root_of_Expr root)
+ , Type0_Constraint Num (Type_Root_of_Expr root)
, Type0_Constraint Ord (Type_Root_of_Expr root)
, Type0_Eq (Type_Root_of_Expr root)
, Type0_Lift Type_Bool (Type_of_Expr root)
, Type0_Lift Type_Fun (Type_of_Expr root)
, Type0_Lift Type_Int (Type_of_Expr root)
+ , Type0_Lift Type_List (Type_of_Expr root)
, Type0_Unlift Type_Fun (Type_of_Expr root)
, Type1_Constraint Foldable (Type_Root_of_Expr root)
, Type1_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Foldable root) root)
) => Expr_From AST (Expr_Foldable root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "foldMap" asts -> from_ast2 asts foldMap_from ex ast ctx k
- AST "null" asts -> from_ast1 asts null_from ex ast ctx k
- AST "length" asts -> from_ast1 asts length_from ex ast ctx k
- AST "minimum" asts -> from_ast1 asts minimum_from ex ast ctx k
- AST "maximum" asts -> from_ast1 asts maximum_from ex ast ctx k
- AST "elem" asts -> from_ast2 asts elem_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "foldMap" asts -> from_ast2 asts foldMap_from ex ast
+ AST "foldr" asts -> from_ast3 asts (foldr_from Expr.foldr) ex ast
+ AST "foldr'" asts -> from_ast3 asts (foldr_from Expr.foldr') ex ast
+ AST "foldl" asts -> from_ast3 asts (foldl_from Expr.foldl) ex ast
+ AST "foldl'" asts -> from_ast3 asts (foldl_from Expr.foldl') ex ast
+ AST "null" asts -> from_ast1 asts null_from ex ast
+ AST "length" asts -> from_ast1 asts length_from ex ast
+ AST "minimum" asts -> from_ast1 asts minimum_from ex ast
+ AST "maximum" asts -> from_ast1 asts maximum_from ex ast
+ AST "elem" asts -> from_ast2 asts elem_from ex ast
+ AST "sum" asts -> from_ast1 asts sum_from ex ast
+ AST "product" asts -> from_ast1 asts product_from ex ast
+ AST "toList" asts -> from_ast1 asts toList_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Monoid
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Monoid root) root)
) => Expr_From AST (Expr_Monoid root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "mempty" asts -> from_ast1 asts mempty_from ex ast ctx k
- AST "mappend" asts -> from_ast012 asts Nothing (Just mappend_from1) mappend_from ex ast ctx k
- AST "<>" asts -> from_ast012 asts Nothing (Just mappend_from1) mappend_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "mempty" asts -> from_ast1 asts mempty_from ex ast
+ AST "mappend" asts -> from_ast012 asts Nothing (Just mappend_from1) mappend_from ex ast
+ AST "<>" asts -> from_ast012 asts Nothing (Just mappend_from1) mappend_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Monad
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Monad root) root)
) => Expr_From AST (Expr_Monad root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "return" asts -> from_ast2 asts return_from ex ast ctx k
- AST ">>=" asts -> from_ast2 asts bind_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "return" asts -> from_ast2 asts return_from ex ast
+ AST ">>=" asts -> from_ast2 asts bind_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Either
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Either root) root)
) => Expr_From AST (Expr_Either root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "left" asts -> from_ast2 asts left_from ex ast ctx k
- AST "right" asts -> from_ast2 asts right_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "left" asts -> from_ast2 asts left_from ex ast
+ AST "right" asts -> from_ast2 asts right_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_From AST Expr_Tuple2
( Expr_From AST root
, Type0_Eq (Type_Root_of_Expr root)
, Root_of_Expr root ~ root
, IBool (Is_Last_Expr (Expr_Tuple2 root) root)
) => Expr_From AST (Expr_Tuple2 root) where
- expr_from ex ast ctx k =
+ expr_from ex ast =
case ast of
- AST "(,)" asts -> from_ast2 asts tuple2_from ex ast ctx k
- AST "fst" asts -> from_ast1 asts fst_from ex ast ctx k
- AST "snd" asts -> from_ast1 asts snd_from ex ast ctx k
- _ -> Left $ error_expr_unsupported ex ast
+ AST "(,)" asts -> from_ast2 asts tuple2_from ex ast
+ AST "fst" asts -> from_ast1 asts fst_from ex ast
+ AST "snd" asts -> from_ast1 asts snd_from ex ast
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
-- * Class 'Sym_Foldable'
-- | Symantic.
class Sym_Foldable repr where
- foldMap :: (Foldable t, Monoid m) => repr (a -> m) -> repr (t a) -> repr m
- length :: Foldable t => repr (t a) -> repr Int
- null :: Foldable t => repr (t a) -> repr Bool
- minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
- maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
- elem :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
- default foldMap :: (Trans tr repr, Foldable t, Monoid m)
- => tr repr (a -> m) -> tr repr (t a) -> tr repr m
- default length :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
- default null :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
- default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
- default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
- default elem :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
+ foldMap :: (Foldable f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
+ foldr :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
+ foldr' :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
+ foldl :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
+ foldl' :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
+ length :: Foldable f => repr (f a) -> repr Int
+ null :: Foldable f => repr (f a) -> repr Bool
+ minimum :: (Foldable f, Ord a) => repr (f a) -> repr a
+ maximum :: (Foldable f, Ord a) => repr (f a) -> repr a
+ elem :: (Foldable f, Eq a) => repr a -> repr (f a) -> repr Bool
+ sum :: (Foldable f, Num a) => repr (f a) -> repr a
+ product :: (Foldable f, Num a) => repr (f a) -> repr a
+ toList :: Foldable f => repr (f a) -> repr [a]
+ default foldMap :: (Trans t repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
+ default foldr :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
+ default foldr' :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
+ default foldl :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
+ default foldl' :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
+ default length :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
+ default null :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
+ default minimum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
+ default maximum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
+ default elem :: (Trans t repr, Foldable f, Eq a) => t repr a -> t repr (f a) -> t repr Bool
+ default sum :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
+ default product :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
+ default toList :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
foldMap = trans_map2 foldMap
+ foldr = trans_map3 foldr
+ foldr' = trans_map3 foldr'
+ foldl = trans_map3 foldl
+ foldl' = trans_map3 foldl'
length = trans_map1 length
null = trans_map1 null
minimum = trans_map1 minimum
maximum = trans_map1 maximum
elem = trans_map2 elem
+ sum = trans_map1 sum
+ product = trans_map1 product
+ toList = trans_map1 toList
instance Sym_Foldable Repr_Host where
foldMap = liftM2 Foldable.foldMap
- null = liftM Foldable.null
- length = liftM Foldable.length
- minimum = liftM Foldable.minimum
- maximum = liftM Foldable.maximum
+ foldr = liftM3 Foldable.foldr
+ foldr' = liftM3 Foldable.foldr'
+ foldl = liftM3 Foldable.foldl
+ foldl' = liftM3 Foldable.foldl'
+ null = liftM Foldable.null
+ length = liftM Foldable.length
+ minimum = liftM Foldable.minimum
+ maximum = liftM Foldable.maximum
elem = liftM2 Foldable.elem
+ sum = liftM Foldable.sum
+ product = liftM Foldable.product
+ toList = liftM Foldable.toList
instance Sym_Foldable Repr_Text where
foldMap = repr_text_app2 "foldMap"
+ foldr = repr_text_app3 "foldr"
+ foldr' = repr_text_app3 "foldr'"
+ foldl = repr_text_app3 "foldl"
+ foldl' = repr_text_app3 "foldl'"
null = repr_text_app1 "null"
length = repr_text_app1 "length"
minimum = repr_text_app1 "minimum"
maximum = repr_text_app1 "maximum"
elem = repr_text_app2 "elem"
-instance
- ( Sym_Foldable r1
- , Sym_Foldable r2
- ) => Sym_Foldable (Repr_Dup r1 r2) where
+ sum = repr_text_app1 "sum"
+ product = repr_text_app1 "product"
+ toList = repr_text_app1 "toList"
+instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
foldMap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
foldMap f1 m1 `Repr_Dup` foldMap f2 m2
+ foldr (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
+ foldr f1 a1 m1 `Repr_Dup` foldr f2 a2 m2
+ foldr' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
+ foldr' f1 a1 m1 `Repr_Dup` foldr' f2 a2 m2
+ foldl (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
+ foldl f1 a1 m1 `Repr_Dup` foldl f2 a2 m2
+ foldl' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
+ foldl' f1 a1 m1 `Repr_Dup` foldl' f2 a2 m2
length (f1 `Repr_Dup` f2) = length f1 `Repr_Dup` length f2
null (f1 `Repr_Dup` f2) = null f1 `Repr_Dup` null f2
minimum (f1 `Repr_Dup` f2) = minimum f1 `Repr_Dup` minimum f2
maximum (f1 `Repr_Dup` f2) = maximum f1 `Repr_Dup` maximum f2
elem (a1 `Repr_Dup` a2) (f1 `Repr_Dup` f2) = elem a1 f1 `Repr_Dup` elem a2 f2
+ sum (f1 `Repr_Dup` f2) = sum f1 `Repr_Dup` sum f2
+ product (f1 `Repr_Dup` f2) = product f1 `Repr_Dup` product f2
+ toList (f1 `Repr_Dup` f2) = toList f1 `Repr_Dup` toList f2
-- * Type 'Expr_Foldable'
-- | Expression.
k ty_f_m $ Forall_Repr_with_Context $
\c -> foldMap (f c) (ta c)
+-- | Parse 'foldr' or |foldr'|.
+foldr_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
+ , Expr_From ast root
+ , Type0_Eq ty
+ , Type0_Lift Type_Fun (Type_of_Expr root)
+ , Type0_Unlift Type_Fun (Type_of_Expr root)
+ , Type1_Constraint Foldable ty
+ , Type1_Unlift (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
+ -> ast -> ast -> ast
+ -> ExprFrom ast (Expr_Foldable root) hs ret
+foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
+ -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
+ expr_from (Proxy::Proxy root) ast_f ctx $
+ \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
+ expr_from (Proxy::Proxy root) ast_b ctx $
+ \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
+ check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
+ check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
+ check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
+ check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
+ check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
+ check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
+ check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
+ k ty_b $ Forall_Repr_with_Context $
+ \c -> fold (f c) (b c) (ta c)
+
+-- | Parse 'foldl' or |foldl'|.
+foldl_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
+ , Expr_From ast root
+ , Type0_Eq ty
+ , Type0_Lift Type_Fun (Type_of_Expr root)
+ , Type0_Unlift Type_Fun (Type_of_Expr root)
+ , Type1_Constraint Foldable ty
+ , Type1_Unlift (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
+ -> ast -> ast -> ast
+ -> ExprFrom ast (Expr_Foldable root) hs ret
+foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
+ -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
+ expr_from (Proxy::Proxy root) ast_f ctx $
+ \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
+ expr_from (Proxy::Proxy root) ast_b ctx $
+ \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
+ check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
+ check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
+ check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
+ check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
+ check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
+ check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
+ check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
+ k ty_b $ Forall_Repr_with_Context $
+ \c -> fold (f c) (b c) (ta c)
+
-- | Parse 'length'.
length_from
:: forall root ty ast hs ret.
check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
k type_bool $ Forall_Repr_with_Context $
\c -> a c `elem` ta c
+
+-- | Parse 'sum'.
+sum_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
+ , Expr_From ast root
+ , Type0_Eq ty
+ , Type0_Constraint Num ty
+ , Type1_Constraint Foldable ty
+ , Type1_Unlift (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast
+ -> ExprFrom ast (Expr_Foldable root) hs ret
+sum_from ast_ta ex ast ctx k =
+ -- sum :: (Foldable t, Num a) => t a -> a
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
+ check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
+ check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
+ check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
+ k ty_t_a $ Forall_Repr_with_Context $
+ \c -> sum (ta c)
+
+-- | Parse 'product'.
+product_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
+ , Expr_From ast root
+ , Type0_Eq ty
+ , Type0_Constraint Num ty
+ , Type1_Constraint Foldable ty
+ , Type1_Unlift (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast
+ -> ExprFrom ast (Expr_Foldable root) hs ret
+product_from ast_ta ex ast ctx k =
+ -- product :: (Foldable t, Num a) => t a -> a
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
+ check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
+ check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
+ check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
+ k ty_t_a $ Forall_Repr_with_Context $
+ \c -> product (ta c)
+
+-- | Parse 'toList'.
+toList_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
+ , Expr_From ast root
+ , Type0_Eq ty
+ , Type0_Lift Type_List (Type_of_Expr root)
+ , Type0_Constraint Num ty
+ , Type1_Constraint Foldable ty
+ , Type1_Unlift (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast
+ -> ExprFrom ast (Expr_Foldable root) hs ret
+toList_from ast_ta ex ast ctx k =
+ -- toList :: Foldable t => t a -> [a]
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
+ check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
+ check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
+ k (type_list ty_t_a) $ Forall_Repr_with_Context $
+ \c -> toList (ta c)
import Prelude hiding (Num(..))
import Prelude (Num)
import qualified Prelude
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(Refl))
import Language.Symantic.Type
import Language.Symantic.Repr
-- * Class 'Sym_Num'
-- | Symantic.
class Sym_Num repr where
- abs :: Num n => repr n -> repr n
- negate :: Num n => repr n -> repr n
- (+) :: Num n => repr n -> repr n -> repr n
- (-) :: Num n => repr n -> repr n -> repr n
- (*) :: Num n => repr n -> repr n -> repr n
+ abs :: Num n => repr n -> repr n
+ negate :: Num n => repr n -> repr n
+ signum :: Num n => repr n -> repr n
+ (+) :: Num n => repr n -> repr n -> repr n
+ (-) :: Num n => repr n -> repr n -> repr n
+ (*) :: Num n => repr n -> repr n -> repr n
+ fromInteger :: Num n => repr Integer -> repr n
- default abs :: (Trans t repr, Num n) => t repr n -> t repr n
- default negate :: (Trans t repr, Num n) => t repr n -> t repr n
- default (+) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
- default (-) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
- default (*) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
+ default abs :: (Trans t repr, Num n) => t repr n -> t repr n
+ default negate :: (Trans t repr, Num n) => t repr n -> t repr n
+ default signum :: (Trans t repr, Num n) => t repr n -> t repr n
+ default (+) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
+ default (-) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
+ default (*) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
+ default fromInteger :: (Trans t repr, Num n) => t repr Integer -> t repr n
- abs = trans_map1 abs
- negate = trans_map1 negate
- (+) = trans_map2 (+)
- (-) = trans_map2 (-)
- (*) = trans_map2 (*)
+ abs = trans_map1 abs
+ negate = trans_map1 negate
+ signum = trans_map1 signum
+ (+) = trans_map2 (+)
+ (-) = trans_map2 (-)
+ (*) = trans_map2 (*)
+ fromInteger = trans_map1 fromInteger
infixl 6 +
infixl 6 -
infixl 7 *
instance Sym_Num Repr_Host where
- abs = liftM Prelude.abs
- negate = liftM Prelude.negate
- (+) = liftM2 (Prelude.+)
- (-) = liftM2 (Prelude.-)
- (*) = liftM2 (Prelude.*)
+ abs = liftM Prelude.abs
+ negate = liftM Prelude.negate
+ signum = liftM Prelude.signum
+ (+) = liftM2 (Prelude.+)
+ (-) = liftM2 (Prelude.-)
+ (*) = liftM2 (Prelude.*)
+ fromInteger = liftM Prelude.fromInteger
instance Sym_Num Repr_Text where
- abs = repr_text_app1 "abs"
- negate = repr_text_app1 "negate"
- (+) = repr_text_infix "+" (Precedence 6)
- (-) = repr_text_infix "-" (Precedence 6)
- (*) = repr_text_infix "-" (Precedence 7)
-instance
- ( Sym_Num r1
- , Sym_Num r2
- ) => Sym_Num (Repr_Dup r1 r2) where
+ abs = repr_text_app1 "abs"
+ negate = repr_text_app1 "negate"
+ signum = repr_text_app1 "signum"
+ (+) = repr_text_infix "+" (Precedence 6)
+ (-) = repr_text_infix "-" (Precedence 6)
+ (*) = repr_text_infix "-" (Precedence 7)
+ fromInteger = repr_text_app1 "fromInteger"
+instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Repr_Dup r1 r2) where
abs (x1 `Repr_Dup` x2) = abs x1 `Repr_Dup` abs x2
negate (x1 `Repr_Dup` x2) = negate x1 `Repr_Dup` negate x2
+ signum (x1 `Repr_Dup` x2) = signum x1 `Repr_Dup` signum x2
(+) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (+) x1 y1 `Repr_Dup` (+) x2 y2
(-) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (-) x1 y1 `Repr_Dup` (-) x2 y2
(*) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (*) x1 y1 `Repr_Dup` (*) x2 y2
+ fromInteger (x1 `Repr_Dup` x2) = fromInteger x1 `Repr_Dup` fromInteger x2
-- * Type 'Expr_Num'
-- | Expression.
type instance Type_of_Expr (Expr_Num root) = No_Type
type instance Sym_of_Expr (Expr_Num root) repr = Sym_Num repr
type instance Error_of_Expr ast (Expr_Num root) = No_Error_Expr
+
+-- | Parse 'fst'.
+fromInteger_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Num root)
+ , Type0_Eq ty
+ , Expr_From ast root
+ , Type0_Lift Type_Integer (Type_of_Expr root)
+ , Type0_Unlift Type_Integer (Type_of_Expr root)
+ , Type0_Constraint Num ty
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast
+ -> ExprFrom ast (Expr_Num root) hs ret
+fromInteger_from ast_i ex ast ctx k =
+ -- fromInteger :: Num a => Integer -> a
+ expr_from (Proxy::Proxy root) ast_i ctx $
+ \(ty_i::ty h_i) (Forall_Repr_with_Context i) ->
+ check_type0_eq ex ast type_integer ty_i $ \Refl ->
+ k ty_i $ Forall_Repr_with_Context $
+ \c -> fromInteger (i c)
type1_constraint _c Type2{} = Just Dict
instance Type1_Constraint Traversable (Type_Either root) where
type1_constraint _c Type2{} = Just Dict
+instance Type1_Constraint Foldable (Type_Either root) where
+ type1_constraint _c Type2{} = Just Dict
instance Type1_Constraint Monad (Type_Either root) where
type1_constraint _c Type2{} = Just Dict
instance Type0_Family Type_Family_MonoElement (Type_Either root) where
sourcephile / git / haskell / symantic.git / commitdiff