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 (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 (zipWith)
  31
  32 import Language.Symantic.Typing
  33 import Language.Symantic.Compiling.Term
  34 import Language.Symantic.Interpreting
  35 import Language.Symantic.Transforming.Trans
  36
  37 -- * Class 'Sym_List'
  38 class Sym_List term where
  39         list_empty :: term [a]
  40         zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
  41
  42         default list_empty :: Trans t term => t term [a]
  43         default zipWith    :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
  44
  45         list_empty = trans_lift list_empty
  46         zipWith    = trans_map3 zipWith
  47
  48         list       :: [term a] -> term [a]
  49
  50         default list       :: Trans t term => [t term a] -> t term [a]
  51
  52         list l     = trans_lift (list (trans_apply Functor.<$> l))
  53
  54 type instance Sym_of_Iface (Proxy []) = Sym_List
  55 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
  56 type instance Consts_imported_by [] =
  57  [ Proxy Applicative
  58  , Proxy Bool
  59  , Proxy Eq
  60  , Proxy Foldable
  61  , Proxy Functor
  62  , Proxy Monad
  63  , Proxy Monoid
  64  , Proxy Ord
  65  , Proxy Traversable
  66  ]
  67
  68 instance Sym_List HostI where
  69         list_empty = return []
  70         list       = Traversable.sequence
  71         zipWith    = liftM3 List.zipWith
  72 instance Sym_List TextI where
  73         list_empty = TextI $ \_p _v -> "[]"
  74         list l = TextI $ \_p v ->
  75                 let p' = precedence_Toplevel in
  76                 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
  77         zipWith = textI_app3 "zipWith"
  78 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  79         list_empty = dupI0 sym_List list_empty
  80         list l =
  81                 let (l1, l2) =
  82                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  83                                 (x1:xs1, x2:xs2)) ([], []) l in
  84                 list l1 `DupI` list l2
  85         zipWith = dupI3 sym_List zipWith
  86
  87 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
  88         const_from "[]" k = k (ConstZ kind)
  89         const_from s k = const_from s $ k . ConstS
  90 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
  91         show_const ConstZ{} = "[]"
  92         show_const (ConstS c) = show_const c
  93
  94 instance -- Proj_ConC
  95  ( Proj_Const cs []
  96  , Proj_Consts cs (Consts_imported_by [])
  97  , Proj_Con cs
  98  ) => Proj_ConC cs (Proxy []) where
  99         proj_conC _ (TyConst q :$ TyConst c)
 100          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 101          , Just Refl <- proj_const c (Proxy::Proxy [])
 102          = case () of
 103                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 104                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 105                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 106                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 107                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 108                  _ -> Nothing
 109         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 110          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 111          , Just Refl <- proj_const c (Proxy::Proxy [])
 112          = case () of
 113                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 114                    , Just Con  <- proj_con (t :$ a) -> Just Con
 115                    | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
 116                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 117                    , Just Con  <- proj_con (t :$ a) -> Just Con
 118                  _ -> Nothing
 119         proj_conC _c _q = Nothing
 120 instance -- Term_fromI
 121  ( AST ast
 122  , Lexem ast ~ LamVarName
 123  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 124  , Inj_Const (Consts_of_Ifaces is) []
 125  , Inj_Const (Consts_of_Ifaces is) (->)
 126  , Term_from is ast
 127  ) => Term_fromI is (Proxy []) ast where
 128         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy [] ': rs)
 129         term_fromI ast ctx k =
 130                 case ast_lexem ast of
 131                  "[]"      -> list_empty_from
 132                  "list"    -> list_from
 133                  "zipWith" -> zipWith_from
 134                  _ -> Left $ Error_Term_unsupported
 135                 where
 136                 list_empty_from =
 137                  -- [] :: [a]
 138                         from_ast1 ast $ \ast_ty_a as ->
 139                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 140                         type_from ast_ty_a $ \ty_a -> Right $
 141                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 142                         k as (tyList :$ ty_a) $ TermLC $
 143                                 Fun.const list_empty
 144                 list_from =
 145                         case ast_nodes ast of
 146                          [] -> Left $ Error_Term_Syntax $
 147                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 148                          ast_ty_a:ast_as ->
 149                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 150                                 type_from ast_ty_a $ \ty_a -> Right $
 151                                 check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 152                                 go ty_a [] ast_as
 153                         where
 154                         go :: Type (Consts_of_Ifaces is) ty_a
 155                            -> [TermLC ctx ty_a is '[] is]
 156                            -> [ast]
 157                            -> Either (Error_Term is ast) ret
 158                         go ty_a as [] =
 159                                 k [] (tyList :$ ty_a) $ TermLC $
 160                                  \c -> list $ (\(TermLC a) -> a c)
 161                                          Functor.<$> List.reverse as
 162                         go ty_a as (ast_x:ast_xs) =
 163                                 term_from ast_x ctx $ \ty_x x ->
 164                                 check_type (At (Just ast) ty_a) (At (Just ast_x) ty_x) $ \Refl ->
 165                                 go ty_a (x:as) ast_xs
 166                 zipWith_from =
 167                  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 168                         from_ast1 ast $ \ast_a2b2c as ->
 169                         term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 170                         check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 171                         check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 172                         k as ( tyList :$ ty_a2b2c_a
 173                          ~> tyList :$ ty_a2b2c_b2c_b
 174                          ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
 175                          \c -> lam $ lam . zipWith (a2b2c c)
 176
 177 -- | The '[]' 'Type'
 178 tyList :: Inj_Const cs [] => Type cs []
 179 tyList = TyConst inj_const
 180
 181 sym_List :: Proxy Sym_List
 182 sym_List = Proxy
 183
 184 syList :: IsString a => [Syntax a] -> Syntax a
 185 syList = Syntax "List"