{- |
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 :: String -> Sign -> [Named Sentence] -> Doc
printIsaTheory tn :: String
tn sign :: Sign
sign sens :: [Named Sentence]
sens = let
    b :: BaseSig
b = Sign -> BaseSig
baseSig Sign
sign
    bs :: String
bs = BaseSig -> String
showBaseSig BaseSig
b
    ld :: String
ld = "$HETS_ISABELLE_LIB/"
    mlFileUse :: Doc
mlFileUse = String -> Doc
text String
mlFileS Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
ld String -> String -> String
forall a. [a] -> [a] -> [a]
++ "prelude.ML")
    in String -> Doc
text String
theoryS Doc -> Doc -> Doc
<+> String -> Doc
text String
tn
    Doc -> Doc -> Doc
$+$ String -> Doc
text String
importsS Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep (case BaseSig
b of
        Custom_thy -> []
        _ -> if case BaseSig
b of
                Main_thy -> Bool
False
                HOLCF_thy -> Bool
False
                Custom_thy -> Bool
True
                _ -> Bool
True then [Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
ld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bs] else [String -> Doc
text String
bs]
      [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (String -> Doc) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text) (Sign -> [String]
imports Sign
sign))
    Doc -> Doc -> Doc
$+$ String -> Doc
text String
beginS
    Doc -> Doc -> Doc
$++$ Doc
mlFileUse
    Doc -> Doc -> Doc
$++$ Sign -> [Named Sentence] -> Doc
printTheoryBody Sign
sign [Named Sentence]
sens
    Doc -> Doc -> Doc
$++$ String -> Doc
text String
endS

printTheoryBody :: Sign -> [Named Sentence] -> Doc
printTheoryBody :: Sign -> [Named Sentence] -> Doc
printTheoryBody sig :: Sign
sig sens :: [Named Sentence]
sens =
 let (sens' :: [Named Sentence]
sens', recFuns :: [String]
recFuns) = [Named Sentence] -> ConstTab -> ([Named Sentence], [String])
findTypesForRecFuns [Named Sentence]
sens (Sign -> ConstTab
constTab Sign
sig)
     sig' :: Sign
sig' = Sign
sig { constTab :: ConstTab
constTab =
      (VName -> Typ -> Bool) -> ConstTab -> ConstTab
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ k :: VName
k _ -> String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (VName -> String
new VName
k) [String]
recFuns) (Sign -> ConstTab
constTab Sign
sig) }
 in String -> Doc -> Doc
callSetup "initialize" (Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas
      ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc)
-> (Named Sentence -> String) -> Named Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuotedString -> String
forall a. Show a => a -> String
show (QuotedString -> String)
-> (Named Sentence -> QuotedString) -> Named Sentence -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> QuotedString
Quote (String -> QuotedString)
-> (Named Sentence -> String) -> Named Sentence -> QuotedString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr)
      ([Named Sentence] -> [Doc]) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ s :: Named Sentence
s -> Bool -> Bool
not (Named Sentence -> Bool
isConstDef Named Sentence
s Bool -> Bool -> Bool
|| Named Sentence -> Bool
isRecDef Named Sentence
s Bool -> Bool -> Bool
|| Named Sentence -> Bool
isInstance Named Sentence
s)
                Bool -> Bool -> Bool
&& Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "") [Named Sentence]
sens')
      Doc -> Doc -> Doc
$++$ Sign -> Doc
printSign Sign
sig'
      Doc -> Doc -> Doc
$++$ [Named Sentence] -> Doc
printNamedSentences [Named Sentence]
sens'
      Doc -> Doc -> Doc
$++$ Sign -> Doc
printMonSign Sign
sig'

findTypesForRecFuns :: [Named Sentence] -> ConstTab
 -> ([Named Sentence], [String])
findTypesForRecFuns :: [Named Sentence] -> ConstTab -> ([Named Sentence], [String])
findTypesForRecFuns ns :: [Named Sentence]
ns ctab :: ConstTab
ctab =
 let (sens :: [Named Sentence]
sens, recFuns' :: [Maybe VName]
recFuns') = [(Named Sentence, Maybe VName)]
-> ([Named Sentence], [Maybe VName])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Named Sentence, Maybe VName)]
 -> ([Named Sentence], [Maybe VName]))
