hermit 0.1.1.0 → 0.1.1.1
raw patch · 6 files changed
+86/−40 lines, 6 filesdep ~ghcdep ~haskelinedep ~kure
Dependency ranges changed: ghc, haskeline, kure
Files
- examples/contents.txt +18/−0
- examples/reverse/Reverse.hss +1/−1
- hermit.cabal +10/−8
- src/Language/HERMIT/Expr.hs +2/−2
- src/Language/HERMIT/Primitive/Fold.hs +42/−29
- src/Language/HERMIT/Primitive/New.hs +13/−0
examples/contents.txt view
@@ -12,6 +12,16 @@ * Notes: unsafe uses of RULES with pre-conditions. +Evaluation+==========++* Evaluation of Hutton's Razor with exceptions.++* Convert to CPS to avoid repeated pattern matching.++* In progress - stuck because "fold" won't fire.++ Fibonacci (Tupling) =================== @@ -103,6 +113,14 @@ * A classic simple example. * Completed.+++Mean+====++* A non-WW tupling example (maybe it can be cast as WW, I'm not sure).++* In progress (stuck because HERMIT crashes). Nub
examples/reverse/Reverse.hss view
@@ -27,4 +27,4 @@ any-call (unfold-rule "[] ++") any-call (unfold 'fix) ; bash unshadow-+ any-call (unfold 'absH)
hermit.cabal view
@@ -1,7 +1,9 @@ Name: hermit-Version: 0.1.1.0+Version: 0.1.1.1 Synopsis: Haskell Equational Reasoning Model-to-Implementation Tunnel Description:+ Note: HERMIT is currently compatible with GHC 7.4.* only.+ . HERMIT uses Haskell to express semi-formal models, efficient implementations, and provide a bridging DSL to describe via stepwise refinement the connection between@@ -38,12 +40,12 @@ . @ $ hermit Reverse.hs Reverse.hss resume- [starting HERMIT v0.1.1.0 on Reverse.hs]+ [starting HERMIT v0.1.1.1 on Reverse.hs] % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main: -fplugin-opt=HERMIT:main:Main:resume [1 of 2] Compiling HList ( HList.hs, HList.o ) Loading package ghc-prim ... linking ... done. ...- Loading package hermit-0.1.1.0 ... linking ... done.+ Loading package hermit-0.1.1.1 ... linking ... done. [2 of 2] Compiling Main ( Reverse.hs, Reverse.o ) Linking Reverse ... $ ./Reverse@@ -54,12 +56,12 @@ . @ $ hermit Reverse.hs- [starting HERMIT v0.1.1.0 on Reverse.hs]+ [starting HERMIT v0.1.1.1 on Reverse.hs] % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main: [1 of 2] Compiling HList ( HList.hs, HList.o ) Loading package ghc-prim ... linking ... done. ...- Loading package hermit-0.1.1.0 ... linking ... done.+ Loading package hermit-0.1.1.1 ... linking ... done. [2 of 2] Compiling Main ( Reverse.hs, Reverse.o ) module main:Main where \ \ rev ∷ ∀ a . [] a -> [] a@@ -129,9 +131,9 @@ ansi-terminal >= 0.5.5, containers >= 0.4.2.1, data-default >= 0.4,- ghc >= 7.4,- haskeline >= 0.6.4.7 && < 0.7,- kure >= 2.2.5,+ ghc == 7.4.*,+ haskeline >= 0.6.4.7,+ kure >= 2.4.1, marked-pretty >= 0.1, mtl >= 2.0.1.0, stm >= 2.2.0.1,
src/Language/HERMIT/Expr.hs view
@@ -135,7 +135,7 @@ parseExprH0 inp = [ (Box (CmdName str),inp1) | (str,inp1) <- parseToken inp- , isId (head str) || head str == ':' -- commands can start with :+ , isAlphaNum (head str) || head str == ':' -- commands can start with : , all isId (tail str) ] ++ [ (InfixableExpr (CmdName str),inp1)@@ -207,7 +207,7 @@ --------------------------------------------- isId :: Char -> Bool-isId c = isAlphaNum c || c `elem` "_-"+isId c = isAlphaNum c || c `elem` "_-'" isInfixId :: Char -> Bool isInfixId c = c `elem` "+._-:<>"
src/Language/HERMIT/Primitive/Fold.hs view
@@ -75,7 +75,7 @@ checkEqual :: Maybe CoreExpr -> Maybe CoreExpr -> Maybe CoreExpr checkEqual m1 m2 = ifM (exprEqual <$> m1 <*> m2) m1 Nothing - al <- foldMatch vs body exp+ al <- foldMatch vs [] body exp let m = Map.fromListWith checkEqual [(k,Just v) | (k,v) <- al ] @@ -88,46 +88,59 @@ where go vs (Lam v e) = go (v:vs) e go vs e = (reverse vs, e) +-- Note: Id in the concrete instance is first+-- (not the Id found in the definition we are trying to fold).+addAlpha :: Id -> Id -> [(Id,Id)] -> [(Id,Id)]+addAlpha rId lId alphas | rId == lId = alphas+ | otherwise = (rId,lId) : alphas+ -- Note: return list can have duplicate keys, caller is responsible -- for checking that dupes refer to same expression foldMatch :: [Var] -- ^ vars that can unify with anything+ -> [(Id,Id)] -- ^ alpha equivalences, wherever there is binding+ -- note: we depend on behavior of lookup here, so new entries+ -- should always be added to the front of the list so+ -- we don't have to explicity remove them when shadowing occurs -> CoreExpr -- ^ pattern we are matching on -> CoreExpr -- ^ expression we are checking -> Maybe [(Var,CoreExpr)] -- ^ mapping of vars to expressions, or failure-foldMatch vs (Var i) e | i `elem` vs = return [(i,e)]- | otherwise = case e of- Var i' | i == i' -> return []- _ -> Nothing-foldMatch _ (Lit l) (Lit l') | l == l' = return []-foldMatch vs (App e a) (App e' a') = do- x <- foldMatch vs e e'- y <- foldMatch vs a a'+-- foldMatch vs as e e' | trace ("foldMatch: " ++ showPpr vs ++ " Alphas: " ++ showPpr as ++ "e:\n" ++ showPpr e ++ "\ne':\n" ++ showPpr e') False = undefined+foldMatch vs as (Var i) e | i `elem` vs = return [(i,e)]+ | otherwise = case e of+ Var i' | maybe False (==i) (lookup i' as) -> return [(i,e)]+ | i == i' -> return []+ _ -> Nothing+foldMatch _ _ (Lit l) (Lit l') | l == l' = return []+foldMatch vs as (App e a) (App e' a') = do+ x <- foldMatch vs as e e'+ y <- foldMatch vs as a a' return (x ++ y)-foldMatch vs (Lam v e) (Lam v' e') | v == v' = foldMatch (filter (==v) vs) e e'-foldMatch vs (Let (NonRec v rhs) e) (Let (NonRec v' rhs') e') | v == v' = do- x <- foldMatch vs rhs rhs'- y <- foldMatch (filter (==v) vs) e e'+foldMatch vs as (Lam v e) (Lam v' e') = foldMatch (filter (==v) vs) (addAlpha v' v as) e e'+foldMatch vs as (Let (NonRec v rhs) e) (Let (NonRec v' rhs') e') = do+ x <- foldMatch vs as rhs rhs'+ y <- foldMatch (filter (==v) vs) (addAlpha v' v as) e e' return (x ++ y)-foldMatch vs (Let (Rec bnds) e) (Let (Rec bnds') e') | length bnds == length bnds' = do+-- TODO: this depends on bindings being in the same order+foldMatch vs as (Let (Rec bnds) e) (Let (Rec bnds') e') | length bnds == length bnds' = do let vs' = filter (`elem` map fst bnds) vs- bmatch (v,rhs) (v',rhs') | v == v' = foldMatch vs' rhs rhs'- bmatch _ _ = Nothing+ as' = [ (v',v) | ((v,_),(v',_)) <- zip bnds bnds' ] ++ as+ bmatch (_,rhs) (_,rhs') = foldMatch vs' as' rhs rhs' x <- zipWithM bmatch bnds bnds'- y <- foldMatch vs' e e'+ y <- foldMatch vs' as' e e' return (concat x ++ y)-foldMatch vs (Tick t e) (Tick t' e') | t == t' = foldMatch vs e e'+foldMatch vs as (Tick t e) (Tick t' e') | t == t' = foldMatch vs as e e' -- TODO: showPpr hack in the rest of these!--- TODO: we don't care if b == b' if they are not used anywhere-foldMatch vs (Case s b ty alts) (Case s' b' ty' alts')- | (b == b') && (showPpr ty == showPpr ty') && (length alts == length alts') = do- x <- foldMatch vs s s'- let vs' = filter (==b) vs- altMatch (ac, is, e) (ac', is', e') | (ac == ac') && (is == is') =- foldMatch (filter (`elem` is) vs') e e'+foldMatch vs as (Case s b ty alts) (Case s' b' ty' alts')+ | (showPpr ty == showPpr ty') && (length alts == length alts') = do+ let as' = addAlpha b' b as+ x <- foldMatch vs as' s s'+ let vs' = filter (/=b) vs+ altMatch (ac, is, e) (ac', is', e') | ac == ac' =+ foldMatch (filter (`notElem` is) vs') (zip is' is ++ as') e e' altMatch _ _ = Nothing y <- zipWithM altMatch alts alts' return (x ++ concat y)-foldMatch vs (Cast e c) (Cast e' c') | showPpr c == showPpr c' = foldMatch vs e e'-foldMatch _ (Type t) (Type t') | showPpr t == showPpr t' = return []-foldMatch _ (Coercion c) (Coercion c') | showPpr c == showPpr c' = return []-foldMatch _ _ _ = Nothing+foldMatch vs as (Cast e c) (Cast e' c') | showPpr c == showPpr c' = foldMatch vs as e e'+foldMatch _ _ (Type t) (Type t') | showPpr t == showPpr t' = return []+foldMatch _ _ (Coercion c) (Coercion c') | showPpr c == showPpr c' = return []+foldMatch _ _ _ _ = Nothing
src/Language/HERMIT/Primitive/New.hs view
@@ -4,6 +4,9 @@ module Language.HERMIT.Primitive.New where import GhcPlugins as GHC hiding (varName)+import TcSplice (lookupThName_maybe)+-- GHC 7.6 only! import TcRnMonad (initTcForLookup)+ --import Convert (thRdrNameGuesses) -- import OccName(varName) @@ -198,6 +201,16 @@ where f True = "Rewrite would succeed." f False = "Rewrite would fail."++{- this will work in 7.6!+findId' :: String -> m Id+findId' = thNameToGhcId . mkName++thNameToGhcId nm = do+ hsc_env <- getHscEnv+ mnm <- liftIO $ initTcForLookup hsc_env $ lookupThName_maybe nm+ maybe (fail "cannot find " ++ show nm) lookupId mnm+-} findId :: (MonadUnique m, MonadIO m, MonadThings m) => Context -> String -> m Id findId c = findIdMG (hermitModGuts c)