content: {- |
  Module      :  ./Isabelle/IsaPrint.hs
  Description :  printing Isabelle entities
  Copyright   :  (c) University of Cambridge, Cambridge, England
                 adaption (c) Till Mossakowski, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Printing functions for Isabelle logic.
  -}
  
  module Isabelle.IsaPrint
      ( showBaseSig
      , printIsaTheory
      , getAxioms
      , printNamedSen
      , printTerm
      ) where
  
  import Isabelle.IsaSign
  import Isabelle.IsaConsts
  import Isabelle.Translate
  
  import Common.AS_Annotation
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Common.Doc hiding (bar)
  import Common.DocUtils
  import Common.Utils (number)
  
  import Data.Char
  import Data.List
  import Data.Maybe (isNothing, catMaybes)
  
  printIsaTheory :: String -> Sign -> [Named Sentence] -> Doc
  printIsaTheory tn sign sens = let
      b = baseSig sign
      bs = showBaseSig b
      ld = "$HETS_ISABELLE_LIB/"
      mlFileUse = text mlFileS <+> doubleQuotes (text $ ld ++ "prelude.ML")
      in text theoryS <+> text tn
      $+$ text importsS <+> fsep (case b of
          Custom_thy -> []
          _ -> if case b of
                  Main_thy -> False
                  HOLCF_thy -> False
                  Custom_thy -> True
                  _ -> True then [doubleQuotes $ text $ ld ++ bs] else [text bs]
        ++ map (doubleQuotes . text) (imports sign))
      $+$ text beginS
      $++$ mlFileUse
      $++$ printTheoryBody sign sens
      $++$ text endS
  
  printTheoryBody :: Sign -> [Named Sentence] -> Doc
  printTheoryBody sig sens =
   let (sens', recFuns) = findTypesForRecFuns sens (constTab sig)
       sig' = sig { constTab =
        Map.filterWithKey (\ k _ -> notElem (new k) recFuns) (constTab sig) }
   in callSetup "initialize" (brackets $ sepByCommas
        $ map (text . show . Quote . senAttr)
        $ filter (\ s -> not (isConstDef s || isRecDef s || isInstance s)
                  && senAttr s /= "") sens')
        $++$ printSign sig'
        $++$ printNamedSentences sens'
        $++$ printMonSign sig'
  
  findTypesForRecFuns :: [Named Sentence] -> ConstTab
   -> ([Named Sentence], [String])
  findTypesForRecFuns ns ctab =
   let (sens, recFuns') = unzip $ map (\ sen ->
        let (sen', recFns') =
             case sentence sen of
               RecDef kw cName cType tm ->
                (case Map.toList $
                   Map.filterWithKey (\ k _ -> new k == new cName) ctab of
                   (_, t) : _ ->
                    case cType of
                     Nothing ->
                      RecDef kw cName (Just t) tm
                     Just t' ->
                      if t /= t' then error "recFun: two types given"
                      else sentence sen
                   [] -> sentence sen
                , Just cName)
               _ -> (sentence sen, Nothing)
        in (sen {sentence = sen'}, recFns')) ns
   in (sens, map new $ catMaybes recFuns')
  
  printNamedSentences :: [Named Sentence] -> Doc
  printNamedSentences sens = case sens of
    [] -> empty
    s : r
      | isIsaAxiom s ->
        let (axs, rest) = span isAxiom sens in
        (if null axs then empty else text axiomatizationS $+$ text whereS)
        $+$ vcat (intersperse (text andS) $ map printNamedSen axs)
        $++$ vcat (map ( \ a -> text declareS <+> text (senAttr a)
                          <+> brackets (text simpS))
                   $ filter ( \ a -> case sentence a of
                         b@Sentence {} -> isSimp b && senAttr a /= ""
                         _ -> False) axs)
        $++$ printNamedSentences rest
      | isConstDef s ->
        let (defs_, rest) = span isConstDef sens in
        text defsS $+$ vsep (map printNamedSen defs_)
        $++$ printNamedSentences rest
      | otherwise ->
        printNamedSen s $++$ (case senAttr s of
          n | n == "" || isRecDef s -> empty
            | otherwise -> callSetup "record" (text $ show $ Quote n))
        $++$ printNamedSentences r
  
  callSetup :: String -> Doc -> Doc
  callSetup fun args =
      text "setup" <+> doubleQuotes (fsep [text ("Header." ++ fun), args])
  
  data QuotedString = Quote String
  instance Show QuotedString where
      show (Quote s) = init . tail . show $ show s
  
  getAxioms :: [Named Sentence] -> ([Named Sentence], [Named Sentence])
  getAxioms = partition isIsaAxiom
  
  isIsaAxiom :: Named Sentence -> Bool
  isIsaAxiom s = case sentence s of
    Sentence {} -> isAxiom s
    _ -> False
  
  isInstance :: Named Sentence -> Bool
  isInstance s = case sentence s of
    Instance {} -> True
    _ -> False
  
  isConstDef :: Named Sentence -> Bool
  isConstDef s = case sentence s of
    ConstDef {} -> True
    _ -> False
  
  isRecDef :: Named Sentence -> Bool
  isRecDef s = case sentence s of
    RecDef {} -> True
    _ -> False
  
  -- --------------------- Printing functions -----------------------------
  
  showBaseSig :: BaseSig -> String
  showBaseSig = takeWhile (/= '_') . show
  
  printClass :: IsaClass -> Doc
  printClass (IsaClass x) = text x
  
  printSort :: Sort -> Doc
  printSort = printSortAux False
  
  printSortAux :: Bool -> Sort -> Doc
  printSortAux b l = case l of
      [c] -> printClass c
      _ -> (if b then doubleQuotes else id)
        . braces . hcat . punctuate comma $ map printClass l
  
  data SynFlag = Quoted | Unquoted | Null
  
  doubleColon :: Doc
  doubleColon = text "::"
  
  isaEquals :: Doc
  isaEquals = text "=="
  
  bar :: [Doc] -> [Doc]
  bar = punctuate $ space <> text "|"
  
  printType :: Typ -> Doc
  printType = printTyp Unquoted
  
  printTyp :: SynFlag -> Typ -> Doc
  printTyp a = fst . printTypeAux a
  
  printTypeAux :: SynFlag -> Typ -> (Doc, Int)
  printTypeAux a t = case t of
   TFree v s -> (let
          d = text $ if isPrefixOf "\'" v || isPrefixOf "?\'" v
                                  then v else '\'' : v
          c = printSort s
       in if null s then d else case a of
           Quoted -> d <> doubleColon <> if null
                       $ tail s then c else doubleQuotes c
           Unquoted -> d <> doubleColon <> c
           Null -> d, 1000)
   TVar iv s -> printTypeAux a $ TFree (unindexed iv) s
   Type name _ args -> case args of
      [t1, t2] | elem name [prodS, sProdS, funS, cFunS, lFunS, sSumS] ->
         printTypeOp a name t1 t2
      _ -> ((case args of
             [] -> empty
             [arg] -> let (d, i) = printTypeAux a arg in
                        if i < 1000 then parens d else d
             _ -> parens $ hsep $ punctuate comma $
                         map (fst . printTypeAux a) args)
            <+> text name, 1000)
  
  printTypeOp :: SynFlag -> TName -> Typ -> Typ -> (Doc, Int)
  printTypeOp x name r1 r2 =
      let (d1, i1) = printTypeAux x r1
          (d2, i2) = printTypeAux x r2
          (l, r) = Map.findWithDefault (0 :: Int, 0 :: Int)
                      name $ Map.fromList
                      [ (funS, (1, 0))
                      , (cFunS, (1, 0))
                      , (lFunS, (1, 0))
                      , (sSumS, (11, 10))
                      , (prodS, (21, 20))
                      , (sProdS, (21, 20))
                      , (lProdS, (21, 20))
                      ]
          d3 = if i1 < l then parens d1 else d1
          d4 = if i2 < r then parens d2 else d2
      in (d3 <+> text name <+> d4, r)
  
  andDocs :: [Doc] -> Doc
  andDocs = vcat . prepPunctuate (text andS <> space)
  
  -- | printing a named sentence
  printNamedSen :: Named Sentence -> Doc
  printNamedSen ns =
    let s = sentence ns
        lab = senAttr ns
        b = isAxiom ns
        d = printSentence s
    in case s of
    TypeDef {} -> d
    RecDef {} -> d
    Lemmas {} -> d
    Instance {} -> d
    Locale {} -> d
    Class {} -> d
    Datatypes _ -> d
    Consts _ -> d
    TypeSynonym {} -> d
    Axioms _ -> d
    Lemma {} -> d
    Definition {} -> d
    Fun {} -> d
    Instantiation {} -> d
    InstanceProof {} -> d
    InstanceArity {} -> d
    InstanceSubclass {} -> d
    Subclass {} -> d
    Typedef {} -> d
    Defs {} -> d
    Fixrec {} -> d
    Domains {} -> d
    Primrec {} -> d
    _ -> let dd = doubleQuotes d in
         if isRefute s then text lemmaS <+> text lab <+> colon
                <+> dd $+$ text refuteS
         else if null lab then dd else fsep [ (case s of
      ConstDef {} -> text $ lab ++ "_def"
      Sentence {} ->
          (if b then empty else text theoremS)
          <+> text lab <+> (if b then text "[rule_format]" else
              if isSimp s then text "[simp]" else empty)
      _ -> error "printNamedSen") <+> colon, dd] $+$ case s of
      Sentence {} -> if b then empty else case thmProof s of
        Nothing -> text oopsS
        Just prf -> pretty prf
      _ -> empty
  
  -- | sentence printing
  printSentence :: Sentence -> Doc
  printSentence s = case s of
    TypeDef nt td pr -> text typedefS
                     <+> printType nt
                     <+> equals
                     <+> doubleQuotes (printSetDecl td)
                     $+$ pretty pr
    RecDef kw cName cType xs ->
      let preparedEq = map (doubleQuotes . printTerm) xs
          preparedEqWithBars =
            map (<+> text barS) (init preparedEq) ++ [last preparedEq]
          tp = case cType of
                Just t -> doubleColon <+> doubleQuotes (printType t)
                Nothing -> empty
          kw' = case kw of
                 Just str -> text str
                 Nothing -> text primrecS
      in kw' <+> text (new cName) <+> tp <+> printAlt cName <+> text whereS $+$
         vcat preparedEqWithBars
    Instance { tName = t, arityArgs = args, arityRes = res, definitions = defs_,
               instProof = prf } ->
        text instantiationS <+> text t <> doubleColon <> (case args of
          [] -> empty
          _ -> parens $ hsep $ punctuate comma $ map (printSortAux True) args)
          <+> printSortAux True res $+$ text beginS $++$ printDefs defs_ $++$
              text instanceS <+> pretty prf $+$ text endS
        where printDefs :: [(String, Term)] -> Doc
              printDefs defs' = vcat (map printDef defs')
              printDef :: (String, Term) -> Doc
              printDef (name, def) =
                  text definitionS <+>
                       printNamedSen (makeNamed name (ConstDef def))
  
    Sentence { isRefuteAux = b, metaTerm = t } -> printPlainMetaTerm (not b) t
    ConstDef t -> printTerm t
    Lemmas name lemmas -> if null lemmas
                          then empty {- only have this lemmas if we have some in
                                     the list -}
                          else text lemmasS <+> text name <+>
                               equals <+> sep (map text lemmas)
    l@(Locale {}) ->
     let h = text "locale" <+> text (show $ localeName l)
         parents = Data.List.intersperse (text "+") $
                    map (text . show) (localeParents l)
         (fxs, ass) = printContext $ localeContext l
     in printFixesAssumes h parents ass fxs
        $+$ printBody (localeBody l)
    c@(Class {}) ->
     let h = text "class" <+> text (show $ className c)
         parents = Data.List.intersperse (text "+") $
                    map (text . show) (classParents c)
         (fxs, ass) = printContext (classContext c)
     in printFixesAssumes h parents ass fxs
        $+$ printBody (classBody c)
    (Datatypes dts) -> if null dts then empty
                       else text "datatype" <+>
                          andDocs (map (\ d ->
                          let vars = map printType $ datatypeTVars d
                              name = text $ show $ datatypeName d
                              pretty_cs c =
                               let cname = case c of
                                    DatatypeNoConstructor {} -> ""
                                    _ -> show $ constructorName c
                                   cname' = if any isSpace cname
                                            then doubleQuotes (text cname)
                                            else text cname
                                   tps = map (doubleQuotes . printType) $
                                           constructorArgs c
                               in hsep (cname' : tps)
                              cs = map pretty_cs $ datatypeConstructors d
                          in hsep vars <+> name <+> text "=" <+>
                             fsep (bar cs)) dts)
    Domains ds -> if null ds then empty
                  else text "domain" <+>
                   andDocs (map (\ d ->
                    let vars = map printType $ domainTVars d
                        name = text $ show $ domainName d
                        pretty_cs c =
                         let cname = text $ show $ domainConstructorName c
                             args' = map (\ arg ->
                              (if domainConstructorArgLazy arg
                               then text "lazy" else empty) <+>
                              (case domainConstructorArgSel arg of
                                Just sel -> text (show sel) <+> text "::"
                                Nothing -> empty) <+> (doubleQuotes . printType)
                              (domainConstructorArgType arg)) $
                              domainConstructorArgs c
                             args = map parens args'
                         in hsep $ cname : args
                        cs = map pretty_cs $ domainConstructors d
                    in hsep vars <+> name <+> text "=" <+>
                       fsep (bar cs)) ds)
    Consts cs -> if null cs then empty
                 else vsep $ text "consts" :
                       map (\ (n, _, t) -> text n <+> text "::" <+>
                                      doubleQuotes (printType t)) cs
    TypeSynonym n _ vs tp -> hsep $ [text "type_synonym",
                                   text $ show n, text "="] ++ map text vs
                                  ++ [doubleQuotes . printType $ tp]
    Axioms axs -> if null axs then empty
                  else vsep $ text "axioms" :
                        map (\ a -> text (show $ axiomName a) <+>
                                   (if axiomArgs a /= ""
                                    then brackets (text $ axiomArgs a)
                                    else empty) <+> text ":" <+>
                                   doubleQuotes (printTerm $ axiomTerm a)) axs
    l@(Lemma {}) ->
     let (fxs, ass) = printContext $ lemmaContext l
     in text "lemma" <+> (case lemmaTarget l of
                             Just t -> braces (text "in" <+> text (show t))
                             Nothing -> empty) <+>
                             (case (null fxs, null ass, lemmaProps l) of
                              (True, True, [sh]) -> printProps sh
                              _ -> vsep (fxs ++ ass ++
                                    [text "shows" <+> andDocs
                                      (map printProps (lemmaProps l))]))
        $+$ (case lemmaProof l of
              Just p -> text p
              Nothing -> empty)
    d@(Definition {}) -> fsep [text "definition" <+>
     (case definitionTarget d of
       Just t -> braces (text "in" <+> text (show t))
       Nothing -> empty) <+>
     (text (show $ definitionName d) <+> text "::" <+>
      doubleQuotes (printType $ definitionType d)), text "where" <+>
     doubleQuotes (text (show $ definitionName d) <+> hsep (map printTerm (
      definitionVars d)) <+> text "=" <+> printTerm (definitionTerm d))]
    f@(Fun {}) -> text "fun" <+> (case funTarget f of
     Just t -> braces (text "in" <+> text (show t))
     Nothing -> empty) <+> (if funDomintros f then braces (text "domintros")
      else empty) <+> vcat (intersperse (text andS) $
       map (\ (name, mx, tp, _) -> text name <+> text "::" <+>
       doubleQuotes (printType tp) <+> case mx of
                        Just (Mixfix _ _ s' _) -> doubleQuotes (text s')
                        _ -> empty) (funEquations f)) <+> text "where" $+$
      (let eqs = concatMap (\ (name, _, _, e) -> map (\ e' -> (name, e')) e)
                               (funEquations f)
           eqs' = map (\ (n, (vs, t)) -> doubleQuotes (text n <+>
                   hsep (map printTerm vs) <+>
                   text "=" <+> printTerm t)) eqs
       in fsep $ bar eqs')
    i@(Instantiation {}) -> fsep $ (text "instantiation" <+> text
     (instantiationType i) <+> text "::" <+> printArity (instantiationArity i)) :
      [printBody (instantiationBody i)]
    InstanceProof prf -> text "instance" $+$ text prf
    i@(InstanceArity {}) -> text "instance" <+>
     hcat (intersperse (text "and") $ map text $ instanceTypes i) <+>
     printArity (instanceArity i) $+$ text (instanceProof i)
    i@(InstanceSubclass {}) -> text "instance" <+> text (instanceClass i) <+>
     text (instanceRel i) <+> text (instanceClass1 i) $+$ text (instanceProof i)
    c@(Subclass {}) -> text "subclass" <+> (case subclassTarget c of
                             Just t -> braces (text "in" <+> text (show t))
                             Nothing -> empty) <+> text (subclassClass c)
                            <+> text (subclassProof c)
    t@(Typedef {}) -> text "typedef" <+> (case typedefVars t of
                       [] -> empty
                       [v] -> printVarWithSort v
                       vs -> parens $ hsep $ punctuate comma $
                             map printVarWithSort vs) <+>
                      text (show $ typedefName t) <+> text "=" <+>
                      doubleQuotes (printTerm $ typedefTerm t) <+>
                      (case typedefMorphisms t of
                        Just (m1, m2) -> text "morphisms" <+> text (show m1)
                                       <+> text (show m2)
                        Nothing -> empty) $+$ text (typedefProof t)
    d@(Defs {}) -> fsep $ (text "defs" <+> (if defsUnchecked d
                                            then text "unchecked"
                                            else empty) <+>
                                           (if defsOverloaded d
                                            then text "overloaded"
                                            else empty))
     : map (\ eq' ->
         text (show (defEquationName eq')) <+> text ":" <+> doubleQuotes (
          text (defEquationConst eq') <+> text "==" <+>
          printTerm (defEquationTerm eq')) <+> if null (defEquationArgs eq')
          then empty else brackets (text $ defEquationArgs eq')) (defsEquations d)
    Fixrec fs ->
     let h = map (\ (name, _, tp, _) -> text name <+> text "::" <+>
                                    (doubleQuotes . printType) tp) fs
         pretty_fixreceq name eq' =
          let unchecked = if fixrecEquationUnchecked eq' then
                          text "(unchecked)" else empty
              premises = fixrecEquationPremises eq'
              p s' = punctuate $ space <> text s'
              patterns = map (parens . printTerm) $ fixrecEquationPatterns eq'
              tm = printTerm $ fixrecEquationTerm eq'
          in unchecked <+> doubleQuotes (printTermWithPremises premises
              (hsep (p "\\<cdot>" (text name : patterns)) <+> text "=" <+> tm))
         body = concatMap (\ (name, _, _, eqs) -> map (pretty_fixreceq name) eqs)
                 fs
     in text "fixrec" <+> andDocs h <+> text "where" $+$ fsep (bar body)
    Primrec t eqs ->
                  let h = map (\ (name, _, tp, _) -> text name <+> text "::" <+>
                                (doubleQuotes . printType) tp) eqs
                      pretty_primrec name (vs, tm) = doubleQuotes (text name
                       <+> hsep (map printTerm vs) <+> text "=" <+> printTerm tm)
                      body = concatMap (\ (name, _, _, tms) ->
                              map (pretty_primrec name) tms) eqs
                  in text "primrec" <+> (case t of
                             Just t' -> braces (text "in" <+> text (show t'))
                             Nothing -> empty) <+> andDocs h <+> text "where"
                     $+$ fsep (bar body)
  
  printTermWithPremises :: [Term] -> Doc -> Doc
  printTermWithPremises ps t =
   let p s = punctuate $ space <> text s
   in fsep $ p "\\<Longrightarrow>" (map printTerm ps ++ [t])
  
  printArity :: (Sort, [Sort]) -> Doc
  printArity (sort', sorts) = parens (hsep $ punctuate comma $
                             map (printSortAux True) sorts) <+> printSort sort'
  
  printVarWithSort :: (String, Sort) -> Doc
  printVarWithSort (name, []) = text name
  printVarWithSort (name, sort') = text name <+> printSortAux True sort'
  
  printBody :: [Sentence] -> Doc
  printBody sens = fsep $ if null sens then []
                 else [text "begin"] ++ map printSentence sens ++ [text "end"]
  
  printContext :: Ctxt -> ([Doc], [Doc])
  printContext ctxt =
   let fixes' = map (\ (n, _, tp) -> if n == "" then empty else text n
                         <+> text "::" <+> (doubleQuotes . printTyp Null) tp)
                       (fixes ctxt)
       assumes' = map (\ (n, tm) -> if n == "" then empty else text n <+> text ":"
                         <+> (doubleQuotes . printTerm) tm)
                       (assumes ctxt)
   in (fixes', assumes')
  
  printProps :: Props -> Doc
  printProps (Props {propsName = n, propsArgs = a, props = p}) =
   printMaybe (text . show) n <+> printMaybe text a
   <+> (if isNothing n && isNothing a
        then empty else text ":") <+>
       vcat (map printProp p)
  
  printProp :: Prop -> Doc
  printProp (Prop {prop = t, propPats = ts}) =
   let t' = doubleQuotes $ printTerm t
       ts' = hsep $ map (\ p -> text "is" <+> (doubleQuotes . printTerm) p) ts
   in t' <+> if null ts then empty
             else parens ts'
  
  printSetDecl :: SetDecl -> Doc
  printSetDecl setdecl =
      case setdecl of
        SubSet v t f -> braces $ printTerm v <> doubleColon <> printType t <> dot
                        <+> printTerm f
        FixedSet elems -> braces $ sepByCommas $ map printTerm elems
  
  printPlainMetaTerm :: Bool -> MetaTerm -> Doc
  printPlainMetaTerm b mt = case mt of
      Term t -> printPlainTerm b t
      Conditional conds t -> sep
        [ text premiseOpenS
          <+> fsep (punctuate semi $ map printTerm conds)
          <+> text premiseCloseS
        , text metaImplS <+> printTerm t ]
  
  -- | print plain term
  printTerm :: Term -> Doc
  printTerm = printPlainTerm True
  
  printPlainTerm :: Bool -> Term -> Doc
  printPlainTerm b = fst . printTrm b
  
  -- | print parens but leave a space if doc starts or ends with a bar
  parensForTerm :: Doc -> Doc
  parensForTerm d =
      let s = show d
          b = '|'
      in parens $ if null s then d
                  else (if head s == b then (space <>) else id)
                           ((if last s == b then (<> space) else id) d)
  
  printParenTerm :: Bool -> Int -> Term -> Doc
  printParenTerm b i t = case printTrm b t of
      (d, j) -> if j < i then parensForTerm d else d
  
  flatTuplex :: [Term] -> Continuity -> [Term]
  flatTuplex cs c = case cs of
      [] -> cs
      _ -> case last cs of
             Tuplex rs@(_ : _ : _) d | d == c -> init cs ++ flatTuplex rs d
             _ -> cs
  
  printMixfixAppl :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
  printMixfixAppl b c f args = case f of
          Const (VName n (Just (AltSyntax s is i))) (Hide {}) ->
               if length is == length args &&
                  (b || n == cNot || isPrefixOf "op " n) then
                     (fsep $ replaceUnderlines s
                       $ zipWith (printParenTerm b) is args, i)
               else printApp b c f args
          Const vn _ | new vn `elem` [allS, exS, ex1S] -> case args of
              [Abs v t _] -> (fsep [text (new vn) <+> printPlainTerm False v
                      <> dot
                      , printPlainTerm b t], lowPrio)
              _ -> printApp b c f args
          App g a d | c == d -> printMixfixAppl b c g (a : args)
          _ -> printApp b c f args
  
  -- | print the term using the alternative syntax (if True)
  printTrm :: Bool -> Term -> (Doc, Int)
  printTrm b trm = case trm of
      Const vn ty -> let
          dvn = text $ new vn
          nvn = case ty of
              Hide {} -> dvn
              Disp w _ _ -> parens $ dvn <+> doubleColon <+> printType w
        in case altSyn vn of
            Nothing -> (nvn, maxPrio)
            Just (AltSyntax s is i) -> if b && null is then
                (fsep $ replaceUnderlines s [], i) else (nvn, maxPrio)
      Free vn -> (text $ new vn, maxPrio)
      Abs v t c -> (text (case c of
          NotCont -> "%"
          IsCont _ -> "Lam") <+> printPlainTerm False v <> dot
                      <+> printPlainTerm b t, lowPrio)
      If i t e c -> let d = fsep [printPlainTerm b i,
                          text (case c of
                                   NotCont -> "then"
                                   IsCont _ -> "THEN")
                              <+> printPlainTerm b t,
                          text (case c of
                                   NotCont -> "else"
                                   IsCont _ -> "ELSE")
                              <+> printPlainTerm b e]
                    in case c of
          NotCont -> (text "if" <+> d, lowPrio)
          IsCont _ -> (text "IF" <+> d <+> text "FI", maxPrio)
      Case e ps -> (text "case" <+> printPlainTerm b e <+> text "of"
          $+$ vcat (bar $ map (\ (p, t) ->
                 fsep [ printPlainTerm b p <+> text "=>"
                      , printParenTerm b (lowPrio + 1) t]) ps), lowPrio)
      Let es i -> (fsep [text "let" <+>
             vcat (punctuate semi $
                 map (\ (p, t) -> fsep [ printPlainTerm b p <+> equals
                                         , printPlainTerm b t]) es)
             , text "in" <+> printPlainTerm b i], lowPrio)
      IsaEq t1 t2 ->
          (fsep [ printParenTerm b (isaEqPrio + 1) t1 <+> isaEquals
                           , printParenTerm b isaEqPrio t2], isaEqPrio)
      Tuplex cs c -> case c of
          NotCont -> (parensForTerm
                        $ sepByCommas (map (printPlainTerm b)
                            $ flatTuplex cs c)
                      , maxPrio)
          IsCont _ -> case cs of
                          [] -> error "IsaPrint, printTrm"
                          [a] -> printTrm b a
                          a : aa -> printTrm b $ App (App
                                    lpairTerm a $ IsCont False)
                                       (Tuplex aa c) (IsCont False)
      App f a c -> printMixfixAppl b c f [a]
      Set setdecl -> (printSetDecl setdecl, lowPrio)
  
  printApp :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
  printApp b c t l = case l of
       [] -> printTrm b t
       _ -> printDocApp b c (printParenTerm b (maxPrio - 1) t) l
  
  printDocApp :: Bool -> Continuity -> Doc -> [Term] -> (Doc, Int)
  printDocApp b c d l =
      ( fsep $ (case c of
          NotCont -> id
          IsCont True -> punctuate $ text " $$"
          IsCont False -> punctuate $ text " $")
            $ d : map (printParenTerm b maxPrio) l
      , maxPrio - 1)
  
  replaceUnderlines :: String -> [Doc] -> [Doc]
  replaceUnderlines str l = case str of
      "" -> []
      '\'' : r@(q : s) -> if q `elem` "_/'()"
                         then consDocBarSep (text [q]) $ replaceUnderlines s l
                         else consDocBarSep (text "'") $ replaceUnderlines r l
      '_' : r -> case l of
                    h : t -> consDocBarSep h $ replaceUnderlines r t
                    _ -> error "replaceUnderlines"
      '/' : ' ' : r -> empty : replaceUnderlines r l
      q : r -> if q `elem` "()/" then replaceUnderlines r l
               else consDocBarSep (text [q]) $ replaceUnderlines r l
  
  consDocBarSep :: Doc -> [Doc] -> [Doc]
  consDocBarSep d r = case r of
    [] -> [d]
    h : t -> let
      b = '|'
      hs = show h
      ds = show d
      hhs = head hs
      lds = last ds
      in if null hs || null ds then (d <> h) : t else
             if hhs == b && lds == '(' || last ds == b && hhs == ')'
             then (d <+> h) : t
             else (d <> h) : t
  
  -- end of term printing
  
  printLocales :: Locales -> Doc
  printLocales = vsep . map printLocale . orderLDecs . Map.toList
  
  printDefinitions :: Defs -> Doc
  printDefinitions = vsep . map printDefinition . Map.toList
  
  printFunctions :: Funs -> Doc
  printFunctions = vsep . map printFunction . Map.toList
  
  printFixesAssumes :: Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
  printFixesAssumes h p' a f = vcat
    [ h <+> (if null $ p' ++ a ++ f then empty else text "=") <+> hsep p'
      <+> if null p' || null a && null f then empty else text "+"
    , if null f then empty else text "fixes" <+> andDocs f
    , if null a then empty else text "assumes" <+> andDocs a
    ]
  
  printDefinition :: (String, Def) -> Doc
  printDefinition (n, (tp, vs, tm)) = text "definition" <+> text n <+> text "::"
   $+$ (doubleQuotes . printTyp Null) tp <+> text "where"
   $+$ doubleQuotes (text n <+> hsep (map (text . fst) vs)
   <+> text "\\<equiv>" <+> printTerm tm)
  
  printFunction :: (String, FunDef) -> Doc
  printFunction (n, (tp, def_eqs)) = text "fun" <+> text n <+> text "::"
   $+$ (doubleQuotes . printTyp Null) tp <+> text "where"
   $+$ (vcat . punctuate (text "|"))
        (map (\ (pats, tm) -> doubleQuotes $ text n
         <+> hsep (map printTerm pats) <+> text "="
         <+> printTerm tm) def_eqs)
  
  printLocale :: (String, LocaleDecl) -> Doc
  printLocale (n, (parents, in_ax, ex_ax, params)) =
   let p' = Data.List.intersperse (text "+") $ map text parents
       a = map (\ (s, t) -> text s <+> text ":"
             <+> (doubleQuotes . printTerm) t) in_ax
       f = map (\ (s, t, alt) -> text s <+> text "::"
                   <+> (doubleQuotes . printTyp Null) t
                   <+> (case alt of
                         Just (AltSyntax s' [i1, i2] i) -> parens (
                          text (if i1 == i2 then "infix "
                          else if i1 < i2 then "infixr "
                          else "infixl ") <+> doubleQuotes (text s')
                          <+> text (show i))
                         _ -> empty
                   )) params
   in vcat [
       printFixesAssumes (text "locale" <+> text n) p' a f,
       vcat (map (\ (s, t) -> text ("theorem (in " ++ n ++ ")")
             <+> text s <+> text ":"
             <+> (doubleQuotes . printTerm) t
             <+> text "apply(auto)"
             <+> text "done") ex_ax)]
  
  printClassrel :: Classrel -> Doc
  printClassrel = vsep . map printClassR . orderCDecs . Map.toList
  
  printClassR :: (IsaClass, ClassDecl) -> Doc
  printClassR (y, (parents, assumptions, fxs)) =
   let a = map (\ (s, t) -> text s <+> text ":"
            <+> (doubleQuotes . printTerm) t) assumptions
       f = map (\ (s, t) -> text s <+> text "::"
            <+> (doubleQuotes . printTyp Null) t) fxs
       parents' = filter (\ (IsaClass s) -> notElem s
         ["HOL.type_class", "HOL.type", "type", "type_class"]) parents
       p' = Data.List.intersperse (text "+") $ map printClass parents'
   in printFixesAssumes (text "class" <+> printClass y) p' a f
  
  orderCDecs :: [(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)]
  orderCDecs =
     topSort crord
   where
     crord (_, (cs, _, _)) (c, _) = elem c cs
  
  orderLDecs :: [(String, LocaleDecl)] -> [(String, LocaleDecl)]
  orderLDecs =
     topSort crord
   where
     crord (_, (cs, _, _, _)) (c, _) = elem c cs
  
  printMonArities :: String -> Arities -> Doc
  printMonArities tn = vcat . map ( \ (t, cl) ->
                    vcat $ map (printThMorp tn t) cl) . Map.toList
  
  printThMorp :: String -> TName -> (IsaClass, [(Typ, Sort)]) -> Doc
  printThMorp tn t xs = case xs of
     (IsaClass "Monad", _) ->
        if isSuffixOf "_mh" tn || isSuffixOf "_mhc" tn
        then printMInstance tn t
        else error "IsaPrint, printInstance: monads not supported"
     _ -> empty
  
  printMInstance :: String -> TName -> Doc
  printMInstance tn t = let nM = text (t ++ "_tm")
                            nM2 = text (t ++ "_tm2")
   in prnThymorph nM "MonadType" tn t [("MonadType.M", "'a")] []
      $+$ text "t_instantiate MonadOps mapping" <+> nM
      $+$ text "renames:" <+>
         brackMapList (\ x -> t ++ "_" ++ x)
              [("MonadOpEta.eta", "eta"), ("MonadOpBind.bind", "bind")]
      $+$ text "without_syntax"
      $++$ text "defs "
      $+$ text (t ++ "_eta_def:") <+> doubleQuotes
            (text (t ++ "_eta") <+> isaEquals <+> text ("return_" ++ t))
      $+$ text (t ++ "_bind_def:") <+> doubleQuotes
            (text (t ++ "_bind") <+> isaEquals <+> text ("mbind_" ++ t))
      $++$ lunitLemma t
      $+$ runitLemma t
      $+$ assocLemma t
      $+$ etaInjLemma t
      $++$ prnThymorph nM2 "MonadAxms" tn t [("MonadType.M", "'a")]
          [("MonadOpEta.eta", t ++ "_eta"),
           ("MonadOpBind.bind", t ++ "_bind")]
      $+$ text "t_instantiate Monad mapping" <+> nM2
      $+$ text "renames:" <+>
         brackMapList (\ x -> t ++ "_" ++ x)
             [("Monad.kapp", "kapp"),
              ("Monad.lift", "lift"),
              ("Monad.lift", "lift"),
              ("Monad.mapF", "mapF"),
              ("Monad.bind'", "mbbind"),
              ("Monad.joinM", "joinM"),
              ("Monad.kapp2", "kapp2"),
              ("Monad.kapp3", "kapp3"),
              ("Monad.lift2", "lift2"),
              ("Monad.lift3", "lift3")]
      $+$ text "without_syntax"
      $++$ text " "
   where
    lunitLemma w = text lemmaS <+> text (w ++ "_lunit:")
          <+> doubleQuotes (text (w ++ "_bind")
          <+> parens (text (w ++ "_eta x"))
          <+> parens (text $ "t::'a => 'b " ++ w)
          <+> equals <+> text "t x")
      $+$ text "sorry "
    runitLemma w = text lemmaS <+> text (w ++ "_runit:")
          <+> doubleQuotes (text (w ++ "_bind")
          <+> parens (text $ "t::'a " ++ w) <+> text (w ++ "_eta")
          <+> equals <+> text "t")
      $+$ text "sorry "
    assocLemma w = text lemmaS <+> text (w ++ "_assoc:")
          <+> doubleQuotes (text (w ++ "_bind")
          <+> parens (text (w ++ "_bind")
          <+> parens (text $ "s::'a " ++ w) <+> text "t") <+> text "u"
          <+> equals <+> text (w ++ "_bind s")
          <+> parens (text "%x." <+>
                   text (w ++ "_bind") <+> text "(t x) u"))
      $+$ text "sorry "
    etaInjLemma w = text lemmaS <+> text (w ++ "_eta_inj:")
          <+> doubleQuotes (parens (text $ w ++ "_eta::'a => 'a " ++ w)
               <+> text "x"
               <+> equals <+> text (w ++ "_eta y")
               <+> text "==>" <+> text "x = y")
      $+$ text "sorry "
  
  prnThymorph :: Doc -> String -> String -> TName -> [(String, String)]
              -> [(String, String)] -> Doc
  prnThymorph nm xn tn t ts ws = let qual s = tn ++ "." ++ s in
       text "thymorph" <+> nm <+> colon <+>
              text xn <+> cfun <+> text tn
       $+$ text "  maps" <+> brackets
         (hcat [ parens $ doubleQuotes (text b <+> text a) <+> mapsto
                 <+> doubleQuotes (text b <+> text (qual t))
               | (a, b) <- ts])
       $+$ brackMapList qual ws
  
  brackMapList :: (String -> String) -> [(String, String)] -> Doc
  brackMapList f ws = brackets $ hsep $ punctuate comma
    [ parens $ doubleQuotes (text a) <+> mapsto <+> doubleQuotes (text $ f b)
    | (a, b) <- ws]
  
  -- filter out types that are given in the domain table
  printTypeDecls :: BaseSig -> DomainTab -> Arities -> Doc
  printTypeDecls bs odt ars =
      let dt = Map.fromList $ map (\ (t, _) -> (typeId t, [])) $ concat odt
      in vcat $ map (printTycon bs) $ Map.toList $ Map.difference ars dt
  
  printTycon :: BaseSig -> (TName, [(IsaClass, [(Typ, Sort)])]) -> Doc
  printTycon bs (t, arity') = case arity' of
    [] -> error "IsaPrint.printTycon"
    (_, rs) : _ ->
           if Set.member t
                $ Map.findWithDefault (error "Isabelle.printTycon") bs
                  $ preTypes isaPrelude
           then empty else
              text typedeclS <+>
              (if null rs then empty else
               parens $ hsep $ punctuate comma
               $ map (text . ("'a" ++) . show . snd) $ number rs) <+> text t
  
  -- | show alternative syntax (computed by comorphisms)
  printAlt :: VName -> Doc
  printAlt (VName _ altV) = case altV of
      Nothing -> empty
      Just (AltSyntax s is i) -> parens $ doubleQuotes (text s)
          <+> if null is then empty else text (show is) <+>
              if i == maxPrio then empty else text (show i)
  
  instance Pretty Sign where
      pretty = printSign
  
  -- | a dummy constant table with wrong types
  constructors :: DomainTab -> ConstTab
  constructors = Map.fromList . map (\ v -> (v, noTypeT))
                 . concatMap (map fst . snd) . concat
  
  printMonSign :: Sign -> Doc
  printMonSign sig = let ars = arities $ tsig sig
                  in
      printMonArities (theoryName sig) ars
  
  printSign :: Sign -> Doc
  printSign sig = let dt = ordDoms $ domainTab sig
                      ars = arities $ tsig sig
                  in
      printAbbrs (abbrs $ tsig sig) $++$
      printTypeDecls (baseSig sig) dt ars $++$
      printDefinitions (defs $ tsig sig) $++$
      printFunctions (funs $ tsig sig) $++$
      printLocales (locales $ tsig sig) $++$
      printClassrel (classrel $ tsig sig) $++$
      printDomainDefs dt $++$
      printConstTab (Map.difference (constTab sig)
                    $ constructors dt) $++$
      (if showLemmas sig
           then showCaseLemmata dt else empty)
      where
      printAbbrs tab = if Map.null tab then empty else text typesS
                       $+$ vcat (map printAbbr $ Map.toList tab)
      printAbbr (n, (vs, t)) = case vs of
          [] -> empty
          [x] -> text ('\'' : x)
          _ -> parens $ hsep $ punctuate comma $
                                     map (text . ('\'' :)) vs
        <+> text n <+> equals <+> doubleQuotes (printType t)
      printConstTab tab = if Map.null tab then empty else text constsS
                          $+$ vcat (map printConst $ Map.toList tab)
      printConst (vn, t) = text (new vn) <+> doubleColon <+>
                            doubleQuotes (printType t) <+> printAlt vn
      isDomain = case baseSig sig of
                 HOLCF_thy -> True
                 HsHOLCF_thy -> True
                 MHsHOLCF_thy -> True
                 _ -> False
      printDomainDefs dtDefs = vcat $ map printDomainDef dtDefs
      printDomainDef dts = if null dts then empty else
          text (if isDomain then domainS else datatypeS)
          <+> andDocs (map printDomain dts)
      printDomain (t, ops) =
         printTyp (if isDomain then Quoted else Null) t <+> equals <+>
         fsep (bar $ map printDOp ops)
      printDOp (vn, args) = let opname = new vn in
         text (if any isSpace opname then show opname else opname)
         <+> hsep (map (printDOpArg opname) $ number args)
         <+> printAlt vn
      printDOpArg o (a, i) = let
        d = case a of
              TFree _ _ -> printTyp Null a
              _ -> doubleQuotes $ printTyp Null a
        in if isDomain then
             parens $ text "lazy" <+>
                 text (o ++ "_" ++ show i) <> doubleColon <> d
             else d
      showCaseLemmata dtDefs = text (concatMap showCaseLemmata1 dtDefs)
      showCaseLemmata1 = concatMap showCaseLemma
      showCaseLemma (_, []) = ""
      showCaseLemma (tyCons, c : cns) =
        let cs = "case caseVar of" ++ sp
            sc b = showCons b c ++ concatMap (("   | " ++) . showCons b) cns
            clSome = sc True
            cl = sc False
            showCons b (VName {new = cName}, args) =
              let pat = cName ++ concatMap ((sp ++) . showArg) args
                              ++ sp ++ "=>" ++ sp
                  term = showCaseTerm cName args
              in
                 pat ++ if b then "Some" ++ sp ++ lb ++ term ++ rb ++ "\n"
                   else term ++ "\n"
            showCaseTerm name args = case name of
              "" -> sa
              n : _ -> toLower n : sa
              where sa = concatMap ((sp ++) . showArg) args
            showArg (TFree [] _) = "varName"
            showArg (TFree (n : ns) _) = toLower n : ns
            showArg (TVar v s) = showArg (TFree (unindexed v) s)
            showArg (Type [] _ _) = "varName"
            showArg (Type m@(n : ns) _ s) =
              if elem m ["typeAppl", "fun", "*"]
                 then concatMap showArg s
                 else toLower n : ns
            showName (TFree v _) = v
            showName (TVar v _) = unindexed v
            showName (Type n _ _) = n
            proof' = "apply (case_tac caseVar)\napply (auto)\ndone\n"
        in
          lemmaS ++ sp ++ "case_" ++ showName tyCons ++ "_SomeProm" ++ sp
                  ++ "[simp]:\"" ++ sp ++ lb ++ cs ++ clSome ++ rb ++ sp
                  ++ "=\n" ++ "Some" ++ sp ++ lb ++ cs ++ cl ++ rb ++ "\"\n"
                  ++ proof'
  
  instance Pretty Sentence where
      pretty = printSentence
  
  sp :: String
  sp = " "
  
  rb :: String
  rb = ")"
  
  lb :: String
  lb = "("
  
  -- Pretty printing of proofs
  
  instance Pretty IsaProof where
      pretty = printIsaProof
  
  printIsaProof :: IsaProof -> Doc
  printIsaProof (IsaProof p e) = fsep $ map pretty p ++ [pretty e]
  
  instance Pretty ProofCommand where
      pretty = printProofCommand
  
  printProofCommand :: ProofCommand -> Doc
  printProofCommand pc =
      case pc of
        Apply pms plus ->
            let plusDoc = if plus then text "+" else empty
            in text applyS <+> parens
                                (sepByCommas $ map pretty pms) <> plusDoc
        Using ls -> text usingS <+> fsep (map text ls)
        Back -> text backS
        Defer x -> text deferS <+> pretty x
        Prefer x -> text preferS <+> pretty x
        Refute -> text refuteS
  
  instance Pretty ProofEnd where
      pretty = printProofEnd
  
  printProofEnd :: ProofEnd -> Doc
  printProofEnd pe =
      case pe of
        By pm -> text byS <+> parens (pretty pm)
        DotDot -> text dotDot
        Done -> text doneS
        Oops -> text oopsS
        Sorry -> text sorryS
  
  instance Pretty Modifier where
      pretty = printModifier
  
  printModifier :: Modifier -> Doc
  printModifier m =
      case m of
        No_asm -> text "no_asm"
        No_asm_simp -> text "no_asm_simp"
        No_asm_use -> text "no_asm_use"
  
  instance Pretty ProofMethod where
      pretty = printProofMethod
  
  printProofMethod :: ProofMethod -> Doc
  printProofMethod pm =
      case pm of
        Auto -> text autoS
        Simp -> text simpS
        AutoSimpAdd m names -> let modDoc = case m of
                                              Just mod' -> parens $ pretty mod'
                                              Nothing -> empty
                               in fsep $ [text autoS, text simpS, modDoc,
                                               text "add:"] ++ map text names
        SimpAdd m names -> let modDoc = case m of
                                          Just mod' -> parens $ pretty mod'
                                          Nothing -> empty
                           in fsep $ [text simpS, modDoc, text "add:"] ++
                              map text names
        Induct var -> text inductS <+> doubleQuotes (printTerm var)
        CaseTac t -> text caseTacS <+> doubleQuotes (printTerm t)
        SubgoalTac t -> text subgoalTacS <+> doubleQuotes (printTerm t)
        Insert ts -> fsep (text insertS : map text ts)
        Other s -> text s
  