From e5839d2d9d2a8c9e9df7589d529e57d377572675 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 1 Jul 2016 19:32:21 -0700 Subject: [PATCH] Saw-core pretty printer can now introduce local let-blocks under lambdas. This means that shared subterms containing De Bruijn indices don't need to be printed multiple times. Fixes GaloisInc/saw-script#155. --- src/Verifier/SAW/SharedTerm.hs | 139 ++++++++++++++++++++------------ src/Verifier/SAW/Term/Pretty.hs | 47 +++++------ 2 files changed, 110 insertions(+), 76 deletions(-) diff --git a/src/Verifier/SAW/SharedTerm.hs b/src/Verifier/SAW/SharedTerm.hs index aeebc1e4..4e2cfc60 100644 --- a/src/Verifier/SAW/SharedTerm.hs +++ b/src/Verifier/SAW/SharedTerm.hs @@ -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) = @@ -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) diff --git a/src/Verifier/SAW/Term/Pretty.hs b/src/Verifier/SAW/Term/Pretty.hs index 69d84109..da282b18 100644 --- a/src/Verifier/SAW/Term/Pretty.hs +++ b/src/Verifier/SAW/Term/Pretty.hs @@ -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) @@ -327,28 +327,29 @@ 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') @@ -356,24 +357,24 @@ ppTermF' _opts pp lcls p (Lambda name tp 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 @@ -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 @@ -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.<$>