-- possibly differentiate between HOL and HOLCF
-- | a topological sort with a @uses@ predicate
quickSort :: (a -> a -> Bool) -> [a] -> [a]
quickSort f ls = case ls of
a : as -> let (xs, ys) = partition (f a) as in
quickSort f xs ++ a : quickSort f ys
-- **** STRINGS ------------------------------------------------
allS, exS, ex1S :: String
-- * Strings of binary ops
-- * some stuff for Isabelle
prodS, sProdS, funS, cFunS, lFunS, sSumS, lProdS, lSumS :: TName
prodS = "*" -- this is printed as it is!
lProdS = "lprod" -- "***"
-- * some stuff for HasCASL
-- * strings for HOLCF lifting functions
-- **** CLASSES & SORTS ---------------------------------------
isaTerm = IsaClass "type"
sortT :: Continuity -> Sort
--------------------- POLY TYPES --------------------------------------
listT :: Continuity -> Typ -> Typ
IsCont _ -> Type "llist" (sortT a) [t]
NotCont -> Type "list" (sortT a) [t]
charT :: Continuity -> Typ
IsCont _ -> Type "charT" (sortT a) []
NotCont -> Type "char" (sortT a) []
ratT :: Continuity -> Typ
IsCont _ -> Type "ratT" (sortT a) []
NotCont -> Type "rat" (sortT a) []
fracT :: Continuity -> Typ
fracT a = Type "fracT" (sortT a) []
integerT :: Continuity -> Typ
IsCont _ -> Type "integerT" (sortT a) []
NotCont -> Type "int" (sortT a) []
boolT :: Continuity -> Typ
IsCont _ -> Type "lBool" (sortT a) []
NotCont -> Type "bool" (sortT a) []
orderingT :: Continuity -> Typ
IsCont _ -> Type "lOrdering" (sortT a) []
NotCont -> Type "sOrdering" (sortT a) []
intT :: Continuity -> Typ
IsCont _ -> Type "intT" (sortT a) []
NotCont -> Type "int" (sortT a) []
prodT :: Continuity -> Typ -> Typ -> Typ
prodT a t1 t2 = case a of
IsCont _ -> mkContProduct t1 t2
NotCont -> prodType t1 t2
funT :: Continuity -> Typ -> Typ -> Typ
IsCont _ -> mkContFun a b
curryFunT :: Continuity -> [Typ] -> Typ -> Typ
curryFunT c ls x = case c of
IsCont _ -> mkCurryContFun ls x
NotCont -> mkCurryFunType ls x
-- **** predefinded HOL TYPES ----------------------------------
noTypeT = Type "dummy" holType []
noType = Hide noTypeT NA Nothing
noTypeC = Hide noTypeT TCon Nothing
hideNN t = Hide t NA Nothing
hideCN t = Hide t TCon Nothing
dispNN t = Disp t NA Nothing
dispMN t = Disp t TMet Nothing
mkListType t = Type "list" holType [t]
mkOptionType :: Typ -> Typ
mkOptionType t = Type "option" holType [t]
prodType :: Typ -> Typ -> Typ
prodType t1 t2 = Type prodS holType [t1,t2]
mkFunType :: Typ -> Typ -> Typ
mkFunType s t = Type funS holType [s,t] -- was "-->" before
{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
mkCurryFunType :: [Typ] -> Typ -> Typ
mkCurryFunType = flip $ foldr mkFunType -- was "--->" before
-- **** predefinded HOLCF TYPES --------------------------------------
voidDom = Type "void" dom []
{- should this be included (as primitive)? -}
flatDom = Type "flat" dom []
tLift t = Type "lift" dom [t]
mkContFun :: Typ -> Typ -> Typ
mkContFun t1 t2 = Type lFunS dom [t1,t2]
mkStrictProduct :: Typ -> Typ -> Typ
mkStrictProduct t1 t2 = Type sProdS dom [t1,t2]
mkContProduct :: Typ -> Typ -> Typ
mkContProduct t1 t2 = Type lProdS dom [t1,t2]
{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
mkCurryContFun :: [Typ] -> Typ -> Typ
mkCurryContFun = flip $ foldr mkContFun -- was "--->" before
mkStrictSum :: Typ -> Typ -> Typ
mkStrictSum t1 t2 = Type lSumS dom [t1,t2]
-- **** TERM FORMATION -------------------------------------------
isaEqPrio = 2 -- left assoc
-- | construct constants and variables
mkConstVD :: String -> Typ -> Term
mkConstVD s t = Const (mkVName s) $ hideNN t
mkConstV :: String -> DTyp -> Term
mkConstV s t = Const (mkVName s) t
mkConstD :: VName -> Typ -> Term
mkConstD s t = Const s $ hideNN t
mkConst :: VName -> DTyp -> Term
mkFree s = Free $ mkVName s
-- | construct a constant with no type
conC s = mkConst s noTypeC
conDouble :: String -> Term
conDouble = con . mkVName
conDoubleC :: String -> Term
conDoubleC = conC . mkVName
-- | apply VName operator to two term
binVNameAppl :: VName -> Term -> Term -> Term
binVNameAppl v t1 t2 = termAppl (termAppl (con v) t1) t2
binConj, binDisj, binImpl, binEqv, binEq, binEqvSim, binUnion,
binMembership, binImageOp
binConj = binVNameAppl conjV
binDisj = binVNameAppl disjV
binImpl = binVNameAppl implV
binEqvSim = binVNameAppl eqvSimV
binUnion = binVNameAppl unionV
binMembership = binVNameAppl membershipV
binImageOp = binVNameAppl imageV
rangeOp t = termAppl (con rangeV) t
-- | HOL function application
termAppl :: Term -> Term -> Term
termAppl t1 t2 = App t1 t2 NotCont
-- **** Poly terms for HOL-HOLCF ----------------------------------
andPT :: Continuity -> Term
IsCont _ -> conDouble "andH"
orPT :: Continuity -> Term
IsCont _ -> conDouble "orH"
notPT :: Continuity -> Term
IsCont _ -> conDouble "notH"
bottomPT :: Continuity -> Term
bottomPT a = conDouble $ case a of
nilPT :: Continuity -> Term
nilPT a = conDoubleC $ case a of
consPT :: Continuity -> Term
IsCont True -> conDouble "llCons"
IsCont False -> conC lconsV
truePT :: Continuity -> Term
truePT a = conDoubleC $ case a of
falsePT :: Continuity -> Term
falsePT a = conDoubleC $ case a of
headPT :: Continuity -> Term
headPT a = conDouble $ case a of
tailPT :: Continuity -> Term
tailPT a = conDouble $ case a of
unitPT :: Continuity -> Term
NotCont -> conDouble "()"
IsCont _ -> termAppl (conDouble "Def") (conDouble "()")
fstPT :: Continuity -> Term
NotCont -> conDoubleC "fst"
IsCont True -> conDouble "llfst"
IsCont False -> conDoubleC "lfst"
sndPT :: Continuity -> Term
NotCont -> conDoubleC "snd"
IsCont True -> conDouble "llsnd"
IsCont False -> conDoubleC "lsnd"
pairPT :: Continuity -> Term
NotCont -> conDoubleC "pair"
IsCont True -> conDouble "llpair"
IsCont False -> conDoubleC "lpair"
nothingPT :: Continuity -> Term
nothingPT a = conDouble $ if a == NotCont
then "None" else "lNothing"
justPT :: Continuity -> Term
NotCont -> conDouble "Some"
IsCont True -> conDouble "llJust"
IsCont False -> conDoubleC "lJust"
leftPT :: Continuity -> Term
NotCont -> conDouble "left"
IsCont True -> conDouble "llLeft"
IsCont False -> conDoubleC "lLeft"
rightPT :: Continuity -> Term
NotCont -> conDouble "right"
IsCont True -> conDouble "llRight"
IsCont False -> conDoubleC "lRight"
compPT = conDouble "compH"
eqTPT t = mkConstVD "eqH" t
neqTPT t = mkConstVD "neqH" t
-- **** TERMS ---------------------------------------------------
true = mkConstVD cTrue boolType
false = mkConstVD cFalse boolType
conSome = conDouble someS
liftString = conDouble "liftList"
lpairTerm = conDoubleC "lpair"
-- **** VNAMES -------------------------------------------------
notV = VName cNot $ Just $ AltSyntax "~/ _" [40] 40
-- * VNames of binary operators
conjV = VName conj $ Just $ AltSyntax "(_ &/ _)" [36, 35] 35
disjV = VName disj $ Just $ AltSyntax "(_ |/ _)" [31, 30] 30
implV = VName impl $ Just $ AltSyntax "(_ -->/ _)" [26, 25] 25
eqV = VName eq $ Just $ AltSyntax "(_ =/ _)" [50, 51] 50
plusV = VName plusS $ Just $ AltSyntax "(_ +/ _)" [65, 66] 65
minusV = VName minusS $ Just $ AltSyntax "(_ -/ _)" [65, 66] 65
divV = VName divS $ Just $ AltSyntax "(_ div/ _)" [70, 71] 70
modV = VName modS $ Just $ AltSyntax "(_ mod/ _)" [70, 71] 70
timesV = VName timesS $ Just $ AltSyntax "(_ */ _)" [70, 71] 70
consV = VName consS $ Just $ AltSyntax "(_ #/ _)" [66, 65] 65
lconsV = VName lconsS $ Just $ AltSyntax "(_ ###/ _)" [66, 65] 65
compV = VName compS $ Just $ AltSyntax "(_ o/ _)" [55, 56] 55
eqvSimV = VName eqvSimS $ Just $ AltSyntax "(_ \\<sim>/ _)" [50,51] 50
unionV = VName unionS $ Just $ AltSyntax "(_ \\<union>/ _)" [65,66] 65
membershipV = VName membershipS $ Just $ AltSyntax "(_ \\<in>/ _)" [65,66] 65
imageV = VName imageS $ Just $ AltSyntax "(_ `/ _)" [65,66] 65
rangeV = VName rangeS Nothing
-- **** keywords in theory files from the Isar Reference Manual 2005
definitionS = "definition"
instantiationS = "instantiation"
subgoalTacS = "subgoal_tac"
[ "--", "chapter" , "section", "subsection", "subsubsection", "text"
, "text_raw", "sect", "subsect", "subsubsect", "txt", "txt_raw"]
-- | toplevel keys that are currently ignored
[ domainS, oopsS, refuteS, fixrecS, primrecS, declareS, usingS
, "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"
, "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" ]
++ map (++ "_translation")
[ "parse_ast", "parse", "print", "print_ast", "typed_print"
[ "commands", "syntax", "methods", "attributes", "theorems"
, "facts", "binds", "drafts", "locale", "locales", "interps"
, "trans_rules", "simp_set", "claset", "cases", "induct_rules" ]
-- | toplevel keywords currently recognized by IsaParse
[ importsS, usesS, beginS, contextS, mlS, axiomsS, defsS, constsS
, constdefsS, lemmasS, theoremsS, lemmaS, corollaryS, theoremS
, classesS, axclassS, instanceS, typesS, typedeclS, endS ]
-- | all Isabelle keywords
isaKeywords = "::" : andS : theoryS : map (:[]) ":=<|"
++ usedTopKeys ++ ignoredKeys