{- |
Module      :  ./Isabelle/IsaConsts.hs
Description :  constants for Isabelle terms
Copyright   :  (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

constants for Isabelle
-}

-- possibly differentiate between HOL and HOLCF

module Isabelle.IsaConsts where

import Isabelle.IsaSign
import qualified Data.Set as Set
import Data.List
import Data.Maybe
import qualified Data.Map as Map

-- | a topological sort with a @uses@ predicate
topSort :: (a -> a -> Bool) -> [a] -> [a]
topSort :: (a -> a -> Bool) -> [a] -> [a]
topSort f :: a -> a -> Bool
f ls :: [a]
ls = case [a]
ls of
  [] -> []
  a :: a
a : as :: [a]
as -> let
    (directPreds :: [a]
directPreds, rest :: [a]
rest) = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a -> a -> Bool
f a
a) [a]
as
    in if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
directPreds then a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
topSort a -> a -> Bool
f [a]
as else
           (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
topSort a -> a -> Bool
f ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Bool
f a
a) [a]
directPreds [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rest

-- | extends a dependency relation to lists using any
liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
liftDep f :: a -> a -> Bool
f as :: [a]
as bs :: [a]
bs = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a :: a
a -> (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a -> a -> Bool
f a
a) [a]
bs) [a]
as

getTypeIds :: Typ -> Set.Set TName
getTypeIds :: Typ -> Set TName
getTypeIds ty :: Typ
ty = case Typ
ty of
  Type { typeId :: Typ -> TName
typeId = TName
n, typeArgs :: Typ -> [Typ]
typeArgs = [Typ]
args }
    -> TName -> Set TName -> Set TName
forall a. Ord a => a -> Set a -> Set a
Set.insert TName
n (Set TName -> Set TName) -> Set TName -> Set TName
forall a b. (a -> b) -> a -> b
$ [Set TName] -> Set TName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TName] -> Set TName) -> [Set TName] -> Set TName
forall a b. (a -> b) -> a -> b
$ (Typ -> Set TName) -> [Typ] -> [Set TName]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Set TName
getTypeIds [Typ]
args
  TVar _ _ -> Set TName
forall a. Set a
Set.empty
  TFree {} -> Set TName
forall a. Set a
Set.empty

deDepOn :: DomainEntry -> DomainEntry -> Bool
deDepOn :: DomainEntry -> DomainEntry -> Bool
deDepOn (_, l :: [(VName, [Typ])]
l) (t :: Typ
t, _) =
  TName -> Set TName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Typ -> TName
typeId Typ
t) (Set TName -> Bool) -> Set TName -> Bool
forall a b. (a -> b) -> a -> b
$ [Set TName] -> Set TName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TName] -> Set TName) -> [Set TName] -> Set TName
forall a b. (a -> b) -> a -> b
$ ((VName, [Typ]) -> [Set TName]) -> [(VName, [Typ])] -> [Set TName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Typ -> Set TName) -> [Typ] -> [Set TName]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Set TName
getTypeIds ([Typ] -> [Set TName])
-> ((VName, [Typ]) -> [Typ]) -> (VName, [Typ]) -> [Set TName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, [Typ]) -> [Typ]
forall a b. (a, b) -> b
snd) [(VName, [Typ])]
l

ordDoms :: DomainTab -> DomainTab
ordDoms :: DomainTab -> DomainTab
ordDoms = ([DomainEntry] -> [DomainEntry] -> Bool) -> DomainTab -> DomainTab
forall a. (a -> a -> Bool) -> [a] -> [a]
topSort ((DomainEntry -> DomainEntry -> Bool)
-> [DomainEntry] -> [DomainEntry] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
liftDep DomainEntry -> DomainEntry -> Bool
deDepOn)

-- * boolean constants strings

cTrue :: String
cTrue :: TName
cTrue = "True"

cFalse :: String
cFalse :: TName
cFalse = "False"

-- | Not string
cNot :: String
cNot :: TName
cNot = "Not"

-- * quantor strings

allS, exS, ex1S :: String
allS :: TName
allS = "ALL"
exS :: TName
exS = "EX"
ex1S :: TName
ex1S = "EX!"

-- * Strings of binary ops

conj :: String
conj :: TName
conj = "op &"

disj :: String
disj :: TName
disj = "op |"

impl :: String
impl :: TName
impl = "op -->"

eq :: String
eq :: TName
eq = "op ="

neq :: String
neq :: TName
neq = "op ~="

plusS :: String
plusS :: TName
plusS = "op +"

minusS :: String
minusS :: TName
minusS = "op -"

timesS :: String
timesS :: TName
timesS = "op *"

divS :: String
divS :: TName
divS = "op div"

modS :: String
modS :: TName
modS = "op mod"

consS :: String
consS :: TName
consS = "op #"

lconsS :: String
lconsS :: TName
lconsS = "op ###"

appendS :: String
appendS :: TName
appendS = "op @"

compS :: String
compS :: TName
compS = "comp"

-- | lower case pair
pairC :: String
pairC :: TName
pairC = "pair"

eqvSimS :: String
eqvSimS :: TName
eqvSimS = "eqvS"

