ddci-core (empty) → 0.2.0.1
raw patch · 15 files changed
+1336/−0 lines, 15 filesdep +basedep +containersdep +ddc-basesetup-changed
Dependencies added: base, containers, ddc-base, ddc-core, ddc-core-eval, ddc-core-simpl, haskeline, haskell-src-exts
Files
- DDCI/Core/Command/Ast.hs +29/−0
- DDCI/Core/Command/Check.hs +237/−0
- DDCI/Core/Command/Eval.hs +194/−0
- DDCI/Core/Command/Help.hs +43/−0
- DDCI/Core/Command/Set.hs +81/−0
- DDCI/Core/Command/Trans.hs +86/−0
- DDCI/Core/IO.hs +37/−0
- DDCI/Core/Mode.hs +29/−0
- DDCI/Core/State.hs +43/−0
- DDCI/Core/Stats/Trace.hs +86/−0
- DDCI/Core/Transform.hs +52/−0
- LICENSE +20/−0
- Main.hs +344/−0
- Setup.hs +2/−0
- ddci-core.cabal +53/−0
+ DDCI/Core/Command/Ast.hs view
@@ -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+
+ DDCI/Core/Command/Check.hs view
@@ -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 "<interactive>" 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 "<interactive>"+ (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 "<interactive>" 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 "<interactive>" 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) +
+ DDCI/Core/Command/Eval.hs view
@@ -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+
+ DDCI/Core/Command/Help.hs view
@@ -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"+ , ""+ ]+
+ DDCI/Core/Command/Set.hs view
@@ -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++
+ DDCI/Core/Command/Trans.hs view
@@ -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 ()+
+ DDCI/Core/IO.hs view
@@ -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+
+ DDCI/Core/Mode.hs view
@@ -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+
+ DDCI/Core/State.hs view
@@ -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 }+
+ DDCI/Core/Stats/Trace.hs view
@@ -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))+
+ DDCI/Core/Transform.hs view
@@ -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+
+ LICENSE view
@@ -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+
+ Main.hs view
@@ -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+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ddci-core.cabal view
@@ -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