{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ViewPatterns #-}
module Language.Symantic.Document.Sym where
import Data.Char (Char)
-import Data.Eq (Eq(..))
import Data.Foldable (Foldable(..))
import Data.Function ((.))
import Data.Functor (Functor(..))
import Data.Int (Int, Int64)
-import Data.Maybe (Maybe(..))
import Data.Semigroup (Semigroup(..))
import Data.String (String, IsString)
import Data.Text (Text)
spaces i = replicate i space
int = integer . toInteger
char = \case '\n' -> eol; c -> charH c
- string = catV . fmap stringH . lines
- text = catV . fmap textH . lines
- ltext = catV . fmap ltextH . lines
+ string = catV . fmap stringH . L.lines
+ text = catV . fmap textH . T.lines
+ ltext = catV . fmap ltextH . TL.lines
catH = foldr (<>) empty
catV l = if null l then empty else foldr1 (\a acc -> a <> eol <> acc) l
paren d = charH '(' <> d <> charH ')'
-> (tr -> tr -> tr -> tr)
trans3 f t1 t2 t3 = trans (f (unTrans t1) (unTrans t2) (unTrans t3))
-
--- * Class 'SplitOnCharWithEmpty'
-class SplitOnCharWithEmpty t where
- splitOnCharWithEmpty :: Char -> t -> [t]
-instance SplitOnCharWithEmpty Text where
- splitOnCharWithEmpty sep t =
- case T.break (== sep) t of
- (chunk, T.uncons -> Just (_, rest)) -> chunk : splitOnCharWithEmpty sep rest
- (chunk, _) -> [chunk]
-instance SplitOnCharWithEmpty TL.Text where
- splitOnCharWithEmpty sep t =
- case TL.break (== sep) t of
- (chunk, TL.uncons -> Just (_, rest)) -> chunk : splitOnCharWithEmpty sep rest
- (chunk, _) -> [chunk]
-instance SplitOnCharWithEmpty String where
- splitOnCharWithEmpty sep t =
- case L.break (== sep) t of
- (chunk, _:rest) -> chunk : splitOnCharWithEmpty sep rest
- (chunk, []) -> [chunk]
-
-lines :: SplitOnCharWithEmpty t => t -> [t]
-lines = splitOnCharWithEmpty '\n'
-
int64OfInt :: Int -> Int64
int64OfInt = fromInteger . toInteger
-
-
-{-
--- * Class 'SplitOnChar'
-
-class SplitOnChar t where
- splitOnChar :: Char -> t -> [t]
-instance SplitOnChar Text where
- splitOnChar sep t =
- case Text.uncons t of
- Nothing -> []
- Just (x, xs) ->
- if x == sep
- then splitOnChar sep xs
- else
- let (chunk, rest) = Text.break (== sep) t in
- chunk:splitOnChar sep rest
-instance SplitOnChar String where
- splitOnChar sep t =
- case t of
- [] -> []
- x:xs ->
- if x == sep
- then splitOnChar sep xs
- else
- let (chunk, rest) = List.break (== sep) t in
- chunk:splitOnChar sep rest
--}
, module Language.Symantic.Grammar.ContextFree
, module Language.Symantic.Grammar.Operators
, module Language.Symantic.Grammar.Meta
+ , module Language.Symantic.Grammar.Error
+ , module Language.Symantic.Grammar.Source
, module Language.Symantic.Grammar.BinTree
) where
import Language.Symantic.Grammar.ContextFree
import Language.Symantic.Grammar.Operators
import Language.Symantic.Grammar.Meta
+import Language.Symantic.Grammar.Error
+import Language.Symantic.Grammar.Source
import Language.Symantic.Grammar.BinTree
f bo (op, SideL) <> " - " <> g bo (op, SideR)
where op = infixL 6
-cf_of_Terminal :: Terminal g a -> CF g a
-cf_of_Terminal (Terminal g) = CF g
-
-cf_of_Reg :: Reg lr g a -> CF g a
-cf_of_Reg (Reg g) = CF g
+class ContextFreeOf gram where
+ cfOf :: gram g a -> CF g a
+instance ContextFreeOf Terminal where
+ cfOf (Terminal g) = CF g
+instance ContextFreeOf (Reg lr) where
+ cfOf (Reg g) = CF g
-- ** Class 'Gram_CF'
-- | Symantics for context-free grammars.
prefix *> many (any `minus` (void (char '\n') <+> eoi))
comment_block :: CF g String -> Reg lr g String -> CF g String
comment_block begin end = rule "comment_block" $
- begin *> many (any `minus` end) <* cf_of_Reg end
+ begin *> many (any `minus` end) <* cfOf end
lexeme :: CF g a -> CF g a
lexeme = rule1 "lexeme" $ \g ->
g <* commentable
-- * 'Text' of the 'EBNF' rendition.
newtype EBNF a = EBNF { unEBNF :: RuleMode -> (Infix, Side) -> Text }
instance Gram_Reader st EBNF where
- g_ask_before (EBNF e) = EBNF e
- g_ask_after (EBNF e) = EBNF e
+ askBefore (EBNF e) = EBNF e
+ askAfter (EBNF e) = EBNF e
instance Gram_State st EBNF where
- g_state_before (EBNF e) = EBNF e
- g_state_after (EBNF e) = EBNF e
+ stateBefore (EBNF e) = EBNF e
+ stateAfter (EBNF e) = EBNF e
instance Gram_Error err EBNF where
- g_catch (EBNF e) = EBNF e
+ catch (EBNF e) = EBNF e
-- | Get textual rendition of given 'EBNF'.
runEBNF :: EBNF a -> Text
--- /dev/null
+{-# LANGUAGE TypeApplications #-}
+module Language.Symantic.Grammar.Error where
+
+import Data.Proxy (Proxy)
+
+-- * Class 'Inj_Error'
+class Inj_Error a b where
+ inj_Error :: a -> b
+instance Inj_Error err e => Inj_Error err (Either e a) where
+ inj_Error = Left . inj_Error
+
+liftError ::
+ forall e0 err e1 a.
+ Inj_Error e0 e1 =>
+ Inj_Error e1 err =>
+ Proxy e1 -> Either e0 a -> Either err a
+liftError _e1 (Right a) = Right a
+liftError _e1 (Left e) = Left $ inj_Error @e1 @err $ inj_Error @e0 @e1 e
{-# LANGUAGE DefaultSignatures #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Grammar.Meta where
-import Data.Function (const)
-import Data.Proxy (Proxy(..))
-import Data.Typeable (Typeable)
+import Language.Symantic.Grammar.Source
-- * Type 'Gram_Reader'
class Gram_Reader st g where
- g_ask_before :: g (st -> a) -> g a
- g_ask_after :: g (st -> a) -> g a
+ askBefore :: g (st -> a) -> g a
+ askAfter :: g (st -> a) -> g a
-- * Type 'Gram_State'
class Gram_State st g where
- g_state_before :: g (st -> (st, a)) -> g a
- g_state_after :: g (st -> (st, a)) -> g a
- g_get_before :: g (st -> a) -> g a
- g_get_after :: g (st -> a) -> g a
- g_put :: g (st, a) -> g a
- default g_get_before :: Functor g => g (st -> a) -> g a
- default g_get_after :: Functor g => g (st -> a) -> g a
- default g_put :: Functor g => g (st, a) -> g a
- g_get_before g = g_state_before ((\f st -> (st, f st)) <$> g)
- g_get_after g = g_state_after ((\f st -> (st, f st)) <$> g)
- g_put g = g_state_after ((\(st, a) -> const (st, a)) <$> g)
+ stateBefore :: g (st -> (st, a)) -> g a
+ stateAfter :: g (st -> (st, a)) -> g a
+ getBefore :: g (st -> a) -> g a
+ getAfter :: g (st -> a) -> g a
+ put :: g (st, a) -> g a
+ default getBefore :: Functor g => g (st -> a) -> g a
+ default getAfter :: Functor g => g (st -> a) -> g a
+ default put :: Functor g => g (st, a) -> g a
+ getBefore g = stateBefore ((\f st -> (st, f st)) <$> g)
+ getAfter g = stateAfter ((\f st -> (st, f st)) <$> g)
+ put g = stateAfter ((\(st, a) -> const (st, a)) <$> g)
-- * Class 'Gram_Error'
-- | Symantics for handling errors at the semantic level (not the syntaxic one).
class Gram_Error err g where
- g_catch :: g (Either err a) -> g a
+ catch :: g (Either err a) -> g a
--- * Class 'Inj_Error'
-class Inj_Error a b where
- inj_Error :: a -> b
-instance Inj_Error err e => Inj_Error err (Either e a) where
- inj_Error = Left . inj_Error
-
-lift_Error ::
- forall e0 err e1 a.
- Inj_Error e0 e1 =>
- Inj_Error e1 err =>
- Proxy e1 -> Either e0 a -> Either err a
-lift_Error _e1 (Right a) = Right a
-lift_Error _e1 (Left e) = Left $ inj_Error @e1 @err $ inj_Error @e0 @e1 e
-
--- * Class 'Source'
-class Source src where
- noSource :: src
-instance Source () where
- noSource = ()
-
--- ** Class 'Inj_Source'
-class Source src => Inj_Source a src where
- inj_Source :: a -> src
-instance Inj_Source a () where
- inj_Source _ = ()
-
--- ** Type family 'SourceOf'
-type family SourceOf a
-
--- ** Type 'Sourced'
-class Source (SourceOf a) => Sourced a where
- sourceOf :: a -> SourceOf a
- setSource :: a -> SourceOf a -> a
-infixl 5 `setSource`
-
-source :: Inj_Source src (SourceOf a) => Sourced a => a -> src -> a
-source a src = a `setSource` inj_Source src
-
--- ** Type 'Source_Input'
-type family Source_Input (src :: *) :: *
-type instance Source_Input () = ()
-
--- ** Type 'Span'
-data Span src
- = Span
- { spanBegin :: !src
- , spanEnd :: !src
- } deriving (Eq, Ord, Show, Typeable)
-
--- ** Class 'Gram_Source'
+-- * Class 'Gram_Source'
class
( Gram_Reader (Source_Input src) g
, Inj_Source (Span (Source_Input src)) src
) => Gram_Source src g where
- g_source :: Functor g => g (src -> a) -> g a
- g_source g =
- g_ask_after $ g_ask_before $
+ source :: Functor g => g (src -> a) -> g a
+ source g =
+ askAfter $ askBefore $
(\f (beg::Source_Input src) (end::Source_Input src) ->
f (inj_Source $ Span beg end::src))
<$> g
( Gram_Reader (Source_Input src) g
, Inj_Source (Span (Source_Input src)) src
) => Gram_Source src g
-
--- ** Type 'At'
--- | Attach a 'Source' to something.
-data At src a
- = At
- { at :: !src
- , unAt :: !a
- } deriving (Eq, Functor, Ord, Show, Typeable)
--- /dev/null
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE TypeFamilies #-}
+module Language.Symantic.Grammar.Source where
+
+import Data.Functor (Functor)
+import Data.Typeable (Typeable)
+
+-- * Class 'Source'
+class Source src where
+ noSource :: src
+instance Source () where
+ noSource = ()
+
+-- ** Class 'Inj_Source'
+class Source src => Inj_Source a src where
+ inj_Source :: a -> src
+instance Inj_Source a () where
+ inj_Source _ = ()
+
+-- ** Type family 'SourceOf'
+type family SourceOf a
+
+-- ** Type 'Sourced'
+class Source (SourceOf a) => Sourced a where
+ sourceOf :: a -> SourceOf a
+ setSource :: a -> SourceOf a -> a
+infixl 5 `setSource`
+
+withSource :: Inj_Source src (SourceOf a) => Sourced a => a -> src -> a
+withSource a src = a `setSource` inj_Source src
+
+-- ** Type 'Source_Input'
+type family Source_Input (src :: *) :: *
+type instance Source_Input () = ()
+
+-- ** Type 'Span'
+data Span src
+ = Span
+ { spanBegin :: !src
+ , spanEnd :: !src
+ } deriving (Eq, Ord, Show, Typeable)
+
+-- ** Type 'At'
+-- | Attach a 'Source' to something.
+data At src a
+ = At
+ { at :: !src
+ , unAt :: !a
+ } deriving (Eq, Functor, Ord, Show, Typeable)
Language.Symantic.Grammar.Operators
Language.Symantic.Grammar.Regular
Language.Symantic.Grammar.Terminal
+ Language.Symantic.Grammar.Source
+ Language.Symantic.Grammar.Error
build-depends:
base >= 4.6 && < 5
, text
-- NonEmpty P.SourcePos
instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where
- g_ask_before g = do
+ askBefore g = do
s <- P.statePos <$> P.getParserState
($ s) <$> g
- g_ask_after g = do
+ askAfter g = do
f <- g
f . P.statePos <$> P.getParserState
type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True
askN _n = P.statePos <$> P.getParserState
-- P.SourcePos
instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where
- g_ask_before g = do
+ askBefore g = do
s <- P.getPosition
($ s) <$> g
- g_ask_after g = do
+ askAfter g = do
f <- g
f <$> P.getPosition
type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True
askN _n = P.getPosition
-- ()
instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where
- g_ask_before = fmap ($ ())
- g_ask_after = fmap ($ ())
+ askBefore = fmap ($ ())
+ askAfter = fmap ($ ())
--
-- States
-- st
type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False
instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where
- g_state_before g = do
+ stateBefore g = do
s <- MC.get
f <- g
let (s', a) = f s
MC.put s'
return a
- g_state_after g = do
+ stateAfter g = do
f <- g
s <- MC.get
let (s_, a) = f s
MC.put s_
return a
- g_get_before g = do
+ getBefore g = do
s <- MC.get
f <- g
return (f s)
- g_get_after g = do
+ getAfter g = do
f <- g
s <- MC.get
return (f s)
- g_put g = do
+ put g = do
(s, a) <- g
MC.put s
return a
-- Sym instances
--
instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where
- g_catch me = do
+ catch me {- if you can :-} = do
e <- me
case e of
Left err -> fail $ show err
import qualified Data.Text as Text
import Language.Symantic.Grammar hiding (char, any)
-import qualified Language.Symantic.Grammar as Gram
+import qualified Language.Symantic.Grammar as G
import Language.Symantic
import Language.Symantic.Lib.List (tyList)
) => Gram_Term_AtomsFor src ss g Char where
g_term_atomsFor =
[ rule "teChar" $
- lexeme $ g_source $
+ lexeme $ source $
(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
<$> between tickG tickG (
- cf_of_Terminal (Gram.any `but` tickG) <+>
+ cfOf (G.any `but` tickG) <+>
'\'' <$ string "\\'"
)
]
where
tickG :: Gram_Terminal g' => g' Char
- tickG = Gram.char '\''
+ tickG = G.char '\''
instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where
moduleFor = ["Char"] `moduleWhere`
[ "toLower" := teChar_toLower
) => Gram_Term_AtomsFor src ss g Integer where
g_term_atomsFor =
[ rule "teinteger" $
- lexeme $ g_source $
+ lexeme $ source $
(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
<$> some (choice $ char <$> ['0'..'9'])
]
import qualified Data.Traversable as Traversable
import Language.Symantic
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
import Language.Symantic.Lib.Function (a0, b1, c2)
import Language.Symantic.Lib.MonoFunctor (Element)
[ rule "teList_list" $
between (symbol "[") (symbol "]") listG
, rule "teList_empty" $
- g_source $
+ G.source $
(\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
<$ symbol "["
<* symbol "]"
where
listG :: CF g (AST_Term src ss)
listG = rule "list" $
- g_source $
+ G.source $
(\a mb src ->
case mb of
Just b -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
g_term_atomsFor =
-- TODO: proper TupleSections
[ rule "teTuple2_2" $
- g_source $ parens $
+ source $ parens $
(\a b src ->
BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
<$> g_term
<* symbol ","
<*> g_term
, rule "teTuple2" $
- g_source $
+ source $
(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
<$ symbol "(,)"
]
) => Gram_Term_AtomsFor src ss g () where
g_term_atomsFor =
[ rule "teUnit" $
- g_source $
+ source $
(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
<$ symbol "("
<* symbol ")"
, module Language.Symantic.Transforming
-- * Re-exports for convenience.
, module Language.Symantic.Grammar.Fixity
- , module Language.Symantic.Grammar.Meta
+ , module Language.Symantic.Grammar.Source
+ , module Language.Symantic.Grammar.Error
) where
import Language.Symantic.Typing
import Language.Symantic.Transforming
import Language.Symantic.Grammar.Fixity
-import Language.Symantic.Grammar.Meta
+import Language.Symantic.Grammar.Source
+import Language.Symantic.Grammar.Error
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
import Language.Symantic.Typing
import Language.Symantic.Compiling.Module
<$> g_term_keywords
<*. (any `but` g_term_idname_tail)
where
- identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
+ identG = (:) <$> headG <*> many (G.cfOf g_term_idname_tail)
headG = unicat $ Unicat Char.UppercaseLetter
g_term_mod_name :: CF g (Mod NameTe)
<$> g_term_keywords
<*. (any `but` g_term_idname_tail)
where
- identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
+ identG = (:) <$> headG <*> many (G.cfOf g_term_idname_tail)
headG = unicat $ Unicat_Letter
g_term_idname_tail :: Terminal g Char
g_term_idname_tail = rule "term_idname_tail" $
<$> g_term_keysyms
<*. (any `but` g_term_opname_ok)
where
- symG = some $ cf_of_Terminal g_term_opname_ok
+ symG = some $ G.cfOf g_term_opname_ok
g_term_opname_ok :: Terminal g Char
g_term_opname_ok = rule "term_opname_ok" $
choice (unicat <$>
]
g_term_operators :: CF g (AST_Term src ss)
g_term_operators = rule "term_operators" $
- g_catch $
+ G.catch $
left Error_Term_Gram_Fixity <$>
g_ops
where
g_prefix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
g_infix :: CF g (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
g_postfix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
- g_prefix = g_catch $ g_source $ g_get_after $ op_prefix <$> g_prefix_op
- g_infix = g_catch $ g_source $ g_get_after $ op_infix <$> g_infix_op
- g_postfix = g_catch $ g_source $ g_get_after $ op_postfix <$> g_postfix_op
+ g_prefix = G.catch $ G.source $ G.getAfter $ op_prefix <$> g_prefix_op
+ g_infix = G.catch $ G.source $ G.getAfter $ op_infix <$> g_infix_op
+ g_postfix = G.catch $ G.source $ G.getAfter $ op_postfix <$> g_postfix_op
op_infix
:: Mod NameTe
-> (Imports, Modules src ss)
g_postfix_op :: CF g (Mod NameTe)
g_postfix_op = rule "term_op_postfix" $
lexeme $
- g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote)
+ g_backquote *> g_term_mod_idname <+> -- <* (G.cfOf $ Gram.Term (pure ' ') `but` g_backquote)
g_term_mod_opname
g_infix_op :: CF g (Mod NameTe)
g_infix_op = rule "term_op_infix" $
g_term_atom = rule "term_atom" $
choice $
{-(try (
- g_source $
+ G.source $
(\typ src -> BinTree0 $ inj_EToken src $ Token_Term_Type typ)
<$ char '@' <*> g_type) :) $
-}
(try <$> g_term_atomsR @_ @_ @ss) <>
[ try $
- g_catch $ g_source $ g_get_after $
+ G.catch $ G.source $ G.getAfter $
(\m (imps, mods) src ->
case lookupDefTerm FixitySing_Infix imps m mods of
Right t -> Right $ BinTree0 $ token_term t src
g_term_group = rule "term_group" $ parens g_term
g_term_abst :: CF g (AST_Term src ss)
g_term_abst = rule "term_abst" $
- g_source $
+ G.source $
((\(xs, te) src ->
foldr (\(x, ty_x) ->
BinTree0 . Token_Term_Abst src x ty_x) te xs) <$>) $
-> CF g ([(NameTe, AST_Type src)], AST_Term src ss)
-- g_term_abst_args_body args body = (,) <$> args <*> body
g_term_abst_args_body cf_args cf_body =
- g_state_before $
+ G.stateBefore $
(\a b (imps::Imports, mods::Modules src ss) -> ((imps, mods), (a, b)))
- <$> g_state_after ((<$> cf_args) $ \args (imps::Imports, Modules mods) ->
+ <$> G.stateAfter ((<$> cf_args) $ \args (imps::Imports, Modules mods) ->
((imps, Modules $ Map.alter (setArgs args) [] mods), args))
<*> cf_body
where
}
g_term_let :: CF g (AST_Term src ss)
g_term_let = rule "term_let" $
- g_source $
+ G.source $
(\name args bound body src ->
BinTree0 $
Token_Term_Let src name
, void g_term_mod_name
, void g_term_name
, void g_term_idname
- , void $ cf_of_Terminal g_term_idname_tail
- , void $ cf_of_Reg g_term_keywords
+ , void $ G.cfOf g_term_idname_tail
+ , void $ G.cfOf g_term_keywords
, void g_term_mod_opname
, void g_term_opname
- , void $ cf_of_Terminal g_term_opname_ok
- , void $ cf_of_Reg g_term_keysyms
+ , void $ G.cfOf g_term_opname_ok
+ , void $ G.cfOf g_term_keysyms
] where
voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g ()
voiD = (() <$)
-- Type
instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
- typeOf t = typeOfTerm t `source` TermT t
+ typeOf t = typeOfTerm t `withSource` TermT t
typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
typeOfTerm (Term q t _) = q #> t
import Data.Text (Text)
import qualified Data.Char as Char
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
import Language.Symantic.Typing.Variable
-- * Type 'NameTy'
g_type = rule "type" $ g_type_fun
g_type_fun :: CF g (AST_Type src)
g_type_fun = rule "type_fun" $
- infixrG g_type_list (g_source $ op <$ symbol "->")
+ infixrG g_type_list (G.source $ op <$ symbol "->")
where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(->)")
-- TODO: maybe not harcoding g_type_list and g_type_tuple2
g_type_list :: CF g (AST_Type src)
g_type_list = rule "type_list" $
- g_source $ inside mk
+ G.source $ inside mk
(symbol "[") (optional g_type) (symbol "]")
(const <$> g_type_tuple2)
where
tok src = BinTree0 $ Token_Type_Const $ At src "[]"
g_type_tuple2 :: CF g (AST_Type src)
g_type_tuple2 = rule "type_tuple2" $
- try (parens (infixrG (g_type) (g_source $ op <$ symbol ","))) <+> (g_type_app)
+ try (parens (infixrG (g_type) (G.source $ op <$ symbol ","))) <+> (g_type_app)
where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(,)")
g_type_app :: CF g (AST_Type src)
g_type_app = rule "type_app" $
g_type_symbol
g_type_name_const :: CF g (AST_Type src)
g_type_name_const = rule "type_name_const" $
- lexeme $ g_source $
+ lexeme $ G.source $
(\n ns src -> BinTree0 $ Token_Type_Const $ At src $ fromString $ n:ns)
<$> unicat (Unicat Char.UppercaseLetter)
<*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
g_type_name_var :: CF g (AST_Type src)
g_type_name_var = rule "type_name_var" $
- lexeme $ g_source $
+ lexeme $ G.source $
(\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
<$> unicat (Unicat Char.LowercaseLetter)
<*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
g_type_symbol :: CF g (AST_Type src)
g_type_symbol = rule "type_symbol" $
- g_source $ (mk <$>) $
- parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
+ G.source $ (mk <$>) $
+ parens $ many $ G.cfOf $ choice g_ok `but` choice g_ko
where
mk s src = BinTree0 $ Token_Type_Const $ At src (fromString $ "(" ++ s ++ ")")
g_ok = unicat <$>
Either err ret
when_KiFun x k =
case x of
- KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
+ KiFun _src a b -> k Refl (a `withSource` KindK x) (b `withSource` KindK x)
_ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)
setSource (TyFam _src l f as) src = TyFam src l f as
instance Inj_Source (TypeVT src) src => KindOf (Type src vs) where
- kindOf t = kindOfType t `source` TypeVT t
+ kindOf t = kindOfType t `withSource` TypeVT t
instance ConstsOf (Type src vs t) where
constsOf (TyConst _src _len c) = Set.singleton $ ConstC c
instance ConstsOf (Const src c) where
constsOf = Set.singleton . ConstC
instance Inj_Source (ConstC src) src => KindOf (Const src) where
- kindOf c@(Const kc) = kc `source` ConstC c
+ kindOf c@(Const kc) = kc `withSource` ConstC c
kindOfConst :: Const src (t::kt) -> Kind src kt
kindOfConst (Const kc) = kc
, Type src tys (FunRes x) )
go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
| Just HRefl <- proj_ConstKi @(K (->)) @(->) f
- = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini))
+ = Just ((a `withSource` TypeVT ty_ini), (b `withSource` TypeVT ty_ini))
go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
| Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
= go b
go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
| Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
= go ctx t -- NOTE: skip the constraint @q@.
- go ctx (TyApp _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f
- go ctx t = (TypeT (t `source` TypeVT typ), ctx)
+ go ctx (TyApp _src f a) = go (TypeT (a `withSource` TypeVT typ) : ctx) f
+ go ctx t = (TypeT (t `withSource` TypeVT typ), ctx)
{-
spineTy
instance Show (Var src tys v) where
showsPrec p v = showsPrec p (indexVar v)
instance Inj_Source (EVar src vs) src => KindOf (Var src vs) where
- kindOf v = kindOfVar v `source` EVar v
+ kindOf v = kindOfVar v `withSource` EVar v
instance LenVars (Var src vs v) where
lenVars (VarZ _k l) = l
lenVars (VarS v) = LenS (lenVars v)
sourcephile / git / haskell / symantic.git / commitdiff