symantic 6.2.0.20170702 → 6.3.0.20170703
raw patch · 6 files changed
+96/−115 lines, 6 filesdep −ghc-prim
Dependencies removed: ghc-prim
Files
- Language/Symantic/Compiling/Grammar.hs +12/−12
- Language/Symantic/Compiling/Read.hs +8/−14
- Language/Symantic/Typing/Grammar.hs +63/−42
- Language/Symantic/Typing/Read.hs +10/−43
- Language/Symantic/Typing/Type.hs +2/−2
- symantic.cabal +1/−2
Language/Symantic/Compiling/Grammar.hs view
@@ -119,15 +119,15 @@ deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g) instance ( Gram_Source src EBNF- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Term_Type src EBNF instance ( Gram_Source src RuleEBNF- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Term_Type src RuleEBNF -- ** Type 'Error_Term_Gram'@@ -316,16 +316,16 @@ instance ( Gram_Term_Atoms src ss EBNF , Gram_Source src EBNF- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Term src ss EBNF instance ( Gram_Term_Atoms src ss RuleEBNF , Gram_Source src RuleEBNF- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Term src ss RuleEBNF -- ** Class 'Gram_Term_Atoms'
Language/Symantic/Compiling/Read.hs view
@@ -19,15 +19,13 @@ SourceInj (KindK src) src => SourceInj (AST_Type src) src => Constable (->) =>- 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 impsTy modsTy ctxTy ast = do+readTerm ctxTy ast = do ts <- go ctxTy `traverse` ast errorInj `left` betaTerms ts where@@ -41,12 +39,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 <- errorInj `left` readType impsTy modsTy ast_ty_arg+ TypeVT ty_arg <- errorInj `left` readType 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 impsTy modsTy (CtxTyS name_arg ta ts) ast_body+ TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name_arg ta ts) ast_body let (qa', qr') = appendVars qa qr let (ta', tr') = appendVars ta tr Right $@@ -65,11 +63,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 impsTy modsTy ts ast_arg+ TermVT (Term qa ta (TeSym arg)) <- readTerm ts ast_arg case lenVars ta of LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta) LenZ -> do- TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body+ TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name ta ts) ast_body let (qa', qr') = appendVars qa qr let tr' = allocVarsL (lenVars ta) tr Right $@@ -143,8 +141,6 @@ SourceInj (AST_Type src) src => Constable (->) => f (NameTe, TermT src ss '[] '[]) ->- Imports NameTy ->- ModulesTy src -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[]) readTermWithCtx env =@@ -167,8 +163,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 impsTy modsTy ctxTy ast = do- TermVT (Term q t (TeSym te)) <- readTe impsTy modsTy (CtxTyS n (qn #> tn) ctxTy) ast+readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe ctxTy ast = do+ TermVT (Term q t (TeSym te)) <- readTe (CtxTyS n (qn #> tn) ctxTy) ast case proveConstraint qn of Nothing -> Left $ Error_Term_proofless $ TypeVT qn Just Dict ->@@ -184,11 +180,9 @@ SourceInj (KindK src) src => SourceInj (AST_Type src) src => Constable (->) =>- Imports NameTy ->- ModulesTy src -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[])-readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ+readTermWithCtxClose readTe = readTe CtxTyZ -- * Type 'CtxTy' -- | /Typing context/
Language/Symantic/Typing/Grammar.hs view
@@ -7,14 +7,14 @@ import Control.Applicative (Applicative(..)) import Data.List (foldl1')-import Data.Proxy (Proxy(..))+import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe) import Data.Semigroup (Semigroup(..)) import Data.String (IsString(..)) 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 qualified Data.Text as Text import Language.Symantic.Grammar as G import Language.Symantic.Typing.Kind@@ -29,15 +29,15 @@ -- ** Type 'Token_Type' data Token_Type src- = Token_Type_Const (At src (Mod NameTy))+ = Token_Type_Const (TypeTLen src) | Token_Type_Var (At src NameVar) -- deriving (Eq, Show) instance Source src => Eq (Token_Type src) where- Token_Type_Const (At _ x) == Token_Type_Const (At _ y) = x == y- Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y+ Token_Type_Const (TypeTLen x) == Token_Type_Const (TypeTLen y) = x LenZ == y LenZ+ Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y _ == _ = False-instance Source src => Show (Token_Type src) where- showsPrec p (Token_Type_Const (At _ x)) =+instance (Source src, Show (TypeT src '[])) => Show (Token_Type src) where+ showsPrec p (Token_Type_Const x) = showParen (p >= 10) $ showString "Token_Type_Const" . showChar ' ' . showsPrec 10 x@@ -60,6 +60,20 @@ instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where showsPrec p (TypeTLen t) = showsPrec p $ t LenZ +typeTLen ::+ forall c src.+ Source src =>+ Constable c =>+ KindInjP (Ty_of_Type (K c)) =>+ K c ~ Type_of_Ty (Ty_of_Type (K c)) =>+ src ->+ TypeTLen src+typeTLen src =+ TypeTLen $ \len -> TypeT $+ TyConst src len $+ constKiInj @(K c) @c $+ kindInjP @(Ty_of_Type (K c)) noSource+ -- ** Class 'ModulesTyInj' -- | Derive a 'ModulesTy' from the given type-level list -- of 'Proxy'-fied /type constants/.@@ -76,9 +90,7 @@ modulesTyInj = Map.insert (nameTyOf $ Proxy @c)- (TypeTLen $ \len -> TypeT $ TyConst noSource len $- constKiInj @(K c) @c $- kindInjP @(Ty_of_Type (K c)) noSource) $+ (typeTLen @c noSource) $ modulesTyInj @ts @@ -187,16 +199,18 @@ , Gram_Comment g , Gram_Op g , Gram_Type_Name g- , NameTyOf (->)- , NameTyOf []- , NameTyOf (,)+ , Gram_Error (Error_Type src) g+ , Gram_State (Imports NameTy, ModulesTy src) g+ , Constable (->)+ , Constable []+ , Constable (,) ) => 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 (source $ op <$ symbol "->")- where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(->))+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(->) src) -- TODO: maybe not harcoding g_type_list and g_type_tuple2 g_type_list :: CF g (AST_Type src) g_type_list = rule "type_list" $@@ -206,11 +220,11 @@ where mk Nothing src = tok src mk (Just a) src = BinTree2 (tok src) a- tok src = BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @[]+ tok = BinTree0 . Token_Type_Const . typeTLen @[] g_type_tuple2 :: CF g (AST_Type src) g_type_tuple2 = rule "type_tuple2" $ try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)- where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(,))+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(,) src) g_type_app :: CF g (AST_Type src) g_type_app = rule "type_app" $ foldl1' BinTree2 <$> some (g_type_atom)@@ -219,48 +233,55 @@ try (parens g_type) <+> g_type_name_const <+> 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 $ source $- (\n src -> BinTree0 $ Token_Type_Const $ At src n)+ lexeme $ catch $ source $ getBefore $+ (\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy 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 $ 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" $- source $ (mk <$>) $- parens $ many $ cfOf $ choice g_ok `but` choice g_ko- where- 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- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Type src EBNF instance ( Gram_Source src RuleEBNF- , NameTyOf (->)- , NameTyOf (,)- , NameTyOf []+ , Constable (->)+ , Constable (,)+ , Constable [] ) => Gram_Type src RuleEBNF++-- | Lookup a 'TyConst' or 'Type' synonym+-- associated with given 'NameTy' in given 'ModulesTy',+-- building it for a @vs@ of given 'Len'.+readTyName ::+ Source src =>+ Imports NameTy ->+ ModulesTy src -> src -> Mod NameTy ->+ Either (Error_Type src) (TypeTLen src)+readTyName is ms src name@(m `Mod` n) =+ let m' = fromMaybe m $ lookupImports FixyInfix name is in+ case Map.lookup (m' `Mod` n) ms of+ Just t -> Right t+ Nothing -> Left $ Error_Type_Constant_unknown $ At src name++-- * Type 'Error_Type'+data Error_Type src+ = Error_Type_Constant_unknown (At src (Mod NameTy))+ | Error_Type_Con_Kind (Con_Kind src)+ deriving (Eq, Show)+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 -- | List of the rules of 'Gram_Type'. gram_type :: Gram_Type () g => [CF g (AST_Type ())]
Language/Symantic/Typing/Read.hs view
@@ -2,30 +2,22 @@ {-# LANGUAGE PolyKinds #-} module Language.Symantic.Typing.Read where -import Data.Maybe (fromMaybe)-import Data.Typeable-import qualified Data.Map.Strict as Map- import Language.Symantic.Grammar-import Language.Symantic.Typing.List import Language.Symantic.Typing.Kind import Language.Symantic.Typing.Type 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 :: 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 is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do- TypeT ty <- readTyVars is ms vs ast+readType ast | EVars vs <- readVars (EVars VarsZ) ast = do+ TypeT ty <- readTyVars vs ast Right $ TypeVT ty -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.@@ -34,38 +26,23 @@ 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 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))) =+readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =+ Right $ t (lenVars vs)+ -- readTyName is ms (sourceInj ast) (lenVars vs) name+readTyVars vs (BinTree0 (Token_Type_Var (At src name))) = case lookupVars name vs of- Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v+ Just (EVar v) -> Right $ TypeT $ TyVar src name v Nothing -> error "[BUG] readTyVars: lookupVars failed"-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+readTyVars vs ast@(ast_x `BinTree2` ast_y) = do+ TypeT ty_x <- readTyVars vs ast_x+ TypeT ty_y <- readTyVars 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 (sourceInj ast) ty_x ty_y --- | Lookup a 'TyConst' or 'Type' synonym--- associated with given 'NameTy' in given 'ModulesTy',--- building it for a @vs@ of given 'Len'.-readTyName ::- Source src =>- Imports NameTy ->- ModulesTy src -> src -> Len vs -> Mod NameTy ->- Either (Error_Type src) (TypeT src vs)-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- -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'. readVars :: Source src => EVars src -> AST_Type src -> EVars src readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =@@ -78,13 +55,3 @@ readVars evs BinTree0{} = evs readVars evs (BinTree2 x y) = readVars (readVars evs x) y---- * Type 'Error_Type'-data Error_Type src- = Error_Type_Constant_unknown (At src (Mod NameTy))- | Error_Type_Con_Kind (Con_Kind src)- deriving (Eq, Show)-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/Type.hs view
@@ -1,10 +1,10 @@-{-# language ConstraintKinds #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-}+{-# language ConstraintKinds #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Language.Symantic.Typing.Type ( module Language.Symantic.Typing.Type
symantic.cabal view
@@ -20,7 +20,7 @@ -- PVP: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change-version: 6.2.0.20170702+version: 6.3.0.20170703 Source-Repository head location: git://git.autogeree.net/symantic@@ -76,7 +76,6 @@ build-depends: base >= 4.6 && < 5 , containers- , ghc-prim , mono-traversable , symantic-grammar , symantic-document