unionS :: String
unionS :: TName
unionS = "op Un"

-- Set membership
membershipS :: String
membershipS :: TName
membershipS = "op :"

-- | Imange of functions
imageS :: String
imageS :: TName
imageS = "image"

rangeS :: String
rangeS :: TName
rangeS = "range"

-- * some stuff for Isabelle

pcpoS :: String
pcpoS :: TName
pcpoS = "pcpo"

prodS, sProdS, funS, cFunS, lFunS, sSumS, lProdS, lSumS :: TName
prodS :: TName
prodS = "*"    -- this is printed as it is!
lProdS :: TName
lProdS = "lprod" -- "***"
sProdS :: TName
sProdS = "**"
funS :: TName
funS = "=>"
cFunS :: TName
cFunS = "->"
lFunS :: TName
lFunS = "-->"
sSumS :: TName
sSumS = "++"
lSumS :: TName
lSumS = "either"

-- * some stuff for HasCASL

aptS :: String
aptS :: TName
aptS = "apt"

appS :: String
appS :: TName
appS = "app"

pAppS :: String
pAppS :: TName
pAppS = "pApp"

defOpS :: String
defOpS :: TName
defOpS = "defOp"

-- | Some string
someS :: String
someS :: TName
someS = "Some"

-- * strings for HOLCF lifting functions

lliftbinS :: String
lliftbinS :: TName
lliftbinS = "lliftbin"

fliftbinS :: String
fliftbinS :: TName
fliftbinS = "fliftbin"

flift2S :: String
flift2S :: TName
flift2S = "flift2"

-- * Predefined CLASSES

pcpo :: IsaClass
pcpo :: IsaClass
pcpo = TName -> IsaClass
IsaClass TName
pcpoS

isaTerm :: IsaClass
isaTerm :: IsaClass
isaTerm = TName -> IsaClass
IsaClass "type"

-- * predefined SORTS

holType :: Sort
holType :: Sort
holType = [IsaClass
isaTerm]

dom :: Sort
dom :: Sort
dom = [IsaClass
pcpo]

sortT :: Continuity -> Sort
sortT :: Continuity -> Sort
sortT a :: Continuity
a = case Continuity
a of
  NotCont -> Sort
holType
  IsCont _ -> Sort
dom

mkSTypeT :: Continuity -> String -> Typ
mkSTypeT :: Continuity -> TName -> Typ
mkSTypeT a :: Continuity
a s :: TName
s = TName -> Sort -> [Typ] -> Typ
Type TName
s (Continuity -> Sort
sortT Continuity
a) []

-- ------------------- POLY TYPES --------------------------------------

listT :: Continuity -> Typ -> Typ
listT :: Continuity -> Typ -> Typ
listT a :: Continuity
a t :: Typ
t = TName -> Sort -> [Typ] -> Typ
Type (case Continuity
a of
   IsCont _ -> "llist"
   NotCont -> "list") (Continuity -> Sort
sortT Continuity
a) [Typ
t]

charT :: Continuity -> Typ
charT :: Continuity -> Typ
charT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
  IsCont _ -> "charT"
  NotCont -> "char"

ratT :: Continuity -> Typ
ratT :: Continuity -> Typ
ratT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
  IsCont _ -> "ratT"
  NotCont -> "rat"

fracT :: Continuity -> Typ
fracT :: Continuity -> Typ
fracT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a "fracT"

integerT :: Continuity -> Typ
integerT :: Continuity -> Typ
integerT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   IsCont _ -> "integerT"
   NotCont -> "int"

boolT :: Continuity -> Typ
boolT :: Continuity -> Typ
boolT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   IsCont _ -> "lBool"
   NotCont -> "bool"

orderingT :: Continuity -> Typ
orderingT :: Continuity -> Typ
orderingT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   IsCont _ -> "lOrdering"
   NotCont -> "sOrdering"

intT :: Continuity -> Typ
intT :: Continuity -> Typ
intT a :: Continuity
a = Continuity -> TName -> Typ
mkSTypeT Continuity
a (TName -> Typ) -> TName -> Typ
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   IsCont _ -> "intT"
   NotCont -> "int"

prodT :: Continuity -> Typ -> Typ -> Typ
prodT :: Continuity -> Typ -> Typ -> Typ
prodT a :: Continuity
a t1 :: Typ
t1 t2 :: Typ
t2 = case Continuity
a of
   IsCont _ -> Typ -> Typ -> Typ
mkContProduct Typ
t1 Typ
t2
   NotCont -> Typ -> Typ -> Typ
prodType Typ
t1 Typ
t2

funT :: Continuity -> Typ -> Typ -> Typ
funT :: Continuity -> Typ -> Typ -> Typ
funT c :: Continuity
c a :: Typ
a b :: Typ
b = case Continuity
c of
   IsCont _ -> Typ -> Typ -> Typ
mkContFun Typ
a Typ
b
   NotCont -> Typ -> Typ -> Typ
mkFunType Typ
a Typ
b

curryFunT :: Continuity -> [Typ] -> Typ -> Typ
curryFunT :: Continuity -> [Typ] -> Typ -> Typ
curryFunT c :: Continuity
c ls :: [Typ]
ls x :: Typ
x = case Continuity
c of
   IsCont _ -> [Typ] -> Typ -> Typ
