packages feed

ghc-core-smallstep (empty) → 0.1.0.1

raw patch · 6 files changed

+566/−0 lines, 6 filesdep +basedep +ghcdep +ghc-core-smallstepsetup-changed

Dependencies added: base, ghc, ghc-core-smallstep, ghc-paths

Files

+ GHC/SmallStep.hs view
@@ -0,0 +1,328 @@+{- |++This module contains an executable, type ignoring small-step semantics for+Haskell Core with lazyness.++It has a heap, a current expression and a stack, and closely follows Sestoft’s+semantics.++Naming is handled the same way as in GHC: When we enter a binder (which we do+when applying a lambda, when moving let-bound things onto the heap and in a+case expression), we freshen the names as required.++This semantics ignores types. This means that intermediate configurations will+not be well-typed.++The semantics ignores the 'IdInfo' of GHC variables. It remains to be seen if+some of the functions from the GHC API that we use look at them, and if that+causes problems.++The semantics handles closed terms. There is no support for a module structure+(although that would not be hard to add).++Relatedly, primitive operations (which are manifest simply as free global+variables) are not supported. It might be possible to parametrize over their+execution.+++-}+module GHC.SmallStep+    ( -- * Trivial expressions and Values+      TrivialArg, exprIsTrivial'+    , Value(..), isValue, isValue_maybe+      -- * Configurations+    , Conf, Heap, Stack, StackElem(..)+      -- * The small-steps semantics+    , initConf+    , Step(..)+    , step+    )+    where++import FastString+import CoreSyn+import CoreSubst+import CoreUtils hiding (exprIsTrivial, exprIsHNF)+import Id+import VarEnv+import VarSet+import Unique+import Outputable+import DataCon+import Literal+import Coercion (Coercion)+import Data.Maybe++-- | The configuration of the semantics.+--+-- Invariant:+--+--  * All free variables are bound in the heap+type Conf = (Heap, CoreExpr, Stack)++-- | The heap of a 'Conf'.+type Heap = [(Var, CoreExpr)]++-- | The stack of a 'Conf'+type Stack = [StackElem]++-- | Stack elements+data StackElem+    = ApplyTo CoreExpr        -- a pending function application+    | Alts CoreBndr [CoreAlt] -- a pending case analysis+    | Update Id               -- a pending thunk update++instance Outputable StackElem where+    ppr (ApplyTo e) = char '$' <+> ppr e+    ppr (Alts b alts) = text "as" <+> ppr b <+> braces (ppr alts)+    ppr (Update v) = char '#' <+> ppr v++in_scope :: Heap -> InScopeSet+in_scope = mkInScopeSet . mkVarSet . map fst++addToHeap :: Id -> CoreExpr -> Heap -> Heap+addToHeap v e heap = (v,e) : filter ((/= v) . fst) heap++addManyToHeap :: [Id] -> [CoreExpr] -> Heap -> Heap+addManyToHeap vs es = foldr (.) id (zipWith addToHeap vs es)++lookupHeap :: Id -> Heap -> Maybe CoreExpr+lookupHeap = lookup++-- | Initial configuration (empty heap and stack)+initConf :: CoreExpr -> Conf+initConf e = ([], e, [])+++-- | A trivial argument+type TrivialArg = CoreArg++-- | A Value+data Value = DataConApp DataCon [TrivialArg]+             -- ^ Saturated data con application (trivial value arguments only)+           | LitVal Literal+             -- ^ Literal+           | LamVal Id CoreExpr+             -- ^ A value lambda+           | CoercionVal Coercion+             -- ^ Coercion token. Can be passed around, but nothing can be done to it.++valueToExpr :: Value -> CoreExpr+valueToExpr (DataConApp dc args) = mkConApp dc args+valueToExpr (LitVal l)           = Lit l+valueToExpr (LamVal v e)         = Lam v e+valueToExpr (CoercionVal co)     = Coercion co++-- | An expression is trivial if it can be passed to a function: Variables,+-- literals and coercions.+exprIsTrivial' :: CoreExpr -> Bool+exprIsTrivial' (Tick _ e)               = exprIsTrivial' e+exprIsTrivial' (App e a) | isTypeArg a  = exprIsTrivial' e+exprIsTrivial' (Lam v e) | not (isId v) = exprIsTrivial' e+exprIsTrivial' (Cast e _)               = exprIsTrivial' e++exprIsTrivial' (Var _)      = True+exprIsTrivial' (Lit _)      = True+exprIsTrivial' (Coercion _) = True+exprIsTrivial' _ = False++-- | An expression is a value if it is a data constructor fully applied to+-- trivial arguments, or a literal, or a value lambda, or a coercion.+--+-- Why only to trivial arguments? Because non-trivial arguments need to be+-- bound on the heap before they can be “stored” in the data constructor, so+-- there is work to be done. Without this provision, sharing would not work as+-- expected.+isValue :: CoreExpr -> Bool+isValue e = isJust (isValue_maybe e)++-- | See 'isValue'+isValue_maybe :: CoreExpr -> Maybe Value+isValue_maybe (Tick _ e)               = isValue_maybe e+isValue_maybe (App e a) | isTypeArg a  = isValue_maybe e+isValue_maybe (Lam v e) | not (isId v) = isValue_maybe e+isValue_maybe (Cast e _)               = isValue_maybe e++isValue_maybe (Lit l)                               = Just (LitVal l)+isValue_maybe (Coercion c)                          = Just (CoercionVal c)+isValue_maybe (Lam v e)                             = Just (LamVal v e)+isValue_maybe e | Just (dc, args) <- isDataConApp e+                , all exprIsTrivial' args = Just (DataConApp dc args)++isValue_maybe _ = Nothing++-- | A small step configuration can either be stuck (with a helpful error+-- message), done (fully evaluated, empty stack) or take a step.+data Step a = Error String | Done | Step a++-- | The small-step semantics+--+-- This calculates the next step of a configuration, if there is one.+--+-- If there is no step, then this may have one of three reasons:+--+--  * The configuration is fully evaluated.+--  * The configuration is stuck (which should not happen for well-typed,+--    closed terms)+--  * There is a bug in the semantics.+step :: Conf -> Step Conf++-- the transparent cases+step (heap, Tick _ e, s)               = step (heap, e, s)+step (heap, App e a, s) | isTypeArg a  = step (heap, e, s)+step (heap, Lam v e, s) | not (isId v) = step (heap, e, s)+step (heap, Cast e _, s)               = step (heap, e, s)++-- The value cases+step (heap, e, s) | Just val <- isValue_maybe  e = valStep (heap, val, s)++-- The non-value cases++-- Variable (non-nullary data constructor)+step (heap, Var v, s)+    | Just dc <- isDataConWorkId_maybe v+    , dataConRepArity dc > 0+    = Step (heap, etaExpandDCWorker dc, s)++-- Variable (evaluated)+step (heap, Var v, s) | Just e <- lookupHeap v heap, isValue e+    = Step (heap, e, s)++-- Variable (unevaluated)+step (heap, Var v, s) | Just e <- lookupHeap v heap+    = Step (heap, e, Update v : s)++-- Variable (unbound)+step (heap, Var v, s) = Error "unbound variable"++-- Function application+step (heap, App e a, s)+    = Step (heap, e, ApplyTo a : s)++-- Let expression (non-recursive)+step (heap, Let (NonRec v rhs) e, s)+    = Step (addToHeap v' rhs heap, e', s)+  where+    subst0 = mkEmptySubst (in_scope heap)+    (subst1, v') = substBndr subst0 v+    e' = substExpr empty subst1 e++-- Let expression (recursive)+step (heap, Let (Rec pairs) e, s)+    = Step (addManyToHeap vars' rhss' heap, e', s)+  where+    subst0 = mkEmptySubst (in_scope heap)+    (vars, rhss) = unzip pairs+    (subst1, vars') = substRecBndrs subst0 vars+        -- we could use substBndrs if that is easier, as we do not care about+        -- the idInfo+    rhss' = map (substExpr empty subst1) rhss+    e' = substExpr empty subst1 e++-- Case expressions+step (heap, Case e b _ alts, s)+    = Step (heap, e, Alts b alts : s)++step (heap, Type _, s) = Error "type expression in control position"+step _ = Error "Should be unreachable"+++-- The value cases.++valStep :: (Heap, Value, Stack) -> Step Conf++-- Stack empty? We are done+valStep (heap, val, []) = Done++-- Update a thunk++valStep (heap, val, Update v : s)+    = Step (addToHeap v (valueToExpr val) heap, valueToExpr val, s)++-- beta-reduction++-- Because terms are not in A-Normal form, we have to ensure sharing here.+-- So let us have two rules, one for trivial arguments and one for non-trivial ones.+valStep (heap, LamVal v e, ApplyTo a : s) | exprIsTrivial' a+    = Step (heap, substExpr empty subst e, s)+  where+    subst = extendSubst (mkEmptySubst (in_scope heap)) v a++valStep (heap, LamVal v e, ApplyTo a : s)+    = Step (addToHeap fresh a heap, substExpr empty subst e, s)+  where+    subst = extendSubstWithVar (mkEmptySubst (in_scope heap)) v fresh++    fresh_tmpl = mkSysLocal (fsLit "arg") (mkBuiltinUnique 1) (exprType a)+    fresh = uniqAway (in_scope heap) fresh_tmpl++valStep (heap, val, ApplyTo a : s)+    = Error "non-function applied to argument"++-- Case analysis++valStep (heap, val, Alts b [] : s)+    = Error "empty case"++valStep (heap, val, Alts b [(DEFAULT, [], rhs)] : s)+    = let rhs' = substExpr empty subst1 rhs+          heap' = addToHeap b' (valueToExpr val) heap+      in  Step (heap', rhs', s)+  where+    subst0 = mkEmptySubst (in_scope heap)+    (subst1, b') = substBndr subst0 b++valStep (heap, LitVal l, Alts b alts : s)+    | Just (_, [], rhs) <- findAlt (LitAlt l) alts+    = let rhs' = substExpr empty subst1 rhs+          heap' = addToHeap b' (Lit l) heap+      in  Step (heap', rhs', s)+  where+    subst0 = mkEmptySubst (in_scope heap)+    (subst1, b') = substBndr subst0 b++valStep (heap, LitVal l, Alts b alts : s)+    = Error "literal not found in alts"++valStep (heap, val@(DataConApp dc args), Alts b alts : s)+    | Just (_, pats, rhs) <- findAlt (DataAlt dc) alts+    = let val_pats = filter isId pats+          (subst2, pats') = substBndrs subst1 val_pats+          rhs' = substExpr empty subst2 rhs+          heap' = addManyToHeap pats' args $ addToHeap b' (valueToExpr val) heap+      in  Step (heap', rhs', s)+  where+    subst0 = mkEmptySubst (in_scope heap)+    (subst1, b') = substBndr subst0 b++valStep (heap, val@(DataConApp dc args), Alts b alts : s)+    = Error "data con not found in alts"++valStep (heap, val, Alts b alts : s)+    = Error "non-datacon scrutinized"+++-- |+--+-- An unsaturated DataCon worker is actually a function, taking enough arguments,+-- and then applying them to the DataCon worker. Only then isValue will trigger on it.+--+-- So treat an non-nullary DataCon worker as if the environment had an entry+-- that does the eta-expansion.+--+-- This would not be necessary if we assumed CorePrep output in our terms.+etaExpandDCWorker :: DataCon -> CoreExpr+etaExpandDCWorker dc = mkLams params (mkConApp dc (map Var params))+  where params = zipWith (\n t -> mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) t)+                         [1..]+                         (dataConRepArgTys dc)++-- Makes sure the DataCon is fully applied, and return only the value arguments+isDataConApp :: CoreExpr -> Maybe (DataCon, [CoreArg])+isDataConApp = go []+  where go args (App e a) | isTypeArg a = go args e+        go args (App e a) = go (a:args) e+        go args (Var v) | Just dc <- isDataConWorkId_maybe v+                        , dataConRepArity dc == length args+                        = Just (dc, args)+        go _ _ = Nothing
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2017 Joachim Breitner++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.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ghc-core-smallstep.cabal view
@@ -0,0 +1,31 @@+name:                ghc-core-smallstep+version:             0.1.0.1+synopsis:            A small-step semantics for Core+description:         This module contains an executable, type ignoring+                     small-step semantics for Haskell Core with lazyness.+license:             MIT+license-file:        LICENSE+author:              Joachim Breitner+maintainer:          mail@joachim-breitner.de+copyright:           2017 Joachim Breitner+category:            Language+build-type:          Simple+cabal-version:       >=1.10+tested-with:         GHC == 8.4.*++library+  exposed-modules:     GHC.SmallStep+  build-depends:       base ==4.11.*+  build-depends:       ghc == 8.4.*+  default-language:    Haskell2010++test-suite tests+  main-is:             run.hs+  other-modules:       Fact+  hs-source-dirs:      tests+  type:                exitcode-stdio-1.0+  build-depends:       base ==4.11.*+  build-depends:       ghc == 8.4.*+  build-depends:       ghc-paths == 0.1.*+  build-depends:       ghc-core-smallstep+  default-language:    Haskell2010
+ tests/Fact.hs view
@@ -0,0 +1,142 @@+module Fact (factExpr) where++import CoreSyn hiding (mkLet)+import CoreUtils+import MkId+import BasicTypes+import Id+import Type+import TyCon+import Name+import TysWiredIn+import TysWiredIn+import FastString+import Literal+import Unique+import DataCon++-- | A core expression of type Nat that evaluates to fact n in unary presentation.+factExpr :: Int -> CoreExpr+factExpr n =+    mkRFun plus [x,y] (+        Case (Var x) b natTy [(DataAlt dcZero, [],  Var y)+                             ,(DataAlt dcSucc, [z], Var dcSuccWrk `App` (Var plus `App` Var z `App` Var y))]+    ) $+    mkRFun times [x,y] (+        Case (Var x) b natTy [(DataAlt dcZero, [],  Var dcZeroWrk)+                             ,(DataAlt dcSucc, [z], Var plus `App` Var y `App` (Var times `App` Var z `App` Var y))]+    ) $+    mkRFun fact [x] (+        Case (Var x) b natTy [(DataAlt dcZero, [],  Var dcSuccWrk `App` Var dcZeroWrk)+                             ,(DataAlt dcSucc, [z], Var times `App` Var b `App` (Var fact `App` Var z))]+    ) $+    mkRFun deepseq [x,y] (+        Case (Var x) b natTy [(DataAlt dcZero, [],  Var y)+                             ,(DataAlt dcSucc, [z], Var deepseq `App` Var z `App` Var y)]+    ) $+    mkLet x (Var fact `App` ((iterate (Var dcSuccWrk `App`) (Var dcZeroWrk)) !! n)) $+    Var deepseq `App` Var x `App` Var x+++-- Build IDs. use mkTemplateLocal, more predictable than proper uniques+plus, times, deepseq, fact, x, y, z, b:: Id+[plus, times, deepseq, fact, x, y, z, b] = mkTestIds+    (words "plus times deepseq fact x y z b")+    [ mkFunTys [natTy, natTy] natTy+    , mkFunTys [natTy, natTy] natTy+    , mkFunTys [natTy, natTy] natTy+    , mkFunTys [natTy] natTy+    , natTy+    , natTy+    , natTy+    , natTy+    ]++-- Build DataCons. This is involved++dcZero :: DataCon+dcZero = mkDataCon+    dcZeroName+    False+    dcZeroName+    [] [] [] [] [] [] [] []+    natTy+    NoRRI+    natTyCon+    []+    dcZeroWrk+    NoDataConRep++dcZeroName :: Name+dcZeroName = mkSystemName (mkBuiltinUnique 100) (mkDataOcc "Zero")++dcZeroWrkName :: Name+dcZeroWrkName = mkSystemName (mkBuiltinUnique 101) (mkVarOcc "Zero")++dcZeroWrk :: Id+dcZeroWrk = mkDataConWorkId dcZeroWrkName dcZero++dcSucc :: DataCon+dcSucc = mkDataCon+    dcSuccName+    False+    dcSuccName+    [] [] [] [] [] [] [] [natTy]+    natTy+    NoRRI+    natTyCon+    []+    dcSuccWrk+    NoDataConRep++dcSuccName :: Name+dcSuccName = mkSystemName (mkBuiltinUnique 102) (mkDataOcc "Succ")++dcSuccWrkName :: Name+dcSuccWrkName = mkSystemName (mkBuiltinUnique 103) (mkVarOcc "Succ")++dcSuccWrk :: Id+dcSuccWrk = mkDataConWorkId dcSuccWrkName dcSucc++natTy :: Type+natTy = mkTyConTy natTyCon++natTcName :: Name+natTcName = mkSystemName (mkBuiltinUnique 104) (mkTcOcc "Nat")++natTyCon :: TyCon+natTyCon = mkAlgTyCon+    natTcName+    []+    liftedTypeKind+    []+    Nothing+    []+    (DataTyCon [dcZero, dcSucc] False)+    (VanillaAlgTyCon natTcName)+    False++-- Utilities+mkLApps :: Id -> [Integer] -> CoreExpr+mkLApps v = mkApps (Var v) . map mkLit++mkTestId :: Int -> String -> Type -> Id+mkTestId i s ty = mkSysLocal (mkFastString s) (mkBuiltinUnique i) ty++mkTestIds :: [String] -> [Type] -> [Id]+mkTestIds ns tys = zipWith3 mkTestId [0..] ns tys++mkLet :: Id -> CoreExpr -> CoreExpr -> CoreExpr+mkLet v rhs body = Let (NonRec v rhs) body++mkRLet :: Id -> CoreExpr -> CoreExpr -> CoreExpr+mkRLet v rhs body = Let (Rec [(v, rhs)]) body++mkFun :: Id -> [Id] -> CoreExpr -> CoreExpr -> CoreExpr+mkFun v xs rhs body = mkLet v (mkLams xs rhs) body++mkRFun :: Id -> [Id] -> CoreExpr -> CoreExpr -> CoreExpr+mkRFun v xs rhs body = mkRLet v (mkLams xs rhs) body++mkLit :: Integer -> CoreExpr+mkLit i = Lit (mkLitInteger i intTy)
+ tests/run.hs view
@@ -0,0 +1,43 @@+import Prelude hiding ((<>))+import GHC.SmallStep+import Outputable+import GHC+import GHC.Paths+import System.Environment+import Control.Monad.IO.Class+import DynFlags++import Fact++eval step x = case step x of Nothing -> x+                             Just y -> eval step y++pp :: Outputable a => a -> String+pp = showSDocUnsafe . ppr++ppConf :: Conf -> SDoc+ppConf (heap, e, stack) =+    nest 2 (text "Heap:") $$+    nest 4 (vcat [hang (ppr v <> colon) 2 (ppr e) | (v,e) <- reverse heap ]) $$+    nest 2 (text "Expression:") $$+    nest 4 (ppr e) $$+    nest 2 (text "Stack:") $$+    nest 4 (vcat [ppr s | s <- stack])++main = do+    runGhc (Just libdir) $ do+        -- getSessionDynFlags >>= setSessionDynFlags . flip gopt_set Opt_SuppressUniques+        liftIO $ do+            let e = factExpr 3+            putStrLn $ "Input expression"+            putStrLn $ pp e+            go (initConf e)+++go c = case step c of+    Error e -> putStrLn $ "Error: " ++ e+    Done -> putStrLn $ "Done"+    Step c' -> do+        putStrLn "Next:"+        putStrLn $ showSDocUnsafe $ ppConf c'+        go c'