1N/A{- |

1N/AModule : $Header$

1N/ACopyright : (c) University of Cambridge, Cambridge, England

1N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2004

1N/ALicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

1N/A

1N/AMaintainer : hets@tzi.de

1N/AStability : provisional

1N/APortability : portable

1N/A

1N/A Printing functions for Isabelle logic.

1N/A-}

1N/A{-

1N/A todo: brackets in (? x . p x) ==> q

1N/A properly construct docs

1N/A-}

1N/A

1N/Amodule Isabelle.IsaPrint where

1N/A

1N/Aimport Isabelle.IsaSign

1N/Aimport Isabelle.IsaConsts

1N/Aimport Common.Lib.Pretty

1N/Aimport Common.PrettyPrint

1N/Aimport Data.Char

1N/Aimport qualified Common.Lib.Map as Map

1N/A

1N/A------------------- Printing functions -------------------

1N/A

1N/Ainstance PrettyPrint IsaClass where

1N/A printText0 _ (IsaClass c) = parens $ text c

1N/A

1N/Ainstance PrintLaTeX Sentence where

1N/A printLatex0 = printText0

1N/A

1N/Ainstance PrettyPrint Sentence where

1N/A printText0 _ = text . showTerm . senTerm

1N/A

1N/Ainstance PrettyPrint Typ where

1N/A printText0 _ = text . showTyp 1000

1N/A

1N/AshowTyp :: Integer -> Typ -> String

1N/AshowTyp pri (Type str _ [s,t])

1N/A | str == funS =

1N/A bracketize (pri<=10) (showTyp 10 s ++ " => " ++ showTyp 10 t)

1N/A | str == "dFun" =

1N/A bracketize (pri<=10) (showTyp 10 s ++ " -> " ++ showTyp 10 t)

1N/A | str == prodS =

1N/A lb ++ showTyp pri s ++ " * " ++ showTyp pri t ++ rb

1N/A | str == "**" =

1N/A lb ++ showTyp pri s ++ " ** " ++ showTyp pri t ++ rb

1N/AshowTyp _ (Type name _ args) =

1N/A case args of

1N/A [] -> name

1N/A arg:[] -> showTyp 10 arg ++ sp ++ name

1N/A _ -> let (tyVars,types) = foldl split ([],[]) args

1N/A in

1N/A lb ++ concat (map ((sp ++ ) . show) tyVars) ++

1N/A concat (map ((sp ++ ) . show) types) ++ rb ++ name

1N/A where split (tv,ty) t = case t of

1N/A TFree _ _ -> (tv++[t],ty)

1N/A _ -> (tv,ty++[t])

1N/AshowTyp _ (TFree v _) = "\'" ++ v

1N/AshowTyp _ (TVar (v,_) _) = "?\'" ++ v

1N/A

1N/Ainstance PrettyPrint TypeSig where

1N/A printText0 _ tysig =

1N/A if Map.isEmpty (arities tysig) then empty

1N/A else text $ Map.foldWithKey showTycon "" (arities tysig)

1N/A where showTycon t arity' rest =

1N/A let arity = if null arity' then

1N/A error "IsaPrint.printText0 (TypeSig)"