mkCurryContFun [Typ]
ls Typ
x
   NotCont -> [Typ] -> Typ -> Typ
mkCurryFunType [Typ]
ls Typ
x

-- * predefined types

mkSType :: String -> Typ
mkSType :: TName -> Typ
mkSType = Continuity -> TName -> Typ
mkSTypeT Continuity
NotCont

noTypeT :: Typ
noTypeT :: Typ
noTypeT = TName -> Typ
mkSType "dummy"

noType :: DTyp
noType :: DTyp
noType = Typ -> TAttr -> Maybe Int -> DTyp
Hide Typ
noTypeT TAttr
NA Maybe Int
forall a. Maybe a
Nothing

noTypeC :: DTyp
noTypeC :: DTyp
noTypeC = Typ -> TAttr -> Maybe Int -> DTyp
Hide Typ
noTypeT TAttr
TCon Maybe Int
forall a. Maybe a
Nothing

hideNN :: Typ -> DTyp
hideNN :: Typ -> DTyp
hideNN t :: Typ
t = Typ -> TAttr -> Maybe Int -> DTyp
Hide Typ
t TAttr
NA Maybe Int
forall a. Maybe a
Nothing

hideCN :: Typ -> DTyp
hideCN :: Typ -> DTyp
hideCN t :: Typ
t = Typ -> TAttr -> Maybe Int -> DTyp
Hide Typ
t TAttr
TCon Maybe Int
forall a. Maybe a
Nothing

dispNN :: Typ -> DTyp
dispNN :: Typ -> DTyp
dispNN t :: Typ
t = Typ -> TAttr -> Maybe Int -> DTyp
Disp Typ
t TAttr
NA Maybe Int
forall a. Maybe a
Nothing

dispMN :: Typ -> DTyp
dispMN :: Typ -> DTyp
dispMN t :: Typ
t = Typ -> TAttr -> Maybe Int -> DTyp
Disp Typ
t TAttr
TMet Maybe Int
forall a. Maybe a
Nothing

boolType :: Typ
boolType :: Typ
boolType = Continuity -> Typ
boolT Continuity
NotCont

mkListType :: Typ -> Typ
mkListType :: Typ -> Typ
mkListType = Continuity -> Typ -> Typ
listT Continuity
NotCont

mkOptionType :: Typ -> Typ
mkOptionType :: Typ -> Typ
mkOptionType t :: Typ
t = TName -> Sort -> [Typ] -> Typ
Type "option" Sort
holType [Typ
t]

prodType :: Typ -> Typ -> Typ
prodType :: Typ -> Typ -> Typ
prodType t1 :: Typ
t1 t2 :: Typ
t2 = TName -> Sort -> [Typ] -> Typ
Type TName
prodS Sort
holType [Typ
t1, Typ
t2]

mkFunType :: Typ -> Typ -> Typ
mkFunType :: Typ -> Typ -> Typ
mkFunType s :: Typ
s t :: Typ
t = TName -> Sort -> [Typ] -> Typ
Type TName
funS Sort
holType [Typ
s, Typ
t] -- was "-->" before

-- handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)
mkCurryFunType :: [Typ] -> Typ -> Typ
mkCurryFunType :: [Typ] -> Typ -> Typ
mkCurryFunType = (Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ)
-> (Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ (Typ -> Typ -> Typ) -> Typ -> [Typ] -> Typ
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Typ -> Typ -> Typ
mkFunType -- was "--->" before

-- * predefinded HOLCF types

mkSDomType :: String -> Typ
mkSDomType :: TName -> Typ
mkSDomType s :: TName
s = TName -> Sort -> [Typ] -> Typ
Type TName
s Sort
dom []

voidDom :: Typ
voidDom :: Typ
voidDom = TName -> Typ
mkSDomType "void"

-- should this be included (as primitive)?
flatDom :: Typ
flatDom :: Typ
flatDom = TName -> Typ
mkSDomType "flat"

tLift :: Typ -> Typ
tLift :: Typ -> Typ
tLift t :: Typ
t = TName -> Sort -> [Typ] -> Typ
Type "lift" Sort
dom [Typ
t]

mkBinDomType :: String -> Typ -> Typ -> Typ
mkBinDomType :: TName -> Typ -> Typ -> Typ
mkBinDomType s :: TName
s t1 :: Typ
t1 t2 :: Typ
t2 = TName -> Sort -> [Typ] -> Typ
Type TName
s Sort
dom [Typ
t1, Typ
t2]

mkContFun :: Typ -> Typ -> Typ
mkContFun :: Typ -> Typ -> Typ
mkContFun = TName -> Typ -> Typ -> Typ
mkBinDomType TName
lFunS

mkStrictProduct :: Typ -> Typ -> Typ
mkStrictProduct :: Typ -> Typ -> Typ
mkStrictProduct = TName -> Typ -> Typ -> Typ
mkBinDomType TName
sProdS

mkContProduct :: Typ -> Typ -> Typ
mkContProduct :: Typ -> Typ -> Typ
mkContProduct = TName -> Typ -> Typ -> Typ
mkBinDomType TName
lProdS

-- handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)
mkCurryContFun :: [Typ] -> Typ -> Typ
mkCurryContFun :: [Typ] -> Typ -> Typ
mkCurryContFun = (Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ)
-> (Typ -> [Typ] -> Typ) -> [Typ] -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ (Typ -> Typ -> Typ) -> Typ -> [Typ] -> Typ
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Typ -> Typ -> Typ
mkContFun

