
   0 | module Test.DepTyCheck.Gen.Emptiness
   1 | 
   2 | import Control.Relation
   3 | import Control.Order
   4 | 
   5 | import public Language.Implicits.IfUnsolved
   6 | 
   7 | %default total
   8 | 
   9 | --- The data ---
  10 | 
  11 | public export
  12 | data Emptiness = NonEmpty | MaybeEmpty
  13 | 
  14 | public export
  15 | Eq Emptiness where
  16 |   NonEmpty   == NonEmpty   = True
  17 |   MaybeEmpty == MaybeEmpty = True
  18 |   NonEmpty   == MaybeEmpty = False
  19 |   MaybeEmpty == NonEmpty   = False
  20 | 
  21 | --- Order by strength ---
  22 | 
  23 | public export
  24 | data NoWeaker : (from, to : Emptiness) -> Type where
  25 |   NN : NonEmpty `NoWeaker` NonEmpty
  26 |   AS : em       `NoWeaker` MaybeEmpty
  27 | 
  28 | export infix 6 `NoWeaker`
  29 | 
  30 | Uninhabited (MaybeEmpty `NoWeaker` NonEmpty) where
  31 |   uninhabited _ impossible
  32 | 
  33 | ||| Smaller is the value that gives less guarantees
  34 | export
  35 | Ord Emptiness where
  36 |   compare MaybeEmpty NonEmpty   = LT
  37 |   compare NonEmpty   MaybeEmpty = GT
  38 |   compare _          _          = EQ
  39 | 
  40 | export
  41 | Reflexive _ NoWeaker where
  42 |   reflexive {x=NonEmpty}   = %search
  43 |   reflexive {x=MaybeEmpty} = %search
  44 | 
  45 | export
  46 | transitive' : x `NoWeaker` y -> y `NoWeaker` z -> x `NoWeaker` z
  47 | transitive' NN NN = %search
  48 | transitive' NN AS = %search
  49 | transitive' AS AS = %search
  50 | 
  51 | export
  52 | Transitive _ NoWeaker where
  53 |   transitive = transitive'
  54 | 
  55 | export
  56 | Antisymmetric _ NoWeaker where
  57 |   antisymmetric NN NN = Refl
  58 |   antisymmetric AS AS = Refl
  59 | 
  60 | export
  61 | Preorder _ NoWeaker where
  62 | 
  63 | export
  64 | PartialOrder _ NoWeaker where
  65 | 
  66 | export
  67 | Connex _ NoWeaker where
  68 |   connex {x=NonEmpty}   {y=NonEmpty}   = %search
  69 |   connex {x=MaybeEmpty} {y=MaybeEmpty} = %search
  70 |   connex {x=NonEmpty}   {y=MaybeEmpty} = %search
  71 |   connex {x=MaybeEmpty} {y=NonEmpty}   = %search
  72 | 
  73 | export
  74 | LinearOrder _ NoWeaker where
  75 | 
  76 | export
  77 | StronglyConnex _ NoWeaker where
  78 |   order NonEmpty   NonEmpty   = %search
  79 |   order NonEmpty   MaybeEmpty = %search
  80 |   order MaybeEmpty NonEmpty   = %search
  81 |   order MaybeEmpty MaybeEmpty = %search
  82 | 
  83 | export %hint
  84 | rev : {a, b : _} -> Not (a `NoWeaker` b) -> b `NoWeaker` a
  85 | rev f = either (absurd . f) id $ order a b
  86 | 
  87 | export %hint
  88 | nonEmptyIsStrongest : {em : _} -> NonEmpty `NoWeaker` em
  89 | nonEmptyIsStrongest {em=NonEmpty}   = NN
  90 | nonEmptyIsStrongest {em=MaybeEmpty} = AS
  91 | 
  92 | export
  93 | maybeEmptyIsMinimal : (0 _ : MaybeEmpty `NoWeaker` em) -> em = MaybeEmpty
  94 | maybeEmptyIsMinimal nw = irrelevantEq $ case nw of AS => Refl
  95 | 
  96 | export
  97 | nonEmptyIsMaximal : (0 _ : em `NoWeaker` NonEmpty) -> em = NonEmpty
  98 | nonEmptyIsMaximal nw = irrelevantEq $ case nw of NN => Refl
  99 | 
 100 | export
 101 | minMaybeEmptyLeft : (0 em : Emptiness) -> min MaybeEmpty em = MaybeEmpty
 102 | minMaybeEmptyLeft em = irrelevantEq $ case em of
 103 |   NonEmpty   => Refl
 104 |   MaybeEmpty => Refl
 105 | 
 106 | export
 107 | minMaybeEmptyRight : (0 em : Emptiness) -> min em MaybeEmpty = MaybeEmpty
 108 | minMaybeEmptyRight em = irrelevantEq $ case em of
 109 |   NonEmpty   => Refl
 110 |   MaybeEmpty => Refl
 111 | 
 112 | export
 113 | minNonEmptyLeft : (0 em : Emptiness) -> min NonEmpty em = em
 114 | minNonEmptyLeft em = irrelevantEq $ case em of
 115 |   NonEmpty   => Refl
 116 |   MaybeEmpty => Refl
 117 | 
 118 | export
 119 | minNonEmptyRight : (0 em : Emptiness) -> min em NonEmpty = em
 120 | minNonEmptyRight em = irrelevantEq $ case em of
 121 |   NonEmpty   => Refl
 122 |   MaybeEmpty => Refl
 123 | 
 124 | export
 125 | minSame : (0 em : Emptiness) -> min em em = em
 126 | minSame em = irrelevantEq $ case em of
 127 |   NonEmpty   => Refl
 128 |   MaybeEmpty => Refl
 129 | 
 130 | export
 131 | minNoWeaker : a1 `NoWeaker` a2 -> b1 `NoWeaker` b2 ->
 132 |               min a1 b1 `NoWeaker` min a2 b2
 133 | minNoWeaker NN nw = rewrite minNonEmptyLeft b1 in
 134 |                     rewrite minNonEmptyLeft b2 in
 135 |                     nw
 136 | minNoWeaker AS _ = rewrite minMaybeEmptyLeft b2 in AS
 137 | 
 138 | export
 139 | minNoWeakerLeft : {c : _} -> a `NoWeaker` b -> min a c `NoWeaker` min b c
 140 | minNoWeakerLeft nw = minNoWeaker nw reflexive
 141 | 
 142 | export
 143 | minNoWeakerRight : {c : _} -> a `NoWeaker` b -> min c a `NoWeaker` min c b
 144 | minNoWeakerRight nw = minNoWeaker reflexive nw
 145 | 
 146 | export
 147 | leftNoWeakerMin : {a, b : _} -> a `NoWeaker` min a b
 148 | leftNoWeakerMin {a=NonEmpty}   = nonEmptyIsStrongest
 149 | leftNoWeakerMin {a=MaybeEmpty} = rewrite minMaybeEmptyLeft b in reflexive
 150 | 
 151 | export
 152 | rightNoWeakerMin : {a, b : _} -> b `NoWeaker` min a b
 153 | rightNoWeakerMin {b=NonEmpty}   = nonEmptyIsStrongest
 154 | rightNoWeakerMin {b=MaybeEmpty} = rewrite minMaybeEmptyRight a in reflexive
 155 | 
 156 | export %hint
 157 | noWeakerReflexive : {em : _} -> em `NoWeaker` em
 158 | noWeakerReflexive = reflexive
 159 |