summaryrefslogtreecommitdiff
path: root/fig-bless/src/Fig/Bless
diff options
context:
space:
mode:
Diffstat (limited to 'fig-bless/src/Fig/Bless')
-rw-r--r--fig-bless/src/Fig/Bless/Builtins.hs39
-rw-r--r--fig-bless/src/Fig/Bless/Runtime.hs21
-rw-r--r--fig-bless/src/Fig/Bless/Syntax.hs19
-rw-r--r--fig-bless/src/Fig/Bless/TypeChecker.hs145
-rw-r--r--fig-bless/src/Fig/Bless/Types.hs60
5 files changed, 255 insertions, 29 deletions
diff --git a/fig-bless/src/Fig/Bless/Builtins.hs b/fig-bless/src/Fig/Bless/Builtins.hs
index 2072ea9..1246e57 100644
--- a/fig-bless/src/Fig/Bless/Builtins.hs
+++ b/fig-bless/src/Fig/Bless/Builtins.hs
@@ -1,22 +1,22 @@
{-# Language ImplicitParams #-}
module Fig.Bless.Builtins
- ( arithmetic
+ ( builtins
) where
import Fig.Prelude
import Control.Monad.State.Strict (execStateT, StateT)
-import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Fig.Bless.Syntax as Syn
+import Fig.Bless.Types
import Fig.Bless.Runtime
-- * Helper functions
-stateful :: Running m t v => StateT (VM m t v) m a -> Builtin m t v
-stateful = execStateT
+stateful :: Running m t v => [BType] -> [BType] -> StateT (VM m t v) m a -> Builtin m t v
+stateful inp out f = (execStateT f, BProgType {..})
push :: (Running m t v, MonadState (VM m' t v) m) => ValueF t v -> m ()
push v = state \vm -> ((), vm { stack = v : vm.stack })
@@ -48,27 +48,43 @@ array :: Running m t v => ValueF t v -> m [v]
array (ValueArray a) = pure a
array v = throwM $ RuntimeErrorSortMismatch ?term ValueSortProgram (valueSort v)
+-- * Stack operations
+stackops :: RunningTop m t v => Builtins m t v
+stackops t = let ?term = t in Map.fromList
+ [ ( "dup", stateful [BTypeVariable "a"] [BTypeVariable "a", BTypeVariable "a"] do
+ x <- pop
+ push x
+ push x
+ )
+ , ( "swap", stateful [BTypeVariable "a", BTypeVariable "b"] [BTypeVariable "b", BTypeVariable "a"] do
+ x <- pop
+ y <- pop
+ push x
+ push y
+ )
+ ]
+
-- * Arithmetic builtins
add :: Running m t v => Builtin m t v
-add = stateful do
+add = stateful [BTypeInteger, BTypeInteger] [BTypeInteger] do
y <- int =<< pop
x <- int =<< pop
push . ValueInteger $ x + y
mul :: Running m t v => Builtin m t v
-mul = stateful do
+mul = stateful [BTypeInteger, BTypeInteger] [BTypeInteger] do
y <- int =<< pop
x <- int =<< pop
push . ValueInteger $ x * y
sub :: Running m t v => Builtin m t v
-sub = stateful do
+sub = stateful [BTypeInteger, BTypeInteger] [BTypeInteger] do
y <- int =<< pop
x <- int =<< pop
push . ValueInteger $ x - y
div :: Running m t v => Builtin m t v
-div = stateful do
+div = stateful [BTypeInteger, BTypeInteger] [BTypeInteger] do
y <- int =<< pop
x <- int =<< pop
push . ValueInteger $ quot x y
@@ -80,3 +96,10 @@ arithmetic t = let ?term = t in Map.fromList
, ("-", sub)
, ("/", div)
]
+
+-- * All builtins
+builtins :: RunningTop m t v => Builtins m t v
+builtins t = Map.unions @[]
+ [ stackops t
+ , arithmetic t
+ ]
diff --git a/fig-bless/src/Fig/Bless/Runtime.hs b/fig-bless/src/Fig/Bless/Runtime.hs
index 8a07e8e..cc19437 100644
--- a/fig-bless/src/Fig/Bless/Runtime.hs
+++ b/fig-bless/src/Fig/Bless/Runtime.hs
@@ -5,8 +5,7 @@ module Fig.Bless.Runtime
, ValueSort(..), valueSort
, RuntimeError(..)
, RunningTop, Running
- , Builtin, Builtins
- , Extractor
+ , BuiltinProgram, Builtin, Builtins
, VM(..)
, initialize
, runProgram, runWord, run
@@ -20,13 +19,13 @@ import qualified Data.Text as Text
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
+import Fig.Bless.Types
import qualified Fig.Bless.Syntax as Syn
data ValueF t v
= ValueInteger Integer
| ValueDouble Double
| ValueString Text
- | ValueWord Syn.Word
| ValueProgram (Syn.ProgramF t)
| ValueArray [v]
deriving (Show, Eq, Ord)
@@ -34,7 +33,6 @@ instance (Pretty t, Pretty v) => Pretty (ValueF t v) where
pretty (ValueInteger i) = tshow i
pretty (ValueDouble d) = tshow d
pretty (ValueString s) = tshow s
- pretty (ValueWord s) = pretty s
pretty (ValueProgram p) = pretty p
pretty (ValueArray vs) = mconcat
[ "["
@@ -63,7 +61,6 @@ valueSort :: ValueF t v -> ValueSort
valueSort (ValueInteger _) = ValueSortInteger
valueSort (ValueDouble _) = ValueSortDouble
valueSort (ValueString _) = ValueSortString
-valueSort (ValueWord _) = ValueSortWord
valueSort (ValueProgram _) = ValueSortProgram
valueSort (ValueArray _) = ValueSortArray
@@ -102,9 +99,9 @@ instance Pretty t => Pretty (RuntimeError t) where
type RunningTop m t v = (MonadThrow m, Typeable t, Show t)
type Running m t v = (RunningTop m t v, ?term :: Maybe t)
-type Builtin m t v = VM m t v -> m (VM m t v)
+type BuiltinProgram m t v = VM m t v -> m (VM m t v)
+type Builtin m t v = (BuiltinProgram m t v, BProgType)
type Builtins m t v = Maybe t -> Map Syn.Word (Builtin m t v)
-type Extractor m t = t -> m (Syn.TermF t)
data VM m t v = VM
{ fuel :: Maybe Integer
, bindings :: Syn.DictionaryF t
@@ -130,15 +127,15 @@ push v vm = vm
{ stack = v : vm.stack
}
-runProgram :: Running m t v => Extractor m t -> Syn.ProgramF t -> VM m t v -> m (VM m t v)
+runProgram :: Running m t v => Syn.Extractor m t -> Syn.ProgramF t -> VM m t v -> m (VM m t v)
runProgram f (Syn.Program p) vm = foldM (flip (run f)) vm p
-runWord :: Running m t v => Extractor m t -> Syn.Word -> VM m t v -> m (VM m t v)
-runWord _ w vm | Just b <- Map.lookup w $ vm.builtins ?term = b vm
-runWord f w vm | Just p <- Map.lookup w vm.bindings.defs = runProgram f p vm
+runWord :: Running m t v => Syn.Extractor m t -> Syn.Word -> VM m t v -> m (VM m t v)
+runWord _ w vm | Just (b, _) <- Map.lookup w $ vm.builtins ?term = b vm
+runWord f w vm | Just p <- lookup w vm.bindings.defs = runProgram f p vm
runWord _ w _ = throwM $ RuntimeErrorWordNotFound ?term w
-run :: Running m t v => Extractor m t -> t -> VM m t v -> m (VM m t v)
+run :: Running m t v => Syn.Extractor m t -> t -> VM m t v -> m (VM m t v)
run f v vm =
let ?term = Just v in f v >>= \case
Syn.TermLiteral (Syn.LiteralInteger i) -> push (ValueInteger i) <$> checkFuel vm
diff --git a/fig-bless/src/Fig/Bless/Syntax.hs b/fig-bless/src/Fig/Bless/Syntax.hs
index ca592f5..b58c516 100644
--- a/fig-bless/src/Fig/Bless/Syntax.hs
+++ b/fig-bless/src/Fig/Bless/Syntax.hs
@@ -9,6 +9,7 @@ module Fig.Bless.Syntax
, Term
, DictionaryF(..)
, Dictionary
+ , Extractor
, word, literal, termF, term, programF, program, dictionaryF, dictionary, P.eof
, Spanning(..), unSpanning, spanning
, ParseError(..)
@@ -18,8 +19,6 @@ module Fig.Bless.Syntax
import Fig.Prelude
import Data.Char (isSpace)
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
import Data.Functor ((<&>))
import Data.Text (unlines)
import Data.String (IsString(..))
@@ -63,16 +62,18 @@ instance Pretty t => Pretty (TermF t) where
type Term = TermF (Fix TermF)
newtype DictionaryF t = Dictionary
- { defs :: Map Word (ProgramF t)
+ { defs :: [(Word, ProgramF t)]
} deriving (Show, Eq, Ord)
instance Pretty t => Pretty (DictionaryF t) where
- pretty d = unlines $ Map.toList d.defs <&> \(w, p) -> mconcat
+ pretty d = unlines $ d.defs <&> \(w, p) -> mconcat
[ pretty w
, " = "
, pretty p
]
type Dictionary = DictionaryF (Fix TermF)
+type Extractor m t = t -> m (TermF t)
+
type Parser = P.Parsec Void Text
ws :: Parser ()
@@ -88,6 +89,9 @@ word = Word . pack <$> P.some (P.satisfy wordChar)
literal :: Parser Literal
literal =
+ P.try ( (LiteralDouble <$> P.C.L.signed (pure ()) P.C.L.float)
+ P.<?> "floating-point literal"
+ ) P.<|>
(
( LiteralInteger <$>
P.C.L.signed (pure ())
@@ -98,9 +102,6 @@ literal =
)
) P.<?> "integer literal"
) P.<|>
- ( (LiteralDouble <$> P.C.L.signed (pure ()) P.C.L.float)
- P.<?> "floating-point literal"
- ) P.<|>
( (LiteralString . pack <$> (P.C.char '"' *> P.manyTill P.C.L.charLiteral (P.C.char '"')))
P.<?> "string literal"
)
@@ -122,7 +123,7 @@ term :: Parser Term
term = termF $ Fix <$> term
dictionaryF :: Parser t -> Parser (DictionaryF t)
-dictionaryF pt = Dictionary . Map.fromList <$> P.many
+dictionaryF pt = Dictionary <$> P.many
( (,)
<$> (ws *> word <* ws <* P.C.char '=')
<*> (ws *> programF pt <* ws <* P.C.char ';')
@@ -132,7 +133,7 @@ dictionary :: Parser Dictionary
dictionary = dictionaryF $ Fix <$> term
newtype ParseError = ParseError (P.ParseErrorBundle Text Void)
- deriving Show
+ deriving (Show)
instance Exception ParseError
instance Pretty ParseError where
pretty (ParseError b) = mconcat
diff --git a/fig-bless/src/Fig/Bless/TypeChecker.hs b/fig-bless/src/Fig/Bless/TypeChecker.hs
new file mode 100644
index 0000000..dedc66a
--- /dev/null
+++ b/fig-bless/src/Fig/Bless/TypeChecker.hs
@@ -0,0 +1,145 @@
+{-# Language ImplicitParams #-}
+
+module Fig.Bless.TypeChecker where
+
+import Fig.Prelude
+
+import Control.Exception.Safe (Typeable)
+
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+
+import Fig.Bless.Syntax
+import Fig.Bless.Types
+import Fig.Bless.Runtime
+
+data Env m t = Env
+ { defs :: [(Word, BProgType)]
+ , ext :: Extractor m t
+ }
+
+data TypeError t
+ = TypeErrorWordNotFound (Maybe t) Word
+ | TypeErrorMismatch (Maybe t) BType BType
+ | TypeErrorArityMismatch (Maybe t) BProgType BProgType
+ deriving (Show, Eq, Ord)
+instance (Show t, Typeable t) => Exception (TypeError t)
+typeErrorPrefix :: Pretty t => Maybe t -> Text
+typeErrorPrefix Nothing = ""
+typeErrorPrefix (Just t) = mconcat
+ [ "while typechecking term: ", pretty t, "\n"
+ ]
+
+instance Pretty t => Pretty (TypeError t) where
+ pretty (TypeErrorWordNotFound t w) = mconcat
+ [ typeErrorPrefix t
+ , "word definition not found for: ", pretty w
+ ]
+ pretty (TypeErrorMismatch t expected actual) = mconcat
+ [ typeErrorPrefix t
+ , "type mismatch:\n"
+ , "expected: ", pretty expected, "\n"
+ , "actual: ", pretty actual
+ ]
+ pretty (TypeErrorArityMismatch t expected actual) = mconcat
+ [ typeErrorPrefix t
+ , "arity mismatch:\n"
+ , "expected: ", pretty expected, "\n"
+ , "actual: ", pretty actual
+ ]
+
+type Typing m t = (MonadThrow m, Typeable t, Show t, ?term :: Maybe t)
+
+completeSubstitution :: [(BType, BType)] -> Either ((BType, BType), [(BType, BType)]) (Map Text BType)
+completeSubstitution = go Map.empty
+ where
+ go acc [] = Right acc
+ go acc ((BTypeVariable v, x):xs) -- ignore variables that are "done", e.g. they don't occur elsewhere
+ | not (Set.member v (Set.unions $ (typeVariables . fst <$> xs) <> (typeVariables . snd <$> xs)))
+ = go (Map.insert v x acc) xs
+ go acc (x:xs) = Left (x, xs <> fmap (first BTypeVariable) (Map.toList acc))
+
+unifyTypes :: forall m t. Typing m t => [(BType, BType)] -> m (Map Text BType)
+unifyTypes subst = case completeSubstitution subst of
+ Right f -> pure f
+ Left ((BTypeProgram p0, BTypeProgram p1), xs) -- decompose programs
+ | length p0.inp == length p1.inp
+ && length p0.out == length p1.out
+ -> unifyTypes (zip p0.inp p1.inp <> zip p0.out p1.out <> xs) -- only if the programs have the same arity
+ | otherwise -> throwM $ TypeErrorArityMismatch ?term p0 p1 -- otherwise, arity mismatch
+ Left ((t0, t1@(BTypeVariable _)), xs) -> unifyTypes $ (t1, t0):xs -- swap variables to lhs
+ Left ((t0@(BTypeVariable v), t1), xs) -> unifyTypes -- eliminate
+ $ (t0, t1):(bimap (substitute v t1) (substitute v t1) <$> xs)
+ Left ((t0, t1), xs)
+ | t0 == t1 -> unifyTypes xs -- delete non-variable matches
+ | otherwise -> throwM $ TypeErrorMismatch ?term t0 t1 -- otherwise, mismatch
+
+combineProgTypes :: forall m t. Typing m t => BProgType -> BProgType -> m BProgType
+combineProgTypes f s = do
+ subst <- unifyTypes $ zip f.out s.inp
+ let finp = applySubstitution subst <$> f.inp
+ let fout = applySubstitution subst <$> f.out
+ let sinp = applySubstitution subst <$> s.inp
+ let sout = applySubstitution subst <$> s.out
+ (leftover, dig) <- foldM
+ ( \(l, d) t -> case l of
+ x:xs
+ | x == t -> pure (xs, d)
+ | otherwise -> throwM $ TypeErrorMismatch ?term x t
+ [] -> pure (l, d <> [t])
+ )
+ (fout, [])
+ sinp
+ pure BProgType
+ { inp = finp <> dig
+ , out = sout <> leftover
+ }
+
+typeOfProgram :: Typing m t => Env m t -> ProgramF t -> m BProgType
+typeOfProgram e (Program p) = case p of
+ ft:ts -> do
+ x <- typeOf e ft
+ foldM (\pt t -> let ?term = Just t in combineProgTypes pt =<< typeOf e t) x ts
+ [] -> pure BProgType {inp = [] , out = []}
+
+typeOf :: Typing m t => Env m t -> t -> m BProgType
+typeOf e wt = do
+ let ?term = Just wt
+ e.ext wt >>= \case
+ TermWord w -> case lookup w e.defs of
+ Nothing -> throwM $ TypeErrorWordNotFound ?term w
+ Just p -> pure p
+ TermLiteral l -> pure BProgType
+ { inp = []
+ , out =
+ [ case l of
+ LiteralInteger _ -> BTypeInteger
+ LiteralDouble _ -> BTypeDouble
+ LiteralString _ -> BTypeString
+ ]
+ }
+ TermQuote p -> do
+ ty <- typeOfProgram e p
+ pure BProgType
+ { inp = []
+ , out = [BTypeProgram ty]
+ }
+
+initializeEnv :: Extractor m t -> Builtins m t v -> Env m t
+initializeEnv ext bs = Env
+ { ext = ext
+ , defs = (\(w, (_, p)) -> (w, p)) <$> Map.toList (bs Nothing)
+ }
+
+checkDictionary :: forall m t. Typing m t => Env m t -> DictionaryF t -> m (Env m t)
+checkDictionary env d = foldM
+ ( \e (w, p) -> do
+ pty <- typeOfProgram e p
+ pure Env
+ { ext = e.ext
+ , defs = (w, pty):e.defs
+ }
+ )
+ env
+ (reverse d.defs)
diff --git a/fig-bless/src/Fig/Bless/Types.hs b/fig-bless/src/Fig/Bless/Types.hs
index 219dc48..162358c 100644
--- a/fig-bless/src/Fig/Bless/Types.hs
+++ b/fig-bless/src/Fig/Bless/Types.hs
@@ -1 +1,61 @@
module Fig.Bless.Types where
+
+import Fig.Prelude
+
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+data BType
+ = BTypeVariable Text
+ | BTypeInteger
+ | BTypeDouble
+ | BTypeString
+ | BTypeProgram BProgType
+ deriving (Show, Eq, Ord)
+instance Pretty BType where
+ pretty (BTypeVariable s) = "!" <> s
+ pretty BTypeInteger = "integer"
+ pretty BTypeDouble = "double"
+ pretty BTypeString = "string"
+ pretty (BTypeProgram p) = "(" <> pretty p <> ")"
+
+data BProgType = BProgType
+ { inp :: [BType]
+ , out :: [BType]
+ }
+ deriving (Show, Eq, Ord)
+instance Pretty BProgType where
+ pretty p = unwords (pretty <$> p.inp) <> " -- " <> unwords (pretty <$> p.out)
+
+renameVars :: (Text -> Text) -> BType -> BType
+renameVars f (BTypeVariable v) = BTypeVariable $ f v
+renameVars f (BTypeProgram p) = BTypeProgram BProgType
+ { inp = renameVars f <$> p.inp
+ , out = renameVars f <$> p.out
+ }
+renameVars _ x = x
+
+substitute :: Text -> BType -> BType -> BType
+substitute n v (BTypeVariable n') | n == n' = v
+substitute n v (BTypeProgram p) = BTypeProgram BProgType
+ { inp = substitute n v <$> p.inp
+ , out = substitute n v <$> p.out
+ }
+substitute _ _ x = x
+
+applySubstitution :: Map Text BType -> BType -> BType
+applySubstitution s (BTypeVariable v)
+ | Just x <- Map.lookup v s = x
+ | otherwise = BTypeVariable v
+applySubstitution s (BTypeProgram p) = BTypeProgram BProgType
+ { inp = applySubstitution s <$> p.inp
+ , out = applySubstitution s <$> p.out
+ }
+applySubstitution _ x = x
+
+typeVariables :: BType -> Set Text
+typeVariables (BTypeVariable v) = Set.singleton v
+typeVariables (BTypeProgram p) = Set.unions $ (typeVariables <$> p.inp) <> (typeVariables <$> p.out)
+typeVariables _ = Set.empty
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-09 17:33:52 +0000