-> [(Named Sentence, Maybe VName)]
-> ([Named Sentence], [Maybe VName])
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> (Named Sentence, Maybe VName))
-> [Named Sentence] -> [(Named Sentence, Maybe VName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ sen :: Named Sentence
sen ->
      let (sen' :: Sentence
sen', recFns' :: Maybe VName
recFns') =
           case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
sen of
             RecDef kw :: Maybe String
kw cName :: VName
cName cType :: Maybe Typ
cType tm :: [Term]
tm ->
              (case ConstTab -> [(VName, Typ)]
forall k a. Map k a -> [(k, a)]
Map.toList (ConstTab -> [(VName, Typ)]) -> ConstTab -> [(VName, Typ)]
forall a b. (a -> b) -> a -> b
$
                 (VName -> Typ -> Bool) -> ConstTab -> ConstTab
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ k :: VName
k _ -> VName -> String
new VName
k String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== VName -> String
new VName
cName) ConstTab
ctab of
                 (_, t :: Typ
t) : _ ->
                  case Maybe Typ
cType of
                   Nothing ->
                    Maybe String -> VName -> Maybe Typ -> [Term] -> Sentence
RecDef Maybe String
kw VName
cName (Typ -> Maybe Typ
forall a. a -> Maybe a
Just Typ
t) [Term]
tm
                   Just t' :: Typ
t' ->
                    if Typ
t Typ -> Typ -> Bool
forall a. Eq a => a -> a -> Bool
/= Typ
t' then String -> Sentence
forall a. HasCallStack => String -> a
error "recFun: two types given"
                    else Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
sen
                 [] -> Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
sen
              , VName -> Maybe VName
forall a. a -> Maybe a
Just VName
cName)
             _ -> (Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
sen, Maybe VName
forall a. Maybe a
Nothing)
      in (Named Sentence
sen {sentence :: Sentence
sentence = Sentence
sen'}, Maybe VName
recFns')) [Named Sentence]
ns
 in ([Named Sentence]
sens, (VName -> String) -> [VName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VName -> String
new ([VName] -> [String]) -> [VName] -> [String]
forall a b. (a -> b) -> a -> b
$ [Maybe VName] -> [VName]
forall a. [Maybe a] -> [a]
catMaybes [Maybe VName]
recFuns')

printNamedSentences :: [Named Sentence] -> Doc
printNamedSentences :: [Named Sentence] -> Doc
printNamedSentences sens :: [Named Sentence]
sens = case [Named Sentence]
sens of
  [] -> Doc
empty
  s :: Named Sentence
s : r :: [Named Sentence]
r
    | Named Sentence -> Bool
isIsaAxiom Named Sentence
s ->
      let (axs :: [Named Sentence]
axs, rest :: [Named Sentence]
rest) = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named Sentence]
sens in
      (if [Named Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named Sentence]
axs then Doc
empty else String -> Doc
text String
axiomatizationS Doc -> Doc -> Doc
$+$ String -> Doc
text String
whereS)
      Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse (String -> Doc
text String
andS) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Doc
printNamedSen [Named Sentence]
axs)
      Doc -> Doc -> Doc
$++$ [Doc] -> Doc
vcat ((Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ a :: Named Sentence
a -> String -> Doc
text String
declareS Doc -> Doc -> Doc
<+> String -> Doc
text (Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
a)
                        Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (String -> Doc
text String
simpS))
                 ([Named Sentence] -> [Doc]) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ a :: Named Sentence
a -> case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
a of
                       b :: Sentence
b@Sentence {} -> Sentence -> Bool
isSimp Sentence
b Bool -> Bool -> Bool
&& Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= ""
                       _ -> Bool
False) [Named Sentence]
axs)
      Doc -> Doc -> Doc
$++$ [Named Sentence] -> Doc
printNamedSentences [Named Sentence]
rest
    | Named Sentence -> Bool
isConstDef Named Sentence
s ->
      let (defs_ :: [Named Sentence]
defs_, rest :: [Named Sentence]
rest) = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Named Sentence -> Bool
isConstDef [Named Sentence]
sens in
      String -> Doc
text String
defsS Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vsep ((Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Doc
printNamedSen [Named Sentence]
defs_)
      Doc -> Doc -> Doc
$++$ [Named Sentence] -> Doc
printNamedSentences [Named Sentence]
rest
    | Bool
otherwise ->
      Named Sentence -> Doc
printNamedSen Named Sentence
s Doc -> Doc -> Doc
$++$ (case Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
s of
        n :: String
n | String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" Bool -> Bool -> Bool
|| Named Sentence -> Bool
isRecDef Named Sentence
s -> Doc
empty
          | Bool
otherwise -> String -> Doc -> Doc
callSetup "record" (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ QuotedString -> String
forall a. Show a => a -> String
show (QuotedString -> String) -> QuotedString -> String
forall a b. (a -> b) -> a -> b
$ String -> QuotedString
Quote String
n))
      Doc -> Doc -> Doc
$++$ [Named Sentence] -> Doc
printNamedSentences [Named Sentence]
r

callSetup :: String -> Doc -> Doc
callSetup :: String -> Doc -> Doc
callSetup fun :: String
fun args :: Doc
args =
    String -> Doc
text "setup" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes ([Doc] -> Doc
fsep [String -> Doc
text ("Header." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fun), Doc
args])

data QuotedString = Quote String
instance Show QuotedString where
    show :: QuotedString -> String
show (Quote s :: String
s) = String -> String
forall a. [a] -> [a]
init (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
tail (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show String
s

getAxioms :: [Named Sentence] -> ([Named Sentence], [Named Sentence])
getAxioms :: [Named Sentence] -> ([Named Sentence], [Named Sentence])
getAxioms = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Named Sentence -> Bool
isIsaAxiom

isIsaAxiom :: Named Sentence -> Bool
isIsaAxiom :: Named Sentence -> Bool
isIsaAxiom s :: Named Sentence
s = case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s of
  Sentence {} -> Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
s
  _ -> Bool
False

isInstance :: Named Sentence -> Bool
isInstance :: Named Sentence -> Bool
isInstance s :: Named Sentence
s = case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s of
  Instance {} -> Bool
True
  _ -> Bool
False

isConstDef :: Named Sentence -> Bool
isConstDef :: Named Sentence -> Bool
isConstDef s :: Named Sentence
s = case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s of
  ConstDef {} -> Bool
True
  _ -> Bool
False

isRecDef :: Named Sentence -> Bool
isRecDef :: Named Sentence -> Bool
isRecDef s :: Named Sentence
s = case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s of
  RecDef {} -> Bool
True
  _ -> Bool
False

-- --------------------- Printing functions -----------------------------

showBaseSig :: BaseSig -> String
showBaseSig :: BaseSig -> String
showBaseSig = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '_') (String -> String) -> (BaseSig -> String) -> BaseSig -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseSig -> String
forall a. Show a => a -> String
show

printClass :: IsaClass -> Doc
printClass :: IsaClass -> Doc
printClass (IsaClass x :: String
x) = String -> Doc
text String
x

printSort :: Sort -> Doc
printSort :: Sort -> Doc
printSort = Bool -> Sort -> Doc
printSortAux Bool
False

printSortAux :: Bool -> Sort -> Doc
printSortAux :: Bool -> Sort -> Doc
printSortAux b :: Bool
b l :: Sort
l = case Sort
l of
    [c :: IsaClass
c] -> IsaClass -> Doc
printClass IsaClass
c
    _ -> (if Bool
b then Doc -> Doc
doubleQuotes else Doc -> Doc
forall a. a -> a
id)
      (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
braces (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (IsaClass -> Doc) -> Sort -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IsaClass -> Doc
printClass Sort
l

data SynFlag = Quoted | Unquoted | Null

doubleColon :: Doc
doubleColon :: Doc
doubleColon = String -> Doc
text "::"

isaEquals :: Doc
isaEquals :: Doc
isaEquals = String -> Doc
text "=="

bar :: [Doc] -> [Doc]
bar :: [Doc] -> [Doc]
bar = Doc -> [Doc] -> [Doc]
punctuate (Doc -> [Doc] -> [Doc]) -> Doc -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "|"

printType :: Typ -> Doc
printType :: Typ -> Doc
printType = SynFlag -> Typ -> Doc
printTyp SynFlag
Unquoted

printTyp :: SynFlag -> Typ -> Doc
printTyp :: SynFlag -> Typ -> Doc
printTyp a :: SynFlag
a = (Doc, Int) -> Doc
forall a b. (a, b) -> a
fst ((Doc, Int) -> Doc) -> (Typ -> (Doc, Int)) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
a

printTypeAux :: SynFlag -> Typ -> (Doc, Int)
printTypeAux :: SynFlag -> Typ -> (Doc, Int)
printTypeAux a :: SynFlag
a t :: Typ
t = case Typ
t of
 TFree v :: String
v s :: Sort
s -> (let
        d :: Doc
d = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "\'" String
v Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "?\'" String
v
                                then String
v else '\'' Char -> String -> String
forall a. a -> [a] -> [a]
: String
v
        c :: Doc
c = Sort -> Doc
printSort Sort
s
     in if Sort -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Sort
s then Doc
d else case SynFlag
a of
         Quoted -> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
doubleColon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> if Sort -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
                     (Sort -> Bool) -> Sort -> Bool
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall a. [a] -> [a]
tail Sort
s then Doc
c else Doc -> Doc
doubleQuotes Doc
c
         Unquoted -> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
doubleColon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
c
         Null -> Doc
d, 1000)
 TVar iv :: Indexname
iv s :: Sort
s -> SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
a (Typ -> (Doc, Int)) -> Typ -> (Doc, Int)
forall a b. (a -> b) -> a -> b
$ String -> Sort -> Typ
TFree (Indexname -> String
unindexed Indexname
iv) Sort
s
 Type name :: String
name _ args :: [Typ]
args -> case [Typ]
args of
    [t1 :: Typ
t1, t2 :: Typ
t2] | String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
name [String
prodS, String
sProdS, String
funS, String
cFunS, String
lFunS, String
sSumS] ->
       SynFlag -> String -> Typ -> Typ -> (Doc, Int)
printTypeOp SynFlag
a String
name Typ
t1 Typ
t2
    _ -> ((case [Typ]
args of
           [] -> Doc
empty
           [arg :: Typ
arg] -> let (d :: Doc
d, i :: Int
i) = SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
a Typ
arg in
                      if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1000 then Doc -> Doc
parens Doc
d else Doc
d
           _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                       (Typ -> Doc) -> [Typ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc, Int) -> Doc
forall a b. (a, b) -> a
fst ((Doc, Int) -> Doc) -> (Typ -> (Doc, Int)) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
a) [Typ]
args)
          Doc -> Doc -> Doc
<+> String -> Doc
text String
name, 1000)

printTypeOp :: SynFlag -> TName -> Typ -> Typ -> (Doc, Int)
printTypeOp :: SynFlag -> String -> Typ -> Typ -> (Doc, Int)
printTypeOp x :: SynFlag
x name :: String
name r1 :: Typ
r1 r2 :: Typ
r2 =
    let (d1 :: Doc
d1, i1 :: Int
i1) = SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
x Typ
r1
        (d2 :: Doc
d2, i2 :: Int
i2) = SynFlag -> Typ -> (Doc, Int)
printTypeAux SynFlag
x Typ
r2
        (l :: Int
l, r :: Int
r) = (Int, Int) -> String -> Map String (Int, Int) -> (Int, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (0 :: Int, 0 :: Int)
                    String
name (Map String (Int, Int) -> (Int, Int))
-> Map String (Int, Int) -> (Int, Int)
forall a b. (a -> b) -> a -> b
$ [(String, (Int, Int))] -> Map String (Int, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                    [ (String
funS, (1, 0))
                    , (String
cFunS, (1, 0))
                    , (String
lFunS, (1, 0))
                    , (String
sSumS, (11, 10))
                    , (String
prodS, (21, 20))
                    , (String
sProdS, (21, 20))
                    , (String
lProdS, (21, 20))
                    ]
        d3 :: Doc
d3 = if Int
i1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
l then Doc -> Doc
parens Doc
d1 else Doc
d1
        d4 :: Doc
d4 = if Int
i2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
r then Doc -> Doc
parens Doc
d2 else Doc
d2
    in (Doc
d3 Doc -> Doc -> Doc
<+> String -> Doc
text String
name Doc -> Doc -> Doc
<+> Doc
d4, Int
r)

andDocs :: [Doc] -> Doc
andDocs :: [Doc] -> Doc
andDocs = [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
prepPunctuate (String -> Doc
text String
andS Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)

-- | printing a named sentence
printNamedSen :: Named Sentence -> Doc
printNamedSen :: Named Sentence -> Doc
printNamedSen ns :: Named Sentence
ns =
  let s :: Sentence
s = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
ns
      lab :: String
lab = Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
ns
      b :: Bool
b = Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
ns
      d :: Doc
d = Sentence -> Doc
printSentence Sentence
s
  in case Sentence
s of
  TypeDef {} -> Doc
d
  RecDef {} -> Doc
d
  Lemmas {} -> Doc
d
  Instance {} -> Doc
d
  Locale {} -> Doc
d
  Class {} -> Doc
d
  Datatypes _ -> Doc
d
  Consts _ -> Doc
d
  TypeSynonym {} -> Doc
d
  Axioms _ -> Doc
d
  Lemma {} -> Doc
d
  Definition {} -> Doc
d
  Fun {} -> Doc
d
  Instantiation {} -> Doc
d
  InstanceProof {} -> Doc
d
  InstanceArity {} -> Doc
d
  InstanceSubclass {} -> Doc
d
  Subclass {} -> Doc
d
  Typedef {} -> Doc
d
  Defs {} -> Doc
d
  Fixrec {} -> Doc
d
  Domains {} -> Doc
d
  Primrec {} -> Doc
d
  _ -> let dd :: Doc
dd = Doc -> Doc
doubleQuotes Doc
d in
       if Sentence -> Bool
isRefute Sentence
s then String -> Doc
text String
lemmaS Doc -> Doc -> Doc
<+> String -> Doc
text String
lab Doc -> Doc -> Doc
<+> Doc
colon
              Doc -> Doc -> Doc
<+> Doc
dd Doc -> Doc -> Doc
$+$ String -> Doc
text String
refuteS
       else if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lab then Doc
dd else [Doc] -> Doc
fsep [ (case Sentence
s of
    ConstDef {} -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
lab String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def"
    Sentence {} ->
        (if Bool
b then Doc
empty else String -> Doc
text String
theoremS)
        Doc -> Doc -> Doc
<+> String -> Doc
text String
lab Doc -> Doc -> Doc
<+> (if Bool
b then String -> Doc
text "[rule_format]" else
            if Sentence -> Bool
isSimp Sentence
s then String -> Doc
text "[simp]" else Doc
empty)
    _ -> String -> Doc
forall a. HasCallStack => String -> a
error "printNamedSen") Doc -> Doc -> Doc
<+> Doc
colon, Doc
dd] Doc -> Doc -> Doc
$+$ case Sentence
s of
    Sentence {} -> if Bool
b then Doc
empty else case Sentence -> Maybe IsaProof
thmProof Sentence
s of
      Nothing -> String -> Doc
text String
oopsS
      Just prf :: IsaProof
prf -> IsaProof -> Doc
forall a. Pretty a => a -> Doc
pretty IsaProof
prf
    _ -> Doc
empty

-- | sentence printing
printSentence :: Sentence -> Doc
printSentence :: Sentence -> Doc
printSentence s :: Sentence
s = case Sentence
s of
  TypeDef nt :: Typ
nt td :: SetDecl
td pr :: IsaProof
pr -> String -> Doc
text String
typedefS
                   Doc -> Doc -> Doc
<+> Typ -> Doc
printType Typ
nt
                   Doc -> Doc -> Doc
<+> Doc
equals
                   Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (SetDecl -> Doc
printSetDecl SetDecl
td)
                   Doc -> Doc -> Doc
$+$ IsaProof -> Doc
forall a. Pretty a => a -> Doc
pretty IsaProof
pr
  RecDef kw :: Maybe String
kw cName :: VName
cName cType :: Maybe Typ
cType xs :: [Term]
xs ->
    let preparedEq :: [Doc]
preparedEq = (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) [Term]
xs
        preparedEqWithBars :: [Doc]
preparedEqWithBars =
          (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc -> Doc
<+> String -> Doc
text String
barS) ([Doc] -> [Doc]
forall a. [a] -> [a]
init [Doc]
preparedEq) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [[Doc] -> Doc
forall a. [a] -> a
last [Doc]
preparedEq]
        tp :: Doc
tp = case Maybe Typ
cType of
              Just t :: Typ
t -> Doc
doubleColon Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Typ -> Doc
printType Typ
t)
              Nothing -> Doc
empty
        kw' :: Doc
kw' = case Maybe String
kw of
               Just str :: String
str -> String -> Doc
text String
str
               Nothing -> String -> Doc
text String
primrecS
    in Doc
kw' Doc -> Doc -> Doc
<+> String -> Doc
text (VName -> String
new VName
cName) Doc -> Doc -> Doc
<+> Doc
tp Doc -> Doc -> Doc
<+> VName -> Doc
printAlt VName
cName Doc -> Doc -> Doc
<+> String -> Doc
text String
whereS Doc -> Doc -> Doc
$+$
       [Doc] -> Doc
vcat [Doc]
preparedEqWithBars
  Instance { tName :: Sentence -> String
tName = String
t, arityArgs :: Sentence -> [Sort]
arityArgs = [Sort]
args, arityRes :: Sentence -> Sort
arityRes = Sort
res, definitions :: Sentence -> [(String, Term)]
definitions = [(String, Term)]
defs_,
             instProof :: Sentence -> IsaProof
instProof = IsaProof
prf } ->
      String -> Doc
text String
instantiationS Doc -> Doc -> Doc
<+> String -> Doc
text String
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
doubleColon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (case [Sort]
args of
        [] -> Doc
empty
        _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Sort -> Doc) -> [Sort] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Sort -> Doc
printSortAux Bool
True) [Sort]
args)
        Doc -> Doc -> Doc
<+> Bool -> Sort -> Doc
printSortAux Bool
True Sort
res Doc -> Doc -> Doc
$+$ String -> Doc
text String
beginS Doc -> Doc -> Doc
$++$ [(String, Term)] -> Doc
printDefs [(String, Term)]
defs_ Doc -> Doc -> Doc
$++$
            String -> Doc
text String
instanceS Doc -> Doc -> Doc
<+> IsaProof -> Doc
forall a. Pretty a => a -> Doc
pretty IsaProof
prf Doc -> Doc -> Doc
$+$ String -> Doc
text String
endS
      where printDefs :: [(String, Term)] -> Doc
            printDefs :: [(String, Term)] -> Doc
printDefs defs' :: [(String, Term)]
defs' = [Doc] -> Doc
vcat (((String, Term) -> Doc) -> [(String, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, Term) -> Doc
printDef [(String, Term)]
defs')
            printDef :: (String, Term) -> Doc
            printDef :: (String, Term) -> Doc
printDef (name :: String
name, def :: Term
def) =
                String -> Doc
text String
definitionS Doc -> Doc -> Doc
<+>
                     Named Sentence -> Doc
printNamedSen (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
name (Term -> Sentence
ConstDef Term
def))

  Sentence { isRefuteAux :: Sentence -> Bool
isRefuteAux = Bool
b, metaTerm :: Sentence -> MetaTerm
metaTerm = MetaTerm
t } -> Bool -> MetaTerm -> Doc
printPlainMetaTerm (Bool -> Bool
not Bool
b) MetaTerm
t
  ConstDef t :: Term
t -> Term -> Doc
printTerm Term
t
  Lemmas name :: String
name lemmas :: [String]
lemmas -> if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
lemmas
                        then Doc
empty {- only have this lemmas if we have some in
                                   the list -}
                        else String -> Doc
text String
lemmasS Doc -> Doc -> Doc
<+> String -> Doc
text String
name Doc -> Doc -> Doc
<+>
                             Doc
equals Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
lemmas)
  l :: Sentence
l@(Locale {}) ->
   let h :: Doc
h = String -> Doc
text "locale" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Sentence -> QName
localeName Sentence
l)
       parents :: [Doc]
parents = Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
Data.List.intersperse (String -> Doc
text "+") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                  (QName -> Doc) -> [QName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (QName -> String) -> QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Show a => a -> String
show) (Sentence -> [QName]
localeParents Sentence
l)
       (fxs :: [Doc]
fxs, ass :: [Doc]
ass) = Ctxt -> ([Doc], [Doc])
printContext (Ctxt -> ([Doc], [Doc])) -> Ctxt -> ([Doc], [Doc])
forall a b. (a -> b) -> a -> b
$ Sentence -> Ctxt
localeContext Sentence
l
   in Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes Doc
h [Doc]
parents [Doc]
ass [Doc]
fxs
      Doc -> Doc -> Doc
$+$ [Sentence] -> Doc
printBody (Sentence -> [Sentence]
localeBody Sentence
l)
  c :: Sentence
c@(Class {}) ->
   let h :: Doc
h = String -> Doc
text "class" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Sentence -> QName
className Sentence
c)
       parents :: [Doc]
parents = Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
Data.List.intersperse (String -> Doc
text "+") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                  (QName -> Doc) -> [QName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (QName -> String) -> QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Show a => a -> String
show) (Sentence -> [QName]
classParents Sentence
c)
       (fxs :: [Doc]
fxs, ass :: [Doc]
ass) = Ctxt -> ([Doc], [Doc])
printContext (Sentence -> Ctxt
classContext Sentence
c)
   in Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes Doc
h [Doc]
parents [Doc]
ass [Doc]
fxs
      Doc -> Doc -> Doc
$+$ [Sentence] -> Doc
printBody (Sentence -> [Sentence]
classBody Sentence
c)
  (Datatypes dts :: [Datatype]
dts) -> if [Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Datatype]
dts then Doc
empty
                     else String -> Doc
text "datatype" Doc -> Doc -> Doc
<+>
                        [Doc] -> Doc
andDocs ((Datatype -> Doc) -> [Datatype] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ d :: Datatype
d ->
                        let vars :: [Doc]
vars = (Typ -> Doc) -> [Typ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Doc
printType ([Typ] -> [Doc]) -> [Typ] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Datatype -> [Typ]
datatypeTVars Datatype
d
                            name :: Doc
name = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Datatype -> QName
datatypeName Datatype
d
                            pretty_cs :: DatatypeConstructor -> Doc
pretty_cs c :: DatatypeConstructor
c =
                             let cname :: String
cname = case DatatypeConstructor
c of
                                  DatatypeNoConstructor {} -> ""
                                  _ -> QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ DatatypeConstructor -> QName
constructorName DatatypeConstructor
c
                                 cname' :: Doc
cname' = if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
cname
                                          then Doc -> Doc
doubleQuotes (String -> Doc
text String
cname)
                                          else String -> Doc
text String
cname
                                 tps :: [Doc]
tps = (Typ -> Doc) -> [Typ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc
printType) ([Typ] -> [Doc]) -> [Typ] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                                         DatatypeConstructor -> [Typ]
constructorArgs DatatypeConstructor
c
                             in [Doc] -> Doc
hsep (Doc
cname' Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
tps)
                            cs :: [Doc]
cs = (DatatypeConstructor -> Doc) -> [DatatypeConstructor] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DatatypeConstructor -> Doc
pretty_cs ([DatatypeConstructor] -> [Doc]) -> [DatatypeConstructor] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Datatype -> [DatatypeConstructor]
datatypeConstructors Datatype
d
                        in [Doc] -> Doc
hsep [Doc]
vars Doc -> Doc -> Doc
<+> Doc
name Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+>
                           [Doc] -> Doc
fsep ([Doc] -> [Doc]
bar [Doc]
cs)) [Datatype]
dts)
  Domains ds :: [Domain]
ds -> if [Domain] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Domain]
ds then Doc
empty
                else String -> Doc
text "domain" Doc -> Doc -> Doc
<+>
                 [Doc] -> Doc
andDocs ((Domain -> Doc) -> [Domain] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ d :: Domain
d ->
                  let vars :: [Doc]
vars = (Typ -> Doc) -> [Typ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Doc
printType ([Typ] -> [Doc]) -> [Typ] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Domain -> [Typ]
domainTVars Domain
d
                      name :: Doc
name = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Domain -> QName
domainName Domain
d
                      pretty_cs :: DomainConstructor -> Doc
pretty_cs c :: DomainConstructor
c =
                       let cname :: Doc
cname = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ DomainConstructor -> QName
domainConstructorName DomainConstructor
c
                           args' :: [Doc]
args' = (DomainConstructorArg -> Doc) -> [DomainConstructorArg] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ arg :: DomainConstructorArg
arg ->
                            (if DomainConstructorArg -> Bool
domainConstructorArgLazy DomainConstructorArg
arg
                             then String -> Doc
text "lazy" else Doc
empty) Doc -> Doc -> Doc
<+>
                            (case DomainConstructorArg -> Maybe QName
domainConstructorArgSel DomainConstructorArg
arg of
                              Just sel :: QName
sel -> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
sel) Doc -> Doc -> Doc
<+> String -> Doc
text "::"
                              Nothing -> Doc
empty) Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc
printType)
                            (DomainConstructorArg -> Typ
domainConstructorArgType DomainConstructorArg
arg)) ([DomainConstructorArg] -> [Doc])
-> [DomainConstructorArg] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                            DomainConstructor -> [DomainConstructorArg]
domainConstructorArgs DomainConstructor
c
                           args :: [Doc]
args = (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> Doc
parens [Doc]
args'
                       in [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
cname Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
args
                      cs :: [Doc]
cs = (DomainConstructor -> Doc) -> [DomainConstructor] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DomainConstructor -> Doc
pretty_cs ([DomainConstructor] -> [Doc]) -> [DomainConstructor] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Domain -> [DomainConstructor]
domainConstructors Domain
d
                  in [Doc] -> Doc
hsep [Doc]
vars Doc -> Doc -> Doc
<+> Doc
name Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+>
                     [Doc] -> Doc
fsep ([Doc] -> [Doc]
bar [Doc]
cs)) [Domain]
ds)
  Consts cs :: [(String, Maybe Mixfix, Typ)]
cs -> if [(String, Maybe Mixfix, Typ)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, Maybe Mixfix, Typ)]
cs then Doc
empty
               else [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "consts" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                     ((String, Maybe Mixfix, Typ) -> Doc)
-> [(String, Maybe Mixfix, Typ)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, _, t :: Typ
t) -> String -> Doc
text String
n Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+>
                                    Doc -> Doc
doubleQuotes (Typ -> Doc
printType Typ
t)) [(String, Maybe Mixfix, Typ)]
cs
  TypeSynonym n :: QName
n _ vs :: [String]
vs tp :: Typ
tp -> [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [String -> Doc
text "type_synonym",
                                 String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Show a => a -> String
show QName
n, String -> Doc
text "="] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
vs
                                [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc
printType (Typ -> Doc) -> Typ -> Doc
forall a b. (a -> b) -> a -> b
$ Typ
tp]
  Axioms axs :: [Axiom]
axs -> if [Axiom] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Axiom]
axs then Doc
empty
                else [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "axioms" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                      (Axiom -> Doc) -> [Axiom] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Axiom
a -> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Axiom -> QName
axiomName Axiom
a) Doc -> Doc -> Doc
<+>
                                 (if Axiom -> String
axiomArgs Axiom
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= ""
                                  then Doc -> Doc
brackets (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Axiom -> String
axiomArgs Axiom
a)
                                  else Doc
empty) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+>
                                 Doc -> Doc
doubleQuotes (Term -> Doc
printTerm (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ Axiom -> Term
axiomTerm Axiom
a)) [Axiom]
axs
  l :: Sentence
l@(Lemma {}) ->
   let (fxs :: [Doc]
fxs, ass :: [Doc]
ass) = Ctxt -> ([Doc], [Doc])
printContext (Ctxt -> ([Doc], [Doc])) -> Ctxt -> ([Doc], [Doc])
forall a b. (a -> b) -> a -> b
$ Sentence -> Ctxt
lemmaContext Sentence
l
   in String -> Doc
text "lemma" Doc -> Doc -> Doc
<+> (case Sentence -> Maybe QName
lemmaTarget Sentence
l of
                           Just t :: QName
t -> Doc -> Doc
braces (String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
t))
                           Nothing -> Doc
empty) Doc -> Doc -> Doc
<+>
                           (case ([Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
fxs, [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
ass, Sentence -> [Props]
lemmaProps Sentence
l) of
                            (True, True, [sh :: Props
sh]) -> Props -> Doc
printProps Props
sh
                            _ -> [Doc] -> Doc
vsep ([Doc]
fxs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
ass [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                                  [String -> Doc
text "shows" Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs
                                    ((Props -> Doc) -> [Props] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Props -> Doc
printProps (Sentence -> [Props]
lemmaProps Sentence
l))]))
      Doc -> Doc -> Doc
$+$ (case Sentence -> Maybe String
lemmaProof Sentence
l of
            Just p :: String
p -> String -> Doc
text String
p
            Nothing -> Doc
empty)
  d :: Sentence
d@(Definition {}) -> [Doc] -> Doc
fsep [String -> Doc
text "definition" Doc -> Doc -> Doc
<+>
   (case Sentence -> Maybe String
definitionTarget Sentence
d of
     Just t :: String
t -> Doc -> Doc
braces (String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text (String -> String
forall a. Show a => a -> String
show String
t))
     Nothing -> Doc
empty) Doc -> Doc -> Doc
<+>
   (String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Sentence -> QName
definitionName Sentence
d) Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+>
    Doc -> Doc
doubleQuotes (Typ -> Doc
printType (Typ -> Doc) -> Typ -> Doc
forall a b. (a -> b) -> a -> b
$ Sentence -> Typ
definitionType Sentence
d)), String -> Doc
text "where" Doc -> Doc -> Doc
<+>
   Doc -> Doc
doubleQuotes (String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Sentence -> QName
definitionName Sentence
d) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm (
    Sentence -> [Term]
definitionVars Sentence
d)) Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Term -> Doc
printTerm (Sentence -> Term
definitionTerm Sentence
d))]
  f :: Sentence
f@(Fun {}) -> String -> Doc
text "fun" Doc -> Doc -> Doc
<+> (case Sentence -> Maybe QName
funTarget Sentence
f of
   Just t :: QName
t -> Doc -> Doc
braces (String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
t))
   Nothing -> Doc
empty) Doc -> Doc -> Doc
<+> (if Sentence -> Bool
funDomintros Sentence
f then Doc -> Doc
braces (String -> Doc
text "domintros")
    else Doc
empty) Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse (String -> Doc
text String
andS) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
     ((String, Maybe Mixfix, Typ, [([Term], Term)]) -> Doc)
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (name :: String
name, mx :: Maybe Mixfix
mx, tp :: Typ
tp, _) -> String -> Doc
text String
name Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+>
     Doc -> Doc
