20070903-2

attach:Bad2.agda

running

  agda -v10 Bad2.agda

loops. As far as our analysis is concerned, pretty printing of the term

   bad2 x + bad2 (succ x)

hangs agda.

Pretty printing of terms is invoked in

  Termination/TermCheck.hs

  termTerm :: MutualNames -> QName -> [DeBruijnPat] -> Term -> TCM Calls
  termTerm names f pats0 t0 = do
    reportSDoc "term.check.clause" 10
      (sep [ text "termination checking clause of" <+> prettyTCM f
           , nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats0)
           , nest 2 $ text "rhs:" <+> prettyTCM t0
           ])

in

  prettyTCM t0