Language/Symantic/Compiling/List.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE InstanceSigs #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE OverloadedStrings #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 {-# OPTIONS_GHC -fno-warn-orphans #-}
  14 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
  15 -- | Symantic for '[]'.
  16 module Language.Symantic.Compiling.List where
  17
  18 import Control.Monad (liftM, liftM2, liftM3)
  19 import qualified Data.Foldable as Foldable
  20 import qualified Data.Function as Fun
  21 import qualified Data.Functor as Functor
  22 import qualified Data.List as List
  23 import Data.Monoid ((<>))
  24 import Data.Proxy
  25 import Data.String (IsString)
  26 import Data.Text (Text)
  27 import qualified Data.Text as Text
  28 import qualified Data.Traversable as Traversable
  29 import Data.Type.Equality ((:~:)(Refl))
  30 import Prelude hiding (filter, reverse, zipWith)
  31
  32 import Language.Symantic.Typing
  33 import Language.Symantic.Compiling.Term
  34 import Language.Symantic.Compiling.Bool (tyBool)
  35 import Language.Symantic.Interpreting
  36 import Language.Symantic.Transforming.Trans
  37
  38 -- * Class 'Sym_List'
  39 class Sym_List term where
  40         list_empty :: term [a]
  41         list_cons  :: term a -> term [a] -> term [a]
  42         list       :: [term a] -> term [a]
  43         filter     :: term (a -> Bool) -> term [a] -> term [a]
  44         zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
  45         reverse    :: term [a] -> term [a]
  46
  47         default list_empty :: Trans t term => t term [a]
  48         default list_cons  :: Trans t term => t term a -> t term [a] -> t term [a]
  49         default list       :: Trans t term => [t term a] -> t term [a]
  50         default filter     :: Trans t term => t term (a -> Bool) -> t term [a] -> t term [a]
  51         default zipWith    :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
  52         default reverse    :: Trans t term => t term [a] -> t term [a]
  53
  54         list_empty = trans_lift list_empty
  55         list_cons  = trans_map2 list_cons
  56         list l     = trans_lift (list (trans_apply Functor.<$> l))
  57         filter     = trans_map2 filter
  58         zipWith    = trans_map3 zipWith
  59         reverse    = trans_map1 reverse
  60
  61 type instance Sym_of_Iface (Proxy []) = Sym_List
  62 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
  63 type instance Consts_imported_by [] =
  64  [ Proxy Applicative
  65  , Proxy Bool
  66  , Proxy Eq
  67  , Proxy Foldable
  68  , Proxy Functor
  69  , Proxy Monad
  70  , Proxy Monoid
  71  , Proxy Ord
  72  , Proxy Traversable
  73  ]
  74
  75 instance Sym_List HostI where
  76         list_empty   = return []
  77         list_cons    = liftM2 (:)
  78         list         = Traversable.sequence
  79         filter  = liftM2 List.filter
  80         zipWith = liftM3 List.zipWith
  81         reverse = liftM  List.reverse
  82 instance Sym_List TextI where
  83         list_empty = TextI $ \_p _v -> "[]"
  84         list_cons (TextI x) (TextI xs) =
  85                 TextI $ \p v ->
  86                         let p' = Precedence 5 in
  87                         paren p p' $ x p' v <> ":" <> xs p' v
  88         list l = TextI $ \_p v ->
  89                 let p' = precedence_Toplevel in
  90                 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
  91         filter  = textI_app2 "filter"
  92         zipWith = textI_app3 "zipWith"
  93         reverse = textI_app1 "reverse"
  94 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  95         list_empty = dupI0 sym_List list_empty
  96         list_cons  = dupI2 sym_List list_cons
  97         list l =
  98                 let (l1, l2) =
  99                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
 100                                 (x1:xs1, x2:xs2)) ([], []) l in
 101                 list l1 `DupI` list l2
 102         filter  = dupI2 sym_List filter
 103         zipWith = dupI3 sym_List zipWith
 104         reverse = dupI1 sym_List reverse
 105
 106 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
 107         const_from "[]" k = k (ConstZ kind)
 108         const_from s k = const_from s $ k . ConstS
 109 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
 110         show_const ConstZ{} = "[]"
 111         show_const (ConstS c) = show_const c
 112
 113 instance -- Proj_ConC
 114  ( Proj_Const cs []
 115  , Proj_Consts cs (Consts_imported_by [])
 116  , Proj_Con cs
 117  ) => Proj_ConC cs (Proxy []) where
 118         proj_conC _ (TyConst q :$ TyConst c)
 119          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 120          , Just Refl <- proj_const c (Proxy::Proxy [])
 121          = case () of
 122                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 123                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 124                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 125                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 126                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 127                  _ -> Nothing
 128         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 129          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 130          , Just Refl <- proj_const c (Proxy::Proxy [])
 131          = case () of
 132                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 133                    , Just Con  <- proj_con (t :$ a) -> Just Con
 134                    | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
 135                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 136                    , Just Con  <- proj_con (t :$ a) -> Just Con
 137                  _ -> Nothing
 138         proj_conC _c _q = Nothing
 139 instance -- Term_fromI
 140  ( AST ast
 141  , Lexem ast ~ LamVarName
 142  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 143  , Inj_Const (Consts_of_Ifaces is) []
 144  , Inj_Const (Consts_of_Ifaces is) (->)
 145  , Inj_Const (Consts_of_Ifaces is) Bool
 146  , Term_from is ast
 147  ) => Term_fromI is (Proxy []) ast where
 148         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy [] ': rs)
 149         term_fromI ast ctx k =
 150                 case ast_lexem ast of
 151                  "[]"      -> list_empty_from
 152                  ":"       -> list_cons_from
 153                  "list"    -> list_from
 154                  "filter"  -> filter_from
 155                  "zipWith" -> zipWith_from
 156                  "reverse" -> reverse_from
 157                  _ -> Left $ Error_Term_unsupported
 158                 where
 159                 list_empty_from =
 160                  -- [] :: [a]
 161                         from_ast1 ast $ \ast_ty_a as ->
 162                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 163                         type_from ast_ty_a $ \ty_a -> Right $
 164                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 165                         k as (tyList :$ ty_a) $ TermLC $
 166                                 Fun.const list_empty
 167                 list_cons_from =
 168                  -- (:) :: a -> [a] -> [a]
 169                         from_ast1 ast $ \ast_a as ->
 170                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 171                         k as (tyList :$ ty_a ~> tyList :$ ty_a) $ TermLC $
 172                          \c -> lam $ list_cons (a c)
 173                 list_from =
 174                         case ast_nodes ast of
 175                          [] -> Left $ Error_Term_Syntax $
 176                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 177                          ast_ty_a:ast_as ->
 178                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 179                                 type_from ast_ty_a $ \ty_a -> Right $
 180                                 check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 181                                 go ty_a [] ast_as
 182                         where
 183                         go :: Type (Consts_of_Ifaces is) ty_a
 184                            -> [TermLC ctx ty_a is '[] is]
 185                            -> [ast]
 186                            -> Either (Error_Term is ast) ret
 187                         go ty_a as [] =
 188                                 k [] (tyList :$ ty_a) $ TermLC $
 189                                  \c -> list $ (\(TermLC a) -> a c)
 190                                          Functor.<$> List.reverse as
 191                         go ty_a as (ast_x:ast_xs) =
 192                                 term_from ast_x ctx $ \ty_x x ->
 193                                 check_type (At (Just ast) ty_a) (At (Just ast_x) ty_x) $ \Refl ->
 194                                 go ty_a (x:as) ast_xs
 195                 filter_from =
 196                  -- filter :: (a -> Bool) -> [a] -> [a]
 197                         from_ast1 ast $ \ast_a2Bool as ->
 198                         term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
 199                         check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
 200                         check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
 201                         k as (tyList :$ ty_a2Bool_a ~> tyList :$ ty_a2Bool_a) $ TermLC $
 202                          \c -> lam $ filter (a2Bool c)
 203                 zipWith_from =
 204                  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 205                         from_ast1 ast $ \ast_a2b2c as ->
 206                         term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 207                         check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 208                         check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 209                         k as ( tyList :$ ty_a2b2c_a
 210                          ~> tyList :$ ty_a2b2c_b2c_b
 211                          ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
 212                          \c -> lam $ lam . zipWith (a2b2c c)
 213                 reverse_from =
 214                  -- reverse :: [a] -> [a]
 215                         from_ast1 ast $ \ast_la as ->
 216                         term_from ast_la ctx $ \ty_la (TermLC la) ->
 217                         check_type1 tyList ast_la ty_la $ \Refl _ty_la_a ->
 218                         k as ty_la $ TermLC $
 219                          \c -> reverse (la c)
 220
 221 -- | The '[]' 'Type'
 222 tyList :: Inj_Const cs [] => Type cs []
 223 tyList = TyConst inj_const
 224
 225 sym_List :: Proxy Sym_List
 226 sym_List = Proxy
 227
 228 syList :: IsString a => [Syntax a] -> Syntax a
 229 syList = Syntax "List"