Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Saw-core pretty printer can now introduce local let-blocks under lamb…
Browse files Browse the repository at this point in the history 
…das.

This means that shared subterms containing De Bruijn indices don't need
to be printed multiple times.

Fixes GaloisInc/saw-script#155.
  • Loading branch information
Brian Huffman committed Jul 2, 2016
1 parent f6e5eb6 commit e5839d2
Show file tree
Hide file tree
Showing 2 changed files with 110 additions and 76 deletions.
139 changes: 86 additions & 53 deletions src/Verifier/SAW/SharedTerm.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -845,12 +845,14 @@ betaNormalize sc t0 =
--------------------------------------------------------------------------------
-- Pretty printing

type OccurrenceMap s = IntMap (Term, Word64)
type OccurrenceMap s = IntMap (Term, Int)

-- | Returns map that associates each term index appearing in the term
-- to the number of occurrences in the shared term.
scTermCount :: Term -> OccurrenceMap s
scTermCount t0 = execState (go [t0]) IntMap.empty
-- to the number of occurrences in the shared term. Subterms that are
-- on the left-hand side of an application are excluded. The boolean
-- flag indicates whether to descend under lambdas and other binders.
scTermCount :: Bool -> Term -> OccurrenceMap s
scTermCount doBinders t0 = execState (go [t0]) IntMap.empty
where go :: [Term] -> State (OccurrenceMap s) ()
go [] = return ()
go (t:r) =
Expand All @@ -868,57 +870,88 @@ scTermCount t0 = execState (go [t0]) IntMap.empty
where
recurse = do
let (h,args) = asApplyAll t
case unwrapTermF h of
Constant{} -> go (args ++ r)
tf -> go (Fold.foldr' (:) (args++r) tf)
go (Fold.foldr' (:) (args ++ r) (subterms h))
subterms h =
case unwrapTermF h of
Lambda _ t1 _ | not doBinders -> [t1]
Pi _ t1 _ | not doBinders -> [t1]
Let{} | not doBinders -> []
Constant{} -> []
tf -> Fold.toList tf

scPrettyTermDoc :: PPOpts -> Term -> Doc
scPrettyTermDoc opts t0
| null bound = ppTermDoc (ppt lcls0 PrecNone t0)
| otherwise = ppLetBlock lets (ppTermDoc (ppt lcls0 PrecNone t0))
where lcls0 = emptyLocalVarDoc
cm = scTermCount t0 -- Occurrence map
-- Return true if variable should be introduced to name term.
shouldName :: Term -> Word64 -> Bool
shouldName t c =
case unwrapTermF t of
FTermF GlobalDef{} -> False
FTermF UnitValue -> False
FTermF UnitType -> False
FTermF EmptyValue -> False
FTermF EmptyType -> False
FTermF (CtorApp _ []) -> False
FTermF (DataTypeApp _ []) -> False
FTermF NatLit{} -> False
FTermF (ArrayValue _ v) | V.length v == 0 -> False
FTermF FloatLit{} -> False
FTermF DoubleLit{} -> False
FTermF StringLit{} -> False
FTermF ExtCns{} -> False
LocalVar{} -> False
_ -> (c > 1) && (looseVars t == 0)

-- Terms bound in map.
bound :: [(TermIndex, Term)]
bound = [ (i, t) | (i, (t,c)) <- IntMap.assocs cm, shouldName t c ]

var :: Word64 -> Doc
var n = char 'x' <> integer (toInteger n)

lets = [ var n <+> char '=' <+> ppTermDoc (ppTermF opts ppt lcls0 PrecNone (unwrapTermF t)) <> char ';'
| ((_, t), n) <- bound `zip` [0..]
]

dm :: IntMap Doc
dm = Fold.foldl' insVar IntMap.empty (bound `zip` [0..])
where insVar m ((i, _), n) = IntMap.insert i (var n) m

ppt :: LocalVarDoc -> Prec -> Term -> TermDoc
ppt lcls p (Unshared tf) = ppTermF opts ppt lcls p tf
ppt lcls p (STApp{ stAppIndex = i, stAppTermF = tf}) =
case IntMap.lookup i dm of
Just d -> TermDoc d
Nothing -> ppTermF opts ppt lcls p tf
scPrettyTermDoc opts t0 =
ppLets lets0 (ppTermDoc (ppt (n0, dm0) False lcls0 PrecNone t0))
where
lcls0 = emptyLocalVarDoc

-- | Terms in top-level let block.
cm0 :: IntMap Term
cm0 =
IntMap.filter (\t -> looseVars t == 0) $ fmap fst $
IntMap.filter shouldName (scTermCount True t0) -- ^ Occurrence map

-- Terms bound in map.
bound0 :: [(TermIndex, Term)]
bound0 = IntMap.assocs cm0

lets0 = [ ppEqn m (n0, dm0) lcls0 PrecNone t | ((_, t), m) <- bound0 `zip` [0..] ]

dm0 :: IntMap Doc
dm0 = IntMap.fromList (zip (IntMap.keys cm0) (map var [0..]))

n0 :: Int
n0 = IntMap.size dm0

ppLets :: [Doc] -> Doc -> Doc
ppLets lets doc
| null lets = doc
| otherwise = ppLetBlock lets doc

-- | Return true if variable should be introduced to name term.
shouldName :: (Term, Int) -> Bool
shouldName (t, c) =
case unwrapTermF t of
FTermF GlobalDef{} -> False
FTermF UnitValue -> False
FTermF UnitType -> False
FTermF EmptyValue -> False
FTermF EmptyType -> False
FTermF (CtorApp _ []) -> False
FTermF (DataTypeApp _ []) -> False
FTermF NatLit{} -> False
FTermF (ArrayValue _ v) | V.length v == 0 -> False
FTermF FloatLit{} -> False
FTermF DoubleLit{} -> False
FTermF StringLit{} -> False
FTermF ExtCns{} -> False
LocalVar{} -> False
_ -> c > 1

var :: Int -> Doc
var n = char 'x' <> integer (toInteger n)

ppEqn :: Int -> (Int, IntMap Doc) -> LocalVarDoc -> Prec -> Term -> Doc
ppEqn m (n, dm) lcls p t =
var m <+> char '=' <+>
ppTermDoc (ppTermF opts (ppt (n, dm)) lcls p (unwrapTermF t)) <> char ';'

ppt :: (Int, IntMap Doc) -> Bool -> LocalVarDoc -> Prec -> Term -> TermDoc
ppt (n, dm) False lcls p (Unshared tf) = ppTermF opts (ppt (n, dm)) lcls p tf
ppt (n, dm) False lcls p (STApp{stAppIndex = i, stAppTermF = tf}) =
case IntMap.lookup i dm of
Just d -> TermDoc d
Nothing -> ppTermF opts (ppt (n, dm)) lcls p tf
ppt (n, dm) True lcls _p t =
TermDoc $ ppLets lets (ppTermDoc (ppt (n', dm') False lcls PrecNone t))
where
cm1 = fmap fst $ IntMap.filter shouldName (scTermCount False t)
cm = IntMap.difference cm1 dm0 -- remove already-named entries
dm1 = IntMap.fromList (zip (IntMap.keys cm) (map var [n ..]))
dm' = IntMap.union dm dm1
n' = n + IntMap.size cm
lets = [ ppEqn m (n', dm') lcls PrecNone rhs
| (rhs, m) <- IntMap.elems cm `zip` [n ..] ]

scPrettyTerm :: PPOpts -> Term -> String
scPrettyTerm opts t = show (scPrettyTermDoc opts t)
Expand Down
47 changes: 24 additions & 23 deletions src/Verifier/SAW/Term/Pretty.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,14 +177,14 @@ ppTypeConstraint :: TermPrinter e -> LocalVarDoc -> Doc -> e -> Doc
ppTypeConstraint f lcls sym tp = hang 2 $ group (sym <<$>> doublecolon <+> f lcls PrecLambda tp)

ppLocalDef :: Applicative f
=> (LocalVarDoc -> Prec -> e -> f Doc)
=> (Bool -> LocalVarDoc -> Prec -> e -> f Doc)
-> LocalVarDoc -- ^ Context outside let
-> LocalVarDoc -- ^ Context inside let
-> LocalDef e
-> f Doc
ppLocalDef pp lcls lcls' (Def nm _qual tp eqs) =
ppd <$> (pptc <$> pp lcls PrecLambda tp)
<*> traverse (ppDefEqnF pp lcls' sym) (reverse eqs)
ppd <$> (pptc <$> pp False lcls PrecLambda tp)
<*> traverse (ppDefEqnF (pp True) lcls' sym) (reverse eqs)
where sym = text nm
pptc tpd = hang 2 $ group (sym <<$>> doublecolon <+> tpd <> semi)
ppd tpd eqds = vcat (tpd : eqds)
Expand Down Expand Up @@ -327,53 +327,54 @@ ppFlatTermF :: Applicative f => PPOpts -> (Prec -> t -> f Doc) -> Prec -> FlatTe
ppFlatTermF opts pp prec tf = fmap ppTermDoc (ppFlatTermF' opts pp' prec tf)
where pp' p t = fmap TermDoc (pp p t)

ppTermF :: PPOpts -> (LocalVarDoc -> Prec -> t -> TermDoc)
ppTermF :: PPOpts
-> (Bool -> LocalVarDoc -> Prec -> t -> TermDoc) -- ^ Boolean indicates whether term is under a binder
-> LocalVarDoc -> Prec -> TermF t -> TermDoc
ppTermF opts pp lcls p tf = runIdentity (ppTermF' opts pp' lcls p tf)
where pp' l' p' t' = pure (pp l' p' t')
where pp' b' l' p' t' = pure (pp b' l' p' t')

ppTermF' :: Applicative f
=> PPOpts
-> (LocalVarDoc -> Prec -> e -> f TermDoc)
-> (Bool -> LocalVarDoc -> Prec -> t -> f TermDoc)
-> LocalVarDoc
-> Prec
-> TermF e
-> TermF t
-> f TermDoc
ppTermF' opts pp lcls prec (FTermF tf) = ppFlatTermF' opts (pp lcls) prec tf
ppTermF' opts pp lcls prec (FTermF tf) = ppFlatTermF' opts (pp False lcls) prec tf
--(group . nest 2) <$> (ppFlatTermF' (pp lcls) p tf)
ppTermF' _opts pp lcls prec (App l r) = ppApp <$> pp lcls PrecApp l <*> pp lcls PrecArg r
ppTermF' _opts pp lcls prec (App l r) = ppApp <$> pp False lcls PrecApp l <*> pp False lcls PrecArg r
where ppApp l' r' = TermDoc $ ppAppParens prec $ group $ hang 2 $
ppTermDoc l' Leijen.<$> ppTermDoc r'

ppTermF' _opts pp lcls p (Lambda name tp rhs) =
ppLam
<$> pp lcls PrecLambda tp
<*> pp lcls' PrecLambda rhs
<$> pp False lcls PrecLambda tp
<*> pp True lcls' PrecLambda rhs
where ppLam tp' rhs' = TermDoc $
ppParens (p > PrecLambda) $ group $ hang 2 $
text "\\" <> parens (text name' <> doublecolon <> ppTermDoc tp')
<+> text "->" Leijen.<$> ppTermDoc rhs'
name' = freshVariant (docUsedMap lcls) name
lcls' = consBinding lcls name'

ppTermF' _opts pp lcls p (Pi name tp rhs) = ppPi <$> lhs <*> pp lcls' PrecLambda rhs
ppTermF' _opts pp lcls p (Pi name tp rhs) = ppPi <$> lhs <*> pp True lcls' PrecLambda rhs
where ppPi lhs' rhs' = TermDoc $ ppParens (p > PrecLambda) $
lhs' <<$>> text "->" <+> ppTermDoc rhs'
subDoc = align . group . nest 2 . ppTermDoc
lhs | name == "_" = subDoc <$> pp lcls PrecApp tp
| otherwise = ppArg <$> pp lcls PrecLambda tp
lhs | name == "_" = subDoc <$> pp False lcls PrecApp tp
| otherwise = ppArg <$> pp False lcls PrecLambda tp
ppArg tp' = parens (text name' <+> doublecolon <+> subDoc tp')
name' = freshVariant (docUsedMap lcls) name
lcls' = consBinding lcls name'

ppTermF' _opts pp lcls p (Let dl u) =
ppLet <$> traverse (ppLocalDef pp' lcls lcls') dl
<*> pp lcls' PrecNone u
<*> pp True lcls' PrecNone u
where ppLet dl' u' = TermDoc $
ppParens (p > PrecNone) $ ppLetBlock dl' (ppTermDoc u')
nms = concatMap localVarNames dl
lcls' = foldl' consBinding lcls nms
pp' a b c = ppTermDoc <$> pp a b c
pp' a b c d = ppTermDoc <$> pp a b c d
ppTermF' _opts _pp lcls _p (LocalVar i)
-- | lcls^.docShowLocalTypes = pptc <$> pp lcls PrecLambda tp
| otherwise = pure $ TermDoc d
Expand All @@ -384,10 +385,10 @@ ppTermF' _ _ _ _ (Constant i _ _) = pure $ TermDoc $ text i

-- | Pretty print a term with the given outer precedence.
ppTermlike :: forall t. Termlike t => PPOpts -> LocalVarDoc -> Prec -> t -> Doc
ppTermlike opts lcls0 p0 trm = ppTermDoc (pp lcls0 p0 trm)
ppTermlike opts lcls0 p0 trm = ppTermDoc (pp False lcls0 p0 trm)
where
pp :: LocalVarDoc -> Prec -> t -> TermDoc
pp lcls p t = ppTermF opts pp lcls p (unwrapTermF t)
pp :: Bool -> LocalVarDoc -> Prec -> t -> TermDoc
pp _ lcls p t = ppTermF opts pp lcls p (unwrapTermF t)

showTermlike :: Termlike t => t -> String
showTermlike t = show $ ppTermlike defaultPPOpts emptyLocalVarDoc PrecNone t
Expand All @@ -396,11 +397,11 @@ ppTermDepth :: forall t. Termlike t => PPOpts -> Int -> t -> Doc
ppTermDepth opts d0 = pp d0 emptyLocalVarDoc PrecNone
where
pp :: Int -> TermPrinter t
pp d lcls p t = ppTermDoc (pp' d lcls p t)
pp d lcls p t = ppTermDoc (pp' d False lcls p t)

pp' :: Int -> LocalVarDoc -> Prec -> t -> TermDoc
pp' 0 _ _ _ = TermDoc $ text "_"
pp' d lcls p t = case unwrapTermF t of
pp' :: Int -> Bool -> LocalVarDoc -> Prec -> t -> TermDoc
pp' 0 _ _ _ _ = TermDoc $ text "_"
pp' d _ lcls p t = case unwrapTermF t of
App t1 t2 -> TermDoc $
ppAppParens p $ group $ hang 2 $
(pp d lcls PrecApp t1) Leijen.<$>
Expand Down

0 comments on commit e5839d2

Please sign in to comment.