content: module Test0 where
  import List(sort)
  import Ix(inRange)
  {-P:
  import PreludeProps(Finite)
  -}
  
  {-P:
  
  property ImpliesToo P Q = -/ P \/ Q
  
  property IsIdentity' = IsIdentity
  
  property IsIdentity f = All x . {f x} === x -- :: Pred(a->a)
  
  property IsIdentityToo f = f === id -- :: Pred(a->a)
  
  assert Id1 = id ::: IsIdentity  {-#cert:id1#-} {-#cert:id1b#-}
  assert MapId1 = {map id} ::: IsIdentity  {-#cert:mapid1#-}
  -}
  
  idid = id . id
  
  --f x = not (not x)
  --f x = not x
  f = not . not
  
  testcase1 = print (f True,f False) {-#cert:testcase1#-}
  
  {-P:
  assert NotNotIsId = f ::: IsIdentity 
  {-#cert:notnot1#-} {-#cert:notnot2#-}
  
  assert not ::: IsIdentity -- unprovable!!
  
  --assert {case True of {True -> id}}:::IsIdentity
  
  -- This style of definition is not supported in Dick's proposed syntax:
  --property IsFunctor1 map = All f . All g . {map (f.g)} === {map f . map g}
  
  property IsFunctor1 map = All f . All g . {map (f.g)}==={map f . map g}
  property IsFunctor2 map = {map id} === id  -- :: Pred ((a->a)->(b->b))
  property IsFunctor      = IsFunctor1 /\ IsFunctor2
  
  assert MF = map ::: IsFunctor
  assert IF = id ::: IsFunctor
  assert CF = (.) ::: IsFunctor
  
  property AndToo P Q = P /\ Q
  property OrToo P Q = P \/ Q
  
  property IsAssoc (*) = All x, y, z . {(x*y)*z} === {x*(y*z)}
  property IsCommutative (*) = All x, y . {x*y} === {y*x}
  
  assert PlusAssoc = {(+)::Int->Int->Int} ::: IsAssoc {-#cert:PlusAssoc#-}
  assert PlusCommutes = {(+)::Int->Int->Int} ::: IsCommutative
  
  assert PlusAssocFloat = {(+)::Float->Float->Float} ::: IsAssoc {-#cert:PlusAssocFloat#-}
  
  property AC = IsAssoc /\ IsCommutative
  
  assert PlusAC = {(+)::Int->Int->Int} ::: AC {-#cert:PlusAC#-}
  
  --property WO Base pred = Lfp X . {| x | x ::: Base \/ {pred x}::: X |}
  
  --property WO_Int = WO !(==0) {subtract (1::Int)}
  -}
  fac 0 = 1
  fac n = n * fac(n-1)
  
  property InRange r = !(inRange r)
  
  testcase2 = putStr $ unlines [show (n,fac n)|n<-[0..10]] {-#cert:testcase2#-}
  
  {-P:
  property Pos x = x::: $ !(>=0)
  
  assert FacPos = {fac::Int->Int} ::: Pos -> Pos {-#cert:FacPos#-}
  
  property PosOp = Pos -> Pos -> Pos
  assert PlusPos = {(+)::Int->Int->Int} ::: PosOp {-#cert:PlusPos#-}
  
  --assert fac ::: WO_Int -> WO_Int
  -}
  x=True
  
  {-P: {--}
  property IsTrue = !(==True)
  property IsTrueToo = True -- a lifted constructor
  -- Are all these equivalent?
  assert x==={True}
  assert x:::True
  assert x::: !(==True)
  assert True x
  assert x:::IsTrue
  assert IsTrue x
  
  --property Finite = Lfp Fin . {| xs | xs:::[] \/ xs::: Univ:Fin |}
  --property Finite = Lfp Fin . [] \/ Univ:Fin
  --property Infinite = Gfp Inf . {| xs | xs:::Univ:Inf |}
  property Infinite = Gfp Inf . Univ:Inf
  
  property Fix P = Lfp X . P X
  --u = Univ
  
  -- The predicate that is true for every value:
  property Univ = Gfp U . U -- Ok?
  
  assert {[1..10]::[Integer]}:::Finite
  assert {[1..]::[Integer]}:::Infinite
  
  assert {Just True} ::: Just True
  
  property LeftUnit m = All x . {fst m x (snd m)} === x
  
  property Eventually P =  Lfp X . ($P : Univ) \/ ($Univ : $X)
  
  property Equal x y = x===y
  
  --property Nub = Lfp Nub . {| x:xs::[a] | True {x `notElem` xs} /\ Nub xs |}
  
  --property InList = Lfp R . {| (x,y:ys) | x === y \/ R {(x,ys)} |}
  
  --property InList2 = Lfp R . {| y:ys,x | x === y \/ R ys x |}
  
  --assert InList {(5, [1..10]::[Integer])}
  --assert InList2 {[1..10]::[Integer]} 5
  --assert Even1_10 = Exist x . x::: !even ==> x ::: InList2 {[1..10::Integer]}
  --assert Even1_10 = Exist x . x::: !even ==> {(x,[1..10::Integer])} ::: InList
  
  property Even = !even
  assert ZeroIsEven = 0:::Even
  
  property OldAllElems P = Lfp X . {| xs | xs:::[] \/ xs:::P:X |}
  property AllElems P = Lfp X . [] \/ (P:X)
  property Minimal ys y = AllElems (!(y<=)) ys
  property Ordered = Lfp P . {| xs | xs:::[] \/ xs:::Minimal xs:P |}
  
  xs = [1..60]
  
  assert M = Minimal xs {1}
  
  assert SortProp = All xs.{sort xs}:::Ordered {-#cert:SortProp#-}
  assert SortProp2 = {sort::[Int]->[Int]}:::Univ->Ordered {-#cert:SortProp2#-}
  
  assert Fst = All x::Maybe a . x==={Nothing} \/  Exist y . x==={Just y}
  {-#cert:Fst#-}
  assert Fst' = All x . x ::: (Nothing \/ Just Univ)
  
  property SyntBug = Univ /\ Univ : Univ
  property SyntaxBug = {| x | x:::Univ /\ x::: Univ:Univ |}
  
  property Pair = (Univ , Univ)
  --property Pair' = {| (x,y) | x:::Univ /\ y:::Univ |}
  property Pair'' = (,) Univ Univ
  property PosPair = (Pos,Pos)
  property Unit = ()
  
  property FiniteToo = $( Lfp P. [] \/ Univ : $P )
  
  assert ExcludedMiddle = All b . b ::: (False \/ True) {-#cert:ExcludedMiddle#-}
  
  property Returns x = {| m | m==={m>>return x} |}
  
  assert RevLength = All xs . {length (reverse xs)} === {length xs}
  assert RevSumInt = All xs::[Int] . {sum (reverse xs)} === {sum xs}
  assert RevSum = All xs .
     IsCommutative {(+) `at` head xs} ==> {sum (reverse xs)} === {sum xs}
  
  op `at` x = op `asTypeOf` optype x
    where optype :: a -> (a->a->a)
          optype = undefined
  
  -}
  