doubleQuotes (Typ -> Doc
printType Typ
tp) Doc -> Doc -> Doc
<+> case Maybe Mixfix
mx of
                      Just (Mixfix _ _ s' :: String
s' _) -> Doc -> Doc
doubleQuotes (String -> Doc
text String
s')
                      _ -> Doc
empty) (Sentence -> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
funEquations Sentence
f)) Doc -> Doc -> Doc
<+> String -> Doc
text "where" Doc -> Doc -> Doc
$+$
    (let eqs :: [(String, ([Term], Term))]
eqs = ((String, Maybe Mixfix, Typ, [([Term], Term)])
 -> [(String, ([Term], Term))])
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
-> [(String, ([Term], Term))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (name :: String
name, _, _, e :: [([Term], Term)]
e) -> (([Term], Term) -> (String, ([Term], Term)))
-> [([Term], Term)] -> [(String, ([Term], Term))]
forall a b. (a -> b) -> [a] -> [b]
map (\ e' :: ([Term], Term)
e' -> (String
name, ([Term], Term)
e')) [([Term], Term)]
e)
                             (Sentence -> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
funEquations Sentence
f)
         eqs' :: [Doc]
eqs' = ((String, ([Term], Term)) -> Doc)
-> [(String, ([Term], Term))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, (vs :: [Term]
vs, t :: Term
t)) -> Doc -> Doc
doubleQuotes (String -> Doc
text String
n Doc -> Doc -> Doc
<+>
                 [Doc] -> Doc
hsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
vs) Doc -> Doc -> Doc
<+>
                 String -> Doc
text "=" Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
t)) [(String, ([Term], Term))]
eqs
     in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
bar [Doc]
eqs')
  i :: Sentence
i@(Instantiation {}) -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc
text "instantiation" Doc -> Doc -> Doc
<+> String -> Doc
text
   (Sentence -> String
instantiationType Sentence
i) Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+> (Sort, [Sort]) -> Doc
printArity (Sentence -> (Sort, [Sort])
instantiationArity Sentence
i)) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
    [[Sentence] -> Doc
printBody (Sentence -> [Sentence]
instantiationBody Sentence
i)]
  InstanceProof prf :: String
prf -> String -> Doc
text "instance" Doc -> Doc -> Doc
$+$ String -> Doc
text String
prf
  i :: Sentence
i@(InstanceArity {}) -> String -> Doc
text "instance" Doc -> Doc -> Doc
<+>
   [Doc] -> Doc
hcat (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse (String -> Doc
text "and") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Sentence -> [String]
instanceTypes Sentence
i) Doc -> Doc -> Doc
<+>
   (Sort, [Sort]) -> Doc
printArity (Sentence -> (Sort, [Sort])
instanceArity Sentence
i) Doc -> Doc -> Doc
$+$ String -> Doc
text (Sentence -> String
instanceProof Sentence
i)
  i :: Sentence
i@(InstanceSubclass {}) -> String -> Doc
text "instance" Doc -> Doc -> Doc
<+> String -> Doc
text (Sentence -> String
instanceClass Sentence
i) Doc -> Doc -> Doc
<+>
   String -> Doc
text (Sentence -> String
instanceRel Sentence
i) Doc -> Doc -> Doc
<+> String -> Doc
text (Sentence -> String
instanceClass1 Sentence
i) Doc -> Doc -> Doc
$+$ String -> Doc
text (Sentence -> String
instanceProof Sentence
i)
  c :: Sentence
c@(Subclass {}) -> String -> Doc
text "subclass" Doc -> Doc -> Doc
<+> (case Sentence -> Maybe QName
subclassTarget Sentence
c of
                           Just t :: QName
t -> Doc -> Doc
braces (String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
t))
                           Nothing -> Doc
empty) Doc -> Doc -> Doc
<+> String -> Doc
text (Sentence -> String
subclassClass Sentence
c)
                          Doc -> Doc -> Doc
<+> String -> Doc
text (Sentence -> String
subclassProof Sentence
c)
  t :: Sentence
t@(Typedef {}) -> String -> Doc
text "typedef" Doc -> Doc -> Doc
<+> (case Sentence -> [(String, Sort)]
typedefVars Sentence
t of
                     [] -> Doc
empty
                     [v :: (String, Sort)
v] -> (String, Sort) -> Doc
printVarWithSort (String, Sort)
v
                     vs :: [(String, Sort)]
vs -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                           ((String, Sort) -> Doc) -> [(String, Sort)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, Sort) -> Doc
printVarWithSort [(String, Sort)]
vs) Doc -> Doc -> Doc
<+>
                    String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Sentence -> QName
typedefName Sentence
t) Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+>
                    Doc -> Doc
doubleQuotes (Term -> Doc
printTerm (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ Sentence -> Term
typedefTerm Sentence
t) Doc -> Doc -> Doc
<+>
                    (case Sentence -> Maybe (QName, QName)
typedefMorphisms Sentence
t of
                      Just (m1 :: QName
m1, m2 :: QName
m2) -> String -> Doc
text "morphisms" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
m1)
                                     Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
m2)
                      Nothing -> Doc