mkStrictSum :: Typ -> Typ -> Typ
mkStrictSum :: Typ -> Typ -> Typ
mkStrictSum = TName -> Typ -> Typ -> Typ
mkBinDomType TName
lSumS


-- * term construction

-- | 1000
maxPrio :: Int
maxPrio :: Int
maxPrio = 1000

-- | 10
lowPrio :: Int
lowPrio :: Int
lowPrio = 10

-- | 2
isaEqPrio :: Int
isaEqPrio :: Int
isaEqPrio = 2 -- left assoc

-- | construct constants and variables
mkConstVD :: String -> Typ -> Term
mkConstVD :: TName -> Typ -> Term
mkConstVD s :: TName
s t :: Typ
t = VName -> DTyp -> Term
Const (TName -> VName
mkVName TName
s) (DTyp -> Term) -> DTyp -> Term
forall a b. (a -> b) -> a -> b
$ Typ -> DTyp
hideNN Typ
t

mkConstV :: String -> DTyp -> Term
mkConstV :: TName -> DTyp -> Term
mkConstV = VName -> DTyp -> Term
Const (VName -> DTyp -> Term)
-> (TName -> VName) -> TName -> DTyp -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TName -> VName
mkVName

mkConstD :: VName -> Typ -> Term
mkConstD :: VName -> Typ -> Term
mkConstD s :: VName
s = VName -> DTyp -> Term
Const VName
s (DTyp -> Term) -> (Typ -> DTyp) -> Typ -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> DTyp
hideNN

mkConst :: VName -> DTyp -> Term
mkConst :: VName -> DTyp -> Term
mkConst = VName -> DTyp -> Term
Const

mkFree :: String -> Term
mkFree :: TName -> Term
mkFree = VName -> Term
Free (VName -> Term) -> (TName -> VName) -> TName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TName -> VName
mkVName

-- | construct a constant with no type
con :: VName -> Term
con :: VName -> Term
con s :: VName
s = VName -> DTyp -> Term
mkConst VName
s DTyp
noType

conC :: VName -> Term
conC :: VName -> Term
conC s :: VName
s = VName -> DTyp -> Term
mkConst VName
s DTyp
noTypeC

conDouble :: String -> Term
conDouble :: TName -> Term
conDouble = VName -> Term
con (VName -> Term) -> (TName -> VName) -> TName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TName -> VName
mkVName

conDoubleC :: String -> Term
conDoubleC :: TName -> Term
conDoubleC = VName -> Term
conC (VName -> Term) -> (TName -> VName) -> TName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TName -> VName
mkVName

