{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Expression for 'List'. module Language.Symantic.Expr.List where import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Language.Symantic.Type import Language.Symantic.Trans.Common import Language.Symantic.Expr.Common import Language.Symantic.Expr.Lambda -- * 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] 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] list_empty = trans_lift list_empty list_cons = trans_map2 list_cons list l = trans_lift $ list (trans_apply Prelude.<$> l) -- | Symantic requiring a 'Lambda'. class Sym_List_Lam lam repr where list_filter :: repr (Lambda lam a Bool) -> repr [a] -> repr [a] default list_filter :: Trans t repr => t repr (Lambda lam a Bool) -> t repr [a] -> t repr [a] list_filter = trans_map2 list_filter -- * Type 'Expr_List' -- | Expression. data Expr_List (lam:: * -> *) (root:: *) type instance Root_of_Expr (Expr_List lam root) = root type instance Type_of_Expr (Expr_List lam root) = Type_List type instance Sym_of_Expr (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr) type instance Error_of_Expr ast (Expr_List lam root) = No_Error_Expr instance Constraint_Type1 Functor (Type_List root) where constraint_type1 _c (Type_Type1 _ _) = Just Dict instance Constraint_Type1 Applicative (Type_List root) where constraint_type1 _c (Type_Type1 _ _) = Just Dict -- | 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 :: Type_Root_of_Expr ex [Var0])) (Exists_Type ty) -- | Parse 'list_empty'. list_empty_from :: forall root lam ty ty_root ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List lam root) , ty_root ~ Type_Root_of_Expr root , Type_from ast ty_root , Lift_Type_Root Type_List ty_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 lam root) hs ret list_empty_from ast_ty_a ex ast _ctx k = either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $ type_from (Proxy::Proxy ty_root) ast_ty_a $ \ty_a -> Right $ k (type_list ty_a) $ Forall_Repr_with_Context $ const list_empty -- | Parse 'list_cons'. list_cons_from :: forall root lam ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List lam root) , Eq_Type (Type_Root_of_Expr root) , 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 lam root) hs ret list_cons_from ast_a ast_l ex ast ctx k = expr_from (Proxy::Proxy root) ast_a ctx $ \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) -> expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::Type_Root_of_Expr root 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 lam ex ty ty_root ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List lam root) , ty_root ~ Type_Root_of_Expr root , ex ~ Expr_List lam root , Eq_Type (Type_Root_of_Expr root) , Type_from ast ty_root , 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 , Root_of_Type ty_root ~ ty_root ) => ast -> [ast] -> Expr_From ast ex hs ret list_from ast_ty_a ast_as = case type_from (Proxy::Proxy ty_root) 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 :: Type_Root_of_Expr root ty_a -> [Forall_Repr_with_Context root hs ty_a] -> [ast] -> Expr_From ast (Expr_List lam 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::Type_Root_of_Expr root 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 lam ty ty_root ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_List lam root) , ty_root ~ Type_of_Expr root , Eq_Type (Type_Root_of_Expr root) , Expr_from ast root , Lift_Type Type_Bool ty_root , Lift_Type (Type_Fun lam) ty_root , Unlift_Type (Type_Fun lam) ty_root , Lift_Type Type_List ty_root , Unlift_Type Type_List ty_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 lam root) hs ret list_filter_from ast_f ast_l ex ast ctx k = expr_from (Proxy::Proxy root) ast_f ctx $ \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) -> expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::Type_Root_of_Expr root 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 lam (Type_Root_of_Expr root) 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)