{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-} -- | Symantic for '[]'. module Language.Symantic.Compiling.List where import Control.Monad (liftM, liftM2, liftM3) import qualified Data.Foldable as Foldable import qualified Data.Function as Fun import qualified Data.Functor as Functor import qualified Data.List as List import Data.Monoid ((<>)) import Data.Proxy import Data.String (IsString) import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Traversable as Traversable import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (filter, reverse, zipWith) import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Compiling.Bool (tyBool) import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_List' class Sym_List term where list_empty :: term [a] list_cons :: term a -> term [a] -> term [a] list :: [term a] -> term [a] filter :: term (a -> Bool) -> term [a] -> term [a] zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c] reverse :: term [a] -> term [a] default list_empty :: Trans t term => t term [a] default list_cons :: Trans t term => t term a -> t term [a] -> t term [a] default list :: Trans t term => [t term a] -> t term [a] default filter :: Trans t term => t term (a -> Bool) -> t term [a] -> t term [a] default zipWith :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c] default reverse :: Trans t term => t term [a] -> t term [a] list_empty = trans_lift list_empty list_cons = trans_map2 list_cons list l = trans_lift (list (trans_apply Functor.<$> l)) filter = trans_map2 filter zipWith = trans_map3 zipWith reverse = trans_map1 reverse type instance Sym_of_Iface (Proxy []) = Sym_List type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by [] type instance Consts_imported_by [] = [ Proxy Applicative , Proxy Eq , Proxy Foldable , Proxy Functor , Proxy Monad , Proxy Monoid , Proxy Ord , Proxy Traversable ] instance Sym_List HostI where list_empty = return [] list_cons = liftM2 (:) list = Traversable.sequence filter = liftM2 List.filter zipWith = liftM3 List.zipWith reverse = liftM List.reverse instance Sym_List TextI where list_empty = TextI $ \_p _v -> "[]" list_cons (TextI x) (TextI xs) = TextI $ \p v -> let p' = Precedence 5 in paren p p' $ x p' v <> ":" <> xs p' v list l = TextI $ \_p v -> let p' = precedence_Toplevel in "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]" filter = textI_app2 "filter" zipWith = textI_app3 "zipWith" reverse = textI_app1 "reverse" instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where list_empty = dupI0 sym_List list_empty list_cons = dupI2 sym_List list_cons list l = let (l1, l2) = Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) -> (x1:xs1, x2:xs2)) ([], []) l in list l1 `DupI` list l2 filter = dupI2 sym_List filter zipWith = dupI3 sym_List zipWith reverse = dupI1 sym_List reverse instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where const_from "[]" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS instance Show_Const cs => Show_Const (Proxy [] ': cs) where show_const ConstZ{} = "[]" show_const (ConstS c) = show_const c instance -- Proj_ConC ( Proj_Const cs [] , Proj_Consts cs (Consts_imported_by []) , Proj_Con cs ) => Proj_ConC cs (Proxy []) where proj_conC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy []) = Just $ case () of _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con _ -> Nothing proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a)) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy []) = Just $ case () of _ | Just Refl <- proj_const q (Proxy::Proxy Eq) , Just Con <- proj_con (t :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monoid) , Just Con <- proj_con (t :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Ord) , Just Con <- proj_con (t :$ a) -> Just Con _ -> Nothing proj_conC _c _q = Nothing instance -- Term_fromI ( AST ast , Lexem ast ~ LamVarName , Const_from (Lexem ast) (Consts_of_Ifaces is) , Inj_Const (Consts_of_Ifaces is) [] , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) Bool , Term_from is ast ) => Term_fromI is (Proxy []) ast where term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy [] ': rs) term_fromI ast ctx k = case ast_lexem ast of "[]" -> list_empty_from ":" -> list_cons_from "list" -> list_from "filter" -> filter_from "zipWith" -> zipWith_from "reverse" -> reverse_from _ -> Left $ Error_Term_unsupported where list_empty_from = -- [] :: [a] from_ast1 ast $ \ast_ty_a as -> either (Left . Error_Term_Typing . At (Just ast)) Fun.id $ type_from ast_ty_a $ \ty_a -> Right $ check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl -> k as (tyList :$ ty_a) $ TermLC $ Fun.const list_empty list_cons_from = -- (:) :: a -> [a] -> [a] from_ast1 ast $ \ast_a as -> term_from ast_a ctx $ \ty_a (TermLC a) -> k as (tyList :$ ty_a ~> tyList :$ ty_a) $ TermLC $ \c -> lam $ list_cons (a c) list_from = case ast_nodes ast of [] -> Left $ Error_Term_Syntax $ Error_Syntax_more_arguments_needed $ At (Just ast) 1 ast_ty_a:ast_as -> either (Left . Error_Term_Typing . At (Just ast)) Fun.id $ type_from ast_ty_a $ \ty_a -> Right $ check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl -> go ty_a [] ast_as where go :: Type (Consts_of_Ifaces is) ty_a -> [TermLC ctx ty_a is '[] is] -> [ast] -> Either (Error_Term is ast) ret go ty_a as [] = k [] (tyList :$ ty_a) $ TermLC $ \c -> list $ (\(TermLC a) -> a c) Functor.<$> List.reverse as go ty_a as (ast_x:ast_xs) = term_from ast_x ctx $ \ty_x x -> check_type (At (Just ast) ty_a) (At (Just ast_x) ty_x) $ \Refl -> go ty_a (x:as) ast_xs filter_from = -- filter :: (a -> Bool) -> [a] -> [a] from_ast1 ast $ \ast_a2Bool as -> term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) -> check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool -> check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl -> k as (tyList :$ ty_a2Bool_a ~> tyList :$ ty_a2Bool_a) $ TermLC $ \c -> lam $ filter (a2Bool c) zipWith_from = -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] from_ast1 ast $ \ast_a2b2c as -> term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) -> check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c -> check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c -> k as ( tyList :$ ty_a2b2c_a ~> tyList :$ ty_a2b2c_b2c_b ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $ \c -> lam $ lam . zipWith (a2b2c c) reverse_from = -- reverse :: [a] -> [a] from_ast1 ast $ \ast_la as -> term_from ast_la ctx $ \ty_la (TermLC la) -> check_type1 tyList ast_la ty_la $ \Refl _ty_la_a -> k as ty_la $ TermLC $ \c -> reverse (la c) -- | The '[]' 'Type' tyList :: Inj_Const cs [] => Type cs [] tyList = TyConst inj_const sym_List :: Proxy Sym_List sym_List = Proxy syList :: IsString a => [Syntax a] -> Syntax a syList = Syntax "List"