-- | apply VName operator to two term
binVNameAppl :: VName -> Term -> Term -> Term
binVNameAppl :: VName -> Term -> Term -> Term
binVNameAppl v :: VName
v = Term -> Term -> Term
termAppl (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
termAppl (VName -> Term
con VName
v)

-- * binary junctors
binConj, binDisj, binImpl, binEqv, binEq, binEqvSim, binUnion,
       binMembership, binImageOp
    :: Term -> Term -> Term
binConj :: Term -> Term -> Term
binConj = VName -> Term -> Term -> Term
binVNameAppl VName
conjV
binDisj :: Term -> Term -> Term
binDisj = VName -> Term -> Term -> Term
binVNameAppl VName
disjV
binImpl :: Term -> Term -> Term
binImpl = VName -> Term -> Term -> Term
binVNameAppl VName
implV
binEq :: Term -> Term -> Term
binEq = VName -> Term -> Term -> Term
binVNameAppl VName
eqV
binEqv :: Term -> Term -> Term
binEqv = Term -> Term -> Term
binEq
binEqvSim :: Term -> Term -> Term
binEqvSim = VName -> Term -> Term -> Term
binVNameAppl VName
eqvSimV
binUnion :: Term -> Term -> Term
binUnion = VName -> Term -> Term -> Term
binVNameAppl VName
unionV
binMembership :: Term -> Term -> Term
binMembership = VName -> Term -> Term -> Term
binVNameAppl VName
membershipV
binImageOp :: Term -> Term -> Term
binImageOp = VName -> Term -> Term -> Term
binVNameAppl VName
imageV

rangeOp :: Term -> Term
rangeOp :: Term -> Term
rangeOp = Term -> Term -> Term
termAppl (VName -> Term
con VName
rangeV)

-- | HOL function application
termAppl :: Term -> Term -> Term
termAppl :: Term -> Term -> Term
termAppl t1 :: Term
t1 t2 :: Term
t2 = Term -> Term -> Continuity -> Term
App Term
t1 Term
t2 Continuity
NotCont

-- * terms for HOL-HOLCF

andPT :: Continuity -> Term
andPT :: Continuity -> Term
andPT a :: Continuity
a = case Continuity
a of
  NotCont -> VName -> Term
con VName
conjV
  IsCont _ -> TName -> Term
conDouble "andH"

orPT :: Continuity -> Term
orPT :: Continuity -> Term
orPT a :: Continuity
a = case Continuity
a of
  NotCont -> VName -> Term
con VName
disjV
  IsCont _ -> TName -> Term
conDouble "orH"

notPT :: Continuity -> Term
notPT :: Continuity -> Term
notPT a :: Continuity
a = case Continuity
a of
  NotCont -> VName -> Term
con VName
notV
  IsCont _ -> TName -> Term
conDouble "notH"

bottomPT :: Continuity -> Term
bottomPT :: Continuity -> Term
bottomPT a :: Continuity
a = TName -> Term
conDouble (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
  NotCont -> "undefined"
  IsCont _ -> "UU"

nilPT :: Continuity -> Term
nilPT :: Continuity -> Term
nilPT a :: Continuity
a = TName -> Term
conDoubleC (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
  NotCont -> "[]"
  IsCont _ -> "lNil"

consPT :: Continuity -> Term
consPT :: Continuity -> Term
consPT a :: Continuity
a = case Continuity
a of
  NotCont -> VName -> Term
conC VName
consV
  IsCont True -> TName -> Term
conDouble "llCons"
  IsCont False -> VName -> Term
conC VName
lconsV

truePT :: Continuity -> Term
truePT :: Continuity -> Term
truePT a :: Continuity
a = TName -> Term
conDoubleC (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   NotCont -> "True"
   IsCont _ -> "TRUE"

falsePT :: Continuity -> Term
falsePT :: Continuity -> Term
falsePT a :: Continuity
a = TName -> Term
conDoubleC (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   NotCont -> "False"
   IsCont _ -> "FALSE"

headPT :: Continuity -> Term
headPT :: Continuity -> Term
headPT a :: Continuity
a = TName -> Term
conDouble (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   NotCont -> "hd"
   IsCont _ -> "llHd"

tailPT :: Continuity -> Term
tailPT :: Continuity -> Term
tailPT a :: Continuity
a = TName -> Term
conDouble (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ case Continuity
a of
   NotCont -> "tl"
   IsCont _ -> "llTl"

unitPT :: Continuity -> Term
unitPT :: Continuity -> Term
unitPT a :: Continuity
a = case Continuity
a of
   NotCont -> TName -> Term
conDouble "()"
   IsCont _ -> Term -> Term -> Term
termAppl (TName -> Term
conDouble "Def") (TName -> Term
conDouble "()")

fstPT :: Continuity -> Term
fstPT :: Continuity -> Term
fstPT a :: Continuity
a = case Continuity
a of
              NotCont -> TName -> Term
conDoubleC "fst"
              IsCont True -> TName -> Term
conDouble "llfst"
              IsCont False -> TName -> Term
conDoubleC "lfst"

sndPT :: Continuity -> Term
sndPT :: Continuity -> Term
sndPT a :: Continuity
a = case Continuity
a of
              NotCont -> TName -> Term
conDoubleC "snd"
              IsCont True -> TName -> Term
conDouble "llsnd"
              IsCont False -> TName -> Term
conDoubleC "lsnd"

pairPT :: Continuity -> Term
pairPT :: Continuity -> Term
pairPT a :: Continuity
a = case Continuity
a of
     NotCont -> TName -> Term
conDoubleC "pair"
     IsCont True -> TName -> Term
conDouble "llpair"
     IsCont False -> TName -> Term
conDoubleC "lpair"

nothingPT :: Continuity -> Term
nothingPT :: Continuity -> Term
nothingPT a :: Continuity
a = TName -> Term
conDouble (TName -> Term) -> TName -> Term
forall a b. (a -> b) -> a -> b
$ if Continuity
a Continuity -> Continuity -> Bool
forall a. Eq a => a -> a -> Bool
== Continuity
NotCont
                then "None" else "lNothing"

justPT :: Continuity -> Term
justPT :: Continuity -> Term
justPT a :: Continuity
a = case Continuity
a of
             NotCont -> TName -> Term
conDouble "Some"
             IsCont True -> TName -> Term
conDouble "llJust"
             IsCont False -> TName -> Term
conDoubleC "lJust"

leftPT :: Continuity -> Term
leftPT :: Continuity -> Term
leftPT a :: Continuity
a = case Continuity
a of
             NotCont -> TName -> Term
conDouble "left"
             IsCont True -> TName -> Term
conDouble "llLeft"
             IsCont False -> TName -> Term
conDoubleC "lLeft"

rightPT :: Continuity -> Term
rightPT :: Continuity -> Term
rightPT a :: Continuity
a = case Continuity
a of
             NotCont -> TName -> Term
conDouble "right"
             IsCont True -> TName -> Term
conDouble "llRight"
             IsCont False -> TName -> Term
conDoubleC "lRight"

compPT :: Term
compPT :: Term
compPT = TName -> Term
conDouble "compH"

eqPT :: Term
eqPT :: Term
eqPT = TName -> Term
conDouble "eqH"

neqPT :: Term
neqPT :: Term
neqPT = TName -> Term
conDouble "neqH"

eqTPT :: Typ -> Term
eqTPT :: Typ -> Term
eqTPT = TName -> Typ -> Term
mkConstVD "eqH"

neqTPT :: Typ -> Term
neqTPT :: Typ -> Term
neqTPT = TName -> Typ -> Term
mkConstVD "neqH"

-- * Boolean constants

true :: Term
true :: Term
true = TName -> Typ -> Term
mkConstVD TName
cTrue Typ
boolType

false :: Term
false :: Term
false = TName -> Typ -> Term
mkConstVD TName
cFalse Typ
boolType

-- * UNTYPED terms

-- | defOp constant
defOp :: Term
defOp :: Term
defOp = TName -> Term
conDouble TName
defOpS

-- | Not constant
notOp :: Term
notOp :: Term
notOp = VName -> Term
con VName
notV

-- | some constant
conSome :: Term
conSome :: Term
conSome = TName -> Term
conDouble TName
someS

-- * HOLCF

liftString :: Term
liftString :: Term
liftString = TName -> Term
conDouble "liftList"

lpairTerm :: Term
lpairTerm :: Term
lpairTerm = TName -> Term
conDoubleC "lpair"

-- * constant names

-- | Not VName
notV :: VName
notV :: VName
notV = TName -> Maybe AltSyntax -> VName
VName TName
cNot (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "~/ _" [40] 40

-- * VNames of binary operators

conjV :: VName
conjV :: VName
conjV = TName -> Maybe AltSyntax -> VName
VName TName
conj (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ &/ _)" [36, 35] 35

disjV :: VName
disjV :: VName
disjV = TName -> Maybe AltSyntax -> VName
VName TName
disj (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ |/ _)" [31, 30] 30

implV :: VName
implV :: VName
implV = TName -> Maybe AltSyntax -> VName
VName TName
impl (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ -->/ _)" [26, 25] 25

eqV :: VName
eqV :: VName
eqV = TName -> Maybe AltSyntax -> VName
VName TName
eq (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ =/ _)" [50, 51] 50

neqV :: VName
neqV :: VName
neqV = TName -> Maybe AltSyntax -> VName
VName TName
neq (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ ~=/ _)" [50, 51] 50

plusV :: VName
plusV :: VName
plusV = TName -> Maybe AltSyntax -> VName
VName TName
plusS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ +/ _)" [65, 66] 65

minusV :: VName
minusV :: VName
minusV = TName -> Maybe AltSyntax -> VName
VName TName
minusS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ -/ _)" [65, 66] 65

divV :: VName
divV :: VName
divV = TName -> Maybe AltSyntax -> VName
VName TName
divS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ div/ _)" [70, 71] 70

modV :: VName
modV :: VName
modV = TName -> Maybe AltSyntax -> VName
VName TName
modS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ mod/ _)" [70, 71] 70

timesV :: VName
timesV :: VName
timesV = TName -> Maybe AltSyntax -> VName
VName TName
timesS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ */ _)" [70, 71] 70

consV :: VName
consV :: VName
consV = TName -> Maybe AltSyntax -> VName
VName TName
consS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ #/ _)" [66, 65] 65

lconsV :: VName
lconsV :: VName
lconsV = TName -> Maybe AltSyntax -> VName
VName TName
lconsS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ ###/ _)" [66, 65] 65

appendV :: VName
appendV :: VName
appendV = TName -> Maybe AltSyntax -> VName
VName TName
appendS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ @/ _)" [66, 65] 65

compV :: VName
compV :: VName
compV = TName -> Maybe AltSyntax -> VName
VName TName
compS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ o/ _)" [55, 56] 55

eqvSimV :: VName
eqvSimV :: VName
eqvSimV = TName -> Maybe AltSyntax -> VName
VName TName
eqvSimS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ \\<sim>/ _)" [50, 51] 50