empty) Doc -> Doc -> Doc
$+$ String -> Doc
text (Sentence -> String
typedefProof Sentence
t)
  d :: Sentence
d@(Defs {}) -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc
text "defs" Doc -> Doc -> Doc
<+> (if Sentence -> Bool
defsUnchecked Sentence
d
                                          then String -> Doc
text "unchecked"
                                          else Doc
empty) Doc -> Doc -> Doc
<+>
                                         (if Sentence -> Bool
defsOverloaded Sentence
d
                                          then String -> Doc
text "overloaded"
                                          else Doc
empty))
   Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (DefEquation -> Doc) -> [DefEquation] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ eq' :: DefEquation
eq' ->
       String -> Doc
text (QName -> String
forall a. Show a => a -> String
show (DefEquation -> QName
defEquationName DefEquation
eq')) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (
        String -> Doc
text (DefEquation -> String
defEquationConst DefEquation
eq') Doc -> Doc -> Doc
<+> String -> Doc
text "==" Doc -> Doc -> Doc
<+>
        Term -> Doc
printTerm (DefEquation -> Term
defEquationTerm DefEquation
eq')) Doc -> Doc -> Doc
<+> if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DefEquation -> String
defEquationArgs DefEquation
eq')
        then Doc
empty else Doc -> Doc
brackets (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ DefEquation -> String
defEquationArgs DefEquation
eq')) (Sentence -> [DefEquation]
defsEquations Sentence
d)
  Fixrec fs :: [(String, Maybe Mixfix, Typ, [FixrecEquation])]
fs ->
   let h :: [Doc]
h = ((String, Maybe Mixfix, Typ, [FixrecEquation]) -> Doc)
-> [(String, Maybe Mixfix, Typ, [FixrecEquation])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (name :: String
name, _, tp :: Typ
tp, _) -> String -> Doc
text String
name Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+>
                                  (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc
printType) Typ
tp) [(String, Maybe Mixfix, Typ, [FixrecEquation])]
fs
       pretty_fixreceq :: String -> FixrecEquation -> Doc
pretty_fixreceq name :: String
name eq' :: FixrecEquation
eq' =
        let unchecked :: Doc
unchecked = if FixrecEquation -> Bool
fixrecEquationUnchecked FixrecEquation
eq' then
                        String -> Doc
text "(unchecked)" else Doc
empty
            premises :: [Term]
premises = FixrecEquation -> [Term]
fixrecEquationPremises FixrecEquation
eq'
            p :: String -> [Doc] -> [Doc]
p s' :: String
s' = Doc -> [Doc] -> [Doc]
punctuate (Doc -> [Doc] -> [Doc]) -> Doc -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
s'
            patterns :: [Doc]
patterns = (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) ([Term] -> [Doc]) -> [Term] -> [Doc]
forall a b. (a -> b) -> a -> b
$ FixrecEquation -> [Term]
fixrecEquationPatterns FixrecEquation
eq'
            tm :: Doc
tm = Term -> Doc
printTerm (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ FixrecEquation -> Term
fixrecEquationTerm FixrecEquation
eq'
        in Doc
unchecked Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes ([Term] -> Doc -> Doc
printTermWithPremises [Term]
premises
            ([Doc] -> Doc
hsep (String -> [Doc] -> [Doc]
p "\\<cdot>" (String -> Doc
text String
name Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
patterns)) Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Doc
tm))
       body :: [Doc]
body = ((String, Maybe Mixfix, Typ, [FixrecEquation]) -> [Doc])
-> [(String, Maybe Mixfix, Typ, [FixrecEquation])] -> [Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (name :: String
name, _, _, eqs :: [FixrecEquation]
eqs) -> (FixrecEquation -> Doc) -> [FixrecEquation] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> FixrecEquation -> Doc
pretty_fixreceq String
name) [FixrecEquation]
eqs)
               [(String, Maybe Mixfix, Typ, [FixrecEquation])]
fs
   in String -> Doc
text "fixrec" Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs [Doc]
h Doc -> Doc -> Doc
<+> String -> Doc
text "where" Doc -> Doc -> Doc
$+$ [Doc] -> Doc
fsep ([Doc] -> [Doc]
bar [Doc]
body)
  Primrec t :: Maybe QName
t eqs :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
eqs ->
                let h :: [Doc]
h = ((String, Maybe Mixfix, Typ, [([Term], Term)]) -> Doc)
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (name :: String
name, _, tp :: Typ
tp, _) -> String -> Doc
text String
name Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+>
                              (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc
printType) Typ
tp) [(String, Maybe Mixfix, Typ, [([Term], Term)])]
eqs
                    pretty_primrec :: String -> ([Term], Term) -> Doc
pretty_primrec name :: String
name (vs :: [Term]
vs, tm :: Term
tm) = Doc -> Doc
doubleQuotes (String -> Doc
text String
name
                     Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
vs) Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
tm)
                    body :: [Doc]
body = ((String, Maybe Mixfix, Typ, [([Term], Term)]) -> [Doc])
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> [Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (name :: String
name, _, _, tms :: [([Term], Term)]
tms) ->
                            (([Term], Term) -> Doc) -> [([Term], Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> ([Term], Term) -> Doc
pretty_primrec String
name) [([Term], Term)]
tms) [(String, Maybe Mixfix, Typ, [([Term], Term)])]
eqs
                in String -> Doc
text "primrec" Doc -> Doc -> Doc
<+> (case Maybe QName
t of
                           Just t' :: QName
t' -> Doc -> Doc
braces (String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text (QName -> String
forall a. Show a => a -> String
show QName
t'))
                           Nothing -> Doc
empty) Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs [Doc]
h Doc -> Doc -> Doc
<+> String -> Doc
text "where"
                   Doc -> Doc -> Doc
$+$ [Doc] -> Doc
fsep ([Doc] -> [Doc]
bar [Doc]
body)

printTermWithPremises :: [Term] -> Doc -> Doc
printTermWithPremises :: [Term] -> Doc -> Doc
printTermWithPremises ps :: [Term]
ps t :: Doc
t =
 let p :: String -> [Doc] -> [Doc]
p s :: String
s = Doc -> [Doc] -> [Doc]
punctuate (Doc -> [Doc] -> [Doc]) -> Doc -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
s
 in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
p "\\<Longrightarrow>" ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
ps [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
t])

printArity :: (Sort, [Sort]) -> Doc
printArity :: (Sort, [Sort]) -> Doc
printArity (sort' :: Sort
sort', sorts :: [Sort]
sorts) = Doc -> Doc
parens ([Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                           (Sort -> Doc) -> [Sort] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Sort -> Doc
printSortAux Bool
True) [Sort]
sorts) Doc -> Doc -> Doc
<+> Sort -> Doc
printSort Sort
sort'

printVarWithSort :: (String, Sort) -> Doc
printVarWithSort :: (String, Sort) -> Doc
printVarWithSort (name :: String
name, []) = String -> Doc
text String
name
printVarWithSort (name :: String
name, sort' :: Sort
sort') = String -> Doc
text String
name Doc -> Doc -> Doc
<+> Bool -> Sort -> Doc
printSortAux Bool
True Sort
sort'

printBody :: [Sentence] -> Doc
printBody :: [Sentence] -> Doc
printBody sens :: [Sentence]
sens = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if [Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sentence]
sens then []
               else [String -> Doc
text "begin"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Sentence -> Doc) -> [Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Sentence -> Doc
printSentence [Sentence]
sens [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text "end"]

printContext :: Ctxt -> ([Doc], [Doc])
printContext :: Ctxt -> ([Doc], [Doc])
printContext ctxt :: Ctxt
ctxt =
 let fixes' :: [Doc]
fixes' = ((String, Maybe Mixfix, Typ) -> Doc)
-> [(String, Maybe Mixfix, Typ)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, _, tp :: Typ
tp) -> if String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then Doc
empty else String -> Doc
text String
n
                       Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> Doc
printTyp SynFlag
Null) Typ
tp)
                     (Ctxt -> [(String, Maybe Mixfix, Typ)]
fixes Ctxt
ctxt)
     assumes' :: [Doc]
assumes' = ((String, Term) -> Doc) -> [(String, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, tm :: Term
tm) -> if String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then Doc
empty else String -> Doc
text String
n Doc -> Doc -> Doc
<+> String -> Doc
text ":"
                       Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) Term
tm)
                     (Ctxt -> [(String, Term)]
assumes Ctxt
ctxt)
 in ([Doc]
fixes', [Doc]
assumes')

printProps :: Props -> Doc
printProps :: Props -> Doc
printProps (Props {propsName :: Props -> Maybe QName
propsName = Maybe QName
n, propsArgs :: Props -> Maybe String
propsArgs = Maybe String
a, props :: Props -> [Prop]
props = [Prop]
p}) =
 (QName -> Doc) -> Maybe QName -> Doc
forall a. (a -> Doc) -> Maybe a -> Doc
printMaybe (String -> Doc
text (String -> Doc) -> (QName -> String) -> QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Show a => a -> String
show) Maybe QName
n Doc -> Doc -> Doc
<+> (String -> Doc) -> Maybe String -> Doc
forall a. (a -> Doc) -> Maybe a -> Doc
printMaybe String -> Doc
text Maybe String
a
 Doc -> Doc -> Doc
<+> (if Maybe QName -> Bool
forall a. Maybe a -> Bool
isNothing Maybe QName
n Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
a
      then Doc
empty else String -> Doc
text ":") Doc -> Doc -> Doc
<+>
     [Doc] -> Doc
vcat ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
printProp [Prop]
p)

printProp :: Prop -> Doc
printProp :: Prop -> Doc
printProp (Prop {prop :: Prop -> Term
prop = Term
t, propPats :: Prop -> [Term]
propPats = [Term]
ts}) =
 let t' :: Doc
t' = Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Term -> Doc
printTerm Term
t
     ts' :: Doc
ts' = [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: Term
p -> String -> Doc
text "is" Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) Term
p) [Term]
ts
 in Doc
t' Doc -> Doc -> Doc
<+> if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts then Doc
empty
           else Doc -> Doc
parens Doc
ts'

printSetDecl :: SetDecl -> Doc
printSetDecl :: SetDecl -> Doc
printSetDecl setdecl :: SetDecl
setdecl =
    case SetDecl
setdecl of
      SubSet v :: Term
v t :: Typ
t f :: Term
f -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Term -> Doc
printTerm Term
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
doubleColon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Typ -> Doc
printType Typ
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
                      Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
f
      FixedSet elems :: [Term]
elems -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
elems

printPlainMetaTerm :: Bool -> MetaTerm -> Doc
printPlainMetaTerm :: Bool -> MetaTerm -> Doc
printPlainMetaTerm b :: Bool
b mt :: MetaTerm
mt = case MetaTerm
mt of
    Term t :: Term
t -> Bool -> Term -> Doc
printPlainTerm Bool
b Term
t
    Conditional conds :: [Term]
conds t :: Term
t -> [Doc] -> Doc
sep
      [ String -> Doc
text String
premiseOpenS
        Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
conds)
        Doc -> Doc -> Doc
<+> String -> Doc
text String
premiseCloseS
      , String -> Doc
text String
metaImplS Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
t ]

-- | print plain term
printTerm :: Term -> Doc
printTerm :: Term -> Doc
printTerm = Bool -> Term -> Doc
printPlainTerm Bool
True

printPlainTerm :: Bool -> Term -> Doc
printPlainTerm :: Bool -> Term -> Doc
printPlainTerm b :: Bool
b = (Doc, Int) -> Doc
forall a b. (a, b) -> a
fst ((Doc, Int) -> Doc) -> (Term -> (Doc, Int)) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Term -> (Doc, Int)
printTrm Bool
b

-- | print parens but leave a space if doc starts or ends with a bar
parensForTerm :: Doc -> Doc
parensForTerm :: Doc -> Doc
parensForTerm d :: Doc
d =
    let s :: String
s = Doc -> String
forall a. Show a => a -> String
show Doc
d
        b :: Char
b = '|'
    in Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then Doc
d
                else (if String -> Char
forall a. [a] -> a
head String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b then (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>) else Doc -> Doc
forall a. a -> a
id)
                         ((if String -> Char
forall a. [a] -> a
last String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b then (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space) else Doc -> Doc
forall a. a -> a
id) Doc
d)

printParenTerm :: Bool -> Int -> Term -> Doc
printParenTerm :: Bool -> Int -> Term -> Doc
printParenTerm b :: Bool
b i :: Int
i t :: Term
t = case Bool -> Term -> (Doc, Int)
printTrm Bool
b Term
t of
    (d :: Doc
d, j :: Int
j) -> if Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i then Doc -> Doc
parensForTerm Doc
d else Doc
d

flatTuplex :: [Term] -> Continuity -> [Term]
flatTuplex :: [Term] -> Continuity -> [Term]
flatTuplex cs :: [Term]
cs c :: Continuity
c = case [Term]
cs of
    [] -> [Term]
cs
    _ -> case [Term] -> Term
forall a. [a] -> a
last [Term]
cs of
           Tuplex rs :: [Term]
rs@(_ : _ : _) d :: Continuity
d | Continuity
d Continuity -> Continuity -> Bool
forall a. Eq a => a -> a -> Bool
== Continuity
c -> [Term] -> [Term]
forall a. [a] -> [a]
init [Term]
cs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term] -> Continuity -> [Term]
flatTuplex [Term]
rs Continuity
d
           _ -> [Term]
