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=7 #-}
  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 Eq
  66  , Proxy Foldable
  67  , Proxy Functor
  68  , Proxy Monad
  69  , Proxy Monoid
  70  , Proxy Ord
  71  , Proxy Traversable
  72  ]
  73
  74 instance Sym_List HostI where
  75         list_empty   = return []
  76         list_cons    = liftM2 (:)
  77         list         = Traversable.sequence
  78         filter  = liftM2 List.filter
  79         zipWith = liftM3 List.zipWith
  80         reverse = liftM  List.reverse
  81 instance Sym_List TextI where
  82         list_empty = TextI $ \_p _v -> "[]"
  83         list_cons (TextI x) (TextI xs) =
  84                 TextI $ \p v ->
  85                         let p' = Precedence 5 in
  86                         paren p p' $ x p' v <> ":" <> xs p' v
  87         list l = TextI $ \_p v ->
  88                 let p' = precedence_Toplevel in
  89                 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
  90         filter  = textI_app2 "filter"
  91         zipWith = textI_app3 "zipWith"
  92         reverse = textI_app1 "reverse"
  93 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  94         list_empty = dupI0 sym_List list_empty
  95         list_cons  = dupI2 sym_List list_cons
  96         list l =
  97                 let (l1, l2) =
  98                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  99                                 (x1:xs1, x2:xs2)) ([], []) l in
 100                 list l1 `DupI` list l2
 101         filter  = dupI2 sym_List filter
 102         zipWith = dupI3 sym_List zipWith
 103         reverse = dupI1 sym_List reverse
 104
 105 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
 106         const_from "[]" k = k (ConstZ kind)
 107         const_from s k = const_from s $ k . ConstS
 108 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
 109         show_const ConstZ{} = "[]"
 110         show_const (ConstS c) = show_const c
 111
 112 instance -- Proj_ConC
 113  ( Proj_Const cs []
 114  , Proj_Consts cs (Consts_imported_by [])
 115  , Proj_Con cs
 116  ) => Proj_ConC cs (Proxy []) where
 117         proj_conC _ (TyConst q :$ TyConst c)
 118          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 119          , Just Refl <- proj_const c (Proxy::Proxy [])
 120          = Just $ case () of
 121                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 122                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 123                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 124                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 125                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 126                  _ -> Nothing
 127         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 128          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 129          , Just Refl <- proj_const c (Proxy::Proxy [])
 130          = Just $ case () of
 131                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 132                    , Just Con  <- proj_con (t :$ a) -> Just Con
 133                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 134                    , Just Con  <- proj_con (t :$ a) -> 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_fromT 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 ->
 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 (tyList :$ ty_a) $ TermLC $
 166                                 Fun.const list_empty
 167                 list_cons_from =
 168                  -- (:) :: a -> [a] -> [a]
 169                         case ast_nodes ast of
 170                          [] -> Left $ Error_Term_Syntax $
 171                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 172                          [ast_a] ->
 173                                 term_from ast_a ctx $ \ty_a (TermLC a) ->
 174                                 k (tyList :$ ty_a ~> tyList :$ ty_a) $ TermLC $
 175                                  \c -> lam $ list_cons (a c)
 176                          [ast_a, ast_la] ->
 177                                 term_from ast_a  ctx $ \ty_a  (TermLC a) ->
 178                                 term_from ast_la ctx $ \ty_la (TermLC la) ->
 179                                 check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
 180                                 check_type (At (Just ast_a) ty_a) (At (Just ast_la) ty_la_a) $ \Refl ->
 181                                 k ty_la $ TermLC $
 182                                  \c -> list_cons (a c) (la c)
 183                          _ -> Left $ Error_Term_Syntax $
 184                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 185                 list_from =
 186                         case ast_nodes ast of
 187                          [] -> Left $ Error_Term_Syntax $
 188                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 189                          ast_ty_a:ast_as ->
 190                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 191                                 type_from ast_ty_a $ \ty_a -> Right $
 192                                 check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 193                                 go ty_a [] ast_as
 194                         where
 195                         go :: Type (Consts_of_Ifaces is) ty_a
 196                            -> [TermLC ctx ty_a is '[] is]
 197                            -> [ast]
 198                            -> Either (Error_Term is ast) ret
 199                         go ty_a as [] =
 200                                 k (tyList :$ ty_a) $ TermLC $
 201                                  \c -> list $ (\(TermLC a) -> a c)
 202                                          Functor.<$> List.reverse as
 203                         go ty_a as (ast_x:ast_xs) =
 204                                 term_from ast_x ctx $ \ty_x x ->
 205                                 check_type (At (Just ast) ty_a) (At (Just ast_x) ty_x) $ \Refl ->
 206                                 go ty_a (x:as) ast_xs
 207                 filter_from =
 208                  -- filter :: (a -> Bool) -> [a] -> [a]
 209                         case ast_nodes ast of
 210                          [] -> Left $ Error_Term_Syntax $
 211                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 212                          [ast_a2Bool] ->
 213                                 term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
 214                                 check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
 215                                 check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
 216                                 k (tyList :$ ty_a2Bool_a ~> tyList :$ ty_a2Bool_a) $ TermLC $
 217                                  \c -> lam $ filter (a2Bool c)
 218                          [ast_a2Bool, ast_la] ->
 219                                 term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
 220                                 term_from ast_la     ctx $ \ty_la     (TermLC la) ->
 221                                 check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
 222                                 check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
 223                                 check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
 224                                 check_type (At (Just ast_a2Bool) ty_a2Bool_a) (At (Just ast_la) ty_la_a) $ \Refl ->
 225                                 k (tyList :$ ty_a2Bool_a) $ TermLC $
 226                                  \c -> filter (a2Bool c) (la c)
 227                          _ -> Left $ Error_Term_Syntax $
 228                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 229                 zipWith_from =
 230                  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 231                         case ast_nodes ast of
 232                          [] -> Left $ Error_Term_Syntax $
 233                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 234                          [ast_a2b2c] ->
 235                                 term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 236                                 check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 237                                 check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 238                                 k ( tyList :$ ty_a2b2c_a
 239                                  ~> tyList :$ ty_a2b2c_b2c_b
 240                                  ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
 241                                  \c -> lam $ lam . zipWith (a2b2c c)
 242                          [ast_a2b2c, ast_la] ->
 243                                 term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 244                                 term_from ast_la    ctx $ \ty_la    (TermLC la) ->
 245                                 check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 246                                 check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 247                                 check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
 248                                 check_type (At (Just ast_a2b2c) ty_a2b2c_a) (At (Just ast_la) ty_la_a) $ \Refl ->
 249                                 k ( tyList :$ ty_a2b2c_b2c_b
 250                                  ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
 251                                  \c -> lam $ zipWith (a2b2c c) (la c)
 252                          [ast_a2b2c, ast_la, ast_lb] ->
 253                                 term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 254                                 term_from ast_la    ctx $ \ty_la    (TermLC la) ->
 255                                 term_from ast_lb    ctx $ \ty_lb    (TermLC lb) ->
 256                                 check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 257                                 check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 258                                 check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
 259                                 check_type (At (Just ast_a2b2c) ty_a2b2c_a) (At (Just ast_la) ty_la_a) $ \Refl ->
 260                                 check_type1 tyList ast_lb ty_lb $ \Refl ty_lb_b ->
 261                                 check_type (At (Just ast_a2b2c) ty_a2b2c_b2c_b) (At (Just ast_lb) ty_lb_b) $ \Refl ->
 262                                 k (tyList :$ ty_a2b2c_b2c_c) $ TermLC $
 263                                  \c -> zipWith (a2b2c c) (la c) (lb c)
 264                          _ -> Left $ Error_Term_Syntax $
 265                                 Error_Syntax_too_many_arguments $ At (Just ast) 3
 266                 reverse_from =
 267                  -- reverse :: [a] -> [a]
 268                         from_ast1 ast $ \ast_la ->
 269                         term_from ast_la ctx $ \ty_la (TermLC la) ->
 270                         check_type1 tyList ast_la ty_la $ \Refl _ty_la_a ->
 271                         k ty_la $ TermLC $
 272                          \c -> reverse (la c)
 273
 274 -- | The '[]' 'Type'
 275 tyList :: Inj_Const cs [] => Type cs []
 276 tyList = TyConst inj_const
 277
 278 sym_List :: Proxy Sym_List
 279 sym_List = Proxy
 280
 281 syList :: IsString a => [Syntax a] -> Syntax a
 282 syList = Syntax "List"