unionV :: VName
unionV :: VName
unionV = TName -> Maybe AltSyntax -> VName
VName TName
unionS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ \\<union>/ _)" [65, 66] 65

membershipV :: VName
membershipV :: VName
membershipV = TName -> Maybe AltSyntax -> VName
VName TName
membershipS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ \\<in>/ _)" [65, 66] 65

imageV :: VName
imageV :: VName
imageV = TName -> Maybe AltSyntax -> VName
VName TName
imageS (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ TName -> [Int] -> Int -> AltSyntax
AltSyntax "(_ `/ _)" [65, 66] 65

rangeV :: VName
rangeV :: VName
rangeV = TName -> Maybe AltSyntax -> VName
VName TName
rangeS Maybe AltSyntax
forall a. Maybe a
Nothing

vMap' :: Map.Map String VName
vMap' :: Map TName VName
vMap' = [(TName, VName)] -> Map TName VName
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(TName
conj, VName
conjV), (TName
disj, VName
disjV), (TName
impl, VName
implV), (TName
eq, VName
eqV),
        (TName
neq, VName
neqV), (TName
plusS, VName
plusV), (TName
minusS, VName
minusV), (TName
divS, VName
divV),
        (TName
modS, VName
modV),
        (TName
timesS, VName
timesV), (TName
consS, VName
consV), (TName
lconsS, VName
lconsV), (TName
compS, VName
compV),
        (TName
eqvSimS, VName
eqvSimV), (TName
unionS, VName
unionV), (TName
membershipS, VName
membershipV),
        (TName
imageS, VName
imageV), (TName
rangeS, VName
rangeV)]