1N/A else length (snd $ head arity') in

1N/A "typedecl "++

1N/A (if arity>0 then lb++concat (map ((" 'a"++).show) [1..arity])++rb

1N/A else "") ++ show t ++"\n"++rest

1N/A

1N/Ainstance PrettyPrint Term where

1N/A printText0 _ = text . showTerm -- outerShowTerm

1N/A -- back to showTerm, because meta !! causes problems with show ?thesis

1N/A

1N/A

1N/A-- NO MORE NEEDED

1N/AstringMap :: (a -> String) -> [a] -> String

1N/AstringMap f ls = concat [" " ++ (f x) | x <- ls]

1N/A

1N/AtypedVars2st :: (a -> String) -> (b -> String) -> [(a,b)] -> String

1N/AtypedVars2st f g ls = concat [" (" ++ (f x) ++ "::" ++ (g y) ++ ")" | (x,y) <- ls]

1N/A

1N/AshowTypedVars :: [(Term,Typ)] -> String

1N/AshowTypedVars ls = typedVars2st showTerm (showTyp 1000) ls

1N/A---

1N/A

1N/A

1N/AshowQuantStr :: String -> String

1N/AshowQuantStr s | s == allS = "!"

1N/A | s == exS = "?"

1N/A | s == ex1S = "?!"

1N/A | otherwise = error "IsaPrint.showQuantStr"

1N/A

1N/AshowTerm :: Term -> String

1N/AshowTerm (Const c _) = c

1N/AshowTerm (Free v _) = v

1N/AshowTerm (Abs v _ t NotCont) = lb++"%"++(showTerm v)++" . "++showTerm t++rb

1N/AshowTerm (Abs v _ t IsCont) = lb++"LAM"++(showTerm v)++" . "++showTerm t++rb

1N/A--showTerm (Abs vs t NotCont) = lb++"%"++(showTypedVars vs)++" . "++showTerm t++rb

1N/A--showTerm (Abs vs t IsCont) = lb++"LAM"++(showTypedVars vs)++" . "++showTerm t++rb

1N/A-- showTerm (Abs vs t NotCont) = lb++"% "++(stringMap (show . fst) vs)++" . "++showTerm t++rb

1N/A-- showTeshowTerm (Abs vs t IsCont) = lb++"LAM "++(stringMap (show . fst) vs)++" . "++showTerm t++rb

1N/AshowTerm (App (Const q _) (Abs v ty t _) _) | q `elem` [allS, exS, ex1S] =

1N/A showQuant (showQuantStr q) v ty t

1N/AshowTerm (Case term alts) =

1N/A let sAlts = map showCaseAlt alts

1N/A in

1N/A lb ++ "case" ++ sp ++ showTerm term ++ sp ++ "of"

1N/A ++ sp ++ head sAlts

1N/A ++ concat (map ((++) ("\n" ++ sp ++ sp ++ sp ++ "|" ++ sp))

1N/A (tail sAlts)) ++ rb

1N/A-- Just t1 `App` t2 left

1N/AshowTerm (If t1 t2 t3) =

1N/A lb ++ "if" ++ sp ++ showTerm t1 ++ sp ++ "then" ++ sp

1N/A ++ showTerm t2 ++ sp ++ "else" ++ sp ++ showTerm t3 ++ 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/A-- showTerm t = showPTree (toPrecTree t) NO GOOD - it loops

1N/AshowTerm t = "(IsaPrint.showTerm, error: unsupported term)"

1N/A-- showTerm t = "(IsaPrint.showTerm, error: "++(show t)++" unsupported term)"

1N/A

1N/A

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

1N/A if b then ";" ++ s

1N/A else s

1N/A

1N/A

1N/AshowCaseAlt :: (Term, Term) -> String

1N/AshowCaseAlt (pat, term) =

1N/A showPattern pat ++ sp ++ "=>" ++ sp ++ showTerm term

1N/A

1N/AshowPattern :: Term -> String

1N/AshowPattern (App t t' _) = showPattern t ++ sp ++ showPattern t'

1N/AshowPattern t = showTerm t

1N/A

1N/AshowQuant :: String -> Term -> Typ -> Term -> String

1N/AshowQuant s var typ term =

1N/A (s++sp++(showTerm var)++" :: "++showTyp 1000 typ++" . "++showTerm term)

1N/A-- showQuant :: String -> [String] -> Term -> String

1N/A-- showQuant s vs term =

1N/A-- (s++sp++(stringMap showTerm vs)++" . "++showTerm term)

1N/A

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/A

1N/AouterShowTerm1 :: Term -> String

1N/AouterShowTerm1 t@(App (App (Const o _) _ _) _ _) | o == impl =

1N/A outerShowTerm t

1N/AouterShowTerm1 t = showTerm t

1N/A

1N/AouterShowQuant :: String -> Term -> Typ -> Term -> String

1N/AouterShowQuant s var typ term =

1N/A (s++sp++(showTerm var)++" :: "++showTyp 1000 typ++" . "++outerShowTerm term)

1N/A

1N/A

1N/A{-

1N/A For nearly perfect parenthesis - they only appear when needed -

1N/A a formula/term is broken open in following pieces:

1N/A (logical) connector

1N/A / \

1N/A / \

1N/A formula's lhs formula's rhs

1N/A

1N/A Every connector is annotated with its precedence, every 'unbreakable'

1N/A formula gets the lowest precedence.

1N/A-}

1N/A

1N/A-- term annotated with precedence

1N/Adata PrecTerm = PrecTerm Term Precedence deriving (Show)

1N/Atype Precedence = Int

1N/A

1N/A{- Precedences (descending): __ __ (Isabelle's term application),

1N/A application of HasCASL ops, <=>, =, /\, \/, =>

1N/A Associativity: = -- left

1N/A => -- right

1N/A /\ -- right

1N/A \/ -- right

1N/A-}

1N/A

1N/Adata PrecTermTree = Node PrecTerm [PrecTermTree]

1N/A

1N/AisaAppPrec :: Term -> PrecTerm

1N/AisaAppPrec t = PrecTerm t 0

1N/A

1N/AappPrec :: Term -> PrecTerm

1N/AappPrec t = PrecTerm t 5

1N/A

1N/AeqvPrec :: Term -> PrecTerm

1N/AeqvPrec t = PrecTerm t 7

1N/A

1N/AeqPrec :: Term -> PrecTerm

1N/AeqPrec t = PrecTerm t 10

1N/A

1N/AandPrec :: Term -> PrecTerm

1N/AandPrec t = PrecTerm t 20

1N/A

1N/AorPrec :: Term -> PrecTerm

1N/AorPrec t = PrecTerm t 30

1N/A

1N/AimplPrec :: Term -> PrecTerm

1N/AimplPrec t = PrecTerm t 40

1N/A

1N/AnoPrec :: Term -> PrecTerm

1N/AnoPrec t = PrecTerm t (-10)

1N/A

1N/AquantS :: String

1N/AquantS = "QUANT"

1N/A

1N/AdummyS :: String

1N/AdummyS = "Dummy"

1N/A

1N/AbinFunct :: String -> Term -> PrecTerm

1N/AbinFunct s | s == eqv = eqvPrec

1N/A | s == eq = eqPrec

1N/A | s == conj = andPrec

1N/A | s == disj = orPrec

1N/A | s == impl = implPrec

1N/A | otherwise = appPrec

1N/A

1N/AtoPrecTree :: Term -> PrecTermTree

1N/AtoPrecTree trm =

1N/A case trm of

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 (App t@(Const o _) t3 _) t2 _ ->

1N/A Node (binFunct o t) [toPrecTree t3, toPrecTree t2]

1N/A App t1 t2 _ -> Node (isaAppPrec $ con dummyS)

1N/A [toPrecTree t1, toPrecTree t2]

1N/A _ -> Node (noPrec trm) []

1N/A

1N/Adata Assoc = LeftAs | NoAs | RightAs

1N/A

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 in

1N/A case term of

1N/A Const c _ | c == eq -> 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 _ -> showTerm term

1N/A

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/A-}

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 case assoc of

1N/A LeftAs -> if pAdult == prRightCld then both else left

1N/A RightAs -> left

1N/A NoAs -> left

1N/A | pAdult < prRightCld =

1N/A case assoc of

1N/A LeftAs -> right

1N/A RightAs -> if pAdult == prLeftCld then both else right

1N/A NoAs -> right

1N/A | (pAdult == prLeftCld) && (pAdult == prRightCld) =

1N/A case assoc of

1N/A LeftAs -> right

1N/A RightAs -> left

1N/A NoAs -> no

1N/A | pAdult == prLeftCld =

1N/A case assoc of

1N/A LeftAs -> no

1N/A RightAs -> left

1N/A NoAs -> no

1N/A | pAdult == prRightCld =

1N/A case assoc of

1N/A LeftAs -> right

1N/A RightAs -> no

1N/A NoAs -> no

1N/A | otherwise = no

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

1N/A

1N/A{- Application of (HasCASL-)operations with two arguments.

1N/A Both arguments are usually bracketed, except single ones.

1N/A-}

1N/AprefixP :: Precedence -> String -> PrecTermTree -> PrecTermTree -> String

1N/AprefixP pAdult stAdult leftChild rightChild

1N/A | (pAdult <= prLeftCld) && (pAdult <= prRightCld) =

1N/A stAdult ++

1N/A sp++lb++ stLeftCld ++rb++

1N/A sp++lb++ stRightCld ++rb

1N/A | pAdult <= prLeftCld =

1N/A stAdult ++

1N/A sp++lb++ stLeftCld ++rb++

1N/A sp++ stRightCld

1N/A | pAdult <= prRightCld =

1N/A stAdult ++

1N/A sp++ stLeftCld ++

1N/A sp++lb++ stRightCld ++rb

1N/A | otherwise = stAdult ++

1N/A sp++ stLeftCld ++

1N/A sp++ stRightCld

1N/A where prLeftCld = pr leftChild

1N/A prRightCld = pr rightChild

1N/A stLeftCld = showPTree leftChild

1N/A stRightCld = showPTree rightChild

1N/A

1N/A{- Isabelle application: An operation/a datatype-constructor is applied

1N/A to one argument. The whole expression is always bracketed.

1N/A-}

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 stRightCld ++rb

1N/A where prLeftCld = pr leftChild

1N/A prRightCld = pr rightChild

1N/A stLeftCld = showPTree leftChild

1N/A stRightCld = showPTree rightChild

1N/A

1N/A

1N/A{- Quantification _in_ Formulas

1N/A-}

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/Aquant _ _ = error "[Isabelle.IsaPrint] Wrong quantification!?"

1N/A

1N/A

1N/Apr :: PrecTermTree -> Precedence

1N/Apr (Node (PrecTerm _ p) _) = p

1N/A

1N/A-- Prints: (p1, p2)

1N/Apair :: PrecTermTree -> PrecTermTree -> String

1N/Apair leftChild rightChild = lb++showPTree leftChild++", "++

1N/A showPTree rightChild++rb

1N/A

1N/Ainstance PrettyPrint Sign where

1N/A printText0 ga sig = text

1N/A (baseSig sig) <> colon $$

1N/A printText0 ga (tsig sig) $$

1N/A showDataTypeDefs (dataTypeTab sig) $$

1N/A showDomainDefs (domainTab sig) $$ --

1N/A showsConstTab (constTab sig) $$

1N/A-- showCaseLemmata (dataTypeTab sig)

1N/A showCaseLemmata (domainTab sig) --

1N/A where

1N/A showsConstTab tab =

1N/A if Map.isEmpty tab then empty

1N/A else text("consts") $$ Map.foldWithKey showConst empty tab

1N/A showConst c t rest = text (show c ++ " :: " ++ "\"" ++ showTyp 1000 t

1N/A ++ "\"" ++ showDecl c) $$ rest

1N/A showDecl c = sp ++ sp ++ sp ++ "( \"" ++ quote_underscores c ++ "\" )"

1N/A showDataTypeDefs dtDefs = vcat $ map (text . showDataTypeDef) dtDefs

1N/A showDataTypeDef [] = ""

1N/A showDataTypeDef (dt:dts) =

1N/A "datatype " ++ showDataType dt

1N/A ++ (concat $ map (("and "++) . showDataType) dts) ++ "\n"

1N/A showDataType (_,[]) = error "IsaPrint.showDataType"

1N/A showDataType (t,op:ops) =

1N/A showTyp 1000 t ++ " = " ++ showOp op

1N/A ++ (concat $ map ((" | "++) . showOp) ops)

1N/A showDomainDefs dtDefs = vcat $ map (text . showDomainDef) dtDefs --

1N/A showDomainDef [] = "" --

1N/A showDomainDef (dt:dts) = --

1N/A "domain " ++ showDomain dt --

1N/A ++ (concat $ map (("and "++) . showDomain) dts) ++ "\n" --

1N/A showDomain (_,[]) = error "IsaPrint.showDomain" --

1N/A showDomain (t,op:ops) = --

1N/A showTyp 1000 t ++ " = " ++ showOp op --

1N/A ++ (concat $ map ((" | "++) . showOp) ops) --

1N/A showOp (opname,args) =

1N/A opname ++ (concat $ map ((sp ++) . showArg) args)

1N/A showArg arg = case arg of

1N/A TFree _ _ -> showTyp 1000 arg

1N/A _ -> "\"" ++ showTyp 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 ((" | " ++) . (showCons b)) cons)

1N/A clSome = sc True

1N/A cl = sc False

1N/A showCons b (cName, args) =

1N/A let pat = cName ++ (concat $ map ((sp ++) . showArg) args)

1N/A ++ sp ++ "=>" ++ sp

1N/A term = showCaseTerm cName args

1N/A in

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 in

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/A ++ proof

1N/A

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/A

1N/A-- instance PrettyPrint Sign where

1N/A-- printText0 _ = ptext . show

1N/A

1N/Ainstance PrintLaTeX Sign where

1N/A printLatex0 = printText0

1N/A

1N/Asp :: String

1N/Asp = " "

1N/A

1N/Arb :: String

1N/Arb = ")"

1N/A

1N/Arbb :: String

1N/Arbb = rb++rb

1N/A

1N/Alb :: String

1N/Alb = "("

1N/A

1N/Albb :: String

1N/Albb = lb++lb

1N/A

1N/A

1N/Abracketize :: Bool -> String -> String

1N/Abracketize b s = if b then lb++s++rb else s

1N/A