{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
-- | Symantic for '[]'.
module Language.Symantic.Lib.List where
-import Control.Monad (liftM, liftM2, liftM3)
-import Data.Monoid ((<>))
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
+import Data.Semigroup ((<>))
import Prelude hiding (zipWith)
-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 qualified Data.MonoTraversable as MT
import qualified Data.Text as Text
import qualified Data.Traversable as Traversable
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
+import Language.Symantic
+import Language.Symantic.Grammar as G
+import Language.Symantic.Lib.Function (a0, b1, c2)
+import Language.Symantic.Lib.MonoFunctor (Element)
-- * Class 'Sym_List'
+type instance Sym [] = Sym_List
class Sym_List term where
- list_empty :: term [a]
- list_singleton :: term a -> term [a]
- (.:) :: term a -> term [a] -> term [a]; infixr 5 .:
- list :: [term a] -> term [a]
- zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
+ list_empty :: term [a]
+ list_cons :: term a -> term [a] -> term [a]; infixr 5 `list_cons`
+ list :: [term a] -> term [a]
+ zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
- default list_empty :: Trans t term => t term [a]
- default list_singleton :: Trans t term => t term a -> t term [a]
- default (.:) :: Trans t term => t term a -> t term [a] -> t term [a]
- default list :: Trans t term => [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 list_empty :: Sym_List (UnT term) => Trans term => term [a]
+ default list_cons :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a]
+ default list :: Sym_List (UnT term) => Trans term => [term a] -> term [a]
+ default zipWith :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c]
- list_empty = trans_lift list_empty
- list_singleton = trans_map1 list_singleton
- (.:) = trans_map2 (.:)
- list l = trans_lift (list (trans_apply Functor.<$> l))
- zipWith = trans_map3 zipWith
+ list_empty = trans list_empty
+ list_cons = trans2 list_cons
+ list l = trans (list (unTrans Functor.<$> l))
+ zipWith = trans3 zipWith
-type instance Sym_of_Iface (Proxy []) = Sym_List
-type instance TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by (Proxy [])
-type instance TyConsts_imported_by (Proxy []) =
- [ Proxy Applicative
- , Proxy Bool
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Monad
- , Proxy MT.MonoFoldable
- , Proxy MT.MonoFunctor
- , Proxy Monoid
- , Proxy Ord
- , Proxy Seqs.IsSequence
- , Proxy Seqs.SemiSequence
- , Proxy Show
- , Proxy Traversable
- ]
-
-instance Sym_List HostI where
- list_empty = return []
- list_singleton = liftM return
- (.:) = liftM2 (:)
- list = Traversable.sequence
- zipWith = liftM3 List.zipWith
-instance Sym_List TextI where
- list_empty = TextI $ \_p _v -> "[]"
- list_singleton a = textI_infix ":" op a list_empty
- where op = infixR 5
- (.:) = textI_infix ":" (infixR 5)
- list l = TextI $ \_po v ->
- "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
- where op = (infixN0, L)
- zipWith = textI3 "zipWith"
-instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
- list_empty = dupI0 @Sym_List list_empty
- list_singleton = dupI1 @Sym_List list_singleton
- (.:) = dupI2 @Sym_List (.:)
+-- Interpreting
+instance Sym_List Eval where
+ list_empty = return []
+ list_cons = eval2 (:)
+ list = Traversable.sequence
+ zipWith = eval3 List.zipWith
+instance Sym_List View where
+ list_empty = View $ \_p _v -> "[]"
+ list_cons = viewInfix ":" (infixR 5)
+ list l = View $ \_po v ->
+ "[" <> Text.intercalate ", " ((\(View a) -> a op v) Functor.<$> l) <> "]"
+ where op = (infixN0, SideL)
+ zipWith = view3 "zipWith"
+instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where
+ list_empty = dup0 @Sym_List list_empty
+ list_cons = dup2 @Sym_List list_cons
list l =
let (l1, l2) =
- Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
+ foldr (\(x1 `Dup` x2) (xs1, xs2) ->
(x1:xs1, x2:xs2)) ([], []) l in
- list l1 `DupI` list l2
- zipWith = dupI3 @Sym_List zipWith
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs []
- ) => Read_TyNameR TyName cs (Proxy [] ': rs) where
- read_TyNameR _cs (TyName "[]") k = k (ty @[])
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy [] ': cs) where
- show_TyConst TyConstZ{} = "[]"
- show_TyConst (TyConstS c) = show_TyConst c
-instance Show_TyConst cs => Show_TyConst (Proxy String ': cs) where
- show_TyConst TyConstZ{} = "String"
- show_TyConst (TyConstS c) = show_TyConst c
+ list l1 `Dup` list l2
+ zipWith = dup3 @Sym_List zipWith
-instance -- Proj_TyFamC TyFam_MonoElement
- ( Proj_TyConst cs []
- ) => Proj_TyFamC cs TyFam_MonoElement [] where
- proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @[])
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
+-- Transforming
+instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)
-instance -- Proj_TyConC
- ( Proj_TyConst cs []
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy []))
- , Proj_TyCon cs
- ) => Proj_TyConC cs (Proxy []) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @[])
+-- Typing
+instance NameTyOf [] where
+ nameTyOf _c = [] `Mod` "[]"
+instance FixityOf []
+instance ClassInstancesFor [] where
+ proveConstraintFor _ (TyConst _ _ q :$ z)
+ | Just HRefl <- proj_ConstKiTy @_ @[] z
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
+ _ | Just Refl <- proj_Const @Applicative q -> Just Dict
+ | Just Refl <- proj_Const @Foldable q -> Just Dict
+ | Just Refl <- proj_Const @Functor q -> Just Dict
+ | Just Refl <- proj_Const @Monad q -> Just Dict
+ | Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @[])
+ proveConstraintFor _ (tq@(TyConst _ _ q) :$ z:@a)
+ | Just HRefl <- proj_ConstKiTy @_ @[] z
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Seqs.IsSequence) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Seqs.SemiSequence) -> Just TyCon
+ _ | Just Refl <- proj_Const @Eq q
+ , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
+ | Just Refl <- proj_Const @Monoid q -> Just Dict
+ | Just Refl <- proj_Const @Show q
+ , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
+ | Just Refl <- proj_Const @Ord q
+ , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
+ | Just Refl <- proj_Const @Seqs.IsSequence q -> Just Dict
+ | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy [])
- = Token_Term_List_empty (EToken meta '[Proxy Token_Type])
- | Token_Term_List_cons (EToken meta ts) (EToken meta ts)
- | Token_Term_List_singleton (EToken meta ts)
- | Token_Term_List_list (EToken meta '[Proxy Token_Type]) [EToken meta ts]
- | Token_Term_List_zipWith (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor [] where
+ expandFamFor _c _len f (z:@a `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @[] z
+ = Just a
+ expandFamFor _c _len _fam _as = Nothing
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs []
- , Inj_TyConst cs (->)
- , Compile cs is
- ) => CompileI cs is (Proxy []) where
- compileI
- :: forall meta ctx ret ls rs.
- TokenT meta is (Proxy [])
- -> CompileT meta ctx ret cs is ls (Proxy [] ': rs)
- compileI tok ctx k =
- case tok of
- Token_Term_List_empty tok_ty_a ->
- -- [] :: [a]
- compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- k (ty @[] :$ ty_a) $ TermO $
- Fun.const list_empty
- Token_Term_List_singleton tok_a ->
- -- [a] :: [a]
- compileO tok_a ctx $ \ty_a (TermO a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
- k (ty @[] :$ ty_a) $ TermO $
- \c -> list_singleton (a c)
- Token_Term_List_cons tok_a tok_as ->
- compileO tok_a ctx $ \ty_a (TermO a) ->
- compileO tok_as ctx $ \ty_as (TermO as) ->
- check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
- check_TyEq (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
- k ty_as $ TermO $
- \c -> a c .: as c
- Token_Term_List_list tok_ty_a tok_as ->
- compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- go (At (Just tok_ty_a) ty_a) [] tok_as
- where
- go :: At meta '[Proxy Token_Type] (Type cs ty_a)
- -> [TermO ctx ty_a is '[] is]
- -> [EToken meta is]
- -> Either (Error_Term meta cs is) ret
- go ty_a as [] =
- k (ty @[] :$ unAt ty_a) $ TermO $
- \c -> list $ (\(TermO a) -> a c)
- Functor.<$> List.reverse as
- go ty_a as (tok_x:tok_xs) =
- compileO tok_x ctx $ \ty_x x ->
- check_Type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
- go ty_a (x:as) tok_xs
- Token_Term_List_zipWith tok_a2b2c ->
- -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
- compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
- k ( ty @[] :$ ty_a2b2c_a
- ~> ty @[] :$ ty_a2b2c_b2c_b
- ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $
- \c -> lam $ lam . zipWith (a2b2c c)
-instance -- TokenizeT
- Inj_Token meta ts [] =>
- TokenizeT meta ts (Proxy []) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ (TeName "[]",) $ ProTok_Term
- { protok_term = \meta -> ProTokPi $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_List_empty a
- , protok_fixity = infixN5
- }
- , tokenize2 ":" (infixR 5) Token_Term_List_cons
- , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
- ]
- }
+-- Compiling
instance
- ( App g
+ ( Gram_App g
, Gram_Rule g
- , Gram_Lexer g
- , Gram_Term ts meta g
- , Inj_Token meta ts (->)
- , Inj_Token meta ts []
- ) => Gram_Term_AtomsT meta ts (Proxy []) g where
- gs_term_atomsT _t =
- [ rule "term_list" $
- ProTok <$> between (symbol "[") (symbol "]") listG
- , rule "term_list_empty" $
- metaG $
- (\meta -> ProTokPi $ \a -> ProTok $ inj_EToken meta $ Token_Term_List_empty a)
+ , Gram_Comment g
+ , Gram_Term src ss g
+ , SymInj ss []
+ ) => Gram_Term_AtomsFor src ss g [] where
+ g_term_atomsFor =
+ [ rule "teList_list" $
+ between (symbol "[") (symbol "]") listG
+ , rule "teList_empty" $
+ G.source $
+ (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
<$ symbol "["
<* symbol "]"
]
where
- listG :: CF g (EToken meta ts)
+ listG :: CF g (AST_Term src ss)
listG = rule "list" $
- metaG $
- (\a mb meta -> inj_EToken meta $ case mb of
- Just b -> Token_Term_List_cons a b
- Nothing -> Token_Term_List_singleton a)
+ G.source $
+ (\a mb src ->
+ case mb of
+ Just b -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
+ Nothing ->
+ BinTree2
+ (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)
+ (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
<$> g_term
<*> option Nothing (Just <$ symbol "," <*> listG)
+instance (Source src, SymInj ss []) => ModuleFor src ss [] where
+ moduleFor = ["List"] `moduleWhere`
+ [ "[]" := teList_empty
+ , "zipWith" := teList_zipWith
+ , ":" `withInfixR` 5 := teList_cons
+ ]
+
+-- ** 'Type's
+tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]
+tyList = (tyConst @(K []) @[] `tyApp`)
+
+-- ** 'Term's
+teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])
+teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
+
+teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
+teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons
+
+teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
+teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith
sourcephile / git / haskell / symantic.git / blobdiff