vMap :: Map.Map String VName
vMap :: Map TName VName
vMap = Map TName VName -> Map TName VName -> Map TName VName
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TName VName
vMap' (Map TName VName -> Map TName VName)
-> ([(TName, VName)] -> Map TName VName)
-> [(TName, VName)]
-> Map TName VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TName, VName)] -> Map TName VName
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
 ([(TName, VName)] -> Map TName VName)
-> ([(TName, VName)] -> [(TName, VName)])
-> [(TName, VName)]
-> Map TName VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TName, VName) -> (TName, VName))
-> [(TName, VName)] -> [(TName, VName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: TName
k, v :: VName
v) -> case TName -> TName -> Maybe TName
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "op " TName
k of
                     Just r :: TName
r -> (TName
r, VName
v)
                     Nothing -> (TName
k, VName
v))
 ([(TName, VName)] -> Map TName VName)
-> [(TName, VName)] -> Map TName VName
forall a b. (a -> b) -> a -> b
$ Map TName VName -> [(TName, VName)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TName VName
vMap'

-- * keywords in theory files from the Isar Reference Manual 2005

endS :: String
endS :: TName
endS = "end"

headerS :: String
headerS :: TName
headerS = "header"

theoryS :: String
theoryS :: TName
theoryS = "theory"

importsS :: String
importsS :: TName
importsS = "imports"

usesS :: String
usesS :: TName
usesS = "uses"

beginS :: String
beginS :: TName
beginS = "begin"

contextS :: String
contextS :: TName
contextS = "context"

axiomsS :: String
axiomsS :: TName
axiomsS = "axioms"

axiomatizationS :: String
axiomatizationS :: TName
axiomatizationS = "axiomatization"

defsS :: String
defsS :: TName
defsS = "defs"

oopsS :: String
oopsS :: TName
oopsS = "oops"

mlS :: String
mlS :: TName
mlS = "ML"

mlFileS :: String
mlFileS :: TName
mlFileS = TName
mlS TName -> TName -> TName
forall a. [a] -> [a] -> [a]
++ "_file"

andS :: String
andS :: TName
andS = "and"

lemmasS :: String
lemmasS :: TName
lemmasS = "lemmas"

lemmaS :: String
lemmaS :: TName
lemmaS = "lemma"

corollaryS :: String
corollaryS :: TName
corollaryS = "corollary"

refuteS :: String
refuteS :: TName
refuteS = "refute"

theoremsS :: String
theoremsS :: TName
theoremsS = "theorems"

theoremS :: String
theoremS :: TName
theoremS = "theorem"

axclassS :: String
axclassS :: TName
axclassS = "axclass"

classesS :: String
classesS :: TName
classesS = "classes"

definitionS :: String
definitionS :: TName
definitionS = "definition"

instanceS :: String
instanceS :: TName
instanceS = "instance"

instantiationS :: String
instantiationS :: TName
instantiationS = "instantiation"

typedeclS :: String
typedeclS :: TName
typedeclS = "typedecl"

typesS :: String
typesS :: TName
typesS = "types"

constsS :: String
constsS :: TName
constsS = "consts"

structureS :: String
structureS :: TName
structureS = "structure"

constdefsS :: String
constdefsS :: TName
constdefsS = "constdefs"

domainS :: String
domainS :: TName
domainS = "domain"

datatypeS :: String
datatypeS :: TName
datatypeS = "datatype"

fixrecS :: String
fixrecS :: TName
fixrecS = "fixrec"

primrecS :: String
primrecS :: TName
primrecS = "primrec"

declareS :: String
declareS :: TName
declareS = "declare"

simpS :: String
simpS :: TName
simpS = "simp"

applyS :: String
applyS :: TName
applyS = "apply"

backS :: String
backS :: TName
backS = "back"

deferS :: String
deferS :: TName
deferS = "defer"

preferS :: String
preferS :: TName
preferS = "prefer"

byS :: String
byS :: TName
byS = "by"

doneS :: String
doneS :: TName
doneS = "done"

sorryS :: String
sorryS :: TName
sorryS = "sorry"

autoS :: String
autoS :: TName
autoS = "auto"

inductS :: String
inductS :: TName
inductS = "induct"

caseTacS :: String
caseTacS :: TName
caseTacS = "case_tac"

insertS :: String
insertS :: TName
insertS = "insert"

subgoalTacS :: String
subgoalTacS :: TName
subgoalTacS = "subgoal_tac"

typedefS :: String
typedefS :: TName
typedefS = "typedef"

premiseOpenS :: String
premiseOpenS :: TName
premiseOpenS = "[|"

premiseCloseS :: String
premiseCloseS :: TName
premiseCloseS = "|]"

metaImplS :: String
metaImplS :: TName
metaImplS = "==>"

usingS :: String
usingS :: TName
usingS = "using"

whereS :: String
whereS :: TName
whereS = "where"

dotDot :: String
dotDot :: TName
dotDot = ".."

barS :: String
barS :: TName
barS = "|"

markups :: [String]
markups :: [TName]
markups =
    [ "--", "chapter" , "section", "subsection", "subsubsection", "text"
    , "text_raw", "sect", "subsect", "subsubsect", "txt", "txt_raw"]

-- | toplevel keys that are currently ignored
ignoredKeys :: [String]
ignoredKeys :: [TName]
ignoredKeys =
    [ TName
domainS, TName
oopsS, TName
refuteS, TName
fixrecS, TName
primrecS, TName
declareS, TName
usingS
    , TName
dotDot, TName
typedefS, TName
mlFileS
    , "open", "sorry", "done", "by", "proof", "apply", "qed"
    , "classrel", "defaultsort", "nonterminls", "arities"
    , "syntax", "no_syntax", "translations"
    , "global", "local", "hide", "use", "setup", "method_setup"
    , "ML_command", "ML_setup", "oracle"
    , "fix", "assume", "presume", "def", "note", "then", "from", "with"
    , "have", "show", "hence", "thus", "shows", "."
-- , "rule", "iprover","OF", "of", "where", "assumption", "this", "-"
    , "let", "is", "next", "apply_end", "defer", "prefer", "back"
    , "pr", "thm", "prf", "term", "prop", "typ", "full_prf"
    , "undo", "redo", "kill", "thms_containing", "thms_deps"
    , "cd", "pwd", "use_thy", "use_thy_only", "update_thy"
    , "update_thy_only"
    , "display_drafts", "in", "locale" -- "intro_classes"
    , "fixes", "constrains" -- "assumes"
    , "defines", "notes", "includes"
    , "interpretation", "interpret", "obtain", "also", "finally"
    , "moreover", "ultimately" -- "trans", "sym", "symmetric"
    , "case", "judgment", "morphisms", "record", "rep_datatype"
    , "recdef", "recdef_tc", "specification", "ax_specification"
    , "inductive", "coinductive", "inductive_cases", "codatatype"
    , "code_module", "code_library", "consts_code", "types_code" ]
    [TName] -> [TName] -> [TName]
forall a. [a] -> [a] -> [a]
++ (TName -> TName) -> [TName] -> [TName]
forall a b. (a -> b) -> [a] -> [b]
map (TName -> TName -> TName
forall a. [a] -> [a] -> [a]
++ "_translation")
       [ "parse_ast", "parse", "print", "print_ast", "typed_print"
       , "token" ]
    [TName] -> [TName] -> [TName]
forall a. [a] -> [a] -> [a]
++ (TName -> TName) -> [TName] -> [TName]
forall a b. (a -> b) -> [a] -> [b]
map ("print_" TName -> TName -> TName
forall a. [a] -> [a] -> [a]
++)
       [ "commands", "syntax", "methods", "attributes", "theorems"
       , "tcset"
       , "facts", "binds", "drafts", "locale", "locales", "interps"
       , "trans_rules", "simp_set", "claset", "cases", "induct_rules" ]

-- | toplevel keywords currently recognized by IsaParse
usedTopKeys :: [String]
usedTopKeys :: [TName]
usedTopKeys = [TName]
markups [TName] -> [TName] -> [TName]
forall a. [a] -> [a] -> [a]
++
    [ TName
importsS, TName
usesS, TName
beginS, TName
contextS, TName
mlS, TName
axiomatizationS, TName
axiomsS
    , TName
defsS, TName
constsS
    , TName
constdefsS, TName
lemmasS, TName
theoremsS, TName
lemmaS, TName
corollaryS, TName
theoremS
    , TName
datatypeS
    , TName
classesS, TName
axclassS, TName
instanceS, TName
typesS, TName
typedeclS, TName
endS ]

-- | all Isabelle keywords
isaKeywords :: [String]
isaKeywords :: [TName]
isaKeywords = "::" TName -> [TName] -> [TName]
forall a. a -> [a] -> [a]
: TName
andS TName -> [TName] -> [TName]
forall a. a -> [a] -> [a]
: TName
theoryS TName -> [TName] -> [TName]
forall a. a -> [a] -> [a]
: (Char -> TName) -> TName -> [TName]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> TName -> TName
forall a. a -> [a] -> [a]
: []) ":=<|"
              [TName] -> [TName] -> [TName]
forall a. [a] -> [a] -> [a]
++ [TName]
usedTopKeys [TName] -> [TName] -> [TName]
forall a. [a] -> [a] -> [a]
++ [TName]
ignoredKeys

mkVName :: String -> VName
mkVName :: TName -> VName
mkVName s :: TName
s = VName -> Maybe VName -> VName
forall a. a -> Maybe a -> a
fromMaybe (TName -> Maybe AltSyntax -> VName
VName TName
s Maybe AltSyntax
forall a. Maybe a
Nothing) (Maybe VName -> VName) -> Maybe VName -> VName
forall a b. (a -> b) -> a -> b
$ TName -> Map TName VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TName
s Map TName VName
vMap