cs

printMixfixAppl :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printMixfixAppl :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printMixfixAppl b :: Bool
b c :: Continuity
c f :: Term
f args :: [Term]
args = case Term
f of
        Const (VName n :: String
n (Just (AltSyntax s :: String
s is :: [Int]
is i :: Int
i))) (Hide {}) ->
             if [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
is Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Bool -> Bool -> Bool
&&
                (Bool
b Bool -> Bool -> Bool
|| String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
cNot Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "op " String
n) then
                   ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
s
                     ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Int -> Term -> Doc) -> [Int] -> [Term] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Bool -> Int -> Term -> Doc
printParenTerm Bool
b) [Int]
is [Term]
args, Int
i)
             else Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printApp Bool
b Continuity
c Term
f [Term]
args
        Const vn :: VName
vn _ | VName -> String
new VName
vn String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
allS, String
exS, String
ex1S] -> case [Term]
args of
            [Abs v :: Term
v t :: Term
t _] -> ([Doc] -> Doc
fsep [String -> Doc
text (VName -> String
new VName
vn) Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
False Term
v
                    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
                    , Bool -> Term -> Doc
printPlainTerm Bool
b Term
t], Int
lowPrio)
            _ -> Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printApp Bool
b Continuity
c Term
f [Term]
args
        App g :: Term
g a :: Term
a d :: Continuity
d | Continuity
c Continuity -> Continuity -> Bool
forall a. Eq a => a -> a -> Bool
== Continuity
d -> Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printMixfixAppl Bool
b Continuity
c Term
g (Term
a Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args)
        _ -> Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printApp Bool
b Continuity
c Term
f [Term]
args

-- | print the term using the alternative syntax (if True)
printTrm :: Bool -> Term -> (Doc, Int)
printTrm :: Bool -> Term -> (Doc, Int)
printTrm b :: Bool
b trm :: Term
trm = case Term
trm of
    Const vn :: VName
vn ty :: DTyp
ty -> let
        dvn :: Doc
dvn = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ VName -> String
new VName
vn
        nvn :: Doc
nvn = case DTyp
ty of
            Hide {} -> Doc
dvn
            Disp w :: Typ
w _ _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
dvn Doc -> Doc -> Doc
<+> Doc
doubleColon Doc -> Doc -> Doc
<+> Typ -> Doc
printType Typ
w
      in case VName -> Maybe AltSyntax
altSyn VName
vn of
          Nothing -> (Doc
nvn, Int
maxPrio)
          Just (AltSyntax s :: String
s is :: [Int]
is i :: Int
i) -> if Bool
b Bool -> Bool -> Bool
&& [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
is then
              ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
s [], Int
i) else (Doc
nvn, Int
maxPrio)
    Free vn :: VName
vn -> (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ VName -> String
new VName
vn, Int
maxPrio)
    Abs v :: Term
v t :: Term
t c :: Continuity
c -> (String -> Doc
text (case Continuity
c of
        NotCont -> "%"
        IsCont _ -> "Lam") Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
False Term
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
                    Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
b Term
t, Int
lowPrio)
    If i :: Term
i t :: Term
t e :: Term
e c :: Continuity
c -> let d :: Doc
d = [Doc] -> Doc
fsep [Bool -> Term -> Doc
printPlainTerm Bool
b Term
i,
                        String -> Doc
text (case Continuity
c of
                                 NotCont -> "then"
                                 IsCont _ -> "THEN")
                            Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
b Term
t,
                        String -> Doc
text (case Continuity
c of
                                 NotCont -> "else"
                                 IsCont _ -> "ELSE")
                            Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
b Term
e]
                  in case Continuity
c of
        NotCont -> (String -> Doc
text "if" Doc -> Doc -> Doc
<+> Doc
d, Int
lowPrio)
        IsCont _ -> (String -> Doc
text "IF" Doc -> Doc -> Doc
<+> Doc
d Doc -> Doc -> Doc
<+> String -> Doc
text "FI", Int
maxPrio)
    Case e :: Term
e ps :: [(Term, Term)]
ps -> (String -> Doc
text "case" Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
b Term
e Doc -> Doc -> Doc
<+> String -> Doc
text "of"
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ([Doc] -> [Doc]
bar ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Term, Term) -> Doc) -> [(Term, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: Term
p, t :: Term
t) ->
               [Doc] -> Doc
fsep [ Bool -> Term -> Doc
printPlainTerm Bool
b Term
p Doc -> Doc -> Doc
<+> String -> Doc
text "=>"
                    , Bool -> Int -> Term -> Doc
printParenTerm Bool
b (Int
lowPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Term
t]) [(Term, Term)]
ps), Int
lowPrio)
    Let es :: [(Term, Term)]
es i :: Term
i -> ([Doc] -> Doc
fsep [String -> Doc
text "let" Doc -> Doc -> Doc
<+>
           [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
               ((Term, Term) -> Doc) -> [(Term, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: Term
p, t :: Term
t) -> [Doc] -> Doc
fsep [ Bool -> Term -> Doc
printPlainTerm Bool
b Term
p Doc -> Doc -> Doc
<+> Doc
equals
                                       , Bool -> Term -> Doc
printPlainTerm Bool
b Term
t]) [(Term, Term)]
es)
           , String -> Doc
text "in" Doc -> Doc -> Doc
<+> Bool -> Term -> Doc
printPlainTerm Bool
b Term
i], Int
lowPrio)
    IsaEq t1 :: Term
t1 t2 :: Term
t2 ->
        ([Doc] -> Doc
fsep [ Bool -> Int -> Term -> Doc
printParenTerm Bool
b (Int
isaEqPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Term
t1 Doc -> Doc -> Doc
<+> Doc
isaEquals
                         , Bool -> Int -> Term -> Doc
printParenTerm Bool
b Int
isaEqPrio Term
t2], Int
isaEqPrio)
    Tuplex cs :: [Term]
cs c :: Continuity
c -> case Continuity
c of
        NotCont -> (Doc -> Doc
parensForTerm
                      (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Term -> Doc
printPlainTerm Bool
b)
                          ([Term] -> [Doc]) -> [Term] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [Term] -> Continuity -> [Term]
flatTuplex [Term]
cs Continuity
c)
                    , Int
maxPrio)
        IsCont _ -> case [Term]
cs of
                        [] -> String -> (Doc, Int)
forall a. HasCallStack => String -> a
error "IsaPrint, printTrm"
                        [a :: Term
a] -> Bool -> Term -> (Doc, Int)
printTrm Bool
b Term
a
                        a :: Term
a : aa :: [Term]
aa -> Bool -> Term -> (Doc, Int)
printTrm Bool
b (Term -> (Doc, Int)) -> Term -> (Doc, Int)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Continuity -> Term
App (Term -> Term -> Continuity -> Term
App
                                  Term
lpairTerm Term
a (Continuity -> Term) -> Continuity -> Term
forall a b. (a -> b) -> a -> b
$ Bool -> Continuity
IsCont Bool
False)
                                     ([Term] -> Continuity -> Term
Tuplex [Term]
aa Continuity
c) (Bool -> Continuity
IsCont Bool
False)
    App f :: Term
f a :: Term
a c :: Continuity
c -> Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printMixfixAppl Bool
b Continuity
c Term
f [Term
a]
    Set setdecl :: SetDecl
setdecl -> (SetDecl -> Doc
printSetDecl SetDecl
setdecl, Int
lowPrio)

printApp :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printApp :: Bool -> Continuity -> Term -> [Term] -> (Doc, Int)
printApp b :: Bool
b c :: Continuity
c t :: Term
t l :: [Term]
l = case [Term]
l of
     [] -> Bool -> Term -> (Doc, Int)
printTrm Bool
b Term
t
     _ -> Bool -> Continuity -> Doc -> [Term] -> (Doc, Int)
printDocApp Bool
b Continuity
c (Bool -> Int -> Term -> Doc
printParenTerm Bool
b (Int
maxPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Term
t) [Term]
l

printDocApp :: Bool -> Continuity -> Doc -> [Term] -> (Doc, Int)
printDocApp :: Bool -> Continuity -> Doc -> [Term] -> (Doc, Int)
printDocApp b :: Bool
b c :: Continuity
c d :: Doc
d l :: [Term]
l =
    ( [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (case Continuity
c of
        NotCont -> [Doc] -> [Doc]
forall a. a -> a
id
        IsCont True -> Doc -> [Doc] -> [Doc]
punctuate (Doc -> [Doc] -> [Doc]) -> Doc -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> Doc
text " $$"
        IsCont False -> Doc -> [Doc] -> [Doc]
punctuate (Doc -> [Doc] -> [Doc]) -> Doc -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> Doc
text " $")
          ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Int -> Term -> Doc
printParenTerm Bool
b Int
maxPrio) [Term]
l
    , Int
maxPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)

replaceUnderlines :: String -> [Doc] -> [Doc]
replaceUnderlines :: String -> [Doc] -> [Doc]
replaceUnderlines str :: String
str l :: [Doc]
l = case String
str of
    "" -> []
    '\'' : r :: String
r@(q :: Char
q : s :: String
s) -> if Char
q Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "_/'()"
                       then Doc -> [Doc] -> [Doc]
consDocBarSep (String -> Doc
text [Char
q]) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
s [Doc]
l
                       else Doc -> [Doc] -> [Doc]
consDocBarSep (String -> Doc
text "'") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
r [Doc]
l
    '_' : r :: String
r -> case [Doc]
l of
                  h :: Doc
h : t :: [Doc]
t -> Doc -> [Doc] -> [Doc]
consDocBarSep Doc
h ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
r [Doc]
t
                  _ -> String -> [Doc]
forall a. HasCallStack => String -> a
error "replaceUnderlines"
    '/' : ' ' : r :: String
r -> Doc
empty Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: String -> [Doc] -> [Doc]
replaceUnderlines String
r [Doc]
l
    q :: Char
q : r :: String
r -> if Char
q Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "()/" then String -> [Doc] -> [Doc]
replaceUnderlines String
r [Doc]
l
             else Doc -> [Doc] -> [Doc]
consDocBarSep (String -> Doc
text [Char
q]) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc] -> [Doc]
replaceUnderlines String
r [Doc]
l

consDocBarSep :: Doc -> [Doc] -> [Doc]
consDocBarSep :: Doc -> [Doc] -> [Doc]
consDocBarSep d :: Doc
d r :: [Doc]
r = case [Doc]
r of
  [] -> [Doc
d]
  h :: Doc
h : t :: [Doc]
t -> let
    b :: Char
b = '|'
    hs :: String
hs = Doc -> String
forall a. Show a => a -> String
show Doc
h
    ds :: String
ds = Doc -> String
forall a. Show a => a -> String
show Doc
d
    hhs :: Char
hhs = String -> Char
forall a. [a] -> a
head String
hs
    lds :: Char
lds = String -> Char
forall a. [a] -> a
last String
ds
    in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
hs Bool -> Bool -> Bool
|| String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
ds then (Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
h) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
t else
           if Char
hhs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b Bool -> Bool -> Bool
&& Char
lds Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '(' Bool -> Bool -> Bool
|| String -> Char
forall a. [a] -> a
last String
ds Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b Bool -> Bool -> Bool
&& Char
hhs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')'
           then (Doc
d Doc -> Doc -> Doc
<+> Doc
h) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
t
           else (Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
h) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
t

-- end of term printing

printLocales :: Locales -> Doc
printLocales :: Locales -> Doc
printLocales = [Doc] -> Doc
vsep ([Doc] -> Doc) -> (Locales -> [Doc]) -> Locales -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, LocaleDecl) -> Doc) -> [(String, LocaleDecl)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, LocaleDecl) -> Doc
printLocale ([(String, LocaleDecl)] -> [Doc])
-> (Locales -> [(String, LocaleDecl)]) -> Locales -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, LocaleDecl)] -> [(String, LocaleDecl)]
orderLDecs ([(String, LocaleDecl)] -> [(String, LocaleDecl)])
-> (Locales -> [(String, LocaleDecl)])
-> Locales
-> [(String, LocaleDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Locales -> [(String, LocaleDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList

printDefinitions :: Defs -> Doc
printDefinitions :: Defs -> Doc
printDefinitions = [Doc] -> Doc
vsep ([Doc] -> Doc) -> (Defs -> [Doc]) -> Defs -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Def) -> Doc) -> [(String, Def)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, Def) -> Doc
printDefinition ([(String, Def)] -> [Doc])
-> (Defs -> [(String, Def)]) -> Defs -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defs -> [(String, Def)]
forall k a. Map k a -> [(k, a)]
Map.toList

printFunctions :: Funs -> Doc
printFunctions :: Funs -> Doc
printFunctions = [Doc] -> Doc
vsep ([Doc] -> Doc) -> (Funs -> [Doc]) -> Funs -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, FunDef) -> Doc) -> [(String, FunDef)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, FunDef) -> Doc
printFunction ([(String, FunDef)] -> [Doc])
-> (Funs -> [(String, FunDef)]) -> Funs -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funs -> [(String, FunDef)]
forall k a. Map k a -> [(k, a)]
Map.toList

printFixesAssumes :: Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes :: Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes h :: Doc
h p' :: [Doc]
p' a :: [Doc]
a f :: [Doc]
f = [Doc] -> Doc
vcat
  [ Doc
h Doc -> Doc -> Doc
<+> (if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Doc] -> Bool) -> [Doc] -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc]
p' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
a [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
f then Doc
empty else String -> Doc
text "=") Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep [Doc]
p'
    Doc -> Doc -> Doc
