symantic 6.0.0.20170623 → 6.2.0.20170702
raw patch · 18 files changed
+1034/−830 lines, 18 files
Files
- Language/Symantic.hs +4/−2
- Language/Symantic/Compiling/Beta.hs +6/−6
- Language/Symantic/Compiling/Grammar.hs +117/−112
- Language/Symantic/Compiling/Module.hs +79/−168
- Language/Symantic/Compiling/Read.hs +63/−38
- Language/Symantic/Compiling/Term.hs +24/−24
- Language/Symantic/Typing.hs +2/−0
- Language/Symantic/Typing/Document.hs +163/−37
- Language/Symantic/Typing/Grammar.hs +178/−35
- Language/Symantic/Typing/Kind.hs +22/−22
- Language/Symantic/Typing/List.hs +14/−14
- Language/Symantic/Typing/Module.hs +240/−0
- Language/Symantic/Typing/Read.hs +33/−64
- Language/Symantic/Typing/Show.hs +8/−5
- Language/Symantic/Typing/Type.hs +61/−78
- Language/Symantic/Typing/Unify.hs +9/−9
- Language/Symantic/Typing/Variable.hs +5/−5
- symantic.cabal +6/−211
Language/Symantic.hs view
@@ -5,7 +5,8 @@ , 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@@ -14,4 +15,5 @@ import Language.Symantic.Transforming import Language.Symantic.Grammar.Fixity-import Language.Symantic.Grammar.Meta+import Language.Symantic.Grammar.Source+import Language.Symantic.Grammar.Error
Language/Symantic/Compiling/Beta.hs view
@@ -12,7 +12,7 @@ -- applying embedded 'TeSym's, or return an error. betaTerm :: forall src ss es vs fun arg.- Inj_Source (TypeVT src) src =>+ SourceInj (TypeVT src) src => Constable (->) => Term src ss es vs (fun::K.Type) -> Term src ss es vs (arg::K.Type) ->@@ -39,7 +39,7 @@ -- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible. betaTerms ::- Inj_Source (TypeVT src) src =>+ SourceInj (TypeVT src) src => Constable (->) => BinTree (TermVT src ss es) -> Either (Error_Beta src) (TermVT src ss es)@@ -74,7 +74,7 @@ -- with the 'Type' of the argument. deriving (Eq, Show) -instance Inj_Error (Error_Beta src) (Error_Beta src) where- inj_Error = id-instance Inj_Error (Error_Unify src) (Error_Beta src) where- inj_Error = Error_Beta_Unify+instance ErrorInj (Error_Beta src) (Error_Beta src) where+ errorInj = id+instance ErrorInj (Error_Unify src) (Error_Beta src) where+ errorInj = Error_Beta_Unify
Language/Symantic/Compiling/Grammar.hs view
@@ -8,19 +8,18 @@ import Control.Arrow (left) import Control.Monad (void)-import Data.Proxy (Proxy(..)) import Data.Semigroup (Semigroup(..))+import Data.Map.Strict (Map) import Prelude hiding (mod, not, any)-import qualified Data.Char as Char import qualified Data.Function as Fun 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 --- * Class 'Gram_Name'+-- * Class 'Gram_Term_Name' class ( Gram_Terminal g , Gram_Rule g@@ -32,74 +31,56 @@ , Gram_CF g , Gram_Comment g , Gram_Op g- ) => Gram_Name g where- g_mod_path :: CF g PathMod- g_mod_path = rule "mod_path" $- infixrG- (pure <$> g_mod_name)- (op <$ char '.')- where op = (<>)- g_mod_name :: CF g NameMod- g_mod_name = rule "mod_name" $- (NameMod . Text.pack <$>) $- (identG `minus`) $- Fun.const- <$> g_term_keywords- <*. (any `but` g_term_idname_tail)- where- identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)- headG = unicat $ Unicat Char.UppercaseLetter- - g_term_mod_name :: CF g (Mod NameTe)- g_term_mod_name = rule "term_mod_name" $+ , Gram_Mod g+ ) => Gram_Term_Name g where+ g_ModNameTe :: CF g (Mod NameTe)+ g_ModNameTe = rule "ModNameTe" $ lexeme $- g_term_mod_idname <+>- parens g_term_mod_opname- g_term_name :: CF g NameTe- g_term_name = rule "term_name" $+ g_ModNameTeId <+>+ parens g_ModNameTeOp+ g_NameTe :: CF g NameTe+ g_NameTe = rule "NameTe" $ lexeme $- g_term_idname <+>- parens g_term_opname+ g_NameTeId <+>+ parens g_NameTeOp - g_term_mod_idname :: CF g (Mod NameTe)- g_term_mod_idname = rule "term_mod_idname" $+ g_ModNameTeId :: CF g (Mod NameTe)+ g_ModNameTeId = rule "ModNameTeId" $ Mod- <$> option [] (try $ g_mod_path <* char '.')- <*> g_term_idname- g_term_idname :: CF g NameTe- g_term_idname = rule "term_idname" $+ <$> option [] (try $ g_PathMod <* char '.')+ <*> g_NameTeId+ g_NameTeId :: CF g NameTe+ g_NameTeId = rule "NameTeId" $ (NameTe . Text.pack <$>) $ (identG `minus`) $ Fun.const- <$> g_term_keywords- <*. (any `but` g_term_idname_tail)+ <$> g_NameTeKey+ <*. (any `but` g_NameTeIdTail) where- identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)+ identG = (:) <$> headG <*> many (cfOf g_NameTeIdTail) headG = unicat $ Unicat_Letter- g_term_idname_tail :: Terminal g Char- g_term_idname_tail = rule "term_idname_tail" $+ g_NameTeIdTail :: Terminal g Char+ g_NameTeIdTail = rule "NameTeIdTail" $ unicat Unicat_Letter <+> unicat Unicat_Number- g_term_keywords :: Reg rl g String- g_term_keywords = rule "term_keywords" $+ g_NameTeKey :: Reg rl g String+ g_NameTeKey = rule "NameTeKey" $ choice $ string <$> ["in", "let"] - g_term_mod_opname :: CF g (Mod NameTe)- g_term_mod_opname = rule "term_mod_opname" $+ g_ModNameTeOp :: CF g (Mod NameTe)+ g_ModNameTeOp = rule "ModNameTeOp" $ Mod- <$> option [] (try $ g_mod_path <* char '.')- <*> g_term_opname- g_term_opname :: CF g NameTe- g_term_opname = rule "term_opname" $+ <$> option [] (try $ g_PathMod <* char '.')+ <*> g_NameTeOp+ g_NameTeOp :: CF g NameTe+ g_NameTeOp = rule "NameTeOp" $ (NameTe . Text.pack <$>) $- (symG `minus`) $+ (some (cfOf g_NameTeOpOk) `minus`) $ Fun.const- <$> g_term_keysyms- <*. (any `but` g_term_opname_ok)- where- symG = some $ cf_of_Terminal g_term_opname_ok- g_term_opname_ok :: Terminal g Char- g_term_opname_ok = rule "term_opname_ok" $+ <$> g_NameTeKeySym+ <*. (any `but` g_NameTeOpOk)+ g_NameTeOpOk :: Terminal g Char+ g_NameTeOpOk = rule "NameTeOpOk" $ choice (unicat <$> [ Unicat_Symbol , Unicat_Punctuation@@ -107,13 +88,13 @@ ]) `but` koG where koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])- g_term_keysyms :: Reg rl g String- g_term_keysyms = rule "term_keysyms" $+ g_NameTeKeySym :: Reg rl g String+ g_NameTeKeySym = rule "NameTeKeySym" $ choice $ string <$> ["\\", "->", "=", "@"] -deriving instance Gram_Name g => Gram_Name (CF g)-instance Gram_Name EBNF-instance Gram_Name RuleEBNF+deriving instance Gram_Term_Name g => Gram_Term_Name (CF g)+instance Gram_Term_Name EBNF+instance Gram_Term_Name RuleEBNF -- * Class 'Gram_Term_Type' class@@ -124,20 +105,30 @@ , Gram_App g , Gram_CF g , Gram_Comment g- , Gram_Name g+ , Gram_Term_Name g , Gram_Type src g ) => Gram_Term_Type src g where g_term_abst_decl :: CF g (NameTe, AST_Type src) g_term_abst_decl = rule "term_abst_decl" $ parens $ (,)- <$> g_term_name+ <$> g_NameTe <* (symbol "::" <+> symbol ":") -- NOTE: "::" is Haskell compatibility and ":" is another common notation. <*> g_type deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g)-instance Gram_Source src EBNF => Gram_Term_Type src EBNF-instance Gram_Source src RuleEBNF => Gram_Term_Type src RuleEBNF+instance+ ( Gram_Source src EBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf []+ ) => Gram_Term_Type src EBNF+instance+ ( Gram_Source src RuleEBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf []+ ) => Gram_Term_Type src RuleEBNF -- ** Type 'Error_Term_Gram' data Error_Term_Gram@@ -162,10 +153,10 @@ , Gram_CF g , Gram_Comment g , Gram_Type src g- , Gram_Name g+ , Gram_Term_Name g , Gram_Term_Type src g , Gram_Term_Atoms src ss g- , Gram_State (Imports, Modules src ss) g+ , Gram_State (Imports NameTe, Modules src ss) g ) => Gram_Term src ss g where g_term :: CF g (AST_Term src ss) g_term = rule "term" $@@ -176,7 +167,7 @@ ] 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@@ -185,53 +176,53 @@ 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)+ -> (Imports NameTe, Modules src ss) -> src -> Either Error_Term_Gram (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss) op_infix name (imps, mods) src = do t <- Error_Term_Gram_Module `left`- lookupDefTerm FixitySing_Infix imps name mods+ lookupDefTerm FixyInfix imps name mods Right $ (token_fixity t,) $ \a b -> (BinTree0 (token_term t src) `BinTree2` a) `BinTree2` b op_prefix, op_postfix :: Mod NameTe- -> (Imports, Modules src ss)+ -> (Imports NameTe, Modules src ss) -> src -> Either Error_Term_Gram ( Unifix , AST_Term src ss -> AST_Term src ss ) op_prefix name (imps, mods) src = do t <- Error_Term_Gram_Module `left`- lookupDefTerm FixitySing_Prefix imps name mods+ lookupDefTerm FixyPrefix imps name mods Right $ (token_fixity t,) $ \a -> BinTree0 (token_term t src) `BinTree2` a op_postfix name (imps, mods) src = do t <- Error_Term_Gram_Module `left`- lookupDefTerm FixitySing_Postfix imps name mods+ lookupDefTerm FixyPostfix imps name mods Right $ (token_fixity t,) $ \a -> BinTree0 (token_term t src) `BinTree2` a 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_term_mod_opname+ g_backquote *> g_ModNameTeId <+> -- <* (G.cfOf $ Gram.Term (pure ' ') `but` g_backquote)+ g_ModNameTeOp g_infix_op :: CF g (Mod NameTe) g_infix_op = rule "term_op_infix" $ lexeme $- between g_backquote g_backquote g_term_mod_idname <+>- try (Fun.const <$> g_term_mod_opname <*> (string " " <+> string "\n")) <+>+ between g_backquote g_backquote g_ModNameTeId <+>+ try (Fun.const <$> g_ModNameTeOp <*> (string " " <+> string "\n")) <+> pure (Mod [] " ") g_prefix_op :: CF g (Mod NameTe) g_prefix_op = rule "term_op_prefix" $ lexeme $- g_term_mod_idname <* g_backquote <+>- g_term_mod_opname+ g_ModNameTeId <* g_backquote <+>+ g_ModNameTeOp g_backquote :: Gram_Terminal g' => g' Char g_backquote = char '`' @@ -239,28 +230,28 @@ 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+ case lookupDefTerm FixyInfix imps m mods of Right t -> Right $ BinTree0 $ token_term t src Left err -> case m of [] `Mod` n -> Right $ BinTree0 $ Token_Term_Var src n _ -> Left $ Error_Term_Gram_Module err- ) <$> g_term_mod_name+ ) <$> g_ModNameTe , g_term_group ] g_term_group :: CF g (AST_Term src ss) 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) <$>) $@@ -273,37 +264,45 @@ -> 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 $- (\a b (imps::Imports, mods::Modules src ss) -> ((imps, mods), (a, b)))- <$> g_state_after ((<$> cf_args) $ \args (imps::Imports, Modules mods) ->- ((imps, Modules $ Map.alter (setArgs args) [] mods), args))+ G.stateBefore $+ (\a b (imps::Imports NameTe, mods::Modules src ss) -> ((imps, mods), (a, b)))+ <$> G.stateAfter ((<$> cf_args) $ \args (imps::Imports NameTe, mods) ->+ ((setArgsImps args imps, setArgsMods args mods), args)) <*> cf_body where- setArgs args = \case- Nothing -> Just $ moduleEmpty {module_infix = insArg mempty args}- Just mod -> Just $ mod- { module_prefix = delArg (module_prefix mod) args- , module_infix = insArg (module_infix mod) args- , module_postfix = delArg (module_postfix mod) args+ setArgsImps args (Imports imps) = Imports $ Map.alter (alterArgsImps args) [] imps+ alterArgsImps args = \case+ Nothing -> Just mempty+ Just m -> Just $ mapMapFixity (delArgImp args) m+ delArgImp :: [(NameTe, _a)] -> Map NameTe PathMod -> Map NameTe PathMod+ delArgImp = flip $ foldr $ \(n, _) -> Map.delete n+ + setArgsMods args (Modules mods) = Modules $ Map.alter (alterArgsMods args) [] mods+ alterArgsMods args = \case+ Nothing -> Just moduleEmpty{byInfix = mempty `insArgMod` args}+ Just m -> Just m+ { byPrefix = byPrefix m `delArgMod` args+ , byInfix = byInfix m `insArgMod` args+ , byPostfix = byPostfix m `delArgMod` args }- delArg :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix- delArg = foldr $ \(n, _) -> Map.delete n- insArg :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix- insArg = foldr $ \(n, _) ->+ delArgMod :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix+ delArgMod = foldr $ \(n, _) -> Map.delete n+ insArgMod :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix+ insArgMod = foldr $ \(n, _) -> Map.insert n Tokenizer { token_term = (`Token_Term_Var` n) , token_fixity = infixN5 } 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 (foldr (\(x, ty_x) -> BinTree0 . Token_Term_Abst src x ty_x) bound args) body) <$ symbol "let"- <*> g_term_name+ <*> g_NameTe <*> many g_term_abst_decl <* symbol "=" <*> g_term@@ -317,10 +316,16 @@ instance ( Gram_Term_Atoms src ss EBNF , Gram_Source src EBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf [] ) => Gram_Term src ss EBNF instance ( Gram_Term_Atoms src ss RuleEBNF , Gram_Source src RuleEBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf [] ) => Gram_Term src ss RuleEBNF -- ** Class 'Gram_Term_Atoms'@@ -356,15 +361,15 @@ , voiD g_term_abst , void (g_term_abst_decl::CF g (NameTe, AST_Type ())) , voiD g_term_let- , 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_term_mod_opname- , void g_term_opname- , void $ cf_of_Terminal g_term_opname_ok- , void $ cf_of_Reg g_term_keysyms+ , void g_ModNameTe+ , void g_NameTe+ , void g_NameTeId+ , void $ G.cfOf g_NameTeIdTail+ , void $ G.cfOf g_NameTeKey+ , void g_ModNameTeOp+ , void g_NameTeOp+ , void $ G.cfOf g_NameTeOpOk+ , void $ G.cfOf g_NameTeKeySym ] where voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g () voiD = (() <$)
Language/Symantic/Compiling/Module.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -10,43 +9,33 @@ import Data.Bool (not) import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe) import Data.Semigroup (Semigroup(..)) import Data.Set (Set) import Data.String (IsString(..))-import Data.Text (Text) import Prelude hiding (mod, not, any)-import qualified Data.Kind as K import qualified Data.Map.Strict as Map import Language.Symantic.Grammar import Language.Symantic.Typing import Language.Symantic.Compiling.Term --- * Type 'Mod'-data Mod a = Mod PathMod a- deriving (Eq, Functor, Ord, Show)---- ** Type 'PathMod'-type PathMod = [NameMod]---- ** Type 'NameMod'-newtype NameMod = NameMod Text- deriving (Eq, Ord, Show)-instance IsString NameMod where- fromString = NameMod . fromString- -- * Class 'ModuleFor' class ModuleFor src ss s where moduleFor :: (PathMod, Module src ss) moduleFor = ([], moduleEmpty) --- * Type 'Imports'-newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))- deriving (Eq, Show)-type FilterImports = Maybe (Set NameTe)--importQualifiedAs :: PathMod -> Modules src ss -> Imports-importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]+importModules :: PathMod -> Modules src ss -> Imports NameTe+importModules as (Modules mods) =+ Imports $ Map.singleton as $+ Map.foldrWithKey+ (\pm (ByFixity mp mi mq) acc ->+ acc <> ByFixity+ { byPrefix = pm <$ mp+ , byInfix = pm <$ mi+ , byPostfix = pm <$ mq+ }+ ) mempty mods -- * Type 'Modules' newtype Modules src ss@@ -71,9 +60,9 @@ let errs = Map.filter (not . null) $ (<$> xy) $ \(a, b) ->- inter a b module_prefix <>- inter a b module_infix <>- inter a b module_postfix in+ inter a b byPrefix <>+ inter a b byInfix <>+ inter a b byPostfix in case errs of e | null e -> Nothing e -> Just $ Error_Module_colliding_Term e@@ -89,74 +78,61 @@ = Error_Module_colliding_Term (Map PathMod (Set NameTe)) | Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe) | Error_Module_missing PathMod- | Error_Module_missing_Term (Mod NameTe)+ | Error_Module_missing_Term (Mod NameTe) -- FixyA deriving (Eq, Show) -- ** Type 'Module'-data Module src ss- = Module- { module_prefix :: ModuleFixy src ss Unifix- , module_infix :: ModuleFixy src ss Infix- , module_postfix :: ModuleFixy src ss Unifix- } deriving (Eq, Show)--module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy-module_fixity = \case- FixitySing_Prefix -> module_prefix- FixitySing_Infix -> module_infix- FixitySing_Postfix -> module_postfix+type Module src ss = ByFixity (ModuleFixy src ss Unifix)+ (ModuleFixy src ss Infix)+ (ModuleFixy src ss Unifix) moduleEmpty :: Module src ss-moduleEmpty = Module- { module_prefix = mempty- , module_infix = mempty- , module_postfix = mempty+moduleEmpty = ByFixity+ { byPrefix = mempty+ , byInfix = mempty+ , byPostfix = mempty } moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss) moduleWhere mod lst =- (mod,) Module- { module_infix = mk $ \(n `WithFixity` fixy := t) ->+ (mod,) ByFixity+ { byInfix = mk $ \(n `WithFixity` fixy := t) -> case fixy of Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))] _ -> []- , module_prefix = mk $ \(n `WithFixity` fixy := t) ->+ , byPrefix = mk $ \(n `WithFixity` fixy := t) -> case fixy of Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))] _ -> []- , module_postfix = mk $ \(n `WithFixity` fixy := t) ->+ , byPostfix = mk $ \(n `WithFixity` fixy := t) -> case fixy of Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))] _ -> [] } where mk ::- (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->- Map NameTe (Tokenizer fixy src ss)+ (DefTerm src ss -> [(NameTe, Tokenizer src ss fixy)]) ->+ Map NameTe (Tokenizer src ss fixy) mk = Map.fromList . (`foldMap` lst) -- *** Type 'ModuleFixy'-type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)--instance Semigroup (Module src ss) where- x <> y =- Module- { module_prefix = module_prefix x <> module_prefix y- , module_infix = module_infix x <> module_infix y- , module_postfix = module_postfix x <> module_postfix y- }+type ModuleFixy src ss fixy = Map NameTe (Tokenizer src ss fixy) -- ** Type 'Tokenizer'-data Tokenizer fixy src ss+data Tokenizer src ss fixy = Tokenizer { token_fixity :: fixy , token_term :: src -> Token_Term src ss }-instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where+instance (Source src, Eq fixy) => Eq (Tokenizer src ss fixy) where Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)-instance Source src => Show (Tokenizer fixy src ss) where+instance Source src => Show (Tokenizer src ss fixy) where show (Tokenizer _fx x) = show (x noSource) +-- ** Type 'AST_Term'+-- | /Abstract Syntax Tree/ of 'Token_Term'.+type AST_Term src ss = BinTree (Token_Term src ss)+ -- ** Type 'Token_Term' data Token_Term src ss = Token_Term (TermAVT src ss)@@ -202,59 +178,34 @@ showsPrec _p (Token_Term_App _) = showString "Token_Term_App" -- ** Type 'NameTe'-newtype NameTe = NameTe Text+newtype NameTe = NameTe Name deriving (Eq, Ord, Show) instance IsString NameTe where fromString = NameTe . fromString---- * Type 'CtxTy'--- | /Typing context/--- accumulating at each /lambda abstraction/--- the 'Type' of the introduced variable.--- It is built top-down from the closest--- including /lambda abstraction/ to the farest.-data CtxTy src (ts::[K.Type]) where- CtxTyZ :: CtxTy src '[]- CtxTyS :: NameTe- -> Type src '[] t- -> CtxTy src ts- -> CtxTy src (t ': ts)-infixr 5 `CtxTyS`--appendCtxTy- :: CtxTy src ts0- -> CtxTy src ts1- -> CtxTy src (ts0 ++ ts1)-appendCtxTy CtxTyZ c = c-appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'------ ** Type 'AST_Term'--- | /Abstract Syntax Tree/ of 'Token_Term'.-type AST_Term src ss = BinTree (Token_Term src ss)+instance NameOf NameTe where+ nameOf (NameTe n) = n --- * Class 'Inj_Modules'-type Inj_Modules src ss- = Inj_ModulesR src ss ss+-- * Class 'ModulesInj'+type ModulesInj src ss+ = ModulesInjR src ss ss -inj_Modules ::+modulesInj :: forall src ss.- Inj_Modules src ss =>+ ModulesInj src ss => Either Error_Module (Modules src ss)-inj_Modules = inj_ModulesR @_ @_ @ss+modulesInj = modulesInjR @_ @_ @ss --- ** Class 'Inj_ModulesR'-class Inj_ModulesR src (ss::[*]) (rs::[*]) where- inj_ModulesR :: Either Error_Module (Modules src ss)-instance Inj_ModulesR src ss '[] where- inj_ModulesR = Right $ Modules mempty+-- ** Class 'ModulesInjR'+class ModulesInjR src (ss::[*]) (rs::[*]) where+ modulesInjR :: Either Error_Module (Modules src ss)+instance ModulesInjR src ss '[] where+ modulesInjR = Right $ Modules mempty instance ( ModuleFor src ss s- , Inj_ModulesR src ss rs- ) => Inj_ModulesR src ss (Proxy s ': rs) where- inj_ModulesR = do- x <- inj_ModulesR @_ @_ @rs+ , ModulesInjR src ss rs+ ) => ModulesInjR src ss (Proxy s ': rs) where+ modulesInjR = do+ x <- modulesInjR @_ @_ @rs let (n, m) = moduleFor @_ @_ @s Modules (Map.singleton n m) `unionModules` x @@ -269,58 +220,48 @@ -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'. lookupDefTerm :: forall src ss fixy.- FixitySing fixy ->- Imports ->+ Fixy (ModuleFixy src ss Unifix)+ (ModuleFixy src ss Infix)+ (ModuleFixy src ss Unifix)+ (ModuleFixy src ss fixy) ->+ Imports NameTe -> Mod NameTe -> Modules src ss ->- Either Error_Module (Tokenizer fixy src ss)-lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =+ Either Error_Module (Tokenizer src ss fixy)+lookupDefTerm FixyInfix _is ([] `Mod` " ") _ms = Right $ Tokenizer { token_term = Token_Term_App @src @ss , token_fixity = Infix (Just AssocL) 9 }-lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =- let mod_fixy = module_fixity fixy in- case Map.lookup m is of- Nothing ->- maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=- maybe (Left $ Error_Module_missing_Term mn) Right .- Map.lookup n . mod_fixy- Just ims ->- let look =- -- n matches amongst ims- (`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe- Map.lookup im mods >>=- Map.lookup n . mod_fixy >>=- Just . Map.singleton n in- case Map.minView look of- Nothing -> Left $ Error_Module_missing_Term mn- Just (r, rs) | null rs -> Right $ snd $ Map.findMin r- | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look+lookupDefTerm fixy imps mn@(m `Mod` n) (Modules mods) =+ let m' = m `fromMaybe` lookupImports fixy mn imps in+ maybe (Left $ Error_Module_missing m') Right (Map.lookup m' mods) >>=+ maybe (Left $ Error_Module_missing_Term mn) Right .+ Map.lookup n . selectByFixity fixy -- | Delete given 'Mod' 'NameTe' into given 'Modules'. deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms where del mod = mod- { module_prefix = Map.delete n $ module_prefix mod- , module_infix = Map.delete n $ module_infix mod- , module_postfix = Map.delete n $ module_postfix mod+ { byPrefix = Map.delete n $ byPrefix mod+ , byInfix = Map.delete n $ byInfix mod+ , byPostfix = Map.delete n $ byPostfix mod } --- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.+-- | Delete given 'Mod' 'NameTe' into 'byInfix's of given 'Modules'. deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms- where del mod = mod{module_infix = Map.delete n $ module_infix mod}+ where del mod = mod{byInfix = Map.delete n $ byInfix mod} --- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.+-- | Delete given 'Mod' 'NameTe' into 'byPrefix's of given 'Modules'. deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms- where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}+ where del mod = mod{byPrefix = Map.delete n $ byPrefix mod} --- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.+-- | Delete given 'Mod' 'NameTe' into 'byPostfix's of given 'Modules'. deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms- where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}+ where del mod = mod{byPostfix = Map.delete n $ byPostfix mod} insertDefTerm :: forall src ss.@@ -348,36 +289,6 @@ Fixity -> Module src ss -> Module src ss insertFixity ins fx mod = case fx of- Fixity1 uni@Prefix{} -> mod {module_prefix = ins uni $ module_prefix mod}- Fixity2 inf@Infix{} -> mod {module_infix = ins inf $ module_infix mod}- Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}---- ** Type 'WithFixity'-data WithFixity a- = WithFixity a Fixity- deriving (Eq, Show)-instance IsString (WithFixity NameTe) where- fromString a = WithFixity (fromString a) (Fixity2 infixN5)--withInfix :: a -> Infix -> WithFixity a-withInfix a inf = a `WithFixity` Fixity2 inf-withInfixR :: a -> Precedence -> WithFixity a-withInfixR a p = a `WithFixity` Fixity2 (infixR p)-withInfixL :: a -> Precedence -> WithFixity a-withInfixL a p = a `WithFixity` Fixity2 (infixL p)-withInfixN :: a -> Precedence -> WithFixity a-withInfixN a p = a `WithFixity` Fixity2 (infixN p)-withInfixB :: a -> (Side, Precedence) -> WithFixity a-withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)-withPrefix :: a -> Precedence -> WithFixity a-withPrefix a p = a `WithFixity` Fixity1 (Prefix p)-withPostfix :: a -> Precedence -> WithFixity a-withPostfix a p = a `WithFixity` Fixity1 (Postfix p)---- ** Type 'FixitySing'-data FixitySing fixy where- FixitySing_Prefix :: FixitySing Unifix- FixitySing_Infix :: FixitySing Infix- FixitySing_Postfix :: FixitySing Unifix-deriving instance Eq (FixitySing fixy)-deriving instance Show (FixitySing fixy)+ Fixity1 uni@Prefix{} -> mod {byPrefix = ins uni $ byPrefix mod}+ Fixity2 inf@Infix{} -> mod {byInfix = ins inf $ byInfix mod}+ Fixity1 uni@Postfix{} -> mod {byPostfix = ins uni $ byPostfix mod}
Language/Symantic/Compiling/Read.hs view
@@ -15,20 +15,21 @@ -- | Convenient type alias for 'readTerm' and related functions. type ReadTerm src ss ts = Source src =>- Inj_Source (TypeVT src) src =>- Inj_Source (KindK src) src =>- Inj_Source (AST_Type src) src =>+ SourceInj (TypeVT src) src =>+ SourceInj (KindK src) src =>+ SourceInj (AST_Type src) src => Constable (->) =>- Name2Type src ->+ Imports NameTy ->+ ModulesTy src -> CtxTy src ts -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss ts) -- | Read a 'TermVT' from and 'AST_Term'. readTerm :: forall src ss ts. ReadTerm src ss ts-readTerm n2t ctxTy ast = do+readTerm impsTy modsTy ctxTy ast = do ts <- go ctxTy `traverse` ast- inj_Error `left` betaTerms ts+ errorInj `left` betaTerms ts where go :: forall ts'.@@ -40,12 +41,12 @@ go ts (Token_Term_Var _src name) = teVar name ts go _ts (Token_Term_App _src) = Right $ TermVT teApp go ts (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do- TypeVT ty_arg <- inj_Error `left` readType n2t ast_ty_arg- when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->+ TypeVT ty_arg <- errorInj `left` readType impsTy modsTy ast_ty_arg+ when_EqKind (kindInj @K.Type) (kindOf ty_arg) $ \Refl -> case lenVars ty_arg of LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do- TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name_arg ta ts) ast_body+ TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name_arg ta ts) ast_body let (qa', qr') = appendVars qa qr let (ta', tr') = appendVars ta tr Right $@@ -64,11 +65,11 @@ Term (qa' # qr') (ta' ~> tr') $ TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c) go ts (Token_Term_Let _src name ast_arg ast_body) = do- TermVT (Term qa ta (TeSym arg)) <- readTerm n2t ts ast_arg+ TermVT (Term qa ta (TeSym arg)) <- readTerm impsTy modsTy ts ast_arg case lenVars ta of LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta) LenZ -> do- TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name ta ts) ast_body+ TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body let (qa', qr') = appendVars qa qr let tr' = allocVarsL (lenVars ta) tr Right $@@ -137,12 +138,13 @@ readTermWithCtx :: Foldable f => Source src =>- Inj_Source (TypeVT src) src =>- Inj_Source (KindK src) src =>- Inj_Source (AST_Type src) src =>+ SourceInj (TypeVT src) src =>+ SourceInj (KindK src) src =>+ SourceInj (AST_Type src) src => Constable (->) => f (NameTe, TermT src ss '[] '[]) ->- Name2Type src ->+ Imports NameTy ->+ ModulesTy src -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[]) readTermWithCtx env =@@ -165,8 +167,8 @@ (NameTe, TermT src ss '[] '[]) -> (forall ts'. ReadTerm src ss ts') -> ReadTerm src ss ts-readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe n2t ctxTy ast = do- TermVT (Term q t (TeSym te)) <- readTe n2t (CtxTyS n (qn #> tn) ctxTy) ast+readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe impsTy modsTy ctxTy ast = do+ TermVT (Term q t (TeSym te)) <- readTe impsTy modsTy (CtxTyS n (qn #> tn) ctxTy) ast case proveConstraint qn of Nothing -> Left $ Error_Term_proofless $ TypeVT qn Just Dict ->@@ -178,15 +180,38 @@ readTermWithCtxClose :: (forall ts'. ReadTerm src ss ts') -> Source src =>- Inj_Source (TypeVT src) src =>- Inj_Source (KindK src) src =>- Inj_Source (AST_Type src) src =>+ SourceInj (TypeVT src) src =>+ SourceInj (KindK src) src =>+ SourceInj (AST_Type src) src => Constable (->) =>- Name2Type src ->+ Imports NameTy ->+ ModulesTy src -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[])-readTermWithCtxClose readTe n2t = readTe n2t CtxTyZ+readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ +-- * Type 'CtxTy'+-- | /Typing context/+-- accumulating at each /lambda abstraction/+-- the 'Type' of the introduced variable.+-- It is built top-down from the closest+-- including /lambda abstraction/ to the farest.+-- It determines the 'Type's of 'CtxTe'.+data CtxTy src (ts::[K.Type]) where+ CtxTyZ :: CtxTy src '[]+ CtxTyS :: NameTe+ -> Type src '[] t+ -> CtxTy src ts+ -> CtxTy src (t ': ts)+infixr 5 `CtxTyS`++appendCtxTy ::+ CtxTy src ts0 ->+ CtxTy src ts1 ->+ CtxTy src (ts0 ++ ts1)+appendCtxTy CtxTyZ c = c+appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'+ -- * Type 'Error_Term' data Error_Term src = Error_Term_unknown NameTe@@ -198,12 +223,12 @@ {- Error_Term_Con_Type (Con_Type src ss) -} {- Error_Term_Con_Kind (Con_Kind src) -} deriving (Eq, Show)-instance Inj_Error (Error_Type src) (Error_Term src) where- inj_Error = Error_Term_Type-instance Inj_Error (Error_Beta src) (Error_Term src) where- inj_Error = Error_Term_Beta-instance Inj_Error (Con_Kind src) (Error_Term src) where- inj_Error = Error_Term_Type . inj_Error+instance ErrorInj (Error_Type src) (Error_Term src) where+ errorInj = Error_Term_Type+instance ErrorInj (Error_Beta src) (Error_Term src) where+ errorInj = Error_Term_Beta+instance ErrorInj (Con_Kind src) (Error_Term src) where+ errorInj = Error_Term_Type . errorInj -- * Type 'SrcTe' -- | A 'Source' usable when using 'readTerm'.@@ -221,13 +246,13 @@ instance Source (SrcTe inp ss) where noSource = SrcTe_Less-instance Inj_Source (Span inp) (SrcTe inp ss) where- inj_Source = SrcTe_Input-instance Inj_Source (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where- inj_Source = SrcTe_AST_Term-instance Inj_Source (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where- inj_Source = SrcTe_AST_Type-instance Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss) where- inj_Source = SrcTe_Kind-instance Inj_Source (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where- inj_Source = SrcTe_Type+instance SourceInj (Span inp) (SrcTe inp ss) where+ sourceInj = SrcTe_Input+instance SourceInj (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where+ sourceInj = SrcTe_AST_Term+instance SourceInj (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where+ sourceInj = SrcTe_AST_Type+instance SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss) where+ sourceInj = SrcTe_Kind+instance SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where+ sourceInj = SrcTe_Type
Language/Symantic/Compiling/Term.hs view
@@ -52,8 +52,8 @@ expandFam (Term q t te) = Term (expandFam q) (expandFam t) te -- Type-instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where- typeOf t = typeOfTerm t `source` TermT t+instance SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where+ 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@@ -111,13 +111,13 @@ ) -- | Like 'TeSym', but 'CtxTe'-free--- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.+-- and using 'symInj' to be able to use 'Sym'@ s@ inside. teSym :: forall s ss ts t.- Inj_Sym ss s =>- (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->+ SymInj ss s =>+ (forall term. Sym s term => Sym_Lambda term => QualOf t => term (UnQualOf t)) -> TeSym ss ts t-teSym t = inj_Sym @s (TeSym $ const t)+teSym t = symInj @s (TeSym $ const t) -- ** Type family 'QualOf' -- | Qualification@@ -166,39 +166,39 @@ -- ** Type 'TermDef' -- | Convenient type alias for defining 'Term'.-type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t+type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t -- ** Type family 'Sym'-type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint+type family Sym (s::k) :: {-term-}(K.Type -> K.Type) -> Constraint -- ** Type family 'Syms'-type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where+type family Syms (ss::[K.Type]) (term::K.Type -> K.Type) :: Constraint where Syms '[] term = ()- Syms (s ': ss) term = (Sym s term, Syms ss term)+ Syms (Proxy s ': ss) term = (Sym s term, Syms ss term) --- ** Type 'Inj_Sym'--- | Convenient type synonym wrapping 'Inj_SymP'+-- ** Type 'SymInj'+-- | Convenient type synonym wrapping 'SymPInj' -- applied on the correct 'Index'.-type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s+type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s -- | Inject a given /symantic/ @s@ into a list of them, -- by returning a function which given a 'TeSym' on @s@ -- returns the same 'TeSym' on @ss@.-inj_Sym ::+symInj :: forall s ss ts t.- Inj_Sym ss s =>+ SymInj ss s => TeSym '[Proxy s] ts t -> TeSym ss ts t-inj_Sym = inj_SymP @(Index ss (Proxy s))+symInj = symInjP @(Index ss (Proxy s)) --- *** Class 'Inj_SymP'-class Inj_SymP p ss s where- inj_SymP :: TeSym '[Proxy s] ts t -> TeSym ss ts t-instance Inj_SymP Zero (Proxy s ': ss) (s::k) where- inj_SymP (TeSym te) = TeSym te-instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where- inj_SymP (te::TeSym '[Proxy s] ts t) =- case inj_SymP @p te :: TeSym ss ts t of+-- *** Class 'SymPInj'+class SymInjP p ss s where+ symInjP :: TeSym '[Proxy s] ts t -> TeSym ss ts t+instance SymInjP Zero (Proxy s ': ss) (s::k) where+ symInjP (TeSym te) = TeSym te+instance SymInjP p ss s => SymInjP (Succ p) (Proxy not_s ': ss) s where+ symInjP (te::TeSym '[Proxy s] ts t) =+ case symInjP @p te :: TeSym ss ts t of TeSym te' -> TeSym te' -- * Class 'Sym_Lambda'
Language/Symantic/Typing.hs view
@@ -4,6 +4,7 @@ , module Language.Symantic.Typing.Peano , module Language.Symantic.Typing.Kind , module Language.Symantic.Typing.Variable+ , module Language.Symantic.Typing.Module , module Language.Symantic.Typing.Type , module Language.Symantic.Typing.Grammar , module Language.Symantic.Typing.Document@@ -16,6 +17,7 @@ import Language.Symantic.Typing.Peano import Language.Symantic.Typing.Kind import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Module import Language.Symantic.Typing.Type import Language.Symantic.Typing.Grammar import Language.Symantic.Typing.Document
Language/Symantic/Typing/Document.hs view
@@ -4,9 +4,9 @@ import Data.Function (id) import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe) import Data.Semigroup (Semigroup(..)) import Data.Set (Set)-import Data.Text (Text) import Data.Typeable import qualified Data.List as L import qualified Data.Map.Strict as Map@@ -17,10 +17,11 @@ import Language.Symantic.Grammar import Language.Symantic.Typing.Kind import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Module import Language.Symantic.Typing.Type -- * Type 'Config_Doc_Type'-newtype Config_Doc_Type+data Config_Doc_Type = Config_Doc_Type { config_Doc_Type_vars_numbering :: Bool -- ^ Style of /type variables/:@@ -29,13 +30,17 @@ -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@) -- -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.+ , config_Doc_Type_imports :: Imports NameTy } -config_doc_type :: Config_Doc_Type-config_doc_type =+config_Doc_Type :: Config_Doc_Type+config_Doc_Type = Config_Doc_Type- { config_Doc_Type_vars_numbering = True }+ { config_Doc_Type_vars_numbering = True+ , config_Doc_Type_imports = mempty+ } +-- * Document 'Type' docType :: forall src vs t d. Semigroup d =>@@ -44,7 +49,7 @@ Config_Doc_Type -> Precedence -> Type src vs t -> d-docType conf pr ty =+docType conf@Config_Doc_Type{config_Doc_Type_imports=imps} pr ty = let (v2n, _) = var2Name conf mempty ty in go v2n (infixB SideL pr, SideL) ty where@@ -53,18 +58,23 @@ (Map IndexVar Name) -> -- names of variables (Infix, Side) -> Type src vs x -> d- go _v2n _po c- | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"- go _v2n _po (TyConst _src _vs c) = D.stringH $ show c+ -- Var go v2n _po (TyVar _src _n v) = let iv = indexVar v in case Map.lookup iv v2n of Nothing -> error "[BUG] docType: variable name missing" Just n -> D.textH n+ -- Const+ go _v2n _po (TyConst _src _vs c@Const{}) =+ (if isNameTyOp c then D.paren else id) $+ docConst imps c+ -- [] Const go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a) | Just HRefl <- proj_ConstKi @(K []) @[] f = "[" <> go v2n (infixB SideL 0, SideL) a <> "]"+ -- Infix Const go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)+ -- () => | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f = go v2n po b@@ -75,8 +85,6 @@ go v2n (op, SideR) b where d_op = D.yellower- unParen ('(':s) | ')':s' <- reverse s = reverse s'- unParen s = s prettyConst :: forall k c. Const src (c::k) -> d prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = d_op "," <> D.space@@ -89,41 +97,23 @@ -- NOTE: cannot use 'proj_ConstKi' here -- because (#~) has a polymorphic kind. = D.space <> d_op "~" <> D.space- | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space+ | otherwise = D.space <> d_op (docConst imps c) <> D.space+ -- TyApp go v2n po (TyApp _src f a) = let op = infixL 11 in (if needsParenInfix po op then D.paren else id) $ go v2n (op, SideL) f <> D.space <> go v2n (op, SideR) a+ -- TyFam go v2n po (TyFam _src _len fam args) = let op = infixL 11 in (if needsParenInfix po op then D.paren else id) $- D.stringH (show fam) <>+ docConst imps fam <> foldlTys (\t acc -> D.space <> go v2n (op, SideL) t <> acc ) args D.empty -docTypes ::- forall src vs ts d.- Semigroup d =>- D.Doc_Text d =>- D.Doc_Color d =>- Config_Doc_Type ->- Types src vs ts -> d-docTypes conf tys =- d_op (D.charH '[') <> go tys <> d_op (D.charH ']')- where- d_op = D.yellower- go :: forall xs. Types src vs xs -> d- go TypesZ = D.empty- go (TypesS t0 (TypesS t1 ts)) =- docType conf 10 t0 <>- d_op (D.charH ',') <> D.space <>- docType conf 10 t1 <>- go ts- go (TypesS t ts) = docType conf 10 t <> go ts- -- | Return a 'Map' associating a distinct 'Name' -- for all the variables of the given 'Type'. var2Name ::@@ -147,10 +137,8 @@ var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st --- ** Type 'Name'-type Name = Text-type NameHint = Name-type Names = Set Name+-- ** Type 'Names'+type Names = Set Name -- | Return given 'Name' renamed a bit to avoid -- conflicting with any given 'Names'.@@ -175,3 +163,141 @@ [ T.singleton n | n <- ['a'..'z'] ] <> [ T.pack (n:show i) | n <- ['a'..'z'] , i <- [1 :: Int ..] ]++-- * Document 'Types'+docTypes ::+ forall src vs ts d.+ Semigroup d =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ Config_Doc_Type ->+ Types src vs ts -> d+docTypes conf tys =+ d_op (D.charH '[') <> go tys <> d_op (D.charH ']')+ where+ d_op = D.yellower+ go :: forall xs. Types src vs xs -> d+ go TypesZ = D.empty+ go (TypesS t0 (TypesS t1 ts)) =+ docType conf 10 t0 <>+ d_op (D.charH ',') <> D.space <>+ docType conf 10 t1 <>+ go ts+ go (TypesS t ts) = docType conf 10 t <> go ts++-- * Document 'Const'+docConst :: D.Doc_Text d => Imports NameTy -> Const src c -> d+docConst imps c@Const{} =+ docMod docNameTy $+ maybe mn (`Mod` n) $+ revlookupImports f (m `Mod` n) imps+ where+ f = fixyOfFixity $ Fixity2 infixN5 `fromMaybe` fixityOf c+ mn@(m `Mod` n) = nameTyOf c++-- * Document 'NameTy'+docNameTy :: D.Doc_Text d => NameTy -> d+docNameTy (NameTy t) = D.textH t++-- * Document 'Mod'+docMod :: D.Doc_Text d => (a -> d) -> Mod a -> d+docMod a2d ([] `Mod` a) = a2d a+docMod a2d (m `Mod` a) = docPathMod m <> (D.charH '.') <> a2d a++-- * Document 'PathMod'+docPathMod :: D.Doc_Text d => PathMod -> d+docPathMod (p::PathMod) =+ D.catH $+ L.intersperse (D.charH '.') $+ (\(NameMod n) -> D.textH n) <$> p+++{-+docModules ::+ Source src =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ D.Doc_Decoration d =>+ ReadTe src ss =>+ Sym.Modules src ss -> d+docModules (Sym.Modules mods) =+ Map.foldrWithKey+ (\p m doc -> docModule p m <> doc)+ D.empty+ mods++docModule ::+ forall src ss d.+ Source src =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ D.Doc_Decoration d =>+ ReadTe src ss =>+ Sym.PathMod -> Sym.Module src ss -> d+docModule m Sym.Module+ { Sym.module_infix+ , Sym.module_prefix+ , Sym.module_postfix+ } =+ go docFixityInfix module_infix <>+ go docFixityPrefix module_prefix <>+ go docFixityPostfix module_postfix+ where+ go :: (fixy -> d) -> ModuleFixy src ss fixy -> d+ go docFixy =+ Map.foldrWithKey+ (\n Sym.Tokenizer+ { Sym.token_fixity+ , Sym.token_term = t+ } doc ->+ docPathTe m n <>+ docFixy token_fixity <>+ D.space <> D.bold (D.yellower "::") <> D.space <>+ docTokenTerm (t Sym.noSource) <>+ D.eol <> doc)+ D.empty++docTokenTerm ::+ forall src ss d.+ Source src =>+ D.Doc_Text d =>+ D.Doc_Color d =>+ ReadTe src ss =>+ Sym.Token_Term src ss -> d+docTokenTerm t =+ let n2t = name2typeInj @ss in+ case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of+ Left{} -> error "[BUG] docTokenTerm: readTerm failed"+ Right (Sym.TermVT te) ->+ Sym.docType Sym.config_doc_type+ { config_Doc_Type_vars_numbering = False+ } 0 $ Sym.typeOfTerm te++docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t+docFixityInfix = \case+ Sym.Infix Nothing 5 -> D.empty+ Sym.Infix a p ->+ let docAssoc = \case+ Sym.AssocL -> "l"+ Sym.AssocR -> "r"+ Sym.AssocB Sym.SideL -> "l"+ Sym.AssocB Sym.SideR -> "r" in+ D.magenta $ " infix" <> maybe D.empty docAssoc a <>+ D.space <> D.bold (D.bluer (D.int p))+docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t+docFixityPrefix p = D.magenta $ " prefix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))+docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t+docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))++docPathTe ::+ D.Doc_Text d =>+ D.Doc_Color d =>+ Sym.PathMod -> Sym.NameTe -> d+docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =+ D.catH $+ L.intersperse (D.charH '.') $+ ((\(Sym.NameMod m) -> D.textH m) <$> ms) <>+ [(if isOp n then id else D.yellower) $ D.text n]+ where+ isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c+-}
Language/Symantic/Typing/Grammar.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -5,32 +7,29 @@ import Control.Applicative (Applicative(..)) import Data.List (foldl1')+import Data.Proxy (Proxy(..))+import Data.Semigroup (Semigroup(..)) import Data.String (IsString(..))-import Data.Text (Text)+import Prelude hiding (any) import qualified Data.Char as Char+import qualified Data.Text as Text+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map -import Language.Symantic.Grammar+import Language.Symantic.Grammar as G+import Language.Symantic.Typing.Kind import Language.Symantic.Typing.Variable---- * Type 'NameTy'-newtype NameTy = NameTy Text- deriving (Eq, Ord, Show)-instance IsString NameTy where- fromString = NameTy . fromString---- ** Type 'NameConst'-type NameConst = NameTy---- ** Type 'NameFam'-type NameFam = NameTy+import Language.Symantic.Typing.List+import Language.Symantic.Typing.Module+import Language.Symantic.Typing.Type -- * Type 'AST_Type' -- | /Abstract Syntax Tree/ of 'Token_Type'.-type AST_Type src = BinTree (Token_Type src) -- (EToken src '[Proxy K.Type])+type AST_Type src = BinTree (Token_Type src) -- ** Type 'Token_Type' data Token_Type src- = Token_Type_Const (At src NameTy)+ = Token_Type_Const (At src (Mod NameTy)) | Token_Type_Var (At src NameVar) -- deriving (Eq, Show) instance Source src => Eq (Token_Type src) where@@ -47,6 +46,133 @@ showString "Token_Type_Var" . showChar ' ' . showsPrec 10 x +-- * Type 'ModulesTy'+type ModulesTy src = Map (Mod NameTy) (TypeTLen src)++-- ** Type 'TypeTLen'+-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.+--+-- Useful to build a 'ModulesTy' which can be used+-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.+newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)+instance Source src => Eq (TypeTLen src) where+ TypeTLen x == TypeTLen y = x LenZ == y LenZ+instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where+ showsPrec p (TypeTLen t) = showsPrec p $ t LenZ++-- ** Class 'ModulesTyInj'+-- | Derive a 'ModulesTy' from the given type-level list+-- of 'Proxy'-fied /type constants/.+class ModulesTyInj ts where+ modulesTyInj :: Source src => ModulesTy src+instance ModulesTyInj '[] where+ modulesTyInj = Map.empty+instance+ ( KindInjP (Ty_of_Type (K c))+ , K c ~ Type_of_Ty (Ty_of_Type (K c))+ , Constable c+ , ModulesTyInj ts+ ) => ModulesTyInj (Proxy c ': ts) where+ modulesTyInj =+ Map.insert+ (nameTyOf $ Proxy @c)+ (TypeTLen $ \len -> TypeT $ TyConst noSource len $+ constKiInj @(K c) @c $+ kindInjP @(Ty_of_Type (K c)) noSource) $+ modulesTyInj @ts+++-- * Class 'Gram_Mod'+class+ ( Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_Try g+ , Gram_App g+ , Gram_AltApp g+ , Gram_RegL g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Op g+ ) => Gram_Mod g where+ g_PathMod :: CF g PathMod+ g_PathMod = rule "PathMod" $+ infixrG+ (pure <$> g_NameMod)+ (op <$ char '.')+ where op = (<>)+ g_NameMod :: CF g NameMod+ g_NameMod = rule "NameMod" $+ NameMod . Text.pack <$> identG+ where+ identG = (:) <$> headG <*> many (cfOf tailG)+ headG = unicat $ Unicat Char.UppercaseLetter+ tailG :: Terminal g Char+ tailG =+ unicat Unicat_Letter <+>+ unicat Unicat_Number++deriving instance Gram_Mod g => Gram_Mod (CF g)+instance Gram_Mod EBNF+instance Gram_Mod RuleEBNF++-- * Class 'Gram_Type_Name'+class+ ( Gram_Terminal g+ , Gram_Rule g+ , Gram_Alt g+ , Gram_Try g+ , Gram_App g+ , Gram_AltApp g+ , Gram_RegL g+ , Gram_CF g+ , Gram_Comment g+ , Gram_Op g+ , Gram_Mod g+ ) => Gram_Type_Name g where+ g_ModNameTy :: CF g (Mod NameTy)+ g_ModNameTy = rule "ModNameTy" $+ lexeme $+ g_ModNameTyId <+>+ parens g_ModNameTyOp+ + g_ModNameTyId :: CF g (Mod NameTy)+ g_ModNameTyId = rule "ModNameTyId" $+ Mod+ <$> option [] (try $ g_PathMod <* char '.')+ <*> g_NameTyId+ g_NameTyId :: CF g NameTy+ g_NameTyId = rule "NameTyId" $+ NameTy . Text.pack <$> identTyG+ where+ identTyG = (:) <$> headTyG <*> many (cfOf tailTyG)+ headTyG = unicat $ Unicat Char.UppercaseLetter+ tailTyG :: Terminal g Char+ tailTyG =+ unicat Unicat_Letter <+>+ unicat Unicat_Number+ + g_ModNameTyOp :: CF g (Mod NameTy)+ g_ModNameTyOp = rule "ModNameTyOp" $+ Mod+ <$> option [] (try $ g_PathMod <* char '.')+ <*> g_NameTyOp+ g_NameTyOp :: CF g NameTy+ g_NameTyOp = rule "NameTyOp" $+ NameTy . Text.pack <$> many (cfOf okG)+ where+ okG :: Terminal g Char+ okG = choice (unicat <$>+ [ Unicat_Symbol+ , Unicat_Punctuation+ , Unicat_Mark+ ]) `but` koG+ koG = choice (char <$> ['(', ')', '`', '\'', '[', ']'])++deriving instance Gram_Type_Name g => Gram_Type_Name (CF g)+instance Gram_Type_Name EBNF+instance Gram_Type_Name RuleEBNF+ -- * Class 'Gram_Type' -- | Read an 'AST_Type' from a textual source. class@@ -60,27 +186,31 @@ , Gram_CF g , Gram_Comment g , Gram_Op g+ , Gram_Type_Name g+ , NameTyOf (->)+ , NameTyOf []+ , NameTyOf (,) ) => Gram_Type src g where g_type :: CF g (AST_Type src) 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 "->")- where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(->)")+ infixrG g_type_list (source $ op <$ symbol "->")+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(->)) -- 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+ source $ inside mk (symbol "[") (optional g_type) (symbol "]") (const <$> g_type_tuple2) where mk Nothing src = tok src mk (Just a) src = BinTree2 (tok src) a- tok src = BinTree0 $ Token_Type_Const $ At src "[]"+ tok src = BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @[] 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)- where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(,)")+ try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(,)) g_type_app :: CF g (AST_Type src) g_type_app = rule "type_app" $ foldl1' BinTree2 <$> some (g_type_atom)@@ -88,36 +218,49 @@ g_type_atom = rule "type_atom" $ try (parens g_type) <+> g_type_name_const <+>- g_type_name_var <+>- g_type_symbol+ g_type_name_var+ -- <+> g_type_symbol g_type_name_const :: CF g (AST_Type src) g_type_name_const = rule "type_name_const" $- 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])+ lexeme $ source $+ (\n src -> BinTree0 $ Token_Type_Const $ At src n)+ <$> g_ModNameTy+ -- <$> 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 $ 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+ source $ (mk <$>) $+ parens $ many $ cfOf $ choice g_ok `but` choice g_ko where- mk s src = BinTree0 $ Token_Type_Const $ At src (fromString $ "(" ++ s ++ ")")+ mk s src = BinTree0 $ Token_Type_Const $ At src $ Mod [] $ fromString $ "(" ++ s ++ ")" g_ok = unicat <$> [ Unicat_Symbol , Unicat_Punctuation , Unicat_Mark ] g_ko = char <$> ['(', ')', '`']+ -} deriving instance Gram_Type src g => Gram_Type src (CF g)-instance Gram_Source src EBNF => Gram_Type src EBNF-instance Gram_Source src RuleEBNF => Gram_Type src RuleEBNF+instance+ ( Gram_Source src EBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf []+ ) => Gram_Type src EBNF+instance+ ( Gram_Source src RuleEBNF+ , NameTyOf (->)+ , NameTyOf (,)+ , NameTyOf []+ ) => Gram_Type src RuleEBNF -- | List of the rules of 'Gram_Type'. gram_type :: Gram_Type () g => [CF g (AST_Type ())]@@ -130,5 +273,5 @@ , g_type_atom , g_type_name_const , g_type_name_var- , g_type_symbol+ -- , g_type_symbol ]
Language/Symantic/Typing/Kind.hs view
@@ -51,33 +51,33 @@ class KindOf (a::kt -> K.Type) where kindOf :: a t -> Kind (SourceOf (a t)) kt --- * Type 'Inj_Kind'+-- * Type 'Kind'Inj -- | Implicit 'Kind'. -- -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933> -- makes it fail to properly build an implicit 'Kind', -- this can however be worked around by having the class instances -- work on a data type 'Ty' instead of 'Data.K.Type',--- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.-class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where-instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k+-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'KindP'.Inj+class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k where+instance (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k -inj_Kind ::+kindInj :: forall k src. Source src =>- Inj_Kind k =>+ KindInj k => Kind src k-inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src)+kindInj = kindInjP @(Ty_of_Type k) (noSource @src) --- ** Type 'Inj_KindP'-class Inj_KindP k where- inj_KindP :: src -> Kind src (Type_of_Ty k)-instance Inj_KindP K.Constraint where- inj_KindP = KiConstraint-instance Inj_KindP Ty where- inj_KindP = KiType-instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where- inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src)+-- ** Type 'KindP'Inj+class KindInjP k where+ kindInjP :: src -> Kind src (Type_of_Ty k)+instance KindInjP K.Constraint where+ kindInjP = KiConstraint+instance KindInjP Ty where+ kindInjP = KiType+instance (KindInjP a, KindInjP b) => KindInjP (a -> b) where+ kindInjP src = KiFun src (kindInjP @a src) (kindInjP @b src) -- ** Type 'Ty' -- | FIXME: workaround to be removed when@@ -118,18 +118,18 @@ deriving (Eq, Show) when_EqKind- :: Inj_Error (Con_Kind src) err+ :: ErrorInj (Con_Kind src) err => Kind src x -> Kind src y -> ((x :~: y) -> Either err ret) -> Either err ret when_EqKind x y k = case x `eqKind` y of Just Refl -> k Refl- Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)+ Nothing -> Left $ errorInj $ Con_Kind_Eq (KindK x) (KindK y) when_KiFun ::- Inj_Error (Con_Kind src) err =>- Inj_Source (KindK src) src =>+ ErrorInj (Con_Kind src) err =>+ SourceInj (KindK src) src => Kind src x -> (forall a b. (x :~: (a -> b)) -> Kind src a ->@@ -138,5 +138,5 @@ Either err ret when_KiFun x k = case x of- KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)- _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)+ KiFun _src a b -> k Refl (a `withSource` KindK x) (b `withSource` KindK x)+ _ -> Left $ errorInj $ Con_Kind_Arrow (KindK x)
Language/Symantic/Typing/List.hs view
@@ -65,13 +65,13 @@ L '[] = 'Z L (x ': xs) = 'S (L xs) --- ** Class 'Inj_L'-class Inj_L (as::[k]) where- inj_L :: SNat (L as)-instance Inj_L '[] where- inj_L = SNatZ-instance Inj_L as => Inj_L (a ': as) where- inj_L = SNatS (inj_L @_ @as)+-- ** Class 'LInj'+class LInj (as::[k]) where+ lInj :: SNat (L as)+instance LInj '[] where+ lInj = SNatZ+instance LInj as => LInj (a ': as) where+ lInj = SNatS (lInj @_ @as) -} -- * Type 'Len'@@ -101,10 +101,10 @@ go i LenZ = i go i (LenS l) = go (1 + i) l --- ** Class 'Inj_Len'-class Inj_Len (vs::[k]) where- inj_Len :: Len vs-instance Inj_Len '[] where- inj_Len = LenZ-instance Inj_Len as => Inj_Len (a ': as) where- inj_Len = LenS inj_Len+-- ** Class 'LenInj'+class LenInj (vs::[k]) where+ lenInj :: Len vs+instance LenInj '[] where+ lenInj = LenZ+instance LenInj as => LenInj (a ': as) where+ lenInj = LenS lenInj
+ Language/Symantic/Typing/Module.hs view
@@ -0,0 +1,240 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.Symantic.Typing.Module where++import Data.Functor (Functor(..))+import Data.Maybe (fromMaybe)+import Data.String (IsString(..))+import Data.Semigroup (Semigroup(..))+import Data.Text (Text)+import Data.Typeable+import Data.Map.Strict (Map)+import qualified Data.Char as C+import qualified Data.List as L+import qualified Data.Kind as K+import qualified Data.Text as T+import qualified Data.Map.Strict as Map++import Language.Symantic.Grammar.Fixity++-- * Type 'NsT'+data NsT+ = NsTerm+ | NsType++-- * Type 'Name'+type Name = Text++-- * Type 'NameTy'+-- | 'Name' of a 'Type'.+newtype NameTy = NameTy Text+ deriving (Eq, Ord, Show)+instance IsString NameTy where+ fromString = NameTy . fromString++-- ** Type 'NameConst'+-- | 'Name' of a 'Const'.+type NameConst = NameTy++-- ** Type 'NameFam'+-- | 'Name' of a 'Fam'.+type NameFam = NameTy++-- ** Class 'NameOf'+class NameOf a where+ nameOf :: a -> Name++-- ** Class 'NameTyOf'+-- | Return the 'NameTy' of something.+class NameTyOf (c::kc) where+ nameTyOf :: proxy c -> Mod NameTy+ default nameTyOf :: Typeable c => proxy c -> Mod NameTy+ nameTyOf c = path (tyConModule repr) `Mod` fromString (tyConName repr)+ where+ repr = typeRepTyCon (typeRep c)+ path = fmap fromString . L.lines . fmap (\case '.' -> '\n'; x -> x)+ + isNameTyOp :: proxy c -> Bool+ default isNameTyOp :: Typeable c => proxy c -> Bool+ isNameTyOp c = let _m `Mod` NameTy n = nameTyOf c in isOp n+ where+ isOp = T.all $ \case+ '_' -> False+ '\'' -> False+ x -> case C.generalCategory x of+ C.NonSpacingMark -> True+ C.SpacingCombiningMark -> True+ C.EnclosingMark -> True+ C.ConnectorPunctuation -> True+ C.DashPunctuation -> True+ C.OpenPunctuation -> True+ C.ClosePunctuation -> True+ C.InitialQuote -> True+ C.FinalQuote -> True+ C.OtherPunctuation -> True+ C.MathSymbol -> True+ C.CurrencySymbol -> True+ C.ModifierSymbol -> True+ C.OtherSymbol -> True+ + C.UppercaseLetter -> False+ C.LowercaseLetter -> False+ C.TitlecaseLetter -> False+ C.ModifierLetter -> False+ C.OtherLetter -> False+ C.DecimalNumber -> False+ C.LetterNumber -> False+ C.OtherNumber -> False+ C.Space -> False+ C.LineSeparator -> False+ C.ParagraphSeparator -> False+ C.Control -> False+ C.Format -> False+ C.Surrogate -> False+ C.PrivateUse -> False+ C.NotAssigned -> False++-- * Type 'Mod'+-- | 'PathMod' of something.+data Mod a = Mod PathMod a+ deriving (Eq, Functor, Ord, Show)++-- ** Type 'PathMod'+-- | Path to a 'Module'.+type PathMod = [NameMod]++-- ** Type 'NameMod'+-- | 'Name' of 'Module'.+newtype NameMod = NameMod Name+ deriving (Eq, Ord, Show)+instance IsString NameMod where+ fromString = NameMod . fromString++-- * Type 'Imports'+-- | Map 'PathMod's of 'Name's.+newtype Imports name = Imports (Map PathMod (MapFixity (Map name PathMod)))+ deriving (Eq, Show)++instance Ord name => Semigroup (Imports name) where+ Imports x <> Imports y = Imports $ Map.unionWith (<>) x y+instance Ord name => Monoid (Imports name) where+ mempty = Imports mempty+ mappend = (<>)++lookupImports :: Ord name => Fixy p i q a -> Mod name -> Imports name -> Maybe PathMod+lookupImports f (m `Mod` n) (Imports is) =+ Map.lookup m is >>=+ Map.lookup n . getByFixity f++revlookupImports :: Ord name => Fixy p i q a -> Mod name -> Imports name -> Maybe PathMod+revlookupImports f (m `Mod` n) (Imports is) =+ (fst . fst <$>) $ Map.minViewWithKey $+ Map.filter (\i ->+ case Map.lookup n $ getByFixity f i of+ Just m' | m' == m -> True+ _ -> False+ ) is++-- ** Class 'ImportTypes'+class ImportTypes ts where+ importTypes :: PathMod -> Imports NameTy++instance ImportTypes '[] where+ importTypes _p = mempty+instance (NameTyOf t, FixityOf t, ImportTypes ts) => ImportTypes (Proxy t ': ts) where+ importTypes p = Imports (Map.singleton p byFixy) <> importTypes @ts p+ where+ t = Proxy @t+ f = Fixity2 infixN5 `fromMaybe` fixityOf t+ m `Mod` n = nameTyOf t+ byFixy :: MapFixity (Map NameTy PathMod)+ byFixy = case f of+ Fixity1 Prefix{} -> ByFixity{byPrefix = Map.singleton n m, byInfix =mempty, byPostfix=mempty}+ Fixity2{} -> ByFixity{byInfix = Map.singleton n m, byPrefix=mempty, byPostfix=mempty}+ Fixity1 Postfix{} -> ByFixity{byPostfix = Map.singleton n m, byPrefix=mempty, byInfix =mempty}++-- * Type 'Fixy'+data Fixy p i q a where+ FixyPrefix :: Fixy p i q p+ FixyInfix :: Fixy p i q i+ FixyPostfix :: Fixy p i q q+deriving instance Eq (Fixy p i q a)+deriving instance Show (Fixy p i q a)++fixyOfFixity :: Fixity -> Fixy a a a a+fixyOfFixity (Fixity1 Prefix{}) = FixyPrefix+fixyOfFixity (Fixity2 Infix{}) = FixyInfix+fixyOfFixity (Fixity1 Postfix{}) = FixyPostfix++-- ** Class 'FixityOf'+-- | Return the 'Fixity' of something.+class FixityOf (c::kc) where+ fixityOf :: proxy c -> Maybe Fixity+ fixityOf _c = Nothing+instance FixityOf (c::K.Type)+instance FixityOf (c::K.Constraint)++-- ** Type 'FixyA'+-- | Like 'Fixy', but when all choices have the same type.+newtype FixyA = FixyA (forall (a:: *). Fixy a a a a)+deriving instance Eq FixyA+deriving instance Show FixyA++-- ** Type 'WithFixity'+data WithFixity a+ = WithFixity a Fixity+ deriving (Eq, Functor, Show)+instance IsString a => IsString (WithFixity a) where+ fromString a = WithFixity (fromString a) (Fixity2 infixN5)++withInfix :: a -> Infix -> WithFixity a+withInfix a inf = a `WithFixity` Fixity2 inf+withInfixR :: a -> Precedence -> WithFixity a+withInfixR a p = a `WithFixity` Fixity2 (infixR p)+withInfixL :: a -> Precedence -> WithFixity a+withInfixL a p = a `WithFixity` Fixity2 (infixL p)+withInfixN :: a -> Precedence -> WithFixity a+withInfixN a p = a `WithFixity` Fixity2 (infixN p)+withInfixB :: a -> (Side, Precedence) -> WithFixity a+withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)+withPrefix :: a -> Precedence -> WithFixity a+withPrefix a p = a `WithFixity` Fixity1 (Prefix p)+withPostfix :: a -> Precedence -> WithFixity a+withPostfix a p = a `WithFixity` Fixity1 (Postfix p)++-- ** Type 'ByFixity'+-- | Fixity namespace.+data ByFixity p i q+ = ByFixity+ { byPrefix :: p+ , byInfix :: i+ , byPostfix :: q+ } deriving (Eq, Show)+instance (Semigroup p, Semigroup i, Semigroup q) => Semigroup (ByFixity p i q) where+ ByFixity px ix qx <> ByFixity py iy qy =+ ByFixity (px <> py) (ix <> iy) (qx <> qy)+instance (Monoid p, Monoid i, Monoid q) => Monoid (ByFixity p i q) where+ mempty = ByFixity mempty mempty mempty+ ByFixity px ix qx `mappend` ByFixity py iy qy =+ ByFixity (px `mappend` py) (ix `mappend` iy) (qx `mappend` qy)++getByFixity :: Fixy p i q a -> MapFixity b -> b+getByFixity FixyPrefix = byPrefix+getByFixity FixyInfix = byInfix+getByFixity FixyPostfix = byPostfix++selectByFixity :: Fixy p i q a -> ByFixity p i q -> a+selectByFixity FixyPrefix = byPrefix+selectByFixity FixyInfix = byInfix+selectByFixity FixyPostfix = byPostfix++-- *** Type 'MapFixity'+-- | Like 'ByFixity', but with the same type parameter.+type MapFixity a = ByFixity a a a++mapMapFixity :: (a -> b) -> MapFixity a -> MapFixity b+mapMapFixity f (ByFixity p i q) = ByFixity (f p) (f i) (f q)
Language/Symantic/Typing/Read.hs view
@@ -2,10 +2,9 @@ {-# LANGUAGE PolyKinds #-} module Language.Symantic.Typing.Read where -import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe) import Data.Typeable import qualified Data.Map.Strict as Map-import qualified Data.Text as Text import Language.Symantic.Grammar import Language.Symantic.Typing.List@@ -14,51 +13,56 @@ import Language.Symantic.Typing.Show () import Language.Symantic.Typing.Grammar import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Module -- | Read a 'Type' from an 'AST_Type', given its 'Vars'. readType ::- Inj_Source (KindK src) src =>- Inj_Source (TypeVT src) src =>- Inj_Source (AST_Type src) src =>- Name2Type src ->+ SourceInj (KindK src) src =>+ SourceInj (TypeVT src) src =>+ SourceInj (AST_Type src) src =>+ Imports NameTy ->+ ModulesTy src -> AST_Type src -> Either (Error_Type src) (TypeVT src)-readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do- TypeT ty <- readTyVars cs vs ast+readType is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do+ TypeT ty <- readTyVars is ms vs ast Right $ TypeVT ty -- | Read a 'Type' from an 'AST_Type', given its 'Vars'. readTyVars :: forall vs src.- Inj_Source (KindK src) src =>- Inj_Source (TypeVT src) src =>- Inj_Source (AST_Type src) src =>- Name2Type src ->+ SourceInj (KindK src) src =>+ SourceInj (TypeVT src) src =>+ SourceInj (AST_Type src) src =>+ Imports NameTy ->+ ModulesTy src -> Vars src vs -> AST_Type src -> Either (Error_Type src) (TypeT src vs)-readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =- readTyName cs (inj_Source ast) (lenVars vs) name-readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =+readTyVars is ms vs ast@(BinTree0 (Token_Type_Const (At _src name))) =+ readTyName is ms (sourceInj ast) (lenVars vs) name+readTyVars _is _ms vs ast@(BinTree0 (Token_Type_Var (At _src name))) = case lookupVars name vs of- Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v+ Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v Nothing -> error "[BUG] readTyVars: lookupVars failed"-readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do- TypeT ty_x <- readTyVars cs vs ast_x- TypeT ty_y <- readTyVars cs vs ast_y+readTyVars is ms vs ast@(ast_x `BinTree2` ast_y) = do+ TypeT ty_x <- readTyVars is ms vs ast_x+ TypeT ty_y <- readTyVars is ms vs ast_y when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b -> when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->- Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y+ Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y -- | Lookup a 'TyConst' or 'Type' synonym--- associated with given 'NameTy' in given 'Name2Type',+-- associated with given 'NameTy' in given 'ModulesTy', -- building it for a @vs@ of given 'Len'. readTyName :: Source src =>- Name2Type src -> src -> Len vs -> NameTy ->+ Imports NameTy ->+ ModulesTy src -> src -> Len vs -> Mod NameTy -> Either (Error_Type src) (TypeT src vs)-readTyName cs src len name =- case Map.lookup name cs of+readTyName is ms src len name@(m `Mod` n) =+ let m' = fromMaybe m $ lookupImports FixyInfix name is in+ case Map.lookup (m' `Mod` n) ms of Just (TypeTLen t) -> Right $ t len Nothing -> Left $ Error_Type_Constant_unknown $ At src name @@ -75,47 +79,12 @@ readVars evs (BinTree2 x y) = readVars (readVars evs x) y --- * Type 'Name2Type'-type Name2Type src = Map NameTy (TypeTLen src)---- ** Type 'TypeTLen'--- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.------ Useful to build a 'Name2Type' which can be used--- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.-newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)-instance Source src => Eq (TypeTLen src) where- TypeTLen x == TypeTLen y = x LenZ == y LenZ-instance Source src => Show (TypeTLen src) where- showsPrec p (TypeTLen t) = showsPrec p $ t LenZ---- ** Class 'Inj_Name2Type'--- | Derive a 'Name2Type' from the given type-level list--- of 'Proxy'-fied /type constants/.-class Inj_Name2Type cs where- inj_Name2Type :: Source src => Name2Type src-instance Inj_Name2Type '[] where- inj_Name2Type = Map.empty-instance- ( Inj_KindP (Ty_of_Type (K c))- , K c ~ Type_of_Ty (Ty_of_Type (K c))- , Constable c- , Inj_Name2Type cs- ) => Inj_Name2Type (Proxy c ': cs) where- inj_Name2Type =- Map.insert- (NameTy $ Text.pack $ show $ typeRep (Proxy @c))- (TypeTLen $ \len -> TypeT $ TyConst noSource len $- inj_ConstKi @(K c) @c $- inj_KindP @(Ty_of_Type (K c)) noSource) $- inj_Name2Type @cs- -- * Type 'Error_Type' data Error_Type src- = Error_Type_Constant_unknown (At src NameTy)+ = Error_Type_Constant_unknown (At src (Mod NameTy)) | Error_Type_Con_Kind (Con_Kind src) deriving (Eq, Show)-instance Inj_Error (Error_Type src) (Error_Type src) where- inj_Error = id-instance Inj_Error (Con_Kind src) (Error_Type src) where- inj_Error = Error_Type_Con_Kind+instance ErrorInj (Error_Type src) (Error_Type src) where+ errorInj = id+instance ErrorInj (Con_Kind src) (Error_Type src) where+ errorInj = Error_Type_Con_Kind
Language/Symantic/Typing/Show.hs view
@@ -2,29 +2,32 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} module Language.Symantic.Typing.Show where -import Data.Semigroup ((<>)) import qualified Data.Text.Lazy as TL import qualified Data.Text.Lazy.Builder as TLB import qualified Language.Symantic.Document as D import Language.Symantic.Grammar import Language.Symantic.Typing.Type+import Language.Symantic.Typing.Module import Language.Symantic.Typing.Document showType :: Config_Doc_Type -> Type src vs t -> String showType conf ty = TL.unpack $ TLB.toLazyText $ D.plain $ docType conf 0 ty showTypeS :: Config_Doc_Type -> Precedence -> Type src vs t -> ShowS-showTypeS conf pr ty s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty)+showTypeS conf pr ty = showString $ TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty) showTypes :: Config_Doc_Type -> Types src vs ts -> String showTypes conf tys = TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys) showTypesS :: Config_Doc_Type -> Types src vs ts -> ShowS-showTypesS conf tys s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)+showTypesS conf tys = showString $ TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys) +instance NameTyOf c => Show (Const src c) where+ showsPrec _p = showString . TL.unpack . TLB.toLazyText . D.plain . docConst mempty+ instance Source src => Show (Type src vs t) where- showsPrec = showTypeS config_doc_type+ showsPrec = showTypeS config_Doc_Type instance Source src => Show (TypeK src vs kt) where showsPrec p (TypeK t) = showsPrec p t instance Source src => Show (TypeVT src) where@@ -32,4 +35,4 @@ instance Source src => Show (TypeT src vs) where showsPrec p (TypeT t) = showsPrec p t instance Source src => Show (Types src vs ts) where- showsPrec _ = showTypesS config_doc_type+ showsPrec _ = showTypesS config_Doc_Type
Language/Symantic/Typing/Type.hs view
@@ -1,12 +1,8 @@ {-# language ConstraintKinds #-} {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE PartialTypeSignatures #-}-{-# LANGUAGE ImpredicativeTypes #-}-{-# LANGUAGE LiberalTypeSynonyms #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -32,6 +28,7 @@ import Language.Symantic.Typing.List import Language.Symantic.Typing.Kind import Language.Symantic.Typing.Variable+import Language.Symantic.Typing.Module -- * Type 'Type' data Type (src::K.Type) (vs::[K.Type]) (t::kt) where@@ -64,7 +61,7 @@ instance Source src => Eq (Type src vs t) where x == y = isJust $ eqType x y-instance Inj_Source (TypeVT src) src => TestEquality (Type src vs) where+instance SourceInj (TypeVT src) src => TestEquality (Type src vs) where testEquality = eqType type instance SourceOf (Type src vs t) = src@@ -79,8 +76,8 @@ setSource (TyVar _src n v) src = TyVar src n v 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+instance SourceInj (TypeVT src) src => KindOf (Type src vs) where+ kindOf t = kindOfType t `withSource` TypeVT t instance ConstsOf (Type src vs t) where constsOf (TyConst _src _len c) = Set.singleton $ ConstC c@@ -121,33 +118,31 @@ allocVarsR len (TyVar src n v) = TyVar src n $ allocVarsR len v allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as --- | Like 'TyConst', but using 'noSource' and 'inj_Const'.+-- | Like 'TyConst', but using 'noSource', 'lenInj' and 'constInj'. -- -- FIXME: remove @kc@ when GHC's #12933 is fixed. tyConst :: forall kc (c::kc) src vs. Source src =>- Inj_Len vs =>+ LenInj vs => Constable c =>- Inj_KindP (Ty_of_Type kc) =>+ KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Type src vs c-tyConst = TyConst noSource inj_Len inj_Const+tyConst = TyConst noSource lenInj constInj -- NOTE: The forall brings @c@ first in the type variables, -- which is convenient to use @TypeApplications@. --- | Like 'TyConst', but using 'noSource' and 'inj_Const'.--- --- FIXME: remove @kc@ when GHC's #12933 is fixed.+-- | Like 'tyConst', but not using 'lenInj'. tyConstLen :: forall kc (c::kc) src vs. Source src => Constable c =>- Inj_KindP (Ty_of_Type kc) =>+ KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Len vs -> Type src vs c-tyConstLen len = TyConst noSource len inj_Const+tyConstLen len = TyConst noSource len constInj -- | Like 'TyApp', but using 'noSource'. tyApp ::@@ -172,13 +167,13 @@ tyFam :: forall kc (c::kc) as vs src. Source src =>- Inj_Len vs =>+ LenInj vs => Constable c =>- Inj_KindP (Ty_of_Type kc) =>+ KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Types src vs as -> Type src vs (Fam c as)-tyFam = TyFam noSource inj_Len (inj_Const @c)+tyFam = TyFam noSource lenInj (constInj @c) -- | Qualify a 'Type'. tyQual ::@@ -223,15 +218,13 @@ -- * Type 'Const' -- | /Type constant/. data Const src (c::kc) where- Const :: Constable c- => Kind src kc- -> Const src (c::kc)+ Const :: Constable c => Kind src kc -> Const src (c::kc) type instance SourceOf (Const src c) = src 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+instance SourceInj (ConstC src) src => KindOf (Const src) where+ kindOf c@(Const kc) = kc `withSource` ConstC c kindOfConst :: Const src (t::kt) -> Kind src kt kindOfConst (Const kc) = kc@@ -240,12 +233,14 @@ class ( Typeable c , FixityOf c+ , NameTyOf c , ClassInstancesFor c , TypeInstancesFor c ) => Constable c instance ( Typeable c , FixityOf c+ , NameTyOf c , ClassInstancesFor c , TypeInstancesFor c ) => Constable c@@ -255,18 +250,6 @@ class ConstsOf a where constsOf :: a -> Set (ConstC (SourceOf a)) --- ** Class 'FixityOf'--- | Return the 'Fixity' of something.-class FixityOf (c::kc) where- fixityOf :: proxy c -> Maybe Fixity- fixityOf _c = Nothing-instance FixityOf (c::K.Type)-instance FixityOf (c::K.Constraint)---- Show-instance Show (Const src c) where- showsPrec p c@Const{} = showsPrec p $ typeRep c- -- ** Type 'ConstC' data ConstC src = forall c. ConstC (Const src c)@@ -307,7 +290,7 @@ -- the argument of that function. unTyFun :: forall t src tys.- Inj_Source (TypeVT src) src =>+ SourceInj (TypeVT src) src => Constable (->) => Type src tys t -> Maybe ( Type src tys (FunArg t)@@ -320,7 +303,7 @@ , 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@@ -332,17 +315,20 @@ -- ** Type @(#>)@ -- | /Type constant/ to qualify a 'Type'. newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)+instance NameTyOf (#>) where+ nameTyOf _c = [] `Mod` "=>" instance FixityOf (#>) where fixityOf _c = Just $ Fixity2 $ infixR 0 instance ClassInstancesFor (#>) instance TypeInstancesFor (#>) +-- | Qualify a 'Type'. (#>) :: Source src =>- Type src vs a ->- Type src vs b ->- Type src vs (a #> b)-(#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b+ Type src vs q ->+ Type src vs t ->+ Type src vs (q #> t)+(#>) q t = (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t infixr 0 #> -- NOTE: should actually be (-1) -- to compose well with @infixr 0 (->)@@@ -352,6 +338,8 @@ -- | 'K.Constraint' union. class (x, y) => x # y instance (x, y) => x # y+instance NameTyOf (#) where+ nameTyOf _c = [] `Mod` "," instance FixityOf (#) where fixityOf _c = Just $ Fixity2 $ infixB SideL 0 instance ClassInstancesFor (#) where@@ -363,6 +351,7 @@ proveConstraintFor _c _q = Nothing instance TypeInstancesFor (#) +-- | Unify two 'K.Constraint's. (#) :: Source src => Type src vs qx ->@@ -371,18 +360,10 @@ (#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b infixr 2 # -noConstraint ::- Source src =>- Inj_Len vs =>- Type src vs (()::K.Constraint)-noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) inj_Len--noConstraintLen ::- Source src =>- Len vs ->- Type src vs (()::K.Constraint)-noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)-+-- ** Type @(() :: @'K.Constraint'@)@+instance NameTyOf (()::K.Constraint) where+ nameTyOf _c = [] `Mod` "()"+-- instance FixityOf (()::Constraint) instance ClassInstancesFor (()::K.Constraint) where proveConstraintFor _c q | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q@@ -390,14 +371,25 @@ proveConstraintFor _c _q = Nothing instance TypeInstancesFor (()::K.Constraint) +-- | Like 'noConstraintLen', but using 'lenInj'.+noConstraint :: Source src => LenInj vs => Type src vs (()::K.Constraint)+noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) lenInj++-- | Empty 'K.Constraint'.+noConstraintLen :: Source src => Len vs -> Type src vs (()::K.Constraint)+noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)+ -- ** Class @(#~)@ -- | /Type equality/ 'K.Constraint'. class (x ~ y) => x #~ y instance (x ~ y) => x #~ y+instance NameTyOf (#~) where+ nameTyOf _c = [] `Mod` "~"+ isNameTyOp _c = True instance FixityOf (#~) where fixityOf _ = Just $ Fixity2 $ infixB SideL 0 instance- ( Inj_Kind k+ ( KindInj k , Typeable k ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where proveConstraintFor _c (TyApp _ (TyApp _ c a) b)@@ -407,27 +399,18 @@ proveConstraintFor _c _q = Nothing instance TypeInstancesFor (#~) +-- | Constraint two 'Type's to be equal. (#~) :: forall k a b src vs. Source src => Typeable k =>- Inj_Kind k =>+ KindInj k => Type src vs (a :: k) -> Type src vs (b :: k) -> Type src vs (a #~ b) (#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b infixr 2 #~ -{--const_EqTy ::- forall k src.- Source src =>- Typeable k =>- Inj_Kind k =>- Const src ((#~)::k -> k -> K.Constraint)-const_EqTy = inj_Const @(#~)--}- -- | /Type equality/. eqType :: Source src =>@@ -525,22 +508,22 @@ where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q) -- ** Injection-inj_Const ::+constInj :: forall c src. Source src => Constable c =>- Inj_KindP (Ty_of_Type (K c)) =>+ KindInjP (Ty_of_Type (K c)) => Type_of_Ty (Ty_of_Type (K c)) ~ K c => Const src c-inj_Const = Const $ inj_KindP @(Ty_of_Type (K c)) noSource+constInj = Const $ kindInjP @(Ty_of_Type (K c)) noSource -inj_ConstKi ::+constKiInj :: forall kc c src. Source src => Constable c => Kind src kc -> Const src (c::kc)-inj_ConstKi = Const+constKiInj = Const -- ** Projection {- XXX: not working because of GHC's #12933@@ -548,11 +531,11 @@ forall c u src. Constable c => (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>- Inj_Kind (K c) =>+ KindInj (K c) => Const src u -> Maybe (c :~~: u) proj_ConstKi (Const ku) = do- Refl <- eqKind ku $ inj_Kind @(K c) @()+ Refl <- eqKind ku $ kindInj @(K c) @() Refl :: u:~:c <- eqT Just HRefl -}@@ -581,11 +564,11 @@ forall kc (c::kc) u src. Typeable c => (kc ~ Type_of_Ty (Ty_of_Type kc)) =>- Inj_KindP (Ty_of_Type kc) =>+ KindInjP (Ty_of_Type kc) => Const src u -> Maybe (c :~~: u) proj_ConstKi (Const ku) = do- Refl <- eqKind ku $ inj_KindP @(Ty_of_Type kc) ()+ Refl <- eqKind ku $ kindInjP @(Ty_of_Type kc) () Refl :: u:~:c <- eqT Just HRefl @@ -594,7 +577,7 @@ forall kc (c::kc) u src vs. Typeable c => (kc ~ Type_of_Ty (Ty_of_Type kc)) =>- Inj_KindP (Ty_of_Type kc) =>+ KindInjP (Ty_of_Type kc) => Type src vs u -> Maybe (c :~~: u) proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c@@ -666,11 +649,11 @@ (Nothing, Nothing) -> case q0' `ordType` q1' of LT ->- let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in+ let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ constInj @(#)) q0') q1' in TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t GT ->- let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in+ let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ constInj @(#)) q1') q0' in TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t -- q => t go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
Language/Symantic/Typing/Unify.hs view
@@ -130,10 +130,10 @@ deriving instance Source src => Eq (Error_Unify src) deriving instance Source src => Show (Error_Unify src) -instance Inj_Error (Error_Unify src) (Error_Unify src) where- inj_Error = id-instance Inj_Error (Con_Kind src) (Error_Unify src) where- inj_Error = Error_Unify_Kind+instance ErrorInj (Error_Unify src) (Error_Unify src) where+ errorInj = id+instance ErrorInj (Con_Kind src) (Error_Unify src) where+ errorInj = Error_Unify_Kind -- | Return the left spine of a 'Type': -- the root 'Type' and its 'Type' parameters,@@ -141,7 +141,7 @@ spineTy :: forall src vs t. Source src =>- Inj_Source (TypeVT src) src =>+ SourceInj (TypeVT src) src => Type src vs t -> (TypeT src vs, [TypeT src vs]) spineTy typ = go [] typ@@ -150,8 +150,8 @@ 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@@ -173,8 +173,8 @@ -- | Return the /most general unification/ of two 'Type's, when it exists. unifyType :: forall ki (x::ki) (y::ki) vs src.- Inj_Source (TypeVT src) src =>- Inj_Error (Con_Kind src) (Error_Unify src) =>+ SourceInj (TypeVT src) src =>+ ErrorInj (Con_Kind src) (Error_Unify src) => Subst src vs -> Type src vs (x::ki) -> Type src vs (y::ki) ->
Language/Symantic/Typing/Variable.hs view
@@ -34,8 +34,8 @@ type instance SourceOf (Var src vs t) = src 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+instance SourceInj (EVar src vs) src => KindOf (Var src vs) where+ 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)@@ -49,10 +49,10 @@ varZ :: forall src vs kv (v::kv). Source src =>- Inj_Len vs =>- Inj_Kind kv =>+ LenInj vs =>+ KindInj kv => Var src (Proxy v ': vs) v-varZ = VarZ inj_Kind inj_Len+varZ = VarZ kindInj lenInj -- | Return the 'Kind' of given 'Var'. kindOfVar :: Var src vs (v::kv) -> Kind src kv
symantic.cabal view
@@ -3,216 +3,10 @@ build-type: Simple cabal-version: >= 1.24 category: Language-description:- __Description__- .- This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting- a custom DSL (Domain-Specific Language) expressing- a subset of GHC's Haskell type system:- .- * /first class functions/ (aka. /lambdas/),- * chosen /monomorphic types/ (like 'Bool' or 'Maybe'),- * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@),- * chosen /type class instances/,- * chosen /type family instances/,- * and chosen /type constraints/;- .- where "chosen X" means declared in Haskell- and selected when composing the DSL.- .- In particular, this library is currently not able to:- .- * do /type inferencing/ for the argument of /lambdas/- (they must all be explicitely annotated, aka. /Church-style/),- * do /pattern matching/ (aka. /case/) (but /Church-encoding/ functions are often enough),- * do /rank-N polymorphic types/ (aka. /non-prenex forall/, like @(forall s. ST s a) -> a@).- .- And by itself, the DSL is only able to define new terms to be interpreted,- no new types, or other type-level structures.- .- __Warning__- .- Please be aware that despite its using of powerful ideas from clever people,- this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY.- Meaning that it IS NOT heavily tested and documented,- DOES NOT have a strong commitment to preserving backward compatibility,- MAY FAIL to comply with the <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,- and CAN die without notice.- You've been warned.- .- __Use cases__- .- The main goal of this library is to enable the runtime interpretation of terms,- type-checked according to some types defined at composing-time (ie. GHC's compile-time).- .- Using a DSL enables to limit expressiveness in order to ease analysis.- Here the idea is that the more complex logic shall remain written in Haskell,- and then this library used to project an interface into a DSL- (using GHC's Haskell as a FFI (Foreign Function Interface)).- This in order to give runtime users the flexibility- to write programs not requiring a full-blown Haskell compiler,- yet enabling enough flexibility to let them express complex needs- with a reasonably advanced type-safe way- and a controlled environment of primitives.- .- Typical use cases:- .- * Enabling runtime users to enter some Haskell-like expressions- (maybe with a more convenient syntax wrt. the domain problem)- without using at runtime all the heavy machinery and ecosystem of GHC- (eg. by using <https://hackage.haskell.org/package/hint hint>),- but still leaning on primitive functions coded in GHC's Haskell.- * Limiting those expressions to be built from well-controlled expressions only.- * Run some analyzes/optimizations on those well-controlled expressions.- .- __Usage__- .- Please pick in <https://hackage.haskell.org/package/symantic-lib symantic-lib>- a few specific @Lib/*.hs@ files near what you want to do- and the corresponding @Lib\/*/Test.hs@ file,- if any in the <git://git.autogeree.net/symantic Git repository>,- to learn by examples how to use this library.- .- Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser- (see @Grammar/Megaparsec.hs@) and a default grammar somehow sticking to Haskell's,- but staying context-free (so in particular: insensitive to the indentation),- and supporting prefix and postfix operators.- This grammar — itself written as a symantic embedded DSL- with <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —- can be reused to build other ones, is not bound to a specific parser,- and can produce its own EBNF rendition.- .- __Acknowledgements__- .- This library would probably be much worse than it is- without the following seminal works:- .- * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.- * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.- .- __Main ideas__- .- * __Symantic DSL__.- Terms are encoded in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way (aka. the /symantic/ way)- which leverages the /type class/ system of Haskell — instead of using /data types/ — to form an embedded DSL.- More specifically, a /class/ encodes the /syntax/ of terms (eg. 'Sym_Bool')- and its /class instances/ on a dedicated type encodes their /semantics/- (eg. @(Sym_Bool Eval)@ interprets a term as a value of its type- in the host language ('Bool' in Haskell here),- or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.).- - DSL are then composed/extended by selecting those symantic /classes/- (and in an embedded DSL those could even be automatically inferred,- when @NoMonomorphismRestriction@ is on).- Otherwise, when using symantics for a non-embedded DSL- — the whole point of this library — the /classes/ composing the DSL- are selected manually at GHC's compile-time,- through the /type-level list/ @ss@ given to 'readTerm'.- - Moreover, those symantic @term@s are parameterized by the type of the value they encode,- in order to get the same type safety as with plain Haskell values.- Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@- instead of just @(* -> Constraint)@.- - Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,- meaning that they directly reuse GHC's internal machinery- to abstract or instantiate variables,- which I think is by far the most efficient and simplest way of doing it- (no (generalized or not) DeBruijn encoding- like in <https://hackage.haskell.org/package/bound bound>'s @Monad@s).- - * __Singleton for any type__.- To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/- for any Haskell /type index/ @t@ of any kind,- which is made possible with the dependant Haskell extensions:- especially @TypeFamilies@, @GADTs@ and @TypeInType@.- - * __Type constants using 'Typeable'__.- /Type constant/ could be introduced by indexing them amongst a /type-level list/,- but since they are /monomorphic types/, using 'Typeable' simplifies- the machinery, and is likely more space/time efficient, including at GHC-compile-time.- - * __Type variables using a type-level list__.- Handling /type variables/ is done by indexing them amongst a @vs@ /type-level list/,- where each /type variable/ is wrapped inside a @Proxy@ to handle different kinds.- Performing a substitution (in 'substVar') preserves the /type index/ @t@,- which is key for preserving any associated 'Term'.- Unifying /type variables/ is done with 'unsafeCoerce' (in 'unifyType'),- which I think is necessary and likely safe.- - -- NOTE: no longer used.- -- * __Extensible data type__.- -- To inject a type into a /type-level list/- -- or project a /type-level list/ onto a type,- -- to compose an /extensible data type/- -- (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,- -- that a parser can build and then give to 'compile').- -- This type-level programming requires @UndecidableInstances@,- -- but not @OverlappingInstances@.- -- - -- There is a similarity with- -- <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>- -- (see for instance <https://hackage.haskell.org/package/compdata compdata>- -- or <https://hackage.haskell.org/package/syntactic syntactic>).- -- Those also enable to compose a DSL using some machinery- -- based upon (co)free(r) (co)monads and (cata|ana)morphisms.- -- Which library fits best your problem domain and brain is for you to judge :)- -- On that topic, see also:- -- <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.- --- -- Here, I just came up using /type-level lists/ by hacking- -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.- .- __Main extensions__- .- * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.- * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,- or reifying any 'Constraint' as an explicit dictionary 'Dict',- or defining /type synonym/ of /type classes/,- or merging /type constraints/.- * @DataKinds@ for type-level data structures (eg. /type-level lists/).- * @DefaultSignatures@ for providing identity transformations of terms,- and thus avoid boilerplate code when a transformation- does not need to alter all semantics.- Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.- * @GADTs@ for knowing types by pattern-matching terms,- or building terms by using type classes.- * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.- * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s.- * @TypeApplications@ for having a more concise syntax- to build 'Type' (eg. 'tyConst'@ @\@Bool).- * @TypeFamilies@ for type-level programming.- * @TypeInType@ (introduced in GHC 8.0.1)- for 'Type' to also bind a kind equality for the type @t@ it encodes.- Which makes the /type application/ ('TyApp')- give us an /arrow kind/ for the Haskell /type constructor/- it applies an Haskell type to, releaving me from tricky workarounds.- * @UndecidableInstances@ for type-level programming that may never terminate.- .- __Bugs__- .- There are some of them hidding in there,- and the whole thing is far from being perfect…- Your comments, problem reports, or questions, are welcome!- You have my email address, so… just send me some emails :]- .- __To do__- .- * Study to which point /type inferencing/ is doable,- now that 'Type' is powerful enough to contain 'TyVar's.- * Study to which point error messages can be improved,- now that there is a 'Source' carried through all 'Kind's or 'Type's,- it should enable some nice reports.- Still, a lot of work and testing remain to be done,- and likely some ideas to find too…- * Add more terms in <https://hackage.haskell.org/package/symantic-lib symantic-lib>.- * Add more transformations.- * Study how to integrate types into the module system.- * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.- * Study how to support /rank-N polymorphic types/,- special cases can likely use the /boxed polymorphism/ workaround,- but even if GHC were supporting /impredicative types/,- I'm currently clueless about how to do this.+description: This is an experimental library for composing, parsing,+ typing, compiling, transforming and interpreting+ a custom DSL (Domain-Specific Language)+ expressing a subset of GHC's Haskell type system. extra-source-files: extra-tmp-files: -- homepage: @@ -226,7 +20,7 @@ -- PVP: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change-version: 6.0.0.20170623+version: 6.2.0.20170702 Source-Repository head location: git://git.autogeree.net/symantic@@ -272,6 +66,7 @@ Language.Symantic.Typing.Grammar Language.Symantic.Typing.Kind Language.Symantic.Typing.List+ Language.Symantic.Typing.Module Language.Symantic.Typing.Peano Language.Symantic.Typing.Read Language.Symantic.Typing.Show