diff --git a/DDCI/Core/Command/Ast.hs b/DDCI/Core/Command/Ast.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Ast.hs @@ -0,0 +1,29 @@ + +module DDCI.Core.Command.Ast + (cmdAst) +where +import DDCI.Core.Command.Check +import DDCI.Core.State +import qualified Language.Haskell.Exts.Parser as H +import qualified Language.Haskell.Exts.Pretty as H + + +-- | Parse, check, and pretty print an expression's internal representation +cmdAst :: State -> Int -> String -> IO () +cmdAst state lineStart str + = cmdParseCheckExp state lineStart str >>= goShow + where + -- Expression had a parse or type error. + goShow Nothing + = return () + + -- Expression is well-typed. + goShow (Just (x, _tX, _effX, _cloX)) + = let p = pretty x in + putStrLn p + + pretty x + = case H.parseExp (show x) of + H.ParseOk parsed -> H.prettyPrint parsed + err -> show err + diff --git a/DDCI/Core/Command/Check.hs b/DDCI/Core/Command/Check.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Check.hs @@ -0,0 +1,237 @@ +module DDCI.Core.Command.Check + ( cmdShowKind + , cmdTypeEquiv + , cmdShowWType + , cmdShowType + , cmdExpRecon + , ShowTypeMode(..) + , cmdParseCheckExp) +where +import DDCI.Core.State +import DDCI.Core.IO +import DDC.Core.Eval.Env +import DDC.Core.Eval.Name +import DDC.Core.Eval.Check +import DDC.Type.Equiv +import DDC.Core.Exp +import DDC.Core.Check +import DDC.Core.Pretty +import DDC.Core.Parser +import DDC.Core.Parser.Tokens +import DDC.Core.Collect +import DDC.Core.Transform.SpreadX +import DDC.Type.Transform.SpreadT +import qualified DDC.Type.Parser as T +import qualified DDC.Type.Check as T +import qualified DDC.Base.Parser as BP +import qualified Data.Set as Set + + +-- kind ------------------------------------------------------------------------ +-- | Show the kind of a type. +cmdShowKind :: State -> Int -> String -> IO () +cmdShowKind state lineStart ss + = goParse (lexString lineStart ss) + where + goParse toks + = case BP.runTokenParser describeTok "" T.pType toks of + Left err -> putStrLn $ renderIndent $ text "parse error " <> ppr err + Right t -> goCheck t + + goCheck t + = case T.checkType primKindEnv (spreadT primKindEnv t) of + Left err -> putStrLn $ renderIndent $ ppr err + Right k -> outDocLn state $ ppr t <+> text "::" <+> ppr k + + +-- tequiv --------------------------------------------------------------------- +-- | Check if two types are equivlant. +cmdTypeEquiv :: State -> Int -> String -> IO () +cmdTypeEquiv _state lineStart ss + = goParse (lexString lineStart ss) + where + goParse toks + = case BP.runTokenParser describeTok "" + (do t1 <- T.pTypeAtom + t2 <- T.pTypeAtom + return (t1, t2)) + toks + of Left err -> putStrLn $ renderIndent $ text "parse error " <> ppr err + Right tt -> goEquiv tt + + goEquiv (t1, t2) + = do b1 <- checkT t1 + b2 <- checkT t2 + if b1 && b2 + then putStrLn $ show $ equivT t1 t2 + else return () + + checkT t + = case T.checkType primKindEnv (spreadT primKindEnv t) of + Left err + -> do putStrLn $ renderIndent $ ppr err + return False + + Right{} + -> return True + + +-- wtype ---------------------------------------------------------------------- +-- | Show the type of a witness. +cmdShowWType :: State -> Int -> String -> IO () +cmdShowWType state lineStart ss + = cmdParseCheckWitness state lineStart ss >>= goResult + where + goResult Nothing + = return () + + goResult (Just (w, t)) + = putStrLn $ renderIndent $ ppr w <> text " :: " <> ppr t + + +-- | Parse the given witness, and return it along with its type. +-- +-- If the expression had a parse error, undefined vars, or type error +-- then print this to the console. +cmdParseCheckWitness + :: State + -> Int -- Starting line number for lexer. + -> String + -> IO (Maybe (Witness Name, Type Name)) + +cmdParseCheckWitness state lineStart str + = goParse (lexString lineStart str) + where + -- Lex and parse the string. + goParse toks + = case BP.runTokenParser describeTok "" pWitness toks of + Left err + -> do putStrLn $ renderIndent $ text "parse error " <> ppr err + return Nothing + + Right x -> goCheck x + + -- Spread type annotations into binders, + -- check for undefined variables, + -- and check its type. + goCheck x + = let fvs = freeX primTypeEnv x -- TODO: also check for free type vars + x' = spreadX primKindEnv primTypeEnv x + in if Set.null fvs + then goResult x' (checkWitness primKindEnv primTypeEnv x') + else do + outDocLn state $ text "Undefined variables: " <> ppr fvs + return Nothing + + -- Expression had a type error. + goResult _ (Left err) + = do putStrLn $ renderIndent $ ppr err + return Nothing + + goResult x (Right t) + = return $ Just (x, t) + + + +-- check / type / effect / closure -------------------------------------------- +-- | What components of the checked type to display. +data ShowTypeMode + = ShowTypeAll + | ShowTypeValue + | ShowTypeEffect + | ShowTypeClosure + deriving (Eq, Show) + + +-- | Show the type of an expression. +cmdShowType :: State -> ShowTypeMode -> Int -> String -> IO () +cmdShowType state mode lineStart ss + = cmdParseCheckExp state lineStart ss >>= goResult + where + goResult Nothing + = return () + + goResult (Just (x, t, eff, clo)) + = case mode of + ShowTypeAll + -> do outDocLn state $ ppr x + outDocLn state $ text ":*: " <+> ppr t + outDocLn state $ text ":!:" <+> ppr eff + outDocLn state $ text ":$:" <+> ppr clo + + ShowTypeValue + -> outDocLn state $ ppr x <+> text "::" <+> ppr t + + ShowTypeEffect + -> outDocLn state $ ppr x <+> text ":!" <+> ppr eff + + ShowTypeClosure + -> outDocLn state $ ppr x <+> text ":$" <+> ppr clo + + +-- | Check expression and reconstruct type annotations on binders. +cmdExpRecon :: State -> Int -> String -> IO () +cmdExpRecon state lineStart ss + = cmdParseCheckExp state lineStart ss >>= goResult + where + goResult Nothing + = return () + + goResult (Just (x, _, _, _)) + = outDocLn state $ ppr x + + +-- | Parse the given core expression, +-- and return it, along with its type, effect and closure. +-- +-- If the expression had a parse error, undefined vars, or type error +-- then print this to the console. +cmdParseCheckExp + :: State + -> Int -- Starting line number. + -> String + -> IO (Maybe ( Exp () Name + , Type Name, Effect Name, Closure Name)) + +cmdParseCheckExp state lineStart str + = goParse (lexString lineStart str) + where + -- Lex and parse the string. + goParse toks + = case BP.runTokenParser describeTok "" pExp toks of + Left err + -> do putStrLn $ renderIndent $ ppr err + return Nothing + + Right x -> goCheckVars x + + -- Check for undefined variables, and spread type annotations into + -- bound occurrences of variables. + goCheckVars x + = let fvs = freeX primTypeEnv x -- TODO also check for free type vars + x' = spreadX primKindEnv primTypeEnv x + in if Set.null fvs + then goCheckType x' + else do outDocLn state $ text "Undefined variables: " <> ppr fvs + return Nothing + + -- Check the type of the expression. + goCheckType x + = case checkExp primDataDefs primKindEnv primTypeEnv x of + Left err + -> do putStrLn $ renderIndent $ ppr err + return Nothing + + Right (x', t, eff, clo) + -> goCheckCaps x' t eff clo + + -- Check the initial capabilities in the expression. + goCheckCaps x t eff clo + = case checkCapsX x of + Just err + -> do putStrLn $ renderIndent $ ppr err + return Nothing + + Nothing + -> return $ Just (x, t, eff, clo) + diff --git a/DDCI/Core/Command/Eval.hs b/DDCI/Core/Command/Eval.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Eval.hs @@ -0,0 +1,194 @@ + +module DDCI.Core.Command.Eval + ( cmdStep + , cmdEval + , evalExp) +where +import DDCI.Core.Stats.Trace +import DDCI.Core.Command.Check +import DDCI.Core.IO +import DDCI.Core.State +import DDC.Core.Eval.Env +import DDC.Core.Eval.Step +import DDC.Core.Eval.Name +import DDC.Core.Check +import DDC.Core.Exp +import DDC.Core.Pretty +import DDC.Core.Collect +import DDC.Type.Equiv +import DDC.Type.Subsumes +import DDC.Type.Compounds +import Control.Monad +import DDC.Core.Eval.Store (Store) +import qualified DDC.Core.Eval.Store as Store +import qualified Data.Set as Set + + +-- | Parse, check, and single step evaluate an expression. +cmdStep :: State -> Int -> String -> IO () +cmdStep state lineStart str + = cmdParseCheckExp state lineStart str >>= goStore + where + -- Expression had a parse or type error. + goStore Nothing + = return () + + -- Expression is well-typed. + goStore (Just (x, tX, effX, cloX)) + = let -- Create the initial store. + store = startingStoreForExp x + + in goStep store x tX effX cloX + + goStep store x tX effX cloX + = do _ <- forcePrint state store x tX effX cloX + return () + + +-- | Parse, check, and fully evaluate an expression. +cmdEval :: State -> Int -> String -> IO () +cmdEval state lineStart str + = cmdParseCheckExp state lineStart str >>= goEval + where + -- Expression had a parse or type error. + goEval Nothing + = return () + + -- Expression is well-typed. + goEval (Just expr) + = evalExp state expr + + +-- | Evaluate an already parsed and type-checked expression. +-- Exported so transforms can test with it. +evalExp :: State -> (Exp () Name, Type Name, Effect Name, Closure Name) -> IO () +evalExp state (x, tX, effX, cloX) + = do -- Create the initial store. + let store = startingStoreForExp x + + -- Print starting expression. + when (Set.member TraceEval $ stateModes state) + $ outDocLn state (text "* STEP: " <> ppr x) + + -- Print starting store. + when (Set.member TraceStore $ stateModes state) + $ do putStrLn $ renderIndent $ ppr store + outStr state "\n" + + goStep store x + + where + goStep store x0 + = do + mResult <- forcePrint state store x0 tX effX cloX + case mResult of + Nothing -> return () + Just (store', x0') -> goStep store' x0' + + +-- | Create a starting store for the given expression. +-- We pre-allocate any region handles in the expression, +-- and ensure that the next region to be allocated is higher +-- than all of these. +startingStoreForExp :: Exp () Name -> Store +startingStoreForExp xx + = let + -- Gather up all the region handles already in the expression. + rs = [ r | UPrim (NameRgn r) _ <- Set.toList $ collectBound xx] + + -- Decide what new region should be allocated first. + -- Region 0 is reserved for thunks. + iFirstAlloc + | _ : _ <- rs + , Rgn iR <- maximum rs + = iR + 1 + + | otherwise + = 1 + + in Store.empty + { Store.storeNextRgn = iFirstAlloc + , Store.storeRegions = Set.fromList (Rgn 0 : rs) + , Store.storeGlobal = Set.fromList (Rgn 0 : rs) } + + +-- | Perform a single step of evaluation and print what happened. +forcePrint + :: State + -> Store + -> Exp () Name + -> Type Name + -> Effect Name + -> Closure Name + -> IO (Maybe (Store, Exp () Name)) + +forcePrint state store x tX effX cloX + = case force store x of + StepProgress store' x' + -> case checkExp primDataDefs primKindEnv primTypeEnv x' of + Left err + -> do + -- Print intermediate expression. + when (Set.member TraceEval $ stateModes state) + $ do outDocLn state $ text "* STEP: " <> ppr x' + + -- Print intermediate store + when (Set.member TraceStore $ stateModes state) + $ do putStrLn $ renderIndent $ ppr store' + outStr state "\n" + + putStrLn $ renderIndent + $ vcat [ text "* OFF THE RAILS!" + , ppr err + , empty ] + + return $ Nothing + + Right (_, tX', effX', cloX') + -> do + -- Print intermediate expression. + when (Set.member TraceEval $ stateModes state) + $ do outDocLn state $ text "* STEP: " <> ppr x' + + -- Print intermediate store + when (Set.member TraceStore $ stateModes state) + $ do putStrLn $ renderIndent $ ppr store' + putStr "\n" + + -- Check expression has the same type as before, + -- and that the effect and closure are no greater. + let deathT = not $ equivT tX tX' + let deathE = not $ subsumesT kEffect effX effX' + let deathC = not $ subsumesT kClosure cloX cloX' + let death = deathT || deathE || deathC + + when deathT + $ putStrLn $ renderIndent + $ vcat [ text "* OFF THE RAILS!" + , ppr tX + , ppr tX' ] + + if death + then return Nothing + else return $ Just (store', x') + + StepDone + -> do -- Load the final expression back from the store to display. + outDocLn state $ ppr $ traceStore store x + return Nothing + + StepStuck + -> do outDocLn state + $ vcat [ text "* STUCK!" + , empty] + + return Nothing + + StepStuckMistyped err + -> do putStrLn $ renderIndent + $ vcat [ ppr "* OFF THE RAILS!" + , ppr err + , empty] + + return Nothing + diff --git a/DDCI/Core/Command/Help.hs b/DDCI/Core/Command/Help.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Help.hs @@ -0,0 +1,43 @@ + +module DDCI.Core.Command.Help where + +help :: String +help = unlines + [ "Commands available from the prompt:" + , " :quit Exit DDCi-core" + , " :help, :? Display this help" + , "" + , "Types" + , " :kind TYPE Show the kind of a type." + , " :tequiv TYPE TYPE Check if two types are equivalent." + , "" + , "Witnesses" + , " :wtype WITNESS Show the type of a witness expression." + , "" + , "Expressions" + , " :check EXP Show the type, effect and closure of a value expression." + , " :type EXP Show the type of a value expression." + , " :effect EXP Show the effect of a value expression." + , " :closure EXP Show the closure of a value expression." + , " :ast EXP Show the abstract syntax tree of a value expression." + , " :eval EXP Evaluate an expression." + , "" + , "Modes" + , " :set Display active modes and transform" + , " :set +MODE Enable a mode" + , " :set -MODE Disable a mode" + , "" + , " Modes are:" + , " Indent Pretty print expressions with indenting." + , " TraceEval Show the expression at every step in the evaluation." + , " TraceStore Show the store at every step in the evaluation." + , "" + , "Transforms" + , " :set trans TRANS Set the current transform." + , " :trans EXP Transform the given expression." + , " :trun EXP Transform the given expression then evaluate it." + , "" + , " TRANS ::= None | Anonymize | Beta" + , "" + ] + diff --git a/DDCI/Core/Command/Set.hs b/DDCI/Core/Command/Set.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Set.hs @@ -0,0 +1,81 @@ + +-- | Display and toggle active interpreter modes. +module DDCI.Core.Command.Set + ( Mode(..) + , cmdSet) +where +import DDCI.Core.State +import DDCI.Core.Transform +import DDCI.Core.Mode +import DDCI.Core.IO +import DDC.Base.Pretty +import Data.Char +import qualified Data.Set as Set + + +cmdSet :: State -> String -> IO State + +-- Display the active modes. +cmdSet state [] + = do outDocLn state + $ text "mode = " + <> text (show $ Set.toList + $ stateModes state) + + outDocLn state + $ text "trans = " + <> ppr (stateTransform state) + + return state + +-- Toggle active modes. +cmdSet state cmd + | "trans" : rest <- words cmd + = do case parseTransform (concat rest) of + Just spec + -> do putStrLn "ok" + return $ state { stateTransform = spec } + + Nothing + -> do putStrLn "transform spec parse error" + return state + + | otherwise + = case parseModeChanges cmd of + Just changes + -> do let state' = foldr (uncurry adjustMode) state changes + putStrLn "ok" + return state' + + Nothing + -> do putStrLn "mode parse error" + return state + + +-- | Parse a string of mode changes. +parseModeChanges :: String -> Maybe [(Bool, Mode)] +parseModeChanges str + = sequence $ map parseModeChange $ words str + + +-- | Parse a mode change setting. +-- "Mode" or "+Mode" to enable. "-Mode" to disable. +parseModeChange :: String -> Maybe (Bool, Mode) +parseModeChange str + = case str of + ('+' : strMode) + | Just mode <- parseMode strMode + -> Just (True, mode) + + ('-' : strMode) + | Just mode <- parseMode strMode + -> Just (False, mode) + + (c : strMode) + | isUpper c + , Just mode <- parseMode (c : strMode) + -> Just (True, mode) + + _ -> Nothing + + diff --git a/DDCI/Core/Command/Trans.hs b/DDCI/Core/Command/Trans.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Command/Trans.hs @@ -0,0 +1,86 @@ + + +module DDCI.Core.Command.Trans + ( cmdTrans + , cmdTransEval) +where +import DDCI.Core.Command.Check +import DDCI.Core.Command.Eval +import DDCI.Core.Transform +import DDCI.Core.State +import DDCI.Core.IO +import DDC.Core.Eval.Env +import DDC.Core.Eval.Name +import DDC.Core.Check +import DDC.Core.Exp +import DDC.Type.Equiv +import DDC.Base.Pretty + + +-- | Apply the current transform to an expression. +cmdTrans :: State -> Int -> String -> IO () +cmdTrans state lineStart str + = cmdParseCheckExp state lineStart str >>= goStore + where + -- Expression had a parse or type error. + goStore Nothing + = do return () + + -- Expression is well-typed. + goStore (Just (x, t1, eff1, clo1)) + = do tr <- applyTrans state (x, t1, eff1, clo1) + case tr of + Nothing -> return () + Just x' -> outDocLn state $ ppr x' + + +-- | Transform an expression, or display errors +applyTrans :: State -> (Exp () Name, Type Name, Effect Name, Closure Name) -> IO (Maybe (Exp () Name)) +applyTrans state (x, t1, _eff1, _clo1) + = do let x' = applyTransformX (stateTransform state) x + case checkExp primDataDefs primKindEnv primTypeEnv x' of + Right (_, t2, eff2, clo2) + | equivT t1 t2 +-- , equivT eff1 eff2 -- TODO: result can have smaller effect +-- , equivT clo1 clo2 -- TODO: result can have smaller closure + -> do return (Just x') + + | otherwise + -> do putStrLn $ renderIndent $ vcat + [ text "* CRASH AND BURN: Transform is not type preserving." + , ppr x' + , text "::" <+> ppr t2 + , text ":!:" <+> ppr eff2 + , text ":$:" <+> ppr clo2 ] + return Nothing + + Left err + -> do putStrLn $ renderIndent $ vcat + [ text "* CRASH AND BURN: Type error in transformed program." + , ppr err + , text "" ] + + outDocLn state $ text "Transformed expression:" + outDocLn state $ ppr x' + return Nothing + + +-- | Apply the current transform to an expression, then evaluate and display the result +cmdTransEval :: State -> Int -> String -> IO () +cmdTransEval state lineStart str + = cmdParseCheckExp state lineStart str >>= goStore + where + -- Expression had a parse or type error. + goStore Nothing + = do return () + + -- Expression is well-typed. + goStore (Just (x, t1, eff1, clo1)) + = do tr <- applyTrans state (x, t1, eff1, clo1) + case tr of + Nothing -> return () + Just x' + -> do outDocLn state $ ppr x' + evalExp state (x',t1,eff1,clo1) + return () + diff --git a/DDCI/Core/IO.hs b/DDCI/Core/IO.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/IO.hs @@ -0,0 +1,37 @@ + +module DDCI.Core.IO + ( outDoc, outDocLn + , outStr, outStrLn) +where +import DDCI.Core.State +import DDC.Base.Pretty +import qualified Data.Set as Set + + +outDoc :: State -> Doc -> IO () +outDoc state doc + | Set.member Indent $ stateModes state + = putDocLn RenderIndent doc + + | otherwise + = putDocLn RenderPlain doc + + +outDocLn :: State -> Doc -> IO () +outDocLn state doc + | Set.member Indent $ stateModes state + = putDocLn RenderIndent doc + + | otherwise + = putDocLn RenderPlain doc + + +outStr :: State -> String -> IO () +outStr _state str + = putStr str + + +outStrLn :: State -> String -> IO () +outStrLn _state str + = putStrLn str + diff --git a/DDCI/Core/Mode.hs b/DDCI/Core/Mode.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Mode.hs @@ -0,0 +1,29 @@ + +module DDCI.Core.Mode + ( Mode(..) + , parseMode) +where + + +-- | Interpreter mode flags. +data Mode + -- | Display the expression at each step in the evaluation. + = TraceEval + + -- | Display the store state at each step in the evaluation. + | TraceStore + + -- | Render expressions displayed to user using indenting. + | Indent + deriving (Eq, Ord, Show) + + +-- | Parse a mode from a string. +parseMode :: String -> Maybe Mode +parseMode str + = case str of + "TraceEval" -> Just TraceEval + "TraceStore" -> Just TraceStore + "Indent" -> Just Indent + _ -> Nothing + diff --git a/DDCI/Core/State.hs b/DDCI/Core/State.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/State.hs @@ -0,0 +1,43 @@ + +module DDCI.Core.State + ( State(..) + , Transform(..) + , initState + + , Mode (..) + , adjustMode) +where +import DDCI.Core.Mode +import DDCI.Core.Transform +import Data.Set (Set) +import qualified Data.Set as Set + + +-- | Interpreter state. +data State + = State + { stateModes :: Set Mode + , stateTransform :: Transform } + + +-- | Adjust a mode setting in the state. +adjustMode + :: Bool -- ^ Whether to enable or disable the mode. + -> Mode -- ^ Mode to adjust. + -> State + -> State + +adjustMode True mode state + = state { stateModes = Set.insert mode (stateModes state) } + +adjustMode False mode state + = state { stateModes = Set.delete mode (stateModes state) } + + +-- | The initial state. +initState :: State +initState + = State + { stateModes = Set.empty + , stateTransform = None } + diff --git a/DDCI/Core/Stats/Trace.hs b/DDCI/Core/Stats/Trace.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Stats/Trace.hs @@ -0,0 +1,86 @@ + +module DDCI.Core.Stats.Trace + (traceStore) +where +import DDC.Core.Eval.Store +import DDC.Core.Eval.Name +import DDC.Type.Compounds +import DDC.Core.Compounds +import DDC.Core.Exp +import qualified Data.Set as Set +import Data.Set (Set) + + +-- | Replace non-recursive store locations in an expression by their values. +-- +-- * If the value is recursive then we just leave the original store location. +-- * Constructors in the result just have *0 for their type annotation. +-- +traceStore :: Store -> Exp () Name -> Exp () Name +traceStore store xx + = traceStoreX store Set.empty xx + + +-- | Trace an expression. +traceStoreX :: Store -> Set Name -> Exp () Name -> Exp () Name +traceStoreX store entered xx + = let down = traceStoreX store entered + in case xx of + XVar{} -> xx + + XCon _ (UPrim n@(NameLoc l) _) + | not $ Set.member n entered + , Just sbind <- lookupBind l store + -> traceStoreX store (Set.insert n entered) (expOfSBind sbind) + + XCon{} -> xx + XApp a x1 x2 -> XApp a (down x1) (down x2) + XLAM a b x -> XLAM a b (down x) + XLam a b x -> XLam a b (down x) + XLet a ls x -> XLet a (traceStoreLs store entered ls) (down x) + XCase a x alts -> XCase a (down x) (map (traceStoreA store entered) alts) + XCast a c x -> XCast a c (down x) + XType{} -> xx + XWitness{} -> xx + + +-- | Trace lets. +traceStoreLs :: Store -> Set Name -> Lets () Name -> Lets () Name +traceStoreLs store entered ls + = let down = traceStoreX store entered + in case ls of + LLet m b x -> LLet m b (down x) + LRec bxs -> LRec [(b, down x) | (b, x) <- bxs] + LLetRegion{} -> ls + LWithRegion{} -> ls + + +-- | Trace case alts. +traceStoreA :: Store -> Set Name -> Alt () Name -> Alt () Name +traceStoreA store entered (AAlt p x) + = AAlt p (traceStoreX store entered x) + + +-- | Convert a store binding to an expression. +expOfSBind :: SBind -> Exp () Name +expOfSBind sbind + = case sbind of + SObj nTag lsArgs + -> makeXApps () (expOfTag nTag) (map expOfLoc lsArgs) + + SLams fbs x + -> makeXLamFlags () fbs x + + SThunk x + -> x + + +-- | Convert a data constructor tag to a constructor expression. +expOfTag :: Name -> Exp () Name +expOfTag n = XCon () (UName n (tBot kData)) + + +-- | Convert a store location to a constructor expression. +expOfLoc :: Loc -> Exp () Name +expOfLoc l = XCon () (UPrim (NameLoc l) (tBot kData)) + diff --git a/DDCI/Core/Transform.hs b/DDCI/Core/Transform.hs new file mode 100644 --- /dev/null +++ b/DDCI/Core/Transform.hs @@ -0,0 +1,52 @@ + +module DDCI.Core.Transform + ( Transform (..) + , parseTransform + , applyTransformX) +where +import DDC.Base.Pretty +import DDC.Core.Exp +import DDC.Core.Transform.AnonymizeX +import DDC.Core.Transform.ANormal +import DDC.Core.Transform.Beta +import DDC.Core.Eval.Name + + +-- | Desription of the transforms to apply to a core program. +data Transform + = None + | Anonymize + | ANormal + | Beta + deriving (Eq, Show) + +parseTransform :: String -> Maybe Transform +parseTransform str + = case str of + "None" -> Just None + "Anonymize" -> Just Anonymize + "ANormal" -> Just ANormal + "Beta" -> Just Beta + _ -> Nothing + +instance Pretty Transform where + ppr ss + = case ss of + None -> text "None" + Anonymize -> text "Anonymize" + ANormal -> text "ANormal" + Beta -> text "Beta" + + +-- Apply ---------------------------------------------------------------------- +applyTransformX + :: Ord Name + => Transform -> Exp a Name -> Exp a Name + +applyTransformX spec xx + = case spec of + None -> xx + Anonymize -> anonymizeX xx + ANormal -> anormalise xx + Beta -> betaReduce xx + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +-------------------------------------------------------------------------------- +The Disciplined Disciple Compiler License (MIT style) + +Copyright (c) 2008-2011 Benjamin Lippmeier + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +-------------------------------------------------------------------------------- +Redistributions of libraries in ./external are governed by their own licenses: + + - TinyPTC GNU Lesser General Public License + diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -0,0 +1,344 @@ + +import DDCI.Core.State +import DDCI.Core.Command.Help +import DDCI.Core.Command.Set +import DDCI.Core.Command.Check +import DDCI.Core.Command.Eval +import DDCI.Core.Command.Trans +import DDCI.Core.Command.Ast +import System.Environment +import Data.List +import Data.Maybe +import qualified System.Console.Haskeline as HL +import qualified System.Console.Haskeline.IO as HL + + +main :: IO () +main + = do args <- getArgs + case args of + [fileName] + -> do file <- readFile fileName + runBatch file + + _ -> runInteractive + + +-- Command -------------------------------------------------------------------- +-- | The commands that the interpreter supports. +data Command + = CommandBlank + | CommandUnknown + | CommandHelp + | CommandSet + | CommandKind + | CommandEquivType + | CommandWitType + | CommandExpCheck + | CommandExpRecon + | CommandExpType + | CommandExpEffect + | CommandExpClosure + | CommandEval + | CommandTrans + | CommandTransEval + | CommandAst + deriving (Eq, Show) + + +-- | Names used to invoke each command. +commands :: [(String, Command)] +commands + = [ (":help", CommandHelp) + , (":?", CommandHelp) + , (":set", CommandSet) + , (":kind", CommandKind) + , (":tequiv", CommandEquivType) + , (":wtype", CommandWitType) + , (":check", CommandExpCheck) + , (":recon", CommandExpRecon) + , (":type", CommandExpType) + , (":effect", CommandExpEffect) + , (":closure", CommandExpClosure) + , (":eval", CommandEval) + , (":trans", CommandTrans) + , (":trun", CommandTransEval) + , (":ast", CommandAst) ] + + +-- | Read the command from the front of a string. +readCommand :: String -> Maybe (Command, String) +readCommand ss + | null $ words ss + = Just (CommandBlank, ss) + + | [(cmd, rest)] <- [ (cmd, drop (length str) ss) + | (str, cmd) <- commands + , isPrefixOf str ss ] + = Just (cmd, rest) + + | ':' : _ <- ss + = Just (CommandUnknown, ss) + + | otherwise + = Nothing + + +-- InputState ---------------------------------------------------------------------- +-- Interpreter input state +data InputState + = InputState + { -- Command that we're still receiving input for, + -- along with the line number it started on. + inputCommand :: Maybe (Command, Int) + + -- Input mode. + , _inputMode :: Input + + -- Current line number, used for parse error messages. + , inputLineNumber :: Int + + -- Accumulation of current input buffer. + , _inputAcc :: String } + + +-- | How we're reading the input expression. +data Input + -- | Read input line-by-line, using a backslash at the end of the + -- line to continue to the next. + = InputLine + + -- | Read input as a block terminated by a double semicolon (;;) + | InputBlock + deriving (Eq, Show) + + +-- | Read the input mode from the front of a string. +readInput :: String -> (Input, String) +readInput ss + | isPrefixOf ".." ss + = (InputBlock, drop 2 ss) + + | otherwise + = (InputLine, ss) + + +-- Interactive ---------------------------------------------------------------- +-- | Run an interactive session +runInteractive :: IO () +runInteractive + = do putStrLn "DDCi-core, version 0.2.0: http://disciple.ouroborus.net. :? for help" + + -- Setup terminal mode. + loopInteractive + + +-- | The main REPL loop. +loopInteractive :: IO () +loopInteractive + = do hlState <- HL.initializeInput HL.defaultSettings + let inputState = InputState Nothing InputLine 1 [] + loop initState inputState hlState + where + loop state inputState hlState + = do -- If this isn't the first line then print the prompt. + let prompt = if isNothing (inputCommand inputState) + then "> " + else "" + + -- Read a line from the user and echo it back. + line <- getInput hlState prompt + + if isPrefixOf ":quit" line + then return () + else do + (state', inputState') + <- eatLine state inputState line + + loop state' inputState' hlState + + +-- | Get an input line from the console, using given prompt +getInput :: HL.InputState -> String -> IO String +getInput hlState prompt + = do line <- HL.queryInput hlState (HL.getInputLine prompt) + return (fromMaybe ":quit" line) + + +-- Batch ---------------------------------------------------------------------- +runBatch :: String -> IO () +runBatch str + = do let inputState = InputState Nothing InputLine 1 [] + loop initState inputState (lines str) + where + -- No more lines, we're done. + -- There might be a command in the buffer though. + loop state inputState [] + = do eatLine state inputState [] + return () + + loop state inputState (l:ls) + -- Echo comment lines back. + | isPrefixOf "--" l + = do putStrLn l + let inputState' + = inputState + { inputLineNumber = inputLineNumber inputState + 1 } + + loop state inputState' ls + + -- Echo blank lines back if we're between commands. + | Nothing <- inputCommand inputState + , null l + = do putStr "\n" + let inputState' + = inputState + { inputLineNumber = inputLineNumber inputState + 1 } + + loop state inputState' ls + + -- Quit the program. + | isPrefixOf ":quit" l + = do return () + + -- Handle a line of input. + | otherwise + = do (state', inputState') <- eatLine state inputState l + loop state' inputState' ls + + +-- Eat ------------------------------------------------------------------------ +-- Eating input lines. +eatLine :: State -> InputState -> String -> IO (State, InputState) +eatLine state (InputState mCommand inputMode lineNumber acc) line + = do -- If this is the first line then try to read the command and + -- input mode from the front so we know how to continue. + -- If we can't read an explicit command then assume this is + -- an expression to evaluate. + let (cmd, lineStart, (input, rest)) + = case mCommand of + Nothing + -> case readCommand line of + Just (cmd', rest') -> (cmd', lineNumber, readInput rest') + Nothing -> (CommandEval, lineNumber, (InputLine, line)) + + Just (cmd', lineStart') + -> (cmd', lineStart', (inputMode, line)) + + case input of + -- For line-by-line mode, if the line ends with backslash then keep + -- reading, otherwise run the command. + -- We also convert the backslash to a newline so the source + -- position comes out right in parser error messages. + InputLine + | not $ null rest + , last rest == '\\' + -> do return ( state + , InputState (Just (cmd, lineStart)) input + (lineNumber + 1) + (acc ++ init rest ++ "\n")) + + | otherwise + -> do state' <- handleCmd state cmd lineStart (acc ++ rest) + return ( state' + , InputState Nothing InputLine + (lineNumber + 1) + []) + + + -- For block mode, if the line ends with ';;' then run the command, + -- otherwise keep reading. + InputBlock + | isSuffixOf ";;" rest + -> do let rest' = take (length rest - 2) rest + state' <- handleCmd state cmd lineStart (acc ++ rest') + return ( state' + , InputState Nothing InputLine + (lineNumber + 1) + []) + + | otherwise + -> return ( state + , InputState (Just (cmd, lineStart)) input + (lineNumber + 1) + (acc ++ rest ++ "\n")) + + +-- Commands ------------------------------------------------------------------- +-- | Handle a single line of input. +handleCmd :: State -> Command -> Int -> String -> IO State +handleCmd state CommandBlank _ _ + = return state + +handleCmd state cmd lineStart line + = do state' <- handleCmd1 state cmd lineStart line + return state' + +handleCmd1 state cmd lineStart line + = case cmd of + CommandBlank + -> return state + + CommandUnknown + -> do putStr $ unlines + [ "unknown command." + , "use :? for help." ] + + return state + + CommandHelp + -> do putStr help + return state + + CommandSet + -> do state' <- cmdSet state line + return state' + + CommandKind + -> do cmdShowKind state lineStart line + return state + + CommandEquivType + -> do cmdTypeEquiv state lineStart line + return state + + CommandWitType + -> do cmdShowWType state lineStart line + return state + + CommandExpCheck + -> do cmdShowType state ShowTypeAll lineStart line + return state + + CommandExpType + -> do cmdShowType state ShowTypeValue lineStart line + return state + + CommandExpEffect + -> do cmdShowType state ShowTypeEffect lineStart line + return state + + CommandExpClosure + -> do cmdShowType state ShowTypeClosure lineStart line + return state + + CommandExpRecon + -> do cmdExpRecon state lineStart line + return state + + CommandEval + -> do cmdEval state lineStart line + return state + + CommandTrans + -> do cmdTrans state lineStart line + return state + + CommandTransEval + -> do cmdTransEval state lineStart line + return state + + CommandAst + -> do cmdAst state lineStart line + return state + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ddci-core.cabal b/ddci-core.cabal new file mode 100644 --- /dev/null +++ b/ddci-core.cabal @@ -0,0 +1,53 @@ +Name: ddci-core +Version: 0.2.0.1 +License: MIT +License-file: LICENSE +Author: Ben Lippmeier +Maintainer: benl@ouroborus.net +Build-Type: Simple +Cabal-Version: >=1.6 +Stability: experimental +Category: Compilers/Interpreters +Homepage: http://disciple.ouroborus.net +Bug-reports: disciple@ouroborus.net +Synopsis: Disciple Core language interactive interpreter. +Description: + DDCi-core is a user-facing interpreter that can type-check, + transform and evaluate expressions. + +Executable ddci-core + Build-depends: + base == 4.5.*, + containers == 0.4.*, + haskeline == 0.6.4.*, + haskell-src-exts== 1.*, + ddc-base == 0.2.0.*, + ddc-core == 0.2.0.*, + ddc-core-eval == 0.2.0.*, + ddc-core-simpl == 0.2.0.* + + Main-is: + Main.hs + + Other-modules: + DDCI.Core.Command.Ast + DDCI.Core.Command.Check + DDCI.Core.Command.Eval + DDCI.Core.Command.Help + DDCI.Core.Command.Set + DDCI.Core.Command.Trans + DDCI.Core.Stats.Trace + DDCI.Core.IO + DDCI.Core.Mode + DDCI.Core.State + DDCI.Core.Transform + + Extensions: + PatternGuards + ParallelListComp + FlexibleContexts + + ghc-options: + -Wall + -fno-warn-missing-signatures + -fno-warn-unused-do-bind