<+> if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
p' Bool -> Bool -> Bool
|| [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
a Bool -> Bool -> Bool
&& [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
f then Doc
empty else String -> Doc
text "+"
  , if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
f then Doc
empty else String -> Doc
text "fixes" Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs [Doc]
f
  , if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
a then Doc
empty else String -> Doc
text "assumes" Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs [Doc]
a
  ]

printDefinition :: (String, Def) -> Doc
printDefinition :: (String, Def) -> Doc
printDefinition (n :: String
n, (tp :: Typ
tp, vs :: [(String, Typ)]
vs, tm :: Term
tm)) = String -> Doc
text "definition" Doc -> Doc -> Doc
<+> String -> Doc
text String
n Doc -> Doc -> Doc
<+> String -> Doc
text "::"
 Doc -> Doc -> Doc
$+$ (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> Doc
printTyp SynFlag
Null) Typ
tp Doc -> Doc -> Doc
<+> String -> Doc
text "where"
 Doc -> Doc -> Doc
$+$ Doc -> Doc
doubleQuotes (String -> Doc
text String
n Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (((String, Typ) -> Doc) -> [(String, Typ)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc)
-> ((String, Typ) -> String) -> (String, Typ) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Typ) -> String
forall a b. (a, b) -> a
fst) [(String, Typ)]
vs)
 Doc -> Doc -> Doc
<+> String -> Doc
text "\\<equiv>" Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
tm)

printFunction :: (String, FunDef) -> Doc
printFunction :: (String, FunDef) -> Doc
printFunction (n :: String
n, (tp :: Typ
tp, def_eqs :: [([Term], Term)]
def_eqs)) = String -> Doc
text "fun" Doc -> Doc -> Doc
<+> String -> Doc
text String
n Doc -> Doc -> Doc
<+> String -> Doc
text "::"
 Doc -> Doc -> Doc
$+$ (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> Doc
printTyp SynFlag
Null) Typ
tp Doc -> Doc -> Doc
<+> String -> Doc
text "where"
 Doc -> Doc -> Doc
$+$ ([Doc] -> Doc
vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text "|"))
      ((([Term], Term) -> Doc) -> [([Term], Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (pats :: [Term]
pats, tm :: Term
tm) -> Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
n
       Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
printTerm [Term]
pats) Doc -> Doc -> Doc
<+> String -> Doc
text "="
       Doc -> Doc -> Doc
<+> Term -> Doc
printTerm Term
tm) [([Term], Term)]
def_eqs)

printLocale :: (String, LocaleDecl) -> Doc
printLocale :: (String, LocaleDecl) -> Doc
printLocale (n :: String
n, (parents :: [String]
parents, in_ax :: [(String, Term)]
in_ax, ex_ax :: [(String, Term)]
ex_ax, params :: [(String, Typ, Maybe AltSyntax)]
params)) =
 let p' :: [Doc]
p' = Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
Data.List.intersperse (String -> Doc
text "+") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
parents
     a :: [Doc]
a = ((String, Term) -> Doc) -> [(String, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Term
t) -> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text ":"
           Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) Term
t) [(String, Term)]
in_ax
     f :: [Doc]
f = ((String, Typ, Maybe AltSyntax) -> Doc)
-> [(String, Typ, Maybe AltSyntax)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Typ
t, alt :: Maybe AltSyntax
alt) -> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text "::"
                 Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> Doc
printTyp SynFlag
Null) Typ
t
                 Doc -> Doc -> Doc
<+> (case Maybe AltSyntax
alt of
                       Just (AltSyntax s' :: String
s' [i1 :: Int
i1, i2 :: Int
i2] i :: Int
i) -> Doc -> Doc
parens (
                        String -> Doc
text (if Int
i1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 then "infix "
                        else if Int
i1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i2 then "infixr "
                        else "infixl ") Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text String
s')
                        Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i))
                       _ -> Doc
empty
                 )) [(String, Typ, Maybe AltSyntax)]
params
 in [Doc] -> Doc
vcat [
     Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes (String -> Doc
text "locale" Doc -> Doc -> Doc
<+> String -> Doc
text String
n) [Doc]
p' [Doc]
a [Doc]
f,
     [Doc] -> Doc
vcat (((String, Term) -> Doc) -> [(String, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Term
t) -> String -> Doc
text ("theorem (in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
           Doc -> Doc -> Doc
<+> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text ":"
           Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) Term
t
           Doc -> Doc -> Doc
<+> String -> Doc
text "apply(auto)"
           Doc -> Doc -> Doc
<+> String -> Doc
text "done") [(String, Term)]
ex_ax)]

printClassrel :: Classrel -> Doc
printClassrel :: Classrel -> Doc
printClassrel = [Doc] -> Doc
vsep ([Doc] -> Doc) -> (Classrel -> [Doc]) -> Classrel -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IsaClass, ClassDecl) -> Doc) -> [(IsaClass, ClassDecl)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (IsaClass, ClassDecl) -> Doc
printClassR ([(IsaClass, ClassDecl)] -> [Doc])
-> (Classrel -> [(IsaClass, ClassDecl)]) -> Classrel -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)]
orderCDecs ([(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)])
-> (Classrel -> [(IsaClass, ClassDecl)])
-> Classrel
-> [(IsaClass, ClassDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Classrel -> [(IsaClass, ClassDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList

printClassR :: (IsaClass, ClassDecl) -> Doc
printClassR :: (IsaClass, ClassDecl) -> Doc
printClassR (y :: IsaClass
y, (parents :: Sort
parents, assumptions :: [(String, Term)]
assumptions, fxs :: [(String, Typ)]
fxs)) =
 let a :: [Doc]
a = ((String, Term) -> Doc) -> [(String, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Term
t) -> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text ":"
          Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
printTerm) Term
t) [(String, Term)]
assumptions
     f :: [Doc]
f = ((String, Typ) -> Doc) -> [(String, Typ)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Typ
t) -> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text "::"
          Doc -> Doc -> Doc
<+> (Doc -> Doc
doubleQuotes (Doc -> Doc) -> (Typ -> Doc) -> Typ -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynFlag -> Typ -> Doc
printTyp SynFlag
Null) Typ
t) [(String, Typ)]
fxs
     parents' :: Sort
parents' = (IsaClass -> Bool) -> Sort -> Sort
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (IsaClass s :: String
s) -> String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem String
s
       ["HOL.type_class", "HOL.type", "type", "type_class"]) Sort
parents
     p' :: [Doc]
p' = Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
Data.List.intersperse (String -> Doc
text "+") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (IsaClass -> Doc) -> Sort -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IsaClass -> Doc
printClass Sort
parents'
 in Doc -> [Doc] -> [Doc] -> [Doc] -> Doc
printFixesAssumes (String -> Doc
text "class" Doc -> Doc -> Doc
<+> IsaClass -> Doc
printClass IsaClass
y) [Doc]
p' [Doc]
a [Doc]
f

orderCDecs :: [(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)]
orderCDecs :: [(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)]
orderCDecs =
   ((IsaClass, ClassDecl) -> (IsaClass, ClassDecl) -> Bool)
-> [(IsaClass, ClassDecl)] -> [(IsaClass, ClassDecl)]
forall a. (a -> a -> Bool) -> [a] -> [a]
topSort (IsaClass, ClassDecl) -> (IsaClass, ClassDecl) -> Bool
forall (t :: * -> *) a a b c b.
(Foldable t, Eq a) =>
(a, (t a, b, c)) -> (a, b) -> Bool
crord
 where
   crord :: (a, (t a, b, c)) -> (a, b) -> Bool
crord (_, (cs :: t a
cs, _, _)) (c :: a
c, _) = a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
c t a
cs

orderLDecs :: [(String, LocaleDecl)] -> [(String, LocaleDecl)]
orderLDecs :: [(String, LocaleDecl)] -> [(String, LocaleDecl)]
orderLDecs =
   ((String, LocaleDecl) -> (String, LocaleDecl) -> Bool)
-> [(String, LocaleDecl)] -> [(String, LocaleDecl)]
forall a. (a -> a -> Bool) -> [a] -> [a]
topSort (String, LocaleDecl) -> (String, LocaleDecl) -> Bool
forall (t :: * -> *) a a b c d b.
(Foldable t, Eq a) =>
(a, (t a, b, c, d)) -> (a, b) -> Bool
crord
 where
   crord :: (a, (t a, b, c, d)) -> (a, b) -> Bool
crord (_, (cs :: t a
cs, _, _, _)) (c :: a
c, _) = a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
c t a
cs

printMonArities :: String -> Arities -> Doc
printMonArities :: String -> Arities -> Doc
printMonArities tn :: String
tn = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (Arities -> [Doc]) -> Arities -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, [(IsaClass, [(Typ, Sort)])]) -> Doc)
-> [(String, [(IsaClass, [(Typ, Sort)])])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (t :: String
t, cl :: [(IsaClass, [(Typ, Sort)])]
cl) ->
                  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((IsaClass, [(Typ, Sort)]) -> Doc)
-> [(IsaClass, [(Typ, Sort)])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> (IsaClass, [(Typ, Sort)]) -> Doc
printThMorp String
tn String
t) [(IsaClass, [(Typ, Sort)])]
cl) ([(String, [(IsaClass, [(Typ, Sort)])])] -> [Doc])
-> (Arities -> [(String, [(IsaClass, [(Typ, Sort)])])])
-> Arities
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arities -> [(String, [(IsaClass, [(Typ, Sort)])])]
forall k a. Map k a -> [(k, a)]
Map.toList

printThMorp :: String -> TName -> (IsaClass, [(Typ, Sort)]) -> Doc
printThMorp :: String -> String -> (IsaClass, [(Typ, Sort)]) -> Doc
printThMorp tn :: String
tn t :: String
t xs :: (IsaClass, [(Typ, Sort)])
xs = case (IsaClass, [(Typ, Sort)])
xs of
   (IsaClass "Monad", _) ->
      if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "_mh" String
tn Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "_mhc" String
tn
      then String -> String -> Doc
printMInstance String
tn String
t
      else String -> Doc
forall a. HasCallStack => String -> a
error "IsaPrint, printInstance: monads not supported"
   _ -> Doc
empty

printMInstance :: String -> TName -> Doc
printMInstance :: String -> String -> Doc
printMInstance tn :: String
tn t :: String
t = let nM :: Doc
nM = String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_tm")
                          nM2 :: Doc
nM2 = String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_tm2")
 in Doc
-> String
-> String
-> String
-> [(String, String)]
-> [(String, String)]
-> Doc
prnThymorph Doc
nM "MonadType" String
tn String
t [("MonadType.M", "'a")] []
    Doc -> Doc -> Doc
$+$ String -> Doc
text "t_instantiate MonadOps mapping" Doc -> Doc -> Doc
<+> Doc
nM
    Doc -> Doc -> Doc
$+$ String -> Doc
text "renames:" Doc -> Doc -> Doc
<+>
       (String -> String) -> [(String, String)] -> Doc
brackMapList (\ x :: String
x -> String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x)
            [("MonadOpEta.eta", "eta"), ("MonadOpBind.bind", "bind")]
    Doc -> Doc -> Doc
$+$ String -> Doc
text "without_syntax"
    Doc -> Doc -> Doc
$++$ String -> Doc
text "defs "
    Doc -> Doc -> Doc
