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.PrettyPrint

1N/Aimport Common.Lib.Pretty

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 == prodS =

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 100 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/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 _) = lb++"% "++showTerm v++" . "++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/AshowTerm t = showPTree (toPrecTree t)

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

showPattern (App t t' _) = showPattern t ++ sp ++ showPattern t'

showPattern t = showTerm t

showQuant :: String -> Term -> Typ -> Term -> String

showQuant s var typ term =

(s++sp++showTerm var++" :: "++showTyp 1000 typ++" . "++showTerm term)

outerShowTerm :: Term -> String

outerShowTerm (App (Const q _ _) (Abs v ty t _) _) | q == allS =

outerShowQuant "!!" v ty t

outerShowTerm (App (App (Const o _ _) t1 _) t2 _) | o == impl =

showTerm t1 ++ " ==> " ++ outerShowTerm1 t2

outerShowTerm t = showTerm t

outerShowTerm1 :: Term -> String

outerShowTerm1 t@(App (App (Const o _ _) _ _) _ _) | o == impl =

outerShowTerm t

outerShowTerm1 t = showTerm t

outerShowQuant :: String -> Term -> Typ -> Term -> String

outerShowQuant s var typ term =

(s++sp++showTerm var++" :: "++showTyp 1000 typ++" . "++outerShowTerm term)

{-

For nearly perfect parenthesis - they only appear when needed -

a formula/term is broken open in following pieces:

(logical) connector

/ \

/ \

formula's lhs formula's rhs

Every connector is annotated with its precedence, every 'unbreakable'

formula gets the lowest precedence.

-}

-- term annotated with precedence

data PrecTerm = PrecTerm Term Precedence deriving (Show)

type Precedence = Int

{- Precedences (descending): __ __ (Isabelle's term application),

application of HasCASL ops, <=>, =, /\, \/, =>

Associativity: = -- left

=> -- right

/\ -- right

\/ -- right

-}

data PrecTermTree = Node PrecTerm [PrecTermTree]

isaAppPrec :: Term -> PrecTerm

isaAppPrec t = PrecTerm t 0

appPrec :: Term -> PrecTerm

appPrec t = PrecTerm t 5

eqvPrec :: Term -> PrecTerm

eqvPrec t = PrecTerm t 7

eqPrec :: Term -> PrecTerm

eqPrec t = PrecTerm t 10

andPrec :: Term -> PrecTerm

andPrec t = PrecTerm t 20

orPrec :: Term -> PrecTerm

orPrec t = PrecTerm t 30

implPrec :: Term -> PrecTerm

implPrec t = PrecTerm t 40

noPrec :: Term -> PrecTerm

noPrec t = PrecTerm t (-10)

quantS :: String

quantS = "QUANT"

dummyS :: String

dummyS = "Dummy"

binFunct :: String -> Term -> PrecTerm

binFunct s | s == eqv = eqvPrec

| s == eq = eqPrec

| s == conj = andPrec

| s == disj = orPrec

| s == impl = implPrec

| otherwise = appPrec

toPrecTree :: Term -> PrecTermTree

toPrecTree trm =

case trm of

App c1@(Const q _ _) a2@(Abs _ _ _ _) _ | q `elem` [allS, exS, ex1S] ->

Node (isaAppPrec $ con quantS) [toPrecTree c1, toPrecTree a2]

App (App t@(Const o _ _) t3 _) t2 _ ->

Node (binFunct o t) [toPrecTree t3, toPrecTree t2]

App t1 t2 _ -> Node (isaAppPrec $ con dummyS)

[toPrecTree t1, toPrecTree t2]

_ -> Node (noPrec trm) []

data Assoc = LeftAs | NoAs | RightAs

showPTree :: PrecTermTree -> String

showPTree (Node (PrecTerm term _) []) = showTerm term

showPTree (Node (PrecTerm term pre) annos) =

let leftChild = head annos

rightChild = last annos

in

case term of

Const c _ _ | c == eq -> infixP pre "=" LeftAs leftChild rightChild

| c `elem` [conj, disj, impl] ->

infixP pre (drop 3 c) RightAs leftChild rightChild

| c == dummyS -> simpleInfix pre leftChild rightChild

| c == isaPair -> pair leftChild rightChild

| c == quantS -> quant leftChild rightChild

| otherwise -> prefixP pre c leftChild rightChild

_ -> showTerm term

{- Logical connectors: For readability and by habit they are written

at an infix position.

If the precedence of one side is weaker (here: higher number) than the

connector's one it is bracketed. Otherwise not.

-}

infixP :: Precedence -> String -> Assoc -> PrecTermTree -> PrecTermTree -> String

infixP pAdult stAdult assoc leftChild rightChild

| (pAdult < prLeftCld) && (pAdult < prRightCld) = both

| pAdult < prLeftCld =

case assoc of

LeftAs -> if pAdult == prRightCld then both else left

RightAs -> left

NoAs -> left

| pAdult < prRightCld =

case assoc of

LeftAs -> right

RightAs -> if pAdult == prLeftCld then both else right

NoAs -> right

| (pAdult == prLeftCld) && (pAdult == prRightCld) =

case assoc of

LeftAs -> right

RightAs -> left

NoAs -> no

| pAdult == prLeftCld =

case assoc of

LeftAs -> no

RightAs -> left

NoAs -> no

| pAdult == prRightCld =

case assoc of

LeftAs -> right

RightAs -> no

NoAs -> no

| otherwise = no

where prLeftCld = pr leftChild

prRightCld = pr rightChild

stLeftCld = showPTree leftChild

stRightCld = showPTree rightChild

left = lb++ stLeftCld ++rb++sp++ stAdult ++sp++ stRightCld

both = lb++ stLeftCld ++rb++sp++ stAdult ++sp++lb++ stRightCld ++rb

right = stLeftCld ++sp++ stAdult ++sp++lb++ stRightCld ++rb

no = stLeftCld ++sp++ stAdult ++sp++ stRightCld

{- Application of (HasCASL-)operations with two arguments.

Both arguments are usually bracketed, except single ones.

-}

prefixP :: Precedence -> String -> PrecTermTree -> PrecTermTree -> String

prefixP pAdult stAdult leftChild rightChild

| (pAdult <= prLeftCld) && (pAdult <= prRightCld) =

stAdult ++

sp++lb++ stLeftCld ++rb++

sp++lb++ stRightCld ++rb

| pAdult <= prLeftCld =

stAdult ++

sp++lb++ stLeftCld ++rb++

sp++ stRightCld

| pAdult <= prRightCld =

stAdult ++

sp++ stLeftCld ++

sp++lb++ stRightCld ++rb

| otherwise = stAdult ++

sp++ stLeftCld ++

sp++ stRightCld

where prLeftCld = pr leftChild

prRightCld = pr rightChild

stLeftCld = showPTree leftChild

stRightCld = showPTree rightChild

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

to one argument. The whole expression is always bracketed.

-}

simpleInfix :: Precedence -> PrecTermTree -> PrecTermTree -> String

simpleInfix pAdult leftChild rightChild

| (pAdult < prLeftCld) && (pAdult < prRightCld) =

lbb++ stLeftCld ++rb++

sp++lb++ stRightCld ++rbb

| pAdult < prLeftCld =

lbb++ stLeftCld ++rb++

sp++ stRightCld ++rb

| pAdult < prRightCld =

lb++ stLeftCld ++sp++

lb++ stRightCld ++rbb

| otherwise = lb++ stLeftCld ++sp++

stRightCld ++rb

where prLeftCld = pr leftChild

prRightCld = pr rightChild

stLeftCld = showPTree leftChild

stRightCld = showPTree rightChild

{- Quantification _in_ Formulas

-}

quant :: PrecTermTree -> PrecTermTree -> String

quant (Node (PrecTerm (Const q _ _) _) [])

(Node (PrecTerm (Abs v ty t _) _) []) =

lb++showQuant (showQuantStr q) v ty t++rb

quant _ _ = error "[Isabelle.IsaPrint] Wrong quantification!?"

pr :: PrecTermTree -> Precedence

pr (Node (PrecTerm _ p) _) = p

-- Prints: (p1, p2)

pair :: PrecTermTree -> PrecTermTree -> String

pair leftChild rightChild = lb++showPTree leftChild++", "++

showPTree rightChild++rb

instance PrettyPrint Sign where

printText0 ga sig = text

(baseSig sig) <> colon $$

printText0 ga (tsig sig) $$

showDataTypeDefs (dataTypeTab sig) $$

showsConstTab (constTab sig) $$

showCaseLemmata (dataTypeTab sig)

where

showsConstTab tab =

if Map.isEmpty tab then empty

else text("consts") $$ Map.foldWithKey showConst empty tab

showConst c t rest = text (show c ++ " :: " ++ "\"" ++ showTyp 1000 t

++ "\"" ++ showDecl c) $$ rest

showDecl c = sp ++ sp ++ sp ++ "( \"" ++ quote_underscores c ++ "\" )"

showDataTypeDefs dtDefs = vcat $ map (text . showDataTypeDef) dtDefs

showDataTypeDef [] = ""

showDataTypeDef (dt:dts) =

"datatype " ++ showDataType dt

++ (concat $ map (("and "++) . showDataType) dts) ++ "\n"

showDataType (_,[]) = error "IsaPrint.showDataType"

showDataType (t,op:ops) =

showTyp 1000 t ++ " = " ++ showOp op

++ (concat $ map ((" | "++) . showOp) ops)

showOp (opname,args) =

opname ++ (concat $ map ((sp ++) . showArg) args)

showArg arg = case arg of

TFree _ _ -> showTyp 1000 arg

_ -> "\"" ++ showTyp 1000 arg ++ "\""

showCaseLemmata dtDefs = text (concat $ map showCaseLemmata1 dtDefs)

showCaseLemmata1 dts = concat $ map showCaseLemma dts

showCaseLemma (_, []) = ""

showCaseLemma (tyCons, (c:cons)) =

let cs = "case caseVar of" ++ sp

sc b = showCons b c ++ (concat $ map ((" | " ++) . (showCons b)) cons)

clSome = sc True

cl = sc False

showCons b (cName, args) =

let pat = cName ++ (concat $ map ((sp ++) . showArg) args)

++ sp ++ "=>" ++ sp

term = showCaseTerm cName args

in

if b then pat ++ "Some" ++ sp ++ lb ++ term ++ rb ++ "\n"

else pat ++ term ++ "\n"

showCaseTerm name args = if null name then sa

else [toLower (head name)] ++ sa

where sa = (concat $ map ((sp ++) . showArg) args)

showArg (TFree [] _) = "varName"

showArg (TFree (n:ns) _) = [toLower n] ++ ns

showArg (TVar ([], _) _) = "varName"

showArg (TVar ((n:ns), _) _) = [toLower n] ++ ns

showArg (Type [] _ _ _) = "varName"

showArg (Type m@(n:ns) _ _ s) =

if m == "typeAppl" || m == "fun" || m == "*" then concat $ map showArg s

else [toLower n] ++ ns

showName (TFree v _) = v

showName (TVar (v, _) _) = v

showName (Type n _ _ _) = n

proof = "apply (case_tac a)\napply (auto)\ndone\n"

in

"lemma" ++ sp ++ "case_" ++ showName tyCons ++ "_SomeProm" ++ sp

++ "[simp]:\"" ++ sp ++ lb ++ cs ++ clSome ++ rb ++ sp

++ "=\n" ++ "Some" ++ sp ++ lb ++ cs ++ cl ++ rb ++ "\"\n"

++ proof

quote_underscores :: String -> String

quote_underscores [] = []

quote_underscores ('_':'_':rest) = '_':quote_underscores rest

quote_underscores ('_':rest) = '\'':'_':quote_underscores rest

quote_underscores (c:rest) = c:quote_underscores rest

-- datatype Bool = True | False

-- lemma case_Type {typeId = "Bool", typeArgKind = [], typeResultKind = [], typeArgs = []}_SomeProm [simp]:"(case a ofTrue => Some( true

-- ) |False => Some( false

-- )) =

-- Some (case a ofTrue => true

-- |False => false

-- )"

-- type DataTypeTab = [DataTypeTabEntry]

-- type DataTypeTabEntry = [(Typ,[DataTypeAlt])] -- (type,[constructors])

-- type DataTypeAlt = (String,[Typ])

-- instance PrettyPrint Sign where

-- printText0 _ = ptext . show

instance PrintLaTeX Sign where

printLatex0 = printText0

sp :: String

sp = " "

rb :: String

rb = ")"

rbb :: String

rbb = rb++rb

lb :: String

lb = "("

lbb :: String

lbb = lb++lb

bracketize :: Bool -> String -> String

bracketize b s = if b then lb++s++rb else s