1N/ACopyright : (c) University of Cambridge, Cambridge, England
1N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2004
1N/AMaintainer : maeder@tzi.de
1N/AStability : provisional
1N/APortability : portable
1N/APrinting functions for Isabelle logic.
1N/A todo: brackets in (? x . p x) ==> q
1N/A properly construct docs
1N/A------------------- Printing functions -------------------
1N/AshowBaseSig :: BaseSig -> String
1N/AshowBaseSig = reverse . drop 4 . reverse . show
1N/Ainstance PrettyPrint BaseSig where
1N/A printText0 _ s = text $ showBaseSig s
1N/Ainstance PrettyPrint IsaClass where
1N/A printText0 _ (IsaClass c) = parens $ text c
1N/Ainstance PrintLaTeX Sentence where
1N/A printLatex0 = printText0
1N/A{- test for sentence translation -}
1N/Ainstance PrettyPrint Sentence where
1N/A printText0 _ = text . showTerm . senTerm
1N/AshowIsaDef :: Named Sentence -> Doc
1N/AshowIsaDef x = let d = senName x in
1N/A if d == "" then empty
1N/A else text (d++"_def:") <+> text ("\""++(showTerm $ senTerm $ sentence x)++"\"")
1N/A-- else text (d++"_def:"++sp++"\""++(showTerm $ senTerm $ sentence x)++"\"")
1N/Ainstance PrettyPrint Typ where
1N/A printText0 _ = text . showTyp Null 1000 -- Unquoted 1000
1N/AshowClass :: Sort -> String
1N/AshowClass s = case s of
1N/A (IsaClass x):(a:as) -> x ++ "," ++ showClass (a:as)
1N/A (IsaClass x) : [] -> x
1N/AshowSort :: Sort -> String
1N/AshowSort s = "{"++(showClass s)++"}"
1N/Adata SynFlag = Unquoted | Quoted | Null
1N/AshowTyp :: SynFlag -> Integer -> Typ -> String
1N/AshowTyp a pri t = case t of
1N/A (TFree v s) -> case a of
1N/A Unquoted -> lb ++ "\'" ++ v ++ "::" ++ (showSort s) ++ rb
1N/A Quoted -> "\'" ++ v ++ "::\"" ++ (showSort s) ++ "\""
1N/A (TVar (v,_) s) -> case a of
1N/A Unquoted -> lb ++ "?\'" ++ v ++ "::" ++ (showSort s) ++ rb
1N/A Quoted -> "?\'" ++ v ++ "::\"" ++ (showSort s) ++ "\""
1N/A (Type name _ args) -> case args of
1N/A arg:[] -> showTyp a 10 arg ++ sp ++ name
1N/A [t1,t2] -> let tyst = showTypeOp a pri name t1 t2
1N/A _ -> lb ++ tyst ++ rb
1N/A _ -> let tyst = (rearrangeVarsInType a pri name args)
1N/A _ -> lb ++ tyst ++ rb
1N/A where rearrangeVarsInType x p n as =
1N/A let (tyVars,types) = foldl split ([],[]) as
1N/A in (encloseTup x p (concRev tyVars types)) ++ sp ++ n
1N/A split (tv,ty) k = case k of
1N/A TFree _ _ -> (tv++[k],ty)
1N/A concRev b c = reverse b ++ reverse c
1N/A encloseTup f g l = if (length l) < 2 then showTypTup f g l else lb++(showTypTup f g l)++rb
1N/A showTypTup f g l = case l of
1N/A [c] -> showTyp f g c
1N/A c:b:as -> (showTyp f g c)++","++sp++(showTypTup f g (b:as))
1N/A showTypeOp x p n r1 r2
1N/A bracketize (p<=10) (showTyp x 10 r1 ++ " => " ++ showTyp x 10 r2)
1N/A bracketize (p<=10) (showTyp x 10 r1 ++ " -> " ++ showTyp x 10 r2)
1N/A lb ++ showTyp x p r1 ++ " * " ++ showTyp x p r2 ++ rb
1N/A lb ++ showTyp x p r1 ++ " ** " ++ showTyp x p r2 ++ rb
1N/A | True = rearrangeVarsInType x p n [r1,r2]
1N/Ainstance PrettyPrint TypeSig where
1N/A printText0 ga tysig = printText0 ga $ arities tysig
1N/Ainstance PrettyPrint Term where
1N/A printText0 _ = text . showTerm -- outerShowTerm
1N/A -- back to showTerm, because meta !! causes problems with show ?thesis
1N/AtypedVars2st :: (a -> String) -> (b -> String) -> [(a,b)] -> String
1N/AtypedVars2st f g ls = concat [" (" ++ (f x) ++ "::" ++ (g y) ++ ")" | (x,y) <- ls]
1N/AshowTypedVars :: [(Term,Typ)] -> String
1N/AshowTypedVars ls = typedVars2st showTerm (showTyp Unquoted 1000) ls
1N/AshowQuantStr :: String -> String
1N/AshowQuantStr s | s == allS = "!"
1N/AshowTerm :: Term -> String
1N/AshowTerm (Const c _) = c
1N/AshowTerm (Free v _) = v
1N/AshowTerm (Tuplex ls c) = case c of
1N/A IsCont -> "< " ++ (showTupleArgs ls) ++ ">" -- the extra space takes care of a minor Isabelle bug
1N/A NotCont -> "(" ++ (showTupleArgs ls) ++ ")"
1N/A showTupleArgs xs = case xs of
1N/A (Free n t) -> (showTerm a) ++ "::" ++ (showTyp Null 1000 t) ++ "," ++ showTupleArgs as
1N/A-- (showTyp Unquoted 1000 t) ++ "," ++ showTupleArgs as
1N/A _ -> (showTerm a) ++ "," ++ showTupleArgs as
1N/AshowTerm (Abs v y t l)
1N/A | y == noType = lb ++ (case l of
1N/A IsCont -> "LAM ") ++ showTerm v ++ ". " ++ showTerm t ++ rb
1N/A | True = lb ++ (case l of
1N/A IsCont -> "LAM ") ++ (case v of
1N/A (Free n y) -> showTerm v ++ "::"
1N/A ++ showTyp Null 1000 y -- Unquoted 1000 y
1N/A _ -> showTerm v) ++ ". " ++ showTerm t ++ rb
1N/A-- showTerm (App (Const q _) (Abs v ty t _) _) | q `elem` [allS, exS, ex1S] =
1N/A-- showQuant (showQuantStr q) v ty t
1N/A-- showTerm t@(Const c _) = showPTree (toPrecTree t)
1N/AshowTerm (Paren t) = showTerm t
1N/AshowTerm (Fix t) = lb++"fix"++"$"++(showTerm t)++rb
1N/AshowTerm t@(App _ _ NotCont) = showPTree (toPrecTree t)
1N/AshowTerm (App t1 t2 IsCont) = lb++(showTerm t1)++"$"++(showTerm t2)++rb
1N/AshowTerm Bottom = "UU"
1N/AshowTerm (IsaEq t1 t2) = lb ++ (showTerm t1) ++ sp ++ "=="
1N/A ++ sp ++ (showTerm t2) ++ rb
1N/AshowTerm (Case term alts) =
1N/A let sAlts = map showCaseAlt alts
1N/A in lb ++ "case" ++ sp ++ showTerm term ++ sp ++ "of"
1N/A ++ concat (map ((++) ("\n" ++ sp ++ sp ++ sp ++ "|" ++ sp))
1N/AshowTerm (If t1 t2 t3 c) = case c of
1N/A lb ++ "if" ++ sp ++ showTerm t1 ++ sp ++ "then" ++ sp
1N/A ++ showTerm t2 ++ sp ++ "else" ++ sp ++ showTerm t3 ++ rb
1N/A lb ++ "If" ++ sp ++ showTerm t1 ++ sp ++ "then" ++ sp
1N/A ++ showTerm t2 ++ sp ++ "else" ++ sp ++ showTerm t3 ++ sp ++ "fi" ++ rb
1N/AshowTerm (Let pts t) = lb ++ "let" ++ sp ++ showPat False (head pts)
1N/A ++ concat (map (showPat True) (tail pts))
1N/A ++ sp ++ "in" ++ sp ++ showTerm t ++ rb
1N/AshowPat :: Bool -> (Term, Term) -> String
1N/AshowPat b (pat, term) =
1N/A let s = sp ++ showTerm pat ++ sp ++ "=" ++ sp ++ showTerm term
1N/A in-- showTerm (Const c _) = c
1N/AshowCaseAlt :: (Term, Term) -> String
1N/AshowCaseAlt (pat, term) =
1N/A showPattern pat ++ sp ++ "=>" ++ sp ++ showTerm term
1N/AshowPattern :: Term -> String
1N/AshowPattern (App t t' _) = showPattern t ++ sp ++ showPattern t'
1N/AshowPattern t = showTerm t
1N/AshowQuant :: String -> Term -> Typ -> Term -> String
1N/AshowQuant s var typ term =
1N/A s++sp++ showTerm var ++" :: "++ showTyp Null 1000 typ ++ " . " -- Unquoted 1000 typ ++ " . "
1N/AouterShowTerm :: Term -> String
1N/AouterShowTerm (App (Const q _) (Abs v ty t _) _) | q == allS =
1N/A outerShowQuant "!!" v ty t
1N/AouterShowTerm (App (App (Const o _) t1 _) t2 _) | o == impl =
1N/A showTerm t1 ++ " ==> " ++ outerShowTerm1 t2
1N/AouterShowTerm t = showTerm t
1N/AouterShowTerm1 :: Term -> String
1N/AouterShowTerm1 t@(App (App (Const o _) _ _) _ _) | o == impl =
1N/AouterShowTerm1 t = showTerm t
1N/AouterShowQuant :: String -> Term -> Typ -> Term -> String
1N/AouterShowQuant s var typ term =
1N/A s++sp++ showTerm var ++" :: "++showTyp Null 1000 typ ++ " . " -- Unquoted 1000 typ++" . "
1N/A ++ outerShowTerm term
1N/A For nearly perfect parenthesis - they only appear when needed -
1N/A formula's lhs formula's rhs
1N/A Every connector is annotated with its precedence, every 'unbreakable'
1N/A formula gets the lowest precedence.
1N/A-- term annotated with precedence
1N/Adata PrecTerm = PrecTerm Term Precedence deriving (Show)
1N/Atype Precedence = Int
1N/A{- Precedences (descending): __ __ (Isabelle's term application),
1N/A application of HasCASL ops, <=>, =, /\, \/, =>
1N/A Associativity: = -- left
1N/Adata PrecTermTree = Node PrecTerm [PrecTermTree]
1N/AisaAppPrec :: Term -> PrecTerm
1N/AisaAppPrec t = PrecTerm t 0
1N/AappPrec :: Term -> PrecTerm
1N/AappPrec t = PrecTerm t 5
1N/AeqvPrec :: Term -> PrecTerm
1N/AeqvPrec t = PrecTerm t 7
1N/AeqPrec :: Term -> PrecTerm
1N/AeqPrec t = PrecTerm t 10
1N/AandPrec :: Term -> PrecTerm
1N/AandPrec t = PrecTerm t 20
1N/AorPrec :: Term -> PrecTerm
1N/AorPrec t = PrecTerm t 30
1N/AimplPrec :: Term -> PrecTerm
1N/AimplPrec t = PrecTerm t 40
1N/AcapplPrec :: Term -> PrecTerm
1N/AcapplPrec t = PrecTerm t 999
1N/AnoPrec :: Term -> PrecTerm
1N/AnoPrec t = PrecTerm t (-10)
1N/AbinFunct :: String -> Term -> PrecTerm
1N/AbinFunct s | s == eqv = eqvPrec
1N/A | s == conj = andPrec
1N/A | s == disj = orPrec
1N/A | s == impl = implPrec
1N/A-- | s == cappl = capplPrec
1N/A | otherwise = appPrec
1N/AtoPrecTree :: Term -> PrecTermTree
1N/A App c1@(Const q _) a2@(Abs _ _ _ _) _ | q `elem` [allS, exS, ex1S] ->
1N/A Node (isaAppPrec $ con quantS) [toPrecTree c1, toPrecTree a2]
1N/A-- App t1 t2 IsCont -> Node (capplPrec $ con cappl)
1N/A-- [toPrecTree t1, toPrecTree t2]
1N/A App (App t@(Const o _) t3 NotCont) t2 NotCont ->
1N/A Node (binFunct o t) [toPrecTree t3, toPrecTree t2]
1N/A App t1 t2 NotCont -> Node (isaAppPrec $ con dummyS)
1N/A [toPrecTree t1, toPrecTree t2]
1N/A _ -> Node (noPrec trm) []
1N/Adata Assoc = LeftAs | NoAs | RightAs
1N/AshowPTree :: PrecTermTree -> String
1N/AshowPTree (Node (PrecTerm term _) []) = showTerm term
1N/AshowPTree (Node (PrecTerm term pre) annos) =
1N/A let leftChild = head annos
1N/A rightChild = last annos
1N/A Const c _ | c == eq -> infixP pre "=" LeftAs leftChild rightChild
1N/A | c == "op +" -> infixP pre "+" LeftAs leftChild rightChild
1N/A | c == "op -" -> infixP pre "-" LeftAs leftChild rightChild
1N/A | c == "op *" -> infixP pre "*" LeftAs leftChild rightChild
1N/A | c == "(op ##)" -> infixP pre "##" RightAs leftChild rightChild
1N/A-- | c == cappl -> infixP pre "$" LeftAs leftChild rightChild
1N/A | c `elem` [conj, disj, impl] ->
1N/A infixP pre (drop 3 c) RightAs leftChild rightChild
1N/A | c == dummyS -> simpleInfix pre leftChild rightChild
1N/A | c == isaPair -> pair leftChild rightChild
1N/A | c == quantS -> quant leftChild rightChild
1N/A | otherwise -> prefixP pre c leftChild rightChild
1N/A{- Logical connectors: For readability and by habit they are written
1N/A at an infix position.
1N/A If the precedence of one side is weaker (here: higher number) than the
1N/A connector's one it is bracketed. Otherwise not.
1N/AinfixP :: Precedence -> String -> Assoc -> PrecTermTree -> PrecTermTree -> String
1N/AinfixP pAdult stAdult assoc leftChild rightChild
1N/A | (pAdult < prLeftCld) && (pAdult < prRightCld) = both
1N/A | pAdult < prLeftCld =
1N/A LeftAs -> if pAdult == prRightCld then both else left
1N/A | pAdult < prRightCld =
1N/A RightAs -> if pAdult == prLeftCld then both else right
1N/A | (pAdult == prLeftCld) && (pAdult == prRightCld) =
1N/A | pAdult == prLeftCld =
1N/A | pAdult == prRightCld =
1N/A where prLeftCld = pr leftChild
1N/A prRightCld = pr rightChild
1N/A stLeftCld = showPTree leftChild
1N/A stRightCld = showPTree rightChild
1N/A left = lb++ stLeftCld ++rb++sp++ stAdult ++sp++ stRightCld
1N/A both = lb++ stLeftCld ++rb++sp++ stAdult ++sp++lb++ stRightCld ++rb
1N/A right = stLeftCld ++sp++ stAdult ++sp++lb++ stRightCld ++rb
1N/A no = stLeftCld ++sp++ stAdult ++sp++ stRightCld
1N/A{- Application of (HasCASL-)operations with two arguments.
1N/A Both arguments are usually bracketed, except single ones.
1N/AprefixP :: Precedence -> String -> PrecTermTree -> PrecTermTree -> String
1N/AprefixP pAdult stAdult leftChild rightChild
1N/A | (pAdult <= prLeftCld) && (pAdult <= prRightCld) =
1N/A sp++lb++ stLeftCld ++rb++
1N/A sp++lb++ stRightCld ++rb
1N/A | pAdult <= prLeftCld =
1N/A sp++lb++ stLeftCld ++rb++
1N/A | pAdult <= prRightCld =
1N/A sp++lb++ stRightCld ++rb
1N/A | otherwise = stAdult ++
1N/A where prLeftCld = pr leftChild
1N/A prRightCld = pr rightChild
1N/A stLeftCld = showPTree leftChild
1N/A stRightCld = showPTree rightChild
1N/A{- Isabelle application: An operation/a datatype-constructor is applied
1N/A to one argument. The whole expression is always bracketed.
1N/AsimpleInfix :: Precedence -> PrecTermTree -> PrecTermTree -> String
1N/AsimpleInfix pAdult leftChild rightChild
1N/A | (pAdult < prLeftCld) && (pAdult < prRightCld) =
1N/A lbb++ stLeftCld ++rb++
1N/A sp++lb++ stRightCld ++rbb
1N/A | pAdult < prLeftCld =
1N/A lbb++ stLeftCld ++rb++
1N/A sp++ stRightCld ++rb
1N/A | pAdult < prRightCld =
1N/A lb++ stLeftCld ++sp++
1N/A lb++ stRightCld ++rbb
1N/A | otherwise = lb++ stLeftCld ++sp++
1N/A where prLeftCld = pr leftChild
1N/A prRightCld = pr rightChild
1N/A stLeftCld = showPTree leftChild
1N/A stRightCld = showPTree rightChild
1N/A{- Quantification _in_ Formulas
1N/Aquant :: PrecTermTree -> PrecTermTree -> String
1N/Aquant (Node (PrecTerm (Const q _) _) [])
1N/A (Node (PrecTerm (Abs v ty t _) _) []) =
1N/A lb++showQuant (showQuantStr q) v ty t++rb
1N/AlistEnum :: [a] -> [(a,Int)]
1N/AlistEnum l = case l of
1N/A a:as -> (a,length (a:as)):(listEnum as)
1N/Apr :: PrecTermTree -> Precedence
1N/Apr (Node (PrecTerm _ p) _) = p
1N/Apair :: PrecTermTree -> PrecTermTree -> String
1N/Apair leftChild rightChild = lb++showPTree leftChild++", "++
1N/A showPTree rightChild++rb
1N/A-- instances for Classrel and Arities, in alternative to TSig
1N/Ainstance PrettyPrint Classrel where
1N/A showTycon t cl rest = case cl of
1N/A Just x -> (text "axclass") <+> (text $ classId t) <+> text "<" <+>
1N/A (if x == [] then (text "pcpo") else (text $ showSort x)) $$ rest
1N/Ainstance PrettyPrint Arities where
1N/A showInstances t cl rest =
1N/A (vcat $ map (showInstance t) cl) $$ rest
1N/A (text "instance") <+> (text $ show t) <+> text "::" <+> text (showInstArgs $ snd xs)
1N/A <+> text (classId $ fst xs) $$ text "by intro_classes"
1N/A showInstArgs ys = case ys of
1N/A a:as -> "(" ++ (showInstArgsR ys) ++ ") "
1N/A showInstArgsR ys = case ys of
1N/A [a] -> "\"" ++ (showSort $ snd a) ++ "\""
1N/A a:as -> "\"" ++ (showSort $ snd a) ++ "\", " ++ (showInstArgsR as)
1N/Ainstance PrettyPrint Sign where
1N/A printText0 ga sig = printText0 ga
1N/A (baseSig sig) <> colon $++$
1N/A printTypeDecls sig $++$
1N/A printText0 ga (classrel $ tsig sig) $++$
1N/A showDataTypeDefs (dataTypeTab sig) $++$
1N/A showDomainDefs (domainTab sig) $++$
1N/A showsConstTab (constTab sig) $++$
1N/A (if showLemmas sig then showCaseLemmata (dataTypeTab sig) else empty) $++$
1N/A -- this may prints an "o"
1N/A printText0 ga (tsig sig)
1N/A printTypeDecls sig = let as = (arities $ tsig sig) in
1N/A showTycon t arity' rest =
1N/A let arity = if null arity' then
1N/A else length (snd $ head arity') in
1N/A if dtyp sig t then empty else
1N/A (if arity>0 then (text $ lb++concat (map ((" 'a"++).show) [
1..arity])++rb)
1N/A else empty) <+> (text $ show t) $$ rest
1N/A dtyp sig t = elem t $
1N/A concat [map (typeId . fst) x | x <- (domainTab sig) ++ (dataTypeTab sig)]
1N/A vvcat = foldr ($+$) empty
1N/A showConst c t rest = text (show c) <+> text "::" <+>
1N/A text ("\"" ++ showTyp Unquoted 1000 t ++ "\"") $$ rest
1N/A showDataTypeDefs dtDefs = vcat $ map showDataTypeDef dtDefs
1N/A showDataTypeDef [] = empty
1N/A showDataTypeDef (dt:dts) =
1N/A (text "datatype") <+> (showDataType dt)
1N/A <+> (vcat $ map ((text ("\n"++"and") <+>) . showDataType) dts) <> text "\n"
1N/A showDataType (t,op:ops) =
1N/A text (showTyp Quoted 1000 t) <+> text "=" <+> (showOp op)
1N/A <+> (hsep $ map ((text "|" <+>) . showOp) ops)
1N/A showDomainDefs dtDefs = vcat $ map showDomainDef dtDefs
1N/A showDomainDef [] = empty
1N/A showDomainDef (dt:dts) =
1N/A (text "domain") <+> (showDomain dt)
1N/A <+> (vcat $ map ((text ("\n"++"and") <+>) . showDomain) dts) <> text "\n"
1N/A showDomain (t,op:ops) =
1N/A text (showTyp Quoted 1000 t) <+> text "=" <+> (showDOp op)
1N/A <+> (hsep $ map ((text "|" <+>) . showDOp) ops)
1N/A showDOp (opname,args) =
1N/A text opname <+> (hsep $ [text $ sp++lb++opname++"_"++(show n)
1N/A ++"::"++sp++(showOpArg x)++rb | (x,n) <- listEnum args])
1N/A showOp (opname,args) =
1N/A text opname <+> (hsep $ map (text . showOpArg) args)
1N/A showOpArg arg = case arg of
1N/A TFree _ _ -> showTyp Null 1000 arg
1N/A _ -> "\"" ++ showTyp Null 1000 arg ++ "\""
1N/A showCaseLemmata dtDefs = text (concat $ map showCaseLemmata1 dtDefs)
1N/A showCaseLemmata1 dts = concat $ map showCaseLemma dts
1N/A showCaseLemma (_, []) = ""
1N/A showCaseLemma (tyCons, (c:cons)) =
1N/A let cs = "case caseVar of" ++ sp
1N/A sc b = showCons b c ++ (concat $ map ((" | " ++)
1N/A . (showCons b)) cons)
1N/A showCons b (cName, args) =
1N/A let pat = cName ++ (concat $ map ((sp ++) . showArg) args)
1N/A term = showCaseTerm cName args
1N/A if b then pat ++ "Some" ++ sp ++ lb ++ term ++ rb ++ "\n"
1N/A else pat ++ term ++ "\n"
1N/A showCaseTerm name args = if null name then sa
1N/A else [toLower (head name)] ++ sa
1N/A where sa = (concat $ map ((sp ++) . showArg) args)
1N/A showArg (TFree [] _) = "varName"
1N/A showArg (TFree (n:ns) _) = [toLower n] ++ ns
1N/A showArg (TVar ([], _) _) = "varName"
1N/A showArg (TVar ((n:ns), _) _) = [toLower n] ++ ns
1N/A showArg (Type [] _ _) = "varName"
1N/A showArg (Type m@(n:ns) _ s) =
1N/A if m == "typeAppl" || m == "fun" || m == "*" then concat $ map showArg s
1N/A else [toLower n] ++ ns
1N/A showName (TFree v _) = v
1N/A showName (TVar (v, _) _) = v
1N/A showName (Type n _ _) = n
1N/A proof = "apply (case_tac caseVar)\napply (auto)\ndone\n"
1N/A "lemma" ++ sp ++ "case_" ++ showName tyCons ++ "_SomeProm" ++ sp
1N/A ++ "[simp]:\"" ++ sp ++ lb ++ cs ++ clSome ++ rb ++ sp
1N/A ++ "=\n" ++ "Some" ++ sp ++ lb ++ cs ++ cl ++ rb ++ "\"\n"
1N/Aquote_underscores :: String -> String
1N/Aquote_underscores [] = []
1N/Aquote_underscores ('_':'_':rest) = '_':quote_underscores rest
1N/Aquote_underscores ('_':rest) = '\'':'_':quote_underscores rest
1N/Aquote_underscores (c:rest) = c:quote_underscores rest
1N/Ainstance PrintLaTeX Sign where
1N/A printLatex0 = printText0
1N/Abracketize :: Bool -> String -> String
1N/Abracketize b s = if b then lb++s++rb else s