$+$ String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta_def:") Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes
          (String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta") Doc -> Doc -> Doc
<+> Doc
isaEquals Doc -> Doc -> Doc
<+> String -> Doc
text ("return_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t))
    Doc -> Doc -> Doc
$+$ String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind_def:") Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes
          (String -> Doc
text (String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind") Doc -> Doc -> Doc
<+> Doc
isaEquals Doc -> Doc -> Doc
<+> String -> Doc
text ("mbind_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t))
    Doc -> Doc -> Doc
$++$ String -> Doc
lunitLemma String
t
    Doc -> Doc -> Doc
$+$ String -> Doc
runitLemma String
t
    Doc -> Doc -> Doc
$+$ String -> Doc
assocLemma String
t
    Doc -> Doc -> Doc
$+$ String -> Doc
etaInjLemma String
t
    Doc -> Doc -> Doc
$++$ Doc
-> String
-> String
-> String
-> [(String, String)]
-> [(String, String)]
-> Doc
prnThymorph Doc
nM2 "MonadAxms" String
tn String
t [("MonadType.M", "'a")]
        [("MonadOpEta.eta", String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta"),
         ("MonadOpBind.bind", String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind")]
    Doc -> Doc -> Doc
$+$ String -> Doc
text "t_instantiate Monad mapping" Doc -> Doc -> Doc
<+> Doc
nM2
    Doc -> Doc -> Doc
$+$ String -> Doc
text "renames:" Doc -> Doc -> Doc
<+>
       (String -> String) -> [(String, String)] -> Doc
brackMapList (\ x :: String
x -> String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
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")]
    Doc -> Doc -> Doc
$+$ String -> Doc
text "without_syntax"
    Doc -> Doc -> Doc
$++$ String -> Doc
text " "
 where
  lunitLemma :: String -> Doc
lunitLemma w :: String
w = String -> Doc
text String
lemmaS Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_lunit:")
        Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind")
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta x"))
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "t::'a => 'b " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w)
        Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text "t x")
    Doc -> Doc -> Doc
$+$ String -> Doc
text "sorry "
  runitLemma :: String -> Doc
runitLemma w :: String
w = String -> Doc
text String
lemmaS Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_runit:")
        Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind")
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "t::'a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w) Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta")
        Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text "t")
    Doc -> Doc -> Doc
$+$ String -> Doc
text "sorry "
  assocLemma :: String -> Doc
assocLemma w :: String
w = String -> Doc
text String
lemmaS Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_assoc:")
        Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind")
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind")
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "s::'a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w) Doc -> Doc -> Doc
<+> String -> Doc
text "t") Doc -> Doc -> Doc
<+> String -> Doc
text "u"
        Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind s")
        Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text "%x." Doc -> Doc -> Doc
<+>
                 String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_bind") Doc -> Doc -> Doc
<+> String -> Doc
text "(t x) u"))
    Doc -> Doc -> Doc
$+$ String -> Doc
text "sorry "
  etaInjLemma :: String -> Doc
etaInjLemma w :: String
w = String -> Doc
text String
lemmaS Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta_inj:")
        Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta::'a => 'a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w)
             Doc -> Doc -> Doc
<+> String -> Doc
text "x"
             Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text (String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_eta y")
             Doc -> Doc -> Doc
<+> String -> Doc
text "==>" Doc -> Doc -> Doc
<+> String -> Doc
text "x = y")
    Doc -> Doc -> Doc
$+$ String -> Doc
text "sorry "

prnThymorph :: Doc -> String -> String -> TName -> [(String, String)]
            -> [(String, String)] -> Doc
prnThymorph :: Doc
-> String
-> String
-> String
-> [(String, String)]
-> [(String, String)]
-> Doc
prnThymorph nm :: Doc
nm xn :: String
xn tn :: String
tn t :: String
t ts :: [(String, String)]
ts ws :: [(String, String)]
ws = let qual :: String -> String
qual s :: String
s = String
tn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s in
     String -> Doc
text "thymorph" Doc -> Doc -> Doc
<+> Doc
nm Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+>
            String -> Doc
text String
xn Doc -> Doc -> Doc
<+> Doc
cfun Doc -> Doc -> Doc
<+> String -> Doc
text String
tn
     Doc -> Doc -> Doc
$+$ String -> Doc
text "  maps" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets
       ([Doc] -> Doc
hcat [ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
doubleQuotes (String -> Doc
text String
b Doc -> Doc -> Doc
<+> String -> Doc
text String
a) Doc -> Doc -> Doc
<+> Doc
mapsto
               Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text String
b Doc -> Doc -> Doc
<+> String -> Doc
text (String -> String
qual String
t))
             | (a :: String
a, b :: String
b) <- [(String, String)]
ts])
     Doc -> Doc -> Doc
$+$ (String -> String) -> [(String, String)] -> Doc
brackMapList String -> String
qual [(String, String)]
ws

brackMapList :: (String -> String) -> [(String, String)] -> Doc
brackMapList :: (String -> String) -> [(String, String)] -> Doc
brackMapList f :: String -> String
f ws :: [(String, String)]
ws = Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
  [ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
doubleQuotes (String -> Doc
text String
a) Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
f String
b)
  | (a :: String
a, b :: String
b) <- [(String, String)]
ws]

-- filter out types that are given in the domain table
printTypeDecls :: BaseSig -> DomainTab -> Arities -> Doc
printTypeDecls :: BaseSig -> DomainTab -> Arities -> Doc
printTypeDecls bs :: BaseSig
bs odt :: DomainTab
odt ars :: Arities
ars =
    let dt :: Map String [a]
dt = [(String, [a])] -> Map String [a]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, [a])] -> Map String [a])
-> [(String, [a])] -> Map String [a]
forall a b. (a -> b) -> a -> b
$ ((Typ, [(VName, [Typ])]) -> (String, [a]))
-> [(Typ, [(VName, [Typ])])] -> [(String, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: Typ
t, _) -> (Typ -> String
typeId Typ
t, [])) ([(Typ, [(VName, [Typ])])] -> [(String, [a])])
-> [(Typ, [(VName, [Typ])])] -> [(String, [a])]
forall a b. (a -> b) -> a -> b
$ DomainTab -> [(Typ, [(VName, [Typ])])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat DomainTab
odt
    in [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((String, [(IsaClass, [(Typ, Sort)])]) -> Doc)
-> [(String, [(IsaClass, [(Typ, Sort)])])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (BaseSig -> (String, [(IsaClass, [(Typ, Sort)])]) -> Doc
printTycon BaseSig
bs) ([(String, [(IsaClass, [(Typ, Sort)])])] -> [Doc])
-> [(String, [(IsaClass, [(Typ, Sort)])])] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Arities -> [(String, [(IsaClass, [(Typ, Sort)])])]
forall k a. Map k a -> [(k, a)]
Map.toList (Arities -> [(String, [(IsaClass, [(Typ, Sort)])])])
-> Arities -> [(String, [(IsaClass, [(Typ, Sort)])])]
forall a b. (a -> b) -> a -> b
$ Arities -> Map String [Any] -> Arities
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Arities
ars Map String [Any]
forall a. Map String [a]
dt

printTycon :: BaseSig -> (TName, [(IsaClass, [(Typ, Sort)])]) -> Doc
printTycon :: BaseSig -> (String, [(IsaClass, [(Typ, Sort)])]) -> Doc
printTycon bs :: BaseSig
bs (t :: String
t, arity' :: [(IsaClass, [(Typ, Sort)])]
arity') = case [(IsaClass, [(Typ, Sort)])]
arity' of
  [] -> String -> Doc
forall a. HasCallStack => String -> a
error "IsaPrint.printTycon"
  (_, rs :: [(Typ, Sort)]
rs) : _ ->
         if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
t
              (Set String -> Bool) -> Set String -> Bool
forall a b. (a -> b) -> a -> b
$ Set String -> BaseSig -> Map BaseSig (Set String) -> Set String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Set String
forall a. HasCallStack => String -> a
error "Isabelle.printTycon") BaseSig
bs
                (Map BaseSig (Set String) -> Set String)
-> Map BaseSig (Set String) -> Set String
forall a b. (a -> b) -> a -> b
$ IsaPreludes -> Map BaseSig (Set String)
preTypes IsaPreludes
isaPrelude
         then Doc
empty else
            String -> Doc
text String
typedeclS Doc -> Doc -> Doc
<+>
            (if [(Typ, Sort)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Typ, Sort)]
rs then Doc
empty else
             Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
             ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (((Typ, Sort), Int) -> Doc) -> [((Typ, Sort), Int)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc)
-> (((Typ, Sort), Int) -> String) -> ((Typ, Sort), Int) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("'a" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (((Typ, Sort), Int) -> String) -> ((Typ, Sort), Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (((Typ, Sort), Int) -> Int) -> ((Typ, Sort), Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Typ, Sort), Int) -> Int
forall a b. (a, b) -> b
snd) ([((Typ, Sort), Int)] -> [Doc]) -> [((Typ, Sort), Int)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [(Typ, Sort)] -> [((Typ, Sort), Int)]
forall a. [a] -> [(a, Int)]
number [(Typ, Sort)]
rs) Doc -> Doc -> Doc
<+> String -> Doc
text String
t

-- | show alternative syntax (computed by comorphisms)
printAlt :: VName -> Doc
printAlt :: VName -> Doc
printAlt (VName _ altV :: Maybe AltSyntax
altV) = case Maybe AltSyntax
altV of
    Nothing -> Doc
empty
    Just (AltSyntax s :: String
s is :: [Int]
is i :: Int
i) -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
doubleQuotes (String -> Doc
text String
s)
        Doc -> Doc -> Doc
<+> if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
is then Doc
empty else String -> Doc
text ([Int] -> String
forall a. Show a => a -> String
show [Int]
is) Doc -> Doc -> Doc
<+>
            if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
maxPrio then Doc
empty else String -> Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i)

instance Pretty Sign where
    pretty :: Sign -> Doc
pretty = Sign -> Doc
printSign

-- | a dummy constant table with wrong types
constructors :: DomainTab -> ConstTab
constructors :: DomainTab -> ConstTab
constructors = [(VName, Typ)] -> ConstTab
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VName, Typ)] -> ConstTab)
-> (DomainTab -> [(VName, Typ)]) -> DomainTab -> ConstTab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> (VName, Typ)) -> [VName] -> [(VName, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VName
v -> (VName
v, Typ
noTypeT))
               ([VName] -> [(VName, Typ)])
-> (DomainTab -> [VName]) -> DomainTab -> [(VName, Typ)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Typ, [(VName, [Typ])]) -> [VName])
-> [(Typ, [(VName, [Typ])])] -> [VName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((VName, [Typ]) -> VName) -> [(VName, [Typ])] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map (VName, [Typ]) -> VName
forall a b. (a, b) -> a
fst ([(VName, [Typ])] -> [VName])
-> ((Typ, [(VName, [Typ])]) -> [(VName, [Typ])])
-> (Typ, [(VName, [Typ])])
-> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Typ, [(VName, [Typ])]) -> [(VName, [Typ])]
forall a b. (a, b) -> b
snd) ([(Typ, [(VName, [Typ])])] -> [VName])
-> (DomainTab -> [(Typ, [(VName, [Typ])])]) -> DomainTab -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DomainTab -> [(Typ, [(VName, [Typ])])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

printMonSign :: Sign -> Doc
printMonSign :: Sign -> Doc
printMonSign sig :: Sign
sig = let ars :: Arities
ars = TypeSig -> Arities
arities (TypeSig -> Arities) -> TypeSig -> Arities
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig
                in
    String -> Arities -> Doc
printMonArities (Sign -> String
theoryName Sign
sig) Arities
ars

printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign sig :: Sign
sig = let dt :: DomainTab
dt = DomainTab -> DomainTab
ordDoms (DomainTab -> DomainTab) -> DomainTab -> DomainTab
forall a b. (a -> b) -> a -> b
$ Sign -> DomainTab
domainTab Sign
sig
                    ars :: Arities
ars = TypeSig -> Arities
arities (TypeSig -> Arities) -> TypeSig -> Arities
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig
                in
    Map String ([String], Typ) -> Doc
printAbbrs (TypeSig -> Map String ([String], Typ)
abbrs (TypeSig -> Map String ([String], Typ))
-> TypeSig -> Map String ([String], Typ)
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig) Doc -> Doc -> Doc
$++$
    BaseSig -> DomainTab -> Arities -> Doc
printTypeDecls (Sign -> BaseSig
baseSig Sign
sig) DomainTab
dt Arities
ars Doc -> Doc -> Doc
$++$
    Defs -> Doc
printDefinitions (TypeSig -> Defs
defs (TypeSig -> Defs) -> TypeSig -> Defs
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig) Doc -> Doc -> Doc
$++$
    Funs -> Doc
printFunctions (TypeSig -> Funs
funs (TypeSig -> Funs) -> TypeSig -> Funs
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig) Doc -> Doc -> Doc
$++$
    Locales -> Doc
printLocales (TypeSig -> Locales
locales (TypeSig -> Locales) -> TypeSig -> Locales
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig) Doc -> Doc -> Doc
$++$
    Classrel -> Doc
printClassrel (TypeSig -> Classrel
classrel (TypeSig -> Classrel) -> TypeSig -> Classrel
forall a b. (a -> b) -> a -> b
$ Sign -> TypeSig
tsig Sign
sig) Doc -> Doc -> Doc
$++$
    DomainTab -> Doc
printDomainDefs DomainTab
dt Doc -> Doc -> Doc
$++$
    ConstTab -> Doc
printConstTab (ConstTab -> ConstTab -> ConstTab
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (Sign -> ConstTab
constTab Sign
sig)
                  (ConstTab -> ConstTab) -> ConstTab -> ConstTab
forall a b. (a -> b) -> a -> b
$ DomainTab -> ConstTab
constructors DomainTab
dt) Doc -> Doc -> Doc
$++$
    (if Sign -> Bool
showLemmas Sign
sig
         then DomainTab -> Doc
forall (t :: * -> *).
Foldable t =>
t [(Typ, [(VName, [Typ])])] -> Doc
showCaseLemmata DomainTab
dt else Doc
empty)
    where
    printAbbrs :: Map String ([String], Typ) -> Doc
printAbbrs tab :: Map String ([String], Typ)
tab = if Map String ([String], Typ) -> Bool
forall k a. Map k a -> Bool
Map.null Map String ([String], Typ)
tab then Doc
empty else String -> Doc
text String
typesS
                     Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (((String, ([String], Typ)) -> Doc)
-> [(String, ([String], Typ))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, ([String], Typ)) -> Doc
printAbbr ([(String, ([String], Typ))] -> [Doc])
-> [(String, ([String], Typ))] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map String ([String], Typ) -> [(String, ([String], Typ))]
forall k a. Map k a -> [(k, a)]
Map.toList Map String ([String], Typ)
tab)
    printAbbr :: (String, ([String], Typ)) -> Doc
printAbbr (n :: String
n, (vs :: [String]
vs, t :: Typ
t)) = case [String]
vs of
        [] -> Doc
empty
        [x :: String
x] -> String -> Doc
text ('\'' Char -> String -> String
forall a. a -> [a] -> [a]
: String
x)
        _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                                   (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (String -> String) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ('\'' Char -> String -> String
forall a. a -> [a] -> [a]
:)) [String]
vs
      Doc -> Doc -> Doc
<+> String -> Doc
text String
n Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Typ -> Doc
printType Typ
t)
    printConstTab :: ConstTab -> Doc
