performing hash-consing declaration in createTerm function

This commit is contained in:
Paul Chiusano 2014-07-08 17:06:25 -04:00
parent 44e732ffbe
commit b8dc00fc3f
3 changed files with 55 additions and 18 deletions

View File

@ -1,3 +1,4 @@
{-# LANGUAGE OverloadedStrings #-}
module Unison.Node.Common (node) where
import qualified Data.Map as M
@ -32,12 +33,18 @@ node eval store =
createTerm e md = do
t <- Type.synthesize readTypeOf e
h <- pure $ E.finalizeHash e
((h,_), subterms) <- pure $ E.hashCons e
ht <- pure $ T.finalizeHash t
writeTerm store h e
writeType store ht t
writeMetadata store h (md { MD.annotation = ht })
pure h
pure h <* mapM_ go subterms where -- declare all subterms extracted via hash-consing
go (h,e) = do
t <- Type.synthesize readTypeOf e
ht <- pure $ T.finalizeHash t
writeTerm store h e
writeType store ht t
writeMetadata store h (MD.syntheticTerm ht)
createType t md = let h = T.finalizeHash t in do
writeType store h t

View File

@ -14,7 +14,7 @@ data Metadata k =
sort :: Sort,
names :: Names,
locals :: [(V.Var, Names)],
description :: k,
description :: Maybe k,
annotation :: k
} deriving (Eq,Ord,Show)
@ -25,6 +25,14 @@ localMatches :: V.Var -> Query -> Metadata k -> Bool
localMatches v (Query txt) (Metadata _ _ m _ _) =
txt `elem` (let Names ns = fromMaybe (Names []) (lookup v m) in ns)
-- | Nameless metadata, contains only the annotation
synthetic :: Sort -> k -> Metadata k
synthetic t ann = Metadata t (Names []) [] Nothing ann
-- | Nameless term metadata, containing only the type annotation
syntheticTerm :: k -> Metadata k
syntheticTerm = synthetic Term
data Names = Names [Text] deriving (Eq,Ord,Show,Read)
data Query = Query Text

View File

@ -154,24 +154,46 @@ string s = Lit (String (Txt.pack s))
text :: Txt.Text -> Term
text s = Lit (String s)
hashCons :: Term -> Writer (M.Map H.Hash Term) Term
hashCons e =
let closedHash = H.finalize . H.lazyBytes . JE.encode
save e | isClosed e = let h = closedHash e in tell (M.singleton h e) >> pure (Ref h)
save e = pure e
in case etaNormalForm e of
l@(Lit _) -> save l
c@(Con _) -> pure c
r@(Ref _) -> pure r
v@(Var _) -> pure v
Lam n body -> hashCons body >>=
\body -> save (lam1 $ \x -> betaReduce (Lam n body `App` x))
Ann e t -> save =<< (Ann <$> hashCons e <*> pure t)
App f x -> save =<< (App <$> hashCons f <*> hashCons x)
-- | Order a collection of declarations such that no declaration
-- references hashes declared later in the returned list
topological :: M.Map H.Hash Term -> [(H.Hash, Term)]
topological terms = go S.empty (M.keys terms)
where
keys = M.keysSet terms
go seen pending = case pending of
[] -> []
(h:pending) | S.member h seen -> go seen pending
(h:pending) ->
let e = maybe (error "unpossible") id $ M.lookup h terms
seen' = S.insert h seen
new = S.difference (dependencies e `S.intersection` keys) seen'
pending' = pending ++ S.toList new
in go seen' pending' ++ [(h,e)]
-- | Factor all closed subterms out into separate declarations, and
-- return a single term which contains 'Ref's into these declarations
-- The list of subterms are topologically sorted, so terms with
-- no dependencies appear first in the returned list, followed by
-- terms which depend on these dependencies
hashCons :: Term -> ((H.Hash, Term), [(H.Hash,Term)])
hashCons e = let (e', hs) = runWriter (go e) in ((closedHash e', e'), topological hs)
where
closedHash = H.finalize . H.lazyBytes . JE.encode
save e | isClosed e = let h = closedHash e in tell (M.singleton h e) >> pure (Ref h)
save e = pure e
go e = case etaNormalForm e of
l@(Lit _) -> save l
c@(Con _) -> pure c
r@(Ref _) -> pure r
v@(Var _) -> pure v
Lam n body -> go body >>=
\body -> save (lam1 $ \x -> betaReduce (Lam n body `App` x))
Ann e t -> save =<< (Ann <$> go e <*> pure t)
App f x -> save =<< (App <$> go f <*> go x)
-- | Computes the nameless hash of the given term
hash :: Term -> H.Digest
hash e = H.lazyBytes . JE.encode . fst . runWriter . hashCons $ e
hash e = H.lazyBytes . JE.encode . fst . fst . hashCons $ e
finalizeHash :: Term -> H.Hash
finalizeHash = H.finalize . hash