PKGS := symantic-grammar symantic-document symantic symantic-lib
-HS := $(shell find $(PKGS) -name '*.hs')
+HS := $(shell find $(PKGS) -name '*.hs' -not -name 'HLint.hs')
all: build
cd $*; if hlint --quiet --report=hlint.html -XNoCPP \
$(shell cabal-cargs --format=ghc --only=default_extensions --sourcefile=$*) $(HLINT_FLAGS) .; \
then rm -f hlint.html; \
- else sensible-browser hlint.html & fi
+ else sensible-browser ./hlint.html & fi
tag: $(PKGS:=/tag)
%/tag:
ignore "Use fmap"
-- BEGIN: generated hints
-infixl 5 `ebnf_arg`
-infixl 5 `setSource`
-infixl 9 :@
-infixr 0 :$
-infixr 5 `VarS`
-- END: generated hints
-resolver: lts-9.0
+resolver: lts-10.5
packages:
- '.'
-- * Type 'CF'
-- | Context-free grammar.
newtype CF g a = CF { unCF :: g a }
- deriving (IsString, Functor, Gram_Terminal, Applicative, Gram_App)
+ deriving (IsString, Functor, Gram_Char, Gram_String, Applicative, Gram_App)
deriving instance Gram_Error err g => Gram_Error err (CF g)
deriving instance Gram_Reader st g => Gram_Reader st (CF g)
deriving instance Gram_State st g => Gram_State st (CF g)
-- * Class 'Gram_Comment'
-- | Symantics for handling comments after each 'lexeme'.
class
- ( Gram_Terminal g
+ ( Gram_Char g
+ , Gram_String g
, Gram_Rule g
, Gram_Alt g
, Gram_App g
, Gram_CF g
) => Gram_Comment g where
commentable :: g () -> g () -> g () -> g ()
- commentable = rule3 "Commentable" $ \space line block ->
- manySkip $ choice [space, line, block]
+ commentable = rule3 "Commentable" $ \sp line block ->
+ manySkip $ choice [sp, line, block]
commentLine :: CF g String -> CF g String
commentLine prefix = rule "CommentLine" $
prefix *> many (any `minus` (void eol <+> eoi))
import Control.Applicative (Applicative(..))
import Control.Monad
-import Data.Semigroup hiding (option)
+import Data.Semigroup
import Data.Text (Text)
-import Prelude hiding (any)
import qualified Data.Text as Text
import Language.Symantic.Grammar.Meta
module Language.Symantic.Grammar.Fixity where
import Data.Bool as Bool
-import Data.Semigroup hiding (option)
+import Data.Semigroup
import Data.String (IsString(..))
-import Prelude hiding (any)
-- * Type 'Fixity'
data Fixity
import Control.Applicative (Applicative(..))
import Control.Monad (void)
-import Data.Foldable hiding (any)
-import Prelude hiding (any)
+import Data.Foldable
import Language.Symantic.Grammar.Fixity
import Language.Symantic.Grammar.EBNF
-- * Class 'Gram_Op'
-- | Symantics for operators.
class
- ( Gram_Terminal g
+ ( Gram_Char g
+ , Gram_String g
, Gram_Rule g
, Gram_Alt g
, Gram_Try g
-- * Type 'Reg'
-- | Left or right regular grammar.
newtype Reg (lr::Side) g a = Reg { unReg :: g a }
- deriving (IsString, Functor, Gram_Terminal)
+ deriving (IsString, Functor, Gram_Char, Gram_String)
deriving instance Gram_Alt g => Gram_Alt (Reg lr g)
deriving instance Gram_Try g => Gram_Try (Reg lr g)
deriving instance Gram_Rule g => Gram_Rule (Reg lr g)
-- | Symantics for terminal grammars.
module Language.Symantic.Grammar.Terminal where
-import Control.Monad
import Data.Semigroup (Semigroup(..))
import Data.String (IsString(..))
-import Prelude hiding (any)
import qualified Data.Bool as Bool
import qualified Data.Char as Char
import qualified Data.List as List
import qualified Data.Text as Text
+import qualified Data.Text.Lazy as TL
import Language.Symantic.Grammar.Fixity
import Language.Symantic.Grammar.EBNF
-- | Terminal grammar.
newtype Terminal g a
= Terminal { unTerminal :: g a }
- deriving (Functor, Gram_Terminal)
+ deriving (Functor, Gram_Char, Gram_String)
deriving instance Gram_Rule g => Gram_Rule (Terminal g)
--- ** Class 'Gram_Terminal'
+-- ** Class 'Gram_Char'
-- | Symantics for terminal grammars.
-class Gram_Rule g => Gram_Terminal g where
+class Gram_Rule g => Gram_Char g where
any :: g Char
but :: Terminal g Char -> Terminal g Char -> Terminal g Char
eoi :: g ()
eol :: g Char
space :: g Char
char :: Char -> g Char
- string :: String -> g String
unicat :: Unicat -> g Char
range :: (Char, Char) -> g Char
eol = rule "NewLine" $ char '\n'
space = rule "Space" $ char ' '
- -- string = foldr (\c -> (<*>) ((:) <$> char c)) (pure "")
- -- string [] = pure []
- -- string (c:cs) = (:) <$> char c <*> string cs
-deriving instance Gram_Terminal RuleEBNF
-instance Gram_Terminal EBNF where
+deriving instance Gram_Char RuleEBNF
+instance Gram_Char EBNF where
any = ebnf_const "_"
Terminal (EBNF f) `but` Terminal (EBNF g) =
Terminal $ EBNF $ \bo po -> parenInfix po op $
where
escape c | Char.isPrint c && c /= '"' = Text.concat $ ["\"", Text.singleton c, "\""]
escape c = Text.concat ["U+", Text.pack $ show $ Char.ord c]
- string s =
- case List.break (\c -> Bool.not (Char.isPrint c) || c == '"') s of
- (ps, "") -> raw ps
- ("", [c]) -> "" <$ char c
- (ps, [c]) -> "" <$ raw ps <* char c
- ("", c:rs) -> "" <$ char c <* string rs
- (ps, c:rs) -> "" <$ raw ps <* char c <* string rs
- where
- raw cs = ebnf_const $ Text.concat $ ["\"", Text.pack cs, "\""]
unicat = ebnf_const . Text.pack . show
range (l, h) = ebnf_const $ Text.concat
[ runEBNF $ char l
, "…"
, runEBNF $ char h
]
-instance IsString (EBNF String) where
- fromString = string
-- *** Type 'Unicat'
-- | Unicode category.
, Char.OtherSymbol
]
Unicat cat -> [cat]
+
+-- ** Class 'Gram_String'
+class Functor g => Gram_String g where
+ string :: String -> g String
+ {-
+ string = foldr (\c -> (<*>) ((:) <$> char c)) (pure "")
+ string [] = pure []
+ string (c:cs) = (:) <$> char c <*> string cs
+ -}
+ text :: Text.Text -> g Text.Text
+ textLazy :: TL.Text -> g TL.Text
+ text t = Text.pack <$> string (Text.unpack t)
+ textLazy t = TL.pack <$> string (TL.unpack t)
+deriving instance Gram_String RuleEBNF
+instance Gram_String EBNF where
+ string s =
+ case List.break (\c -> Bool.not (Char.isPrint c) || c == '"') s of
+ (ps, "") -> raw ps
+ ("", [c]) -> "" <$ char c
+ (ps, [c]) -> "" <$ raw ps <* char c
+ ("", c:rs) -> "" <$ char c <* string rs
+ (ps, c:rs) -> "" <$ raw ps <* char c <* string rs
+ where
+ raw cs = ebnf_const $ Text.concat $ ["\"", Text.pack cs, "\""]
+instance IsString (EBNF String) where
+ fromString = string
import Control.Monad
import Data.Semigroup ((<>))
import Data.String (IsString(..))
-import Prelude hiding (any, (^), exp)
import qualified Control.Applicative as Gram_AltApp
import qualified Data.Char as Char
import qualified Data.Text as Text
import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
import Language.Symantic.Grammar
-- * Type 'ParsecT'
-type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)
-instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where
- fromString = P.string
+type ParsecC e s = (P.Token s ~ Char, P.Stream s, Ord e)
+instance (ParsecC e s, Gram_String (P.ParsecT e s m)) => IsString (P.ParsecT e s m String) where
+ fromString = string
instance ParsecC e s => Gram_Rule (P.ParsecT e s m) where
rule = P.label . Text.unpack
-instance ParsecC e s => Gram_Terminal (P.ParsecT e s m) where
+instance ParsecC e s => Gram_Char (P.ParsecT e s m) where
any = P.anyChar
eoi = P.eof
char = P.char
- string = P.string
unicat cat = P.satisfy $ (`elem` cats) . Char.generalCategory
where cats = unicode_categories cat
range (l, h) = P.satisfy $ \c -> l <= c && c <= h
but (Terminal f) (Terminal p) = Terminal $ P.notFollowedBy (P.try p) *> f
+instance ParsecC e String => Gram_String (P.ParsecT e String m) where
+ string = P.string
instance ParsecC e s => Gram_Alt (P.ParsecT e s m) where
empty = Gram_AltApp.empty
(<+>) = (Gram_AltApp.<|>)
CF f <& Reg p = CF $ P.lookAhead f <*> p
Reg f &> CF p = CF $ P.lookAhead f <*> p
CF f `minus` Reg p = CF $ P.notFollowedBy (P.try p) *> f
-instance ParsecC e s => Gram_Comment (P.ParsecT e s m)
+instance ParsecC e String => Gram_Comment (P.ParsecT e String m)
elide :: Text.Text -> String
elide s | Text.length s > 42 = take 42 (Text.unpack s) <> ['…']
elide s = Text.unpack s
-tests :: TestTree
-tests = testGroup "Grammar"
+hunits :: TestTree
+hunits = testGroup "Grammar"
[ testGroup "Terminal" $
- let (==>) inp exp =
- testCase (elide exp) $
- runEBNF (unTerminal (void inp)) @?= exp
+ let (==>) input expected =
+ testCase (elide expected) $
+ runEBNF (unTerminal (void input)) @?= expected
; infix 1 ==> in
[ string "" ==> "\"\""
, string "abé\"to" ==> "\"abé\", U+34, \"to\""
, unicat (Unicat Char.LowercaseLetter) ==> "Unicat LowercaseLetter"
]
, testGroup "Reg" $
- let (==>) inp exp =
- testCase (elide exp) $
- runEBNF (unReg (void inp)) @?= exp
+ let (==>) input expected =
+ testCase (elide expected) $
+ runEBNF (unReg (void input)) @?= expected
; infix 1 ==> in
[ (<>) <$> string "0" .*> someR (char '1') ==> "\"0\", {\"1\"}-"
, (<>) <$> someL (char '1') <*. string "0" ==> "{\"1\"}-, \"0\""
]
, testGroup "CF" $
- let (==>) inp exp =
- testCase (elide exp) $
- runEBNF (unCF (void inp)) @?= exp
+ let (==>) input expected =
+ testCase (elide expected) $
+ runEBNF (unCF (void input)) @?= expected
; infix 1 ==> in
[ (<>) <$> string "0" <*> string "1" ==> "\"0\", \"1\""
, (<>) <$> string "0" <* string "X" <*> string "1" ==> "\"0\", \"X\", \"1\""
main =
defaultMain $
testGroup "Language.Symantic"
- [tests]
+ [hunits]
-resolver: lts-9.0
+resolver: lts-10.5
packages:
- '.'
-- PVP: +-+------- breaking API changes
-- | | +----- non-breaking API additions
-- | | | +--- code changes with no API change
-version: 0.2.1.20170818
+version: 0.3.1.20180213
Source-Repository head
location: git://git.autogeree.net/symantic
import Data.Functor.Identity (Identity(..))
import Data.Text (Text)
import Data.Type.Equality
+import Data.Void (Void)
import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Strict as SS
import qualified Data.List as List
import Grammar.Megaparsec ()
type G src ss =
- P.ParsecT P.Dec Text
+ P.ParsecT Void Text
(SS.StateT (Imports NameTe, Modules src ss)
((SS.StateT (Imports NameTy, ModulesTy src))
Identity))
ModulesTyInj ss =>
ModulesInj src ss =>
Gram_Term src ss (G src ss) =>
- Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
+ Text -> Either (P.ParseError Char Void) (AST_Term src ss)
parseTe inp =
let modsTe :: Modules src ss = either (error . show) id modulesInj in
let impsTe = [] `importModules` modsTe in
) =>
Text ->
Either ( Type src '[] t
- , Either (P.ParseError Char P.Dec)
+ , Either (P.ParseError Char Void)
(Error_Term src) )
(Type src '[] t, t, Text) ->
TestTree
import qualified Control.Monad.Classes as MC
import qualified Data.Char as Char
import qualified Data.Text as Text
+import qualified Data.Text.Lazy as TL
import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
import Language.Symantic.Grammar as Sym
import qualified Language.Symantic as Sym
-- * Type 'ParsecC'
-- | Convenient alias for defining instances involving 'P.ParsecT'.
-type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)
-instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where
+type ParsecC e s = (P.Token s ~ Char, P.Stream s, Ord e)
+instance ParsecC e [Char] => IsString (P.ParsecT e [Char] m [Char]) where
fromString = P.string
--
Right a -> return a
instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where
rule = P.label . Text.unpack
-instance ParsecC e s => Sym.Gram_Terminal (P.ParsecT e s m) where
+instance ParsecC e s => Sym.Gram_Char (P.ParsecT e s m) where
any = P.anyChar
eoi = P.eof
char = P.char
- string = P.string
unicat cat = P.satisfy $ (`elem` cats) . Char.generalCategory
where cats = unicode_categories cat
range (l, h) = P.satisfy $ \c -> l <= c && c <= h
Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f
+instance ParsecC e String => Sym.Gram_String (P.ParsecT e String m) where
+ string = P.string
+instance ParsecC e Text.Text => Sym.Gram_String (P.ParsecT e Text.Text m) where
+ string t = Text.unpack <$> P.string (Text.pack t)
+ text = P.string
+ textLazy t = TL.fromStrict <$> P.string (TL.toStrict t)
instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where
empty = Alt.empty
(<+>) = (Alt.<|>)
CF f <& Reg p = CF $ P.lookAhead f <*> p
Reg f &> CF p = CF $ P.lookAhead f <*> p
minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f
-instance ParsecC e s => Sym.Gram_Comment (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Op (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Mod (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Type_Name (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Term_Name (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Comment (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Op (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Mod (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Type_Name (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Term_Name (P.ParsecT e s m)
instance -- Sym.Gram_Type
( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
, Gram_Source src (P.ParsecT e s m)
, Show src
, MC.MonadState ( Sym.Imports Sym.NameTy
- , Sym.ModulesTy src ) (P.ParsecT e s m)
+ , Sym.ModulesTy src )
+ (P.ParsecT e s m)
) => Sym.Gram_Type src (P.ParsecT e s m)
instance -- Sym.Gram_Term_Type
( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
, Show src
, MC.MonadState ( Sym.Imports Sym.NameTy
- , Sym.ModulesTy src ) (P.ParsecT e s m)
+ , Sym.ModulesTy src )
+ (P.ParsecT e s m)
, Gram_Source src (P.ParsecT e s m)
) => Sym.Gram_Term_Type src (P.ParsecT e s m)
instance -- Sym.Gram_Term
( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
, Show src
, MC.MonadState ( Sym.Imports Sym.NameTy
- , Sym.ModulesTy src ) (P.ParsecT e s m)
+ , Sym.ModulesTy src )
+ (P.ParsecT e s m)
, MC.MonadState ( Sym.Imports Sym.NameTe
- , Sym.Modules src ss ) (P.ParsecT e s m)
+ , Sym.Modules src ss )
+ (P.ParsecT e s m)
, Sym.Gram_Source src (P.ParsecT e s m)
, Sym.Gram_Term_Atoms src ss (P.ParsecT e s m)
) => Sym.Gram_Term src ss (P.ParsecT e s m)
module Language.Symantic.Lib.Alternative where
import Control.Applicative (Alternative)
-import Prelude hiding (Functor(..), (<$>), id, const)
+import Prelude hiding (Functor(..))
import qualified Control.Applicative as Alternative
import Language.Symantic
module Language.Symantic.Lib.Applicative where
import Control.Applicative (Applicative)
-import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
+import Prelude hiding (Functor(..), (<$>), Applicative(..))
import qualified Control.Applicative as Applicative
import qualified Data.Function as Fun
import Test.Tasty
import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
import Language.Symantic.Lib
import Compiling.Test
import qualified Data.Char as Char
import qualified Data.Text as Text
-import Language.Symantic.Grammar hiding (char, any)
+import Language.Symantic.Grammar hiding (char)
import qualified Language.Symantic.Grammar as G
import Language.Symantic
import Language.Symantic.Lib.List (tyList)
)
]
where
- tickG :: Gram_Terminal g' => g' Char
+ tickG :: Gram_Char g' => g' Char
tickG = G.char '\''
instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
moduleFor = ["Char"] `moduleWhere`
import qualified Data.Foldable as Foldable
import Prelude hiding (Foldable(..)
, all, and, any, concat, concatMap
- , mapM_, notElem, or, sequence, sequence_)
+ , mapM_, notElem, or, sequence_)
import Language.Symantic
import Language.Symantic.Lib.Alternative (tyAlternative)
import Test.Tasty
import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
import Language.Symantic.Lib
import Compiling.Test
import Test.Tasty
import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
import Language.Symantic ()
import Language.Symantic.Lib
import Data.Map.Strict (Map)
import Data.Proxy (Proxy(..))
import Data.Text as Text
-import Prelude hiding (zipWith)
import qualified Data.Map.Strict as Map
import Language.Symantic.Lib
import Test.Tasty
import Data.Proxy (Proxy(..))
-import Prelude hiding (zipWith)
import qualified Data.MonoTraversable as MT
import Language.Symantic.Lib
import Test.Tasty
-import Prelude hiding ((&&), not, (||), (==), id)
+import Prelude hiding ((&&), not, (||), id)
import Language.Symantic
import Language.Symantic.Lib
import qualified Data.Sequences as Seqs
import qualified Data.Text as Text
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar hiding (text)
import Language.Symantic
import Language.Symantic.Lib.Char ()
import Language.Symantic.Lib.MonoFunctor (Element)
import Test.Tasty
import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
import Language.Symantic.Lib
import Compiling.Test
-- | Symantic for '()'.
module Language.Symantic.Lib.Unit where
-import Prelude hiding ((&&), not, (||))
-
import Language.Symantic
import Language.Symantic.Grammar
{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where
import Data.Proxy
import Data.Ratio (Ratio)
import Data.Text (Text)
+import Data.Void (Void)
import GHC.Exts (Constraint)
import Prelude hiding (exp)
import qualified Control.Monad.Classes.Run as MC
import qualified Data.Sequences as Seqs
import qualified System.IO as IO
import qualified Text.Megaparsec as P
-import qualified Text.Megaparsec.Prim as P
import Language.Symantic.Grammar
import Language.Symantic
-import Language.Symantic.Lib hiding ((<$>), (<*), show)
+import Language.Symantic.Lib hiding ((<$>), (<*))
import Grammar.Megaparsec ()
let run inp (TypeT exp :: TypeT SRC '[]) =
testCase inp $ got @?= Right (Right $ TypeVT exp)
where
- got :: Either (P.ParseError Char P.Dec)
+ got :: Either (P.ParseError Char Void)
(Either (Error_Type SRC) (TypeVT SRC))
got = readType <$> parseTy inp
in
let run inp = testCase inp $ got @?= Left ()
where
got :: Either () (AST_Type SRC)
- got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ parseTy inp in
+ got = left (\(_::P.ParseError (P.Token String) Void) -> ()) $ parseTy inp in
run <$>
[ "Bool, Int"
, "(Bool -> Int) Char"
, testGroup "Compiling errors" $
let run inp = testCase inp $ got @?= Right (Left ())
where
- got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
+ got :: Either (P.ParseError Char Void) (Either () (TypeVT SRC))
got = left (Fun.const ()) . readType <$> parseTy inp in
run <$>
[ "Bool Int"
-resolver: lts-9.0
+resolver: lts-10.5
packages:
- '.'
- location: '../symantic'
extra-dep: true
- location: '../symantic-document'
extra-dep: true
+- location: '../monad-classes'
+ extra-dep: true
extra-deps:
-- monad-classes-0.3.2.0
- peano-0.1.0.1
-- | Term application: apply second given 'TermT' to the first,
-- applying embedded 'TeSym's, or return an error.
betaTerm ::
- forall src ss es vs fun arg.
+ forall src ss ts vs fun arg.
SourceInj (TypeVT src) src =>
Constable (->) =>
- Term src ss es vs (fun::K.Type) ->
- Term src ss es vs (arg::K.Type) ->
- Either (Error_Beta src) (TermT src ss es vs)
+ Term src ss ts vs (fun::K.Type) ->
+ Term src ss ts vs (arg::K.Type) ->
+ Either (Error_Beta src) (TermT src ss ts vs)
betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
case tf of
TyApp _ (TyApp _ a2b a2b_a) a2b_b
betaTerms ::
SourceInj (TypeVT src) src =>
Constable (->) =>
- BinTree (TermVT src ss es) ->
- Either (Error_Beta src) (TermVT src ss es)
+ BinTree (TermVT src ss ts) ->
+ Either (Error_Beta src) (TermVT src ss ts)
betaTerms t =
collapseBT (\acc ele -> do
TermVT (Term qf tf te_fun) <- acc
let tf'' = subst mgu tf'
let ta'' = subst mgu ta'
TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
- normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
+ normalizeVarsTy (qr #> tr) $ \case
+ TyApp _ (TyApp _ _c qr') tr' ->
Right $ TermVT $ Term qr' tr' te_res
+ _ -> undefined -- FIXME: as of GHC 8.2, GHC is no longer clever enough to rule out other cases
) (Right <$> t)
-- * Type 'Error_Beta'
import Control.Monad (void)
import Data.Semigroup (Semigroup(..))
import Data.Map.Strict (Map)
-import Prelude hiding (mod, not, any)
+import Prelude hiding (any)
import qualified Data.Function as Fun
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text
-- * Class 'Gram_Term_Name'
class
- ( Gram_Terminal g
+ ( Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_Try g
-- * Class 'Gram_Term_Type'
class
- ( Gram_Terminal g
+ ( Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_AltApp g
class
( Gram_Source src g
, Gram_Error Error_Term_Gram g
- , Gram_Terminal g
+ , Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_App g
lexeme $
g_ModNameTeId <* g_backquote <+>
g_ModNameTeOp
- g_backquote :: Gram_Terminal g' => g' Char
+ g_backquote :: Gram_Char g' => g' Char
g_backquote = char '`'
g_term_atom :: CF g (AST_Term src ss)
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Compiling.Module where
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.String (IsString(..))
-import Prelude hiding (mod, not, any)
+import Prelude hiding (mod, not)
import qualified Data.Map.Strict as Map
import Language.Symantic.Grammar
infixr 5 `CtxTeS`
-- ** Type 'TermDef'
--- | Convenient type alias for defining 'Term'.
+-- | Convenient type alias to define a 'Term'.
type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
-- ** Type family 'Sym'
-- | Interpreter's data.
newtype View a
= View
- { unView -- Inherited attribuctx:
+ { unView -- Inherited attributes:
:: (Infix, Side)
-> DepthLam
- -- Synthetised attribuctx:
+ -- Synthetised attributes:
-> Text
}
type DepthLam = Int
{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Document where
go v2n (infixB SideL pr, SideL) ty
where
go ::
- forall x.
- (Map IndexVar Name) -> -- names of variables
+ forall kx (x::kx).
+ Map IndexVar Name -> -- names of variables
(Infix, Side) ->
Type src vs x -> d
-- Var
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.Map.Strict as Map
import qualified Data.Text as Text
-- * Class 'Gram_Mod'
class
- ( Gram_Terminal g
+ ( Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_Try g
-- * Class 'Gram_Type_Name'
class
- ( Gram_Terminal g
+ ( Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_Try g
-- | Read an 'AST_Type' from a textual source.
class
( Gram_Source src g
- , Gram_Terminal g
+ , Gram_Char g
, Gram_Rule g
, Gram_Alt g
, Gram_Try g
{-# LANGUAGE GADTs #-}
-{-# OPTIONS_GHC -fno-warn-missing-methods #-}
-- | Natural numbers inductivey defined at the type-level, and of kind @*@.
module Language.Symantic.Typing.Peano where
kindOfType (TyVar _src _n v) = kindOfVar v
kindOfType (TyFam _src _len fam _as) = kindOfConst fam
--- | Remove unused 'Var's from ther context.
+-- | Remove unused 'Var's from the context.
normalizeVarsTy ::
Type src vs (t::kt) ->
(forall vs'. Type src vs' (t::kt) -> ret) -> ret
(TypeT src vs, [TypeT src vs])
spineTy typ = go [] typ
where
- go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
+ go :: forall kx (x::kx). [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
| Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
= go ctx t -- NOTE: skip the constraint @q@.
import Data.Proxy (Proxy(..))
import Data.String (IsString(..))
import Data.Text (Text)
-import Data.Type.Equality ((:~:)(..))
+import Data.Type.Equality ((:~:)(..), (:~~:)(..))
import qualified Data.Kind as K
import Language.Symantic.Grammar
import Language.Symantic.Typing.List
import Language.Symantic.Typing.Kind
--- | /Heterogeneous propositional equality/:
--- like (:~:) but prove also that the kinds are equal.
-data (:~~:) (a::ka) (b::kb) where
- HRefl :: a :~~: a
-
-- * Type 'Var'
-- | A /type variable/, indexed amongst a type-level list.
-- @v@ is wrapped within a 'Proxy' to have a kind-heterogeneous list.
* `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`).
+ 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.
-resolver: lts-9.0
+resolver: lts-10.5
packages:
- '.'
- location: '../symantic-grammar'
name: symantic
stability: experimental
synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
-tested-with: GHC==8.0.2
+tested-with: GHC==8.2.2
-- PVP: +-+------- breaking API changes
-- | | +----- non-breaking API additions
-- | | | +--- code changes with no API change
-version: 6.3.0.20170807
+version: 6.3.1.20180213
Source-Repository head
location: git://git.autogeree.net/symantic
TypeApplications
TypeFamilies
TypeOperators
- ghc-options: -Wall
- -fno-warn-tabs
+ ghc-options:
+ -Wall
+ -Wincomplete-uni-patterns
+ -Wincomplete-record-updates
+ -fno-warn-tabs
+ -fhide-source-paths
default-language: Haskell2010
exposed-modules:
Language.Symantic
sourcephile / git / haskell / symantic.git / commitdiff