{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Expression for 'List'. module Language.Symantic.Expr.List where import Control.Monad import qualified Data.Function as Fun import qualified Data.List as List import Data.Monoid import Data.Proxy (Proxy(..)) import qualified Data.Text as Text import Data.Type.Equality ((:~:)(Refl)) import Language.Symantic.Type import Language.Symantic.Repr import Language.Symantic.Expr.Root import Language.Symantic.Expr.Error import Language.Symantic.Expr.From import Language.Symantic.Expr.Lambda import Language.Symantic.Trans.Common -- * Class 'Sym_List_Lam' -- | Symantic. class Sym_List repr where list_empty :: repr [a] list_cons :: repr a -> repr [a] -> repr [a] list :: [repr a] -> repr [a] list_filter :: repr (a -> Bool) -> repr [a] -> repr [a] list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c] list_reverse :: repr [a] -> repr [a] default list_empty :: Trans t repr => t repr [a] default list_cons :: Trans t repr => t repr a -> t repr [a] -> t repr [a] default list :: Trans t repr => [t repr a] -> t repr [a] default list_filter :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a] default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c] default list_reverse :: Trans t repr => t repr [a] -> t repr [a] list_empty = trans_lift list_empty list_cons = trans_map2 list_cons list l = trans_lift $ list (trans_apply Prelude.<$> l) list_filter = trans_map2 list_filter list_zipWith = trans_map3 list_zipWith list_reverse = trans_map1 list_reverse instance Sym_List Repr_Host where list_empty = return [] list_cons = liftM2 (:) list = sequence list_filter = liftM2 List.filter list_zipWith = liftM3 List.zipWith list_reverse = liftM List.reverse instance Sym_List Repr_Text where list_empty = Repr_Text $ \_p _v -> "[]" list_cons (Repr_Text x) (Repr_Text xs) = Repr_Text $ \p v -> let p' = precedence_List_Cons in paren p p' $ x p' v <> ":" <> xs p' v list l = Repr_Text $ \_p v -> let p' = precedence_Toplevel in "[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]" list_filter = repr_text_app2 "list_filter" list_zipWith = repr_text_app3 "list_zipWith" list_reverse = repr_text_app1 "list_reverse" instance ( Sym_List r1 , Sym_List r2 ) => Sym_List (Dup r1 r2) where list_empty = list_empty `Dup` list_empty list_cons (a1 `Dup` a2) (l1 `Dup` l2) = list_cons a1 l1 `Dup` list_cons a2 l2 list l = let (l1, l2) = foldr (\(x1 `Dup` x2) (xs1, xs2) -> (x1:xs1, x2:xs2)) ([], []) l in list l1 `Dup` list l2 list_filter (f1 `Dup` f2) (l1 `Dup` l2) = list_filter f1 l1 `Dup` list_filter f2 l2 list_zipWith (f1 `Dup` f2) (la1 `Dup` la2) (lb1 `Dup` lb2) = list_zipWith f1 la1 lb1 `Dup` list_zipWith f2 la2 lb2 list_reverse (l1 `Dup` l2) = list_reverse l1 `Dup` list_reverse l2 -- * Type 'Expr_List' -- | Expression. data Expr_List (root:: *) type instance Root_of_Expr (Expr_List root) = root type instance Type_of_Expr (Expr_List root) = Type_List type instance Sym_of_Expr (Expr_List root) repr = (Sym_List repr) type instance Error_of_Expr ast (Expr_List root) = No_Error_Expr -- | Parsing utility to check that the given type is a 'Type_List' -- or raise 'Error_Expr_Type_mismatch'. check_type_list :: forall ast ex root ty h ret. ( root ~ Root_of_Expr ex , ty ~ Type_Root_of_Expr ex , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) ) => Proxy ex -> ast -> ty h -> (Type_List ty h -> Either (Error_of_Expr ast root) ret) -> Either (Error_of_Expr ast root) ret check_type_list ex ast ty k = case unlift_type $ unType_Root ty of Just ty_l -> k ty_l Nothing -> Left $ error_expr ex $ Error_Expr_Type_mismatch ast (Exists_Type (type_list $ type_var0 SZero :: ty [Var0])) (Exists_Type ty) -- | Parse 'list_empty'. list_empty_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , Type_from ast ty , Lift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> Expr_From ast (Expr_List root) hs ret list_empty_from ast_ty_a ex ast _ctx k = either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $ type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $ k (type_list ty_a) $ Forall_Repr_with_Context $ Fun.const list_empty -- | Parse 'list_cons'. list_cons_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> Expr_From ast (Expr_List root) hs ret list_cons_from ast_a ast_l ex ast ctx k = expr_from (Proxy::Proxy root) ast_a ctx $ \(ty_a::ty h_a) (Forall_Repr_with_Context a) -> expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::ty h_l) (Forall_Repr_with_Context l) -> check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) -> check_eq_type ex ast ty_a ty_l_a $ \Refl -> k (type_list ty_a) $ Forall_Repr_with_Context $ \c -> list_cons (a c) (l c) -- | Parse 'list'. list_from :: forall root ex ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , ex ~ Expr_List root , Eq_Type ty , Type_from ast ty , Expr_from ast root , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> [ast] -> Expr_From ast ex hs ret list_from ast_ty_a ast_as = case type_from (Proxy::Proxy ty) ast_ty_a (Right . Exists_Type) of Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast Right (Exists_Type ty_a) -> go ty_a [] ast_as where go :: ty ty_a -> [Forall_Repr_with_Context root hs ty_a] -> [ast] -> Expr_From ast (Expr_List root) hs ret go ty_a as [] _ex _ast _ctx k = k (type_list ty_a) $ Forall_Repr_with_Context $ \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as) go ty_a as (ast_x:ast_xs) ex ast ctx k = expr_from (Proxy::Proxy root) ast_x ctx $ \(ty_x::ty h_x) x -> check_eq_type ex ast ty_a ty_x $ \Refl -> go ty_a (x:as) ast_xs ex ast ctx k -- | Parse 'list_filter'. list_filter_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_Bool (Type_of_Expr root) , Lift_Type Type_Fun (Type_of_Expr root) , Unlift_Type Type_Fun (Type_of_Expr root) , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> Expr_From ast (Expr_List root) hs ret list_filter_from ast_f ast_l ex ast ctx k = expr_from (Proxy::Proxy root) ast_f ctx $ \(ty_f::ty h_f) (Forall_Repr_with_Context f) -> expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::ty h_l) (Forall_Repr_with_Context l) -> check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b :: Type_Fun ty h_f) -> check_eq_type ex ast type_bool ty_f_b $ \Refl -> check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) -> check_eq_type ex ast ty_f_a ty_l_a $ \Refl -> k ty_l $ Forall_Repr_with_Context $ \c -> list_filter (f c) (l c) -- | Parse 'list_zipWith'. list_zipWith_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_Fun (Type_of_Expr root) , Unlift_Type Type_Fun (Type_of_Expr root) , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> ast -> Expr_From ast (Expr_List root) hs ret list_zipWith_from ast_f ast_la ast_lb ex ast ctx k = -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] expr_from (Proxy::Proxy root) ast_f ctx $ \(ty_f::ty h_f) (Forall_Repr_with_Context f) -> expr_from (Proxy::Proxy root) ast_la ctx $ \(ty_la::ty h_la) (Forall_Repr_with_Context la) -> expr_from (Proxy::Proxy root) ast_lb ctx $ \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) -> check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b2c :: Type_Fun ty h_f) -> check_type_fun ex ast ty_f_b2c $ \(Type_Type2 Proxy ty_f_b ty_f_c :: Type_Fun ty h_f_b2c) -> check_type_list ex ast ty_la $ \(Type_Type1 _ ty_l_a) -> check_type_list ex ast ty_lb $ \(Type_Type1 _ ty_l_b) -> check_eq_type ex ast ty_f_a ty_l_a $ \Refl -> check_eq_type ex ast ty_f_b ty_l_b $ \Refl -> check_eq_type ex ast ty_f_a ty_l_a $ \Refl -> k (type_list ty_f_c) $ Forall_Repr_with_Context $ \c -> list_zipWith (f c) (la c) (lb c) -- | Parse 'list_reverse'. list_reverse_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_List (Type_of_Expr root) , Unlift_Type Type_List (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> Expr_From ast (Expr_List root) hs ret list_reverse_from ast_l ex ast ctx k = expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::ty h_l) (Forall_Repr_with_Context l) -> check_type_list ex ast ty_l $ \(Type_Type1 _ _ty_l_a) -> k ty_l $ Forall_Repr_with_Context $ \c -> list_reverse (l c)