{- |
Module      :  $Header$
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/"
    use = text usesS <+> 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))
    $+$ use
    $+$ text beginS
    $++$ 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
