-
Notifications
You must be signed in to change notification settings - Fork 85
3 classes for Symbol #511
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
3 classes for Symbol #511
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Large diffs are not rendered by default.
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -3,15 +3,29 @@ module Data.TypeLits( | |
| Nat, | ||
| KnownNat(..), | ||
| KnownSymbol(..), | ||
| SymbolEq, | ||
| AppendSymbol, | ||
| ConsSymbol | ||
| ) where | ||
| import qualified Prelude() | ||
| import Primitives | ||
| import Data.Char_Type | ||
| import Data.Integer | ||
| import {-# SOURCE #-} Data.Typeable | ||
|
|
||
| -- Special classes solved by the typechecker. | ||
| -- An instance of one of these classes would be useless. | ||
|
|
||
| class KnownNat (n :: Nat) where | ||
| natVal :: forall (proxy :: Nat -> Type) . proxy n -> Integer | ||
|
|
||
| class KnownSymbol (s :: Symbol) where | ||
| symbolVal :: forall (proxy :: Symbol -> Type) . proxy s -> String | ||
|
|
||
| -- Tests two litteral Symbols equality and returns "True" or "False". | ||
| class SymbolEq (s :: Symbol) (t :: Symbol) (b :: Symbol) | s t -> b | ||
|
Owner
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is this what GHC does? I try to be compatible.
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Title: GHC-compatible MotivationMicroHs already supports In GHC, type family AppendSymbol (m :: Symbol) (n :: Symbol) :: SymbolCrucially, it is used inline, in type position, and reduces during f :: Proxy (AppendSymbol "foo" "bar") -> ...What I tried as a workaroundWithout class AppendSymbol (s :: Symbol) (t :: Symbol) (st :: Symbol)
| s t -> st, st t -> s, st s -> tsolveAppendSymbol :: SolveOne
solveAppendSymbol loc iCls [s, t, st] = ...
-- pattern-matches on ELit (LStr ...) literals, computes the concatenation
-- or the missing side (given the other two), unifies via Improve, or
-- errors out on a literal mismatch
solveAppendSymbol loc iCls ts = solveInst loc iCls tsThis works well as a relation: it can check, complete, or reject a triple Where this workaround falls shortA class-based relation can never be GHC-compatible in the way Proposed scopeGiven MicroHs's stated goal of GHC compatibility, and that a similarly
This would be intentionally much narrower than general If this is out of scope for MicroHs's design goals, the class/fundep Happy to share the full prototype ( |
||
|
|
||
| class AppendSymbol (s :: Symbol) (t :: Symbol) (st :: Symbol) | s t -> st, st s -> t, st t -> s | ||
|
|
||
| class ConsSymbol (h :: Symbol) (t :: Symbol) (s :: Symbol) | ||
| | h t -> s, s -> h t | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,83 @@ | ||
| -- mhs keys | ||
| -- packageDbPath package lookup path | ||
| -- The path is expanded from the environment. | ||
| -- $MHSPKG is always the package directory relative | ||
| -- to the mhs binary, and $VERSION is the compiler version. | ||
| [mhs] | ||
| packageDbPath = "$MHSPKG:$HOME/.mcabal-user/mhs-$VERSION" | ||
|
|
||
| -- Target keys | ||
| -- cc C compiler to use, default "cc" | ||
| -- ccflags flags to pass at the beginning of the compiler command, default "" | ||
| -- cclibs flags to pass at the end of the compilation command, default "" | ||
| -- conf the config directory to use, default "unix" | ||
| -- cout flag to set the output file to cc, default "-o" | ||
|
|
||
| -- If no target is set, we use 'unix' on non-Windows and 'windows' on Windows. | ||
|
|
||
| -- Typical Unix-like flags | ||
| -- Assumes gcc or clang | ||
| [unix] | ||
| cc = "cc" | ||
| ccflags = "-w -Wall -O3 " | ||
| cclibs = " -lm" | ||
| conf = "unix" | ||
|
|
||
| -- As above, but with -flto | ||
| -- This flag improves performance, but generates a warning with gcc. | ||
| [unix_lto] | ||
| cc = "cc" | ||
| ccflags = "-w -Wall -O3 -flto " | ||
| cclibs = " -lm" | ||
| conf = "unix" | ||
|
|
||
| -- As above, but with the non-portable flag -march=native | ||
| [unix_x86] | ||
| cc = "cc" | ||
| ccflags = "-w -Wall -O3 -flto -march=native " | ||
| cclibs = " -lm" | ||
| conf = "unix" | ||
|
|
||
| -- Compile with debugging instead of optimization | ||
| [debug] | ||
| cc = "cc" | ||
| ccflags = "-w -Wall -g" | ||
| cclibs = "-lm" | ||
| conf = "unix" | ||
|
|
||
| -- Generate JavaScript&Wasm | ||
| [emscripten] | ||
| cc = "emcc" | ||
| ccflags = "-O3 -sEXPORTED_RUNTIME_METHODS=stringToNewUTF8 -sALLOW_MEMORY_GROWTH -sTOTAL_STACK=5MB -sNODERAWFS -sSINGLE_FILE -DUSE_SYSTEM_RAW -sEXIT_RUNTIME -Wno-address-of-packed-member" | ||
| cclibs = "-lm" | ||
| conf = "unix" | ||
|
|
||
| -- Generate JavaScript&Wasm, with xterm.js support | ||
| [emscripten_web] | ||
| cc = "emcc" | ||
| ccflags = "-O3 -sASYNCIFY -sEXPORTED_FUNCTIONS=['_main','_set_input_char'] -sEXPORTED_RUNTIME_METHODS=['FS','ccall'] -sFORCE_FILESYSTEM=1 -sALLOW_MEMORY_GROWTH -sTOTAL_STACK=5MB -DUSE_WEB_INPUT -Wno-address-of-packed-member" | ||
| cclibs = "-lm" | ||
| conf = "unix" | ||
|
|
||
| -- Use the Tiny C Compiler | ||
| [tcc] | ||
| cc = "tcc" | ||
| ccflags = "-D__TCC__=1" | ||
| cclibs = "-lm" | ||
| conf = "unix" | ||
|
|
||
| -- Windows flags, with stdout supressed | ||
| [windows] | ||
| cc = "cl > NUL /nologo" | ||
| ccflags = "-O2" | ||
| cclibs = "" | ||
| conf = "windows" | ||
| cout = "-Fe" | ||
|
|
||
| -- Take all flags from environment variables | ||
| [environment] | ||
| -- Get all values from the environment | ||
| cc = "$CC" | ||
| ccflags = "$MHSCCFLAGS" | ||
| cclibs = "$MHSCCLIBS" | ||
| conf = "$MHSCONF" |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -3592,6 +3592,9 @@ solvers = | |
| , ((== mkIdent nameTypeEq), solveTypeEq) -- handle equality constraints, i.e. (t1 ~ t2) | ||
| , ((== mkIdent nameKnownNat), solveKnownNat) -- KnownNat 123 constraints | ||
| , ((== mkIdent nameKnownSymbol), solveKnownSymbol) -- KnownSymbol "abc" constraints | ||
| , ((== mkIdent nameSymbolEq), solveSymbolEq) -- SymbolEq "hello" "h3ll0" "False" | ||
| , ((== mkIdent nameAppendSymbol),solveAppendSymbol) -- AppendSymbol "ab" "cd" "abcd" constraints | ||
| , ((== mkIdent nameConsSymbol), solveConsSymbol) -- ConsSymbol "h" "tail" "htail" ("h" always 1 character) contraints | ||
| , ((== mkIdent nameCoercible), solveCoercible) -- Coercible a b constraints | ||
| , (const True, solveInst) -- handle constraints with instances | ||
| ] | ||
|
|
@@ -3777,6 +3780,72 @@ solveKnownSymbol :: SolveOne | |
| solveKnownSymbol loc iCls [e@(ELit _ (LStr _))] = mkConstDict loc iCls e | ||
| solveKnownSymbol loc iCls ts = solveInst loc iCls ts -- look for a dict argument | ||
|
|
||
| solveSymbolEq :: SolveOne | ||
| solveSymbolEq loc iCls [s, t, b] = | ||
| case (s, t) of | ||
| (ELit _ (LStr sStr), ELit _ (LStr tStr)) -> | ||
| let result = if sStr == tStr then "True" else "False" | ||
| in case b of | ||
| ELit _ (LStr bStr) | ||
| | bStr == result -> return $ Just (ETuple [], [], []) | ||
| | otherwise -> return Nothing | ||
| _ | isEUVar b -> return $ Just (ETuple [], [], [(loc, b, ELit loc (LStr result))]) | ||
| | otherwise -> return Nothing | ||
| _ -> solveInst loc iCls [s, t, b] -- s ou t pas encore concrets : on defere | ||
|
Owner
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. English, please |
||
| solveSymbolEq loc iCls ts = solveInst loc iCls ts | ||
|
|
||
| solveAppendSymbol :: SolveOne | ||
| solveAppendSymbol loc iCls [s, t, st] = | ||
| case (getLit s, getLit t, getLit st) of | ||
| (Just sStr, Just tStr, _) -> | ||
| unifyOrCheck loc st (sStr ++ tStr) | ||
| (Just sStr, Nothing, Just stStr) | ||
| | sStr `isPrefixOf` stStr -> unifyOrCheck loc t (drop (length sStr) stStr) | ||
| | otherwise -> tcError loc $ "AppendSymbol: " ++ show stStr | ||
| ++ " does not start with " ++ show sStr | ||
| (Nothing, Just tStr, Just stStr) | ||
| | tStr `isSuffixOf` stStr -> unifyOrCheck loc s (take (length stStr - length tStr) stStr) | ||
| | otherwise -> tcError loc $ "AppendSymbol: " ++ show stStr | ||
| ++ " does not end with " ++ show tStr | ||
| _ -> solveInst loc iCls [s, t, st] -- not enough info : we defere | ||
|
Owner
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Spelling |
||
| where | ||
| getLit (ELit _ (LStr x)) = Just x | ||
| getLit _ = Nothing | ||
| unifyOrCheck l ty target = case ty of | ||
| ELit _ (LStr actual) | actual == target -> return $ Just (ETuple [], [], []) | ||
| | otherwise -> tcError l $ "AppendSymbol mismatch" | ||
| _ | isEUVar ty -> return $ Just (ETuple [], [], [(l, ty, ELit l (LStr target))]) | ||
| | otherwise -> return Nothing | ||
| solveAppendSymbol loc iCls ts = solveInst loc iCls ts | ||
|
|
||
| solveConsSymbol :: SolveOne | ||
| -- Case 1 : s already known -> we split a head (1 character) and a tail | ||
| solveConsSymbol loc iCls [h, t, s@(ELit _ (LStr sStr))] | ||
| | null sStr = return Nothing -- empty Symbol has neither head nor tail | ||
| | otherwise = do | ||
| let hStr = take 1 sStr | ||
| tStr = drop 1 sStr | ||
| check ty target = case ty of | ||
| ELit _ (LStr actual) | ||
| | actual == target -> Right [] | ||
| | otherwise -> Left actual | ||
| _ | isEUVar ty -> Right [(loc, ty, ELit loc (LStr target))] | ||
| | otherwise -> Right [] | ||
| case (check h hStr, check t tStr) of | ||
| (Left actual, _) -> | ||
| tcError loc $ "ConsSymbol: expected head " ++ show hStr ++ ", received " ++ show actual | ||
| (_, Left actual) -> | ||
| tcError loc $ "ConsSymbol: expected tail " ++ show tStr ++ ", received " ++ show actual | ||
| (Right is1, Right is2) -> return $ Just (ETuple [], [], is1 ++ is2) | ||
| -- Case 2 : h and t already known (and s not litteral, otherwise case 1 should match) | ||
| solveConsSymbol loc iCls [h@(ELit _ (LStr hStr)), t@(ELit _ (LStr tStr)), s] | ||
| | length hStr /= 1 = | ||
| tcError loc $ "ConsSymbol: head should be 1 character, received " ++ show hStr | ||
| | isEUVar s = return $ Just (ETuple [], [], [(loc, s, ELit loc (LStr (hStr ++ tStr)))]) | ||
| | otherwise = return Nothing | ||
| -- not enough info : we defer | ||
| solveConsSymbol loc iCls ts = solveInst loc iCls ts | ||
|
|
||
| mkConstDict :: SLoc -> Ident -> Expr -> T (Maybe (Expr, [Goal], [Improve])) | ||
| mkConstDict loc iCls e = do | ||
| let res = EApp (EVar $ mkClassConstructor iCls) fcn | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| module AppendSymbol where | ||
| import Data.Proxy | ||
| import Data.TypeLits | ||
|
|
||
| testSuccess :: AppendSymbol "ab" "cd" "abcd" => Bool | ||
| testSuccess = True | ||
|
|
||
| testAppend :: AppendSymbol s1 s2 s3 => Proxy s1 -> Proxy s2 -> Proxy s3 | ||
| testAppend _ _ = Proxy | ||
|
|
||
| testPrefix :: AppendSymbol s1 s2 s3 => Proxy s3 -> Proxy s2 -> Proxy s1 | ||
| testPrefix _ _ = Proxy | ||
|
|
||
| testSuffix :: AppendSymbol s1 s2 s3 => Proxy s3 -> Proxy s1 -> Proxy s2 | ||
| testSuffix _ _ = Proxy | ||
|
|
||
| testChain :: | ||
| ( AppendSymbol s1 s2 s3 | ||
| , AppendSymbol s3 s4 s7) | ||
| => Proxy s1 -> Proxy s2 -> Proxy s4 -> Proxy s7 | ||
| testChain _ _ _ = Proxy | ||
|
|
||
| main = do | ||
| putStrLn $ show testSuccess | ||
| putStrLn $ symbolVal $ testAppend (Proxy :: Proxy "ab") (Proxy :: Proxy "cd") | ||
| putStrLn $ symbolVal $ testPrefix (Proxy :: Proxy "abcd") (Proxy :: Proxy "cd") | ||
| putStrLn $ symbolVal $ testSuffix (Proxy :: Proxy "abcd") (Proxy :: Proxy "ab") | ||
| putStrLn $ symbolVal $ | ||
| testChain (Proxy :: Proxy "ab") (Proxy :: Proxy "cd") (Proxy :: Proxy "ef") |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,5 @@ | ||
| True | ||
| abcd | ||
| ab | ||
| cd | ||
| abcdef |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| module ConsSymbolEq where | ||
|
|
||
| import Data.Proxy | ||
| import Data.TypeLits (Symbol, KnownSymbol, symbolVal, AppendSymbol, ConsSymbol, SymbolEq) | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Specifier : Lit wraps a Symbol. | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| data D -- digit | ||
| data S -- string | ||
| data Lit (lit :: Symbol) | ||
|
|
||
| class Specifier s | ||
| instance Specifier D | ||
| instance Specifier S | ||
| instance (KnownSymbol lit) => Specifier (Lit lit) | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- FList : lists the formats. | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| data FNil | ||
| data FCons s fl | ||
|
|
||
| class FList fl | ||
| instance FList FNil | ||
| instance (Specifier s, FList fl) => FList (FCons s fl) | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- FormatF : splits the %d / %s formats | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| class (FList format) => FormatF format fun | format -> fun where | ||
| formatF :: Proxy format -> String -> fun | ||
|
|
||
| instance FormatF FNil String where | ||
| formatF _ = id | ||
|
|
||
| instance (FormatF rest fun) | ||
| => FormatF (FCons D rest) (Int -> fun) where | ||
| formatF _ str = \i -> formatF (Proxy :: Proxy rest) (str ++ show i) | ||
|
|
||
| instance (FormatF rest fun) | ||
| => FormatF (FCons S rest) (String -> fun) where | ||
| formatF _ str = \s -> formatF (Proxy :: Proxy rest) (str ++ s) | ||
|
|
||
| instance (KnownSymbol lit, FormatF rest fun) | ||
| => FormatF (FCons (Lit lit) rest) fun where | ||
| formatF _ str | ||
| = formatF (Proxy :: Proxy rest) (str ++ symbolVal (Proxy :: Proxy lit)) | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- MatchFmt | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| class (Specifier out) => MatchFmt (head :: Symbol) out | head -> out | ||
| instance MatchFmt "d" D | ||
| instance MatchFmt "s" S | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Parse : uses SymbolEq -> "True"/"False" to avoid instance overlappings. | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| class (FList format) => Parse (string :: Symbol) format | string -> format | ||
| instance (SymbolEq string "" isEmpty, ParseC isEmpty string format) | ||
| => Parse string format | ||
|
|
||
| class (FList out) => ParseC (isEmpty :: Symbol) (string :: Symbol) out | isEmpty string -> out | ||
|
|
||
| instance ParseC "True" string (FCons (Lit "") FNil) | ||
|
|
||
| instance (ConsSymbol h t string, Match h t out) | ||
| => ParseC "False" string out | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Match : uses SymbolEq also. | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| class (FList out) => Match (h :: Symbol) (t :: Symbol) out | h t -> out | ||
| instance (SymbolEq h "%" isPct, MatchC isPct h t out) | ||
| => Match h t out | ||
|
|
||
| class (FList out) => MatchC (isPct :: Symbol) (h :: Symbol) (t :: Symbol) out | ||
| | isPct h t -> out | ||
|
|
||
| -- '%' : on decompose t pour recuperer le caractere de specification (h2) | ||
| -- et le reste (t2) | ||
| instance (ConsSymbol h2 t2 t, MatchFmt h2 spec, Parse t2 rest) | ||
| => MatchC "True" h t (FCons (Lit "") (FCons spec rest)) | ||
|
|
||
| -- caractere ordinaire : accumule via AppendSymbol (h prefixe acc) | ||
| instance (FList r, KnownSymbol acc', AppendSymbol h acc acc', Parse t (FCons (Lit acc) r)) | ||
| => MatchC "False" h t (FCons (Lit acc') r) | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Format | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| class Format (string :: Symbol) fun | string -> fun where | ||
| format :: Proxy string -> fun | ||
|
|
||
| instance (Parse string format, FormatF format fun) | ||
| => Format string fun where | ||
| format _ = formatF (Proxy :: Proxy format) "" | ||
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Exemple | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| main :: IO () | ||
| main = do | ||
| let formatted = format (Proxy :: Proxy "Hi %s! You are %d") "Bill" 12 | ||
| putStrLn formatted -- "Hi Bill! You are 12" |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| Hi Bill! You are 12 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since these are not exactly GHC compatible, I'd like them to have names that are not the same as GHC's. I will eventually implement GHC compatible type level operations.