printConstTab tab :: ConstTab
tab = if ConstTab -> Bool
forall k a. Map k a -> Bool
Map.null ConstTab
tab then Doc
empty else String -> Doc
text String
constsS
                        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (((VName, Typ) -> Doc) -> [(VName, Typ)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VName, Typ) -> Doc
printConst ([(VName, Typ)] -> [Doc]) -> [(VName, Typ)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ConstTab -> [(VName, Typ)]
forall k a. Map k a -> [(k, a)]
Map.toList ConstTab
tab)
    printConst :: (VName, Typ) -> Doc
printConst (vn :: VName
vn, t :: Typ
t) = String -> Doc
text (VName -> String
new VName
vn) Doc -> Doc -> Doc
<+> Doc
doubleColon Doc -> Doc -> Doc
<+>
                          Doc -> Doc
doubleQuotes (Typ -> Doc
printType Typ
t) Doc -> Doc -> Doc
<+> VName -> Doc
printAlt VName
vn
    isDomain :: Bool
isDomain = case Sign -> BaseSig
baseSig Sign
sig of
               HOLCF_thy -> Bool
True
               HsHOLCF_thy -> Bool
True
               MHsHOLCF_thy -> Bool
True
               _ -> Bool
False
    printDomainDefs :: DomainTab -> Doc
printDomainDefs dtDefs :: DomainTab
dtDefs = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([(Typ, [(VName, [Typ])])] -> Doc) -> DomainTab -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [(Typ, [(VName, [Typ])])] -> Doc
printDomainDef DomainTab
dtDefs
    printDomainDef :: [(Typ, [(VName, [Typ])])] -> Doc
printDomainDef dts :: [(Typ, [(VName, [Typ])])]
dts = if [(Typ, [(VName, [Typ])])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Typ, [(VName, [Typ])])]
dts then Doc
empty else
        String -> Doc
text (if Bool
isDomain then String
domainS else String
datatypeS)
        Doc -> Doc -> Doc
<+> [Doc] -> Doc
andDocs (((Typ, [(VName, [Typ])]) -> Doc)
-> [(Typ, [(VName, [Typ])])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Typ, [(VName, [Typ])]) -> Doc
printDomain [(Typ, [(VName, [Typ])])]
dts)
    printDomain :: (Typ, [(VName, [Typ])]) -> Doc
printDomain (t :: Typ
t, ops :: [(VName, [Typ])]
ops) =
       SynFlag -> Typ -> Doc
printTyp (if Bool
isDomain then SynFlag
Quoted else SynFlag
Null) Typ
t Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
       [Doc] -> Doc
fsep ([Doc] -> [Doc]
bar ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((VName, [Typ]) -> Doc) -> [(VName, [Typ])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VName, [Typ]) -> Doc
printDOp [(VName, [Typ])]
ops)
    printDOp :: (VName, [Typ]) -> Doc
printDOp (vn :: VName
vn, args :: [Typ]
args) = let opname :: String
opname = VName -> String
new VName
vn in
       String -> Doc
text (if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
opname then String -> String
forall a. Show a => a -> String
show String
opname else String
opname)
       Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (((Typ, Int) -> Doc) -> [(Typ, Int)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> (Typ, Int) -> Doc
forall a. Show a => String -> (Typ, a) -> Doc
printDOpArg String
opname) ([(Typ, Int)] -> [Doc]) -> [(Typ, Int)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [Typ] -> [(Typ, Int)]
forall a. [a] -> [(a, Int)]
number [Typ]
args)
       Doc -> Doc -> Doc
<+> VName -> Doc
printAlt VName
vn
    printDOpArg :: String -> (Typ, a) -> Doc
printDOpArg o :: String
o (a :: Typ
a, i :: a
i) = let
      d :: Doc
d = case Typ
a of
            TFree _ _ -> SynFlag -> Typ -> Doc
printTyp SynFlag
Null Typ
a
            _ -> Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ SynFlag -> Typ -> Doc
printTyp SynFlag
Null Typ
a
      in if Bool
isDomain then
           Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "lazy" Doc -> Doc -> Doc
<+>
               String -> Doc
text (String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
doubleColon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d
           else Doc
d
    showCaseLemmata :: t [(Typ, [(VName, [Typ])])] -> Doc
showCaseLemmata dtDefs :: t [(Typ, [(VName, [Typ])])]
dtDefs = String -> Doc
text (([(Typ, [(VName, [Typ])])] -> String)
-> t [(Typ, [(VName, [Typ])])] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [(Typ, [(VName, [Typ])])] -> String
showCaseLemmata1 t [(Typ, [(VName, [Typ])])]
dtDefs)
    showCaseLemmata1 :: [(Typ, [(VName, [Typ])])] -> String
showCaseLemmata1 = ((Typ, [(VName, [Typ])]) -> String)
-> [(Typ, [(VName, [Typ])])] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Typ, [(VName, [Typ])]) -> String
forall (t :: * -> *).
Foldable t =>
(Typ, [(VName, t Typ)]) -> String
showCaseLemma
    showCaseLemma :: (Typ, [(VName, t Typ)]) -> String
showCaseLemma (_, []) = ""
    showCaseLemma (tyCons :: Typ
tyCons, c :: (VName, t Typ)
c : cns :: [(VName, t Typ)]
cns) =
      let cs :: String
cs = "case caseVar of" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp
          sc :: Bool -> String
sc b :: Bool
b = Bool -> (VName, t Typ) -> String
forall (t :: * -> *).
Foldable t =>
Bool -> (VName, t Typ) -> String
showCons Bool
b (VName, t Typ)
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ ((VName, t Typ) -> String) -> [(VName, t Typ)] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (("   | " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> ((VName, t Typ) -> String) -> (VName, t Typ) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> (VName, t Typ) -> String
forall (t :: * -> *).
Foldable t =>
Bool -> (VName, t Typ) -> String
showCons Bool
b) [(VName, t Typ)]
cns
          clSome :: String
clSome = Bool -> String
sc Bool
True
          cl :: String
cl = Bool -> String
sc Bool
False
          showCons :: Bool -> (VName, t Typ) -> String
showCons b :: Bool
b (VName {new :: VName -> String
new = String
cName}, args :: t Typ
args) =
            let pat :: String
pat = String
cName String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Typ -> String) -> t Typ -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Typ -> String) -> Typ -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> String
showArg) t Typ
args
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ "=>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp
                term :: String
term = String -> t Typ -> String
forall (t :: * -> *). Foldable t => String -> t Typ -> String
showCaseTerm String
cName t Typ
args
            in
               String
pat String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool
b then "Some" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rb String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
                 else String
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
          showCaseTerm :: String -> t Typ -> String
showCaseTerm name :: String
name args :: t Typ
args = case String
name of
            "" -> String
sa
            n :: Char
n : _ -> Char -> Char
toLower Char
n Char -> String -> String
forall a. a -> [a] -> [a]
: String
sa
            where sa :: String
sa = (Typ -> String) -> t Typ -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Typ -> String) -> Typ -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> String
showArg) t Typ
args
          showArg :: Typ -> String
showArg (TFree [] _) = "varName"
          showArg (TFree (n :: Char
n : ns :: String
ns) _) = Char -> Char
toLower Char
n Char -> String -> String
forall a. a -> [a] -> [a]
: String
ns
          showArg (TVar v :: Indexname
v s :: Sort
s) = Typ -> String
showArg (String -> Sort -> Typ
TFree (Indexname -> String
unindexed Indexname
v) Sort
s)
          showArg (Type [] _ _) = "varName"
          showArg (Type m :: String
m@(n :: Char
n : ns :: String
ns) _ s :: [Typ]
s) =
            if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
m ["typeAppl", "fun", "*"]
               then (Typ -> String) -> [Typ] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Typ -> String
showArg [Typ]
s
               else Char -> Char
toLower Char
n Char -> String -> String
forall a. a -> [a] -> [a]
: String
ns
          showName :: Typ -> String
showName (TFree v :: String
v _) = String
v
          showName (TVar v :: Indexname
v _) = Indexname -> String
unindexed Indexname
v
          showName (Type n :: String
n _ _) = String
n
          proof' :: String
proof' = "apply (case_tac caseVar)\napply (auto)\ndone\n"
      in
        String
lemmaS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ "case_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Typ -> String
showName Typ
tyCons String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_SomeProm" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "[simp]:\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
clSome String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "=\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Some" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cl String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rb String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"\n"
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proof'

instance Pretty Sentence where
    pretty :: Sentence -> Doc
pretty = Sentence -> Doc
printSentence

sp :: String
sp :: String
sp = " "

rb :: String
rb :: String
rb = ")"

lb :: String
lb :: String
lb = "("

-- Pretty printing of proofs

instance Pretty IsaProof where
    pretty :: IsaProof -> Doc
pretty = IsaProof -> Doc
printIsaProof

printIsaProof :: IsaProof -> Doc
printIsaProof :: IsaProof -> Doc
printIsaProof (IsaProof p :: [ProofCommand]
p e :: ProofEnd
e) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (ProofCommand -> Doc) -> [ProofCommand] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProofCommand -> Doc
forall a. Pretty a => a -> Doc
pretty [ProofCommand]
p [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ProofEnd -> Doc
forall a. Pretty a => a -> Doc
pretty ProofEnd
e]

instance Pretty ProofCommand where
    pretty :: ProofCommand -> Doc
pretty = ProofCommand -> Doc
printProofCommand

printProofCommand :: ProofCommand -> Doc
printProofCommand :: ProofCommand -> Doc
printProofCommand pc :: ProofCommand
pc =
    case ProofCommand
pc of
      Apply pms :: [ProofMethod]
pms plus :: Bool
plus ->
          let plusDoc :: Doc
plusDoc = if Bool
plus then String -> Doc
text "+" else Doc
empty
          in String -> Doc
text String
applyS Doc -> Doc -> Doc
<+> Doc -> Doc
parens
                              ([Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (ProofMethod -> Doc) -> [ProofMethod] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProofMethod -> Doc
forall a. Pretty a => a -> Doc
pretty [ProofMethod]
pms) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
plusDoc
      Using ls :: [String]
ls -> String -> Doc
text String
usingS Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
ls)
      Back -> String -> Doc
text String
backS
      Defer x :: Int
x -> String -> Doc
text String
deferS Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
x
      Prefer x :: Int
x -> String -> Doc
text String
preferS Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
x
      Refute -> String -> Doc
text String
refuteS

instance Pretty ProofEnd where
    pretty :: ProofEnd -> Doc
pretty = ProofEnd -> Doc
printProofEnd

printProofEnd :: ProofEnd -> Doc
printProofEnd :: ProofEnd -> Doc
printProofEnd pe :: ProofEnd
pe =
    case ProofEnd
pe of
      By pm :: ProofMethod
pm -> String -> Doc
text String
byS Doc -> Doc -> Doc
<+> Doc -> Doc
parens (ProofMethod -> Doc
forall a. Pretty a => a -> Doc
pretty ProofMethod
pm)
      DotDot -> String -> Doc
text String
dotDot
      Done -> String -> Doc
text String
doneS
      Oops -> String -> Doc
text String
oopsS
      Sorry -> String -> Doc
text String
sorryS

instance Pretty Modifier where
    pretty :: Modifier -> Doc
pretty = Modifier -> Doc
printModifier

printModifier :: Modifier -> Doc
printModifier :: Modifier -> Doc
printModifier m :: Modifier
m =
    case Modifier
m of
      No_asm -> String -> Doc
text "no_asm"
      No_asm_simp -> String -> Doc
text "no_asm_simp"
      No_asm_use -> String -> Doc
text "no_asm_use"

instance Pretty ProofMethod where
    pretty :: ProofMethod -> Doc
pretty = ProofMethod -> Doc
printProofMethod

printProofMethod :: ProofMethod -> Doc
printProofMethod :: ProofMethod -> Doc
printProofMethod pm :: ProofMethod
pm =
    case ProofMethod
pm of
      Auto -> String -> Doc
text String
autoS
      Simp -> String -> Doc
text String
simpS
      AutoSimpAdd m :: Maybe Modifier
m names :: [String]
names -> let modDoc :: Doc
modDoc = case Maybe Modifier
m of
                                            Just mod' :: Modifier
mod' -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Modifier -> Doc
forall a. Pretty a => a -> Doc
pretty Modifier
mod'
                                            Nothing -> Doc
empty
                             in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [String -> Doc
text String
autoS, String -> Doc
text String
simpS, Doc
modDoc,
                                             String -> Doc
text "add:"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
names
      SimpAdd m :: Maybe Modifier
m names :: [String]
names -> let modDoc :: Doc
modDoc = case Maybe Modifier
m of
                                        Just mod' :: Modifier
mod' -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Modifier -> Doc
forall a. Pretty a => a -> Doc
pretty Modifier
mod'
                                        Nothing -> Doc
empty
                         in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [String -> Doc
text String
simpS, Doc
modDoc, String -> Doc
text "add:"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                            (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
names
      Induct var :: Term
var -> String -> Doc
text String
inductS Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Term -> Doc
printTerm Term
var)
      CaseTac t :: Term
t -> String -> Doc
text String
caseTacS Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Term -> Doc
printTerm Term
t)
      SubgoalTac t :: Term
t -> String -> Doc
text String
subgoalTacS Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Term -> Doc
printTerm Term
t)
      Insert ts :: [String]
ts -> [Doc] -> Doc
fsep (String -> Doc
text String
insertS Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
ts)
      Other s :: String
s -> String -> Doc
text String
s