module IsabelleProp where
import IsabelleTerm
import IsabelleType
import Mixfix
type TypedId = (String, Maybe Type)
data Prop
= PropTrue {- truth value -}
| PropFalse {- truth value -}
| PropVar String {- Propositional variable -}
| PropHas [PredArg] Pred {- Predicate membership -}
| PropEqual Term Term {- equality assertion -}
| PropConj Prop Prop {- propositional conjunct -}
| PropDisj Prop Prop {- propositional disjunct -}
| PropImpl Prop Prop {- implication chain -}
| PropEquiv Prop Prop {- equivalence -}
| PropNeg Prop {- negation -}
| PropForall [TypedId] Prop {- universal quantification -}
| PropExists [TypedId] Prop {- existential quantification -}
-- maybe should add type field to quantifiers
data PropDecl
= PropDecl String Prop {- prop. declaration -}
data Pred = PredStrong Pred' | PredWeak Pred'
data Pred'
{- PredConst : String -> Pred -} {- predicate constant -}
= PredUniv
| PredUndef
| PredArrow Pred Pred {- arrow predicate -}
| PredLfp String Pred {- least fixed-point predicate -}
| PredGfp String Pred {- greatest fixed-point predicate-}
| PredVar String {- predicate variable -}
| PredLifted Term {- lifted section predicate -}
| PredNeg Pred {- negated predicate -}
| PredTuple [Pred] {- tuple predicate -}
| PredLit Integer {- literal predicate -}
| PredCong String [PredArg] {- constructor congruence pred. -}
| PredComp [Pattern] Prop {- set comprehension -}
| PredDisj Pred Pred {- pred. disjunction -}
| PredConj Pred Pred {- pred. conjunction -}
| PredImpl Pred Pred {- pred. implication chain -}
| PredEquiv Pred Pred {- pred. equivalence -}
-- shouldn't PredEquiv return Prop? or is this pointwise equivalence?
data PredArg
= TermArg Term
| PredArg Pred
data PredPat
= PredAbs String [String] {- pred. abstraction -}
{-
data Param
= TermParam String
| PredParam String
-}
data PredDecl
= PredDecl PredPat Pred {- pred. declaration -}
------------------------------------------------------------
propForall x (PropForall xs u) = PropForall (x:xs) u
propForall x u = PropForall [x] u
propExists x (PropExists xs u) = PropExists (x:xs) u
propExists x u = PropExists [x] u
--signature sorts Pred PredPat PredFormula PredDecl
------------------------------------------------------------
instance Show Prop where
showsPrec p x = case x of
PropTrue -> showString "PropTrue"
PropFalse -> showString "PropFalse"
PropVar x -> showString x
PropHas [x] a -> mixfix "_ \\<in> _" [showsPrec 50 x, showsPrec 51 a] 50 p
PropHas xs a -> mixfix "_ \\<in> _" [showTuple (map shows xs), showsPrec 51 a] 50 p
PropEqual u v -> showHBrackets (shows u . showString " = " . shows v)
PropConj u v -> mixfix "_ \\<conj> _" [showsPrec 36 u, showsPrec 35 v] 35 p
PropDisj u v -> mixfix "_ \\<or> _" [showsPrec 31 u, showsPrec 30 v] 30 p
PropImpl u v -> mixfix "_ \\<longrightarrow> _" [showsPrec 26 u, showsPrec 25 v] 25 p
PropEquiv u v -> mixfix "_ = _" [showsPrec 50 u, showsPrec 51 v] 50 p
PropNeg u -> mixfix "\\<not> _" [showsPrec 40 u] 40 p
PropForall xs u ->
mixfix "\\<forall>_. _" [showTypedIds xs, showsPrec 10 u] 10 p
PropExists xs u ->
mixfix "\\<exists>_. _" [showTypedIds xs, showsPrec 10 u] 10 p
where
showTypedId p (x, Nothing) = showString x
showTypedId p (x, Just t) = mixfix "_::_" [showString x, shows t] 0 p
showTypedIds (x:[]) = showTypedId 0 x
showTypedIds (x:xs) = mixfix "_ _" [showTypedId 1 x, showTypedIds xs] 0 0
instance Show Pred where
showsPrec p x = case x of
PredStrong a -> mixfix "strong _" [showsPrec 1000 a] 999 p
PredWeak a -> mixfix "weak _" [showsPrec 1000 a] 999 p
instance Show Pred' where
showsPrec p x = case x of
PredUniv -> showString "UNIV"
PredUndef -> showString "{UU}"
PredArrow a b -> mixfix "arrow _ _" [showsPrec 1000 a, showsPrec 1000 b] 999 p
PredLfp x a -> mixfix "lfp (%_. _)" [showString x, shows a] 999 p
PredGfp x a -> mixfix "gfp (%_. _)" [showString x, shows a] 999 p
PredVar x -> showString x
PredLifted x -> mixfix "lifted _" [showsPrec 1000 x] 999 p
PredNeg a -> mixfix "- _" [showsPrec 81 a] 80 p
PredTuple as -> showTuple (map shows as)
PredLit n -> showBraces (shows (HInt n))
PredCong c [] -> showBraces (showString c)
PredCong c xs -> mixfix "cong_ _ _"
[shows (length xs), showString c, showSpaceSep (map showCongArg xs)] 999 p
PredComp [x] a -> mixfix "{_. _}" [shows x, shows a] 1000 p
PredComp xs a -> mixfix "{_. _}" [showTuple (map shows xs), shows a] 1000 p
PredDisj a b -> mixfix "_ Un _" [showsPrec 65 a, showsPrec 66 b] 65 p
PredConj a b -> mixfix "_ Int _" [showsPrec 70 a, showsPrec 71 b] 70 p
PredImpl a b -> mixfix "- _ Un _" [showsPrec 81 a, showsPrec 71 b] 65 p
PredEquiv a b -> mixfix "_ <=> _" [showsPrec 50 a, showsPrec 51 b] 50 p
instance Show PredArg where
showsPrec p x = case x of
TermArg t -> showsPrec p t
PredArg a -> showsPrec p a
showCongArg x = case x of
TermArg t -> showBraces (shows t)
PredArg a -> showsPrec 1000 a
instance Show PredPat where
showsPrec p (PredAbs f xs) = case xs of
[] -> showString f
_ -> mixfix "_ _" [showString f, showSpaceSep (map showString xs)] 999 p
{-
instance Show Param where
showsPrec p x = case x of
TermParam s -> showString s
PredParam s -> showString s
-}
instance Show PredDecl where
showsPrec p (PredDecl (lhs@(PredAbs x _)) rhs) =
mixfix "constdefs\n _ :: \"\\_\"\n \"_ == _\"\n"
[showString x, showsPrec 3 lhs, showsPrec 2 rhs] 2 p
instance Show PropDecl where
showsPrec p (PropDecl lhs rhs) =
mixfix "\nlocale _ = assumes\n \"_\"\n" [showString lhs, shows rhs] 0 0
{-
mixfix "constdefs\n _ :: bool\n \"_ == _\"\n"
[showString lhs, showString lhs, showsPrec 2 rhs] 2 p
-}