add Decidable-related stuff

lib/Quox/Decidable.idr

@@ -0,0 +1,37 @@
+module Quox.Decidable
+
+import public Decidable.Decidable
+import public Decidable.Equality
+import public Control.Relation
+
+
+public export
+0 REL : Type -> Type -> Type
+REL a b = a -> b -> Type
+
+
+public export
+0 Pred : Type -> Type
+Pred a = a -> Type
+
+
+public export
+0 Dec1 : Pred a -> Type
+Dec1 p = (x : a) -> Dec (p x)
+
+public export
+0 Dec2 : REL a b -> Type
+Dec2 p = (x : a) -> (y : b) -> Dec (p x y)
+
+
+public export
+(||) : Dec p -> Dec q -> Dec (Either p q)
+Yes y1 || _      = Yes $ Left y1
+No  _  || Yes y2 = Yes $ Right y2
+No  n1 || No  n2 = No  $ \case Left y1 => n1 y1; Right y2 => n2 y2
+
+public export
+(&&) : Dec p -> Dec q -> Dec (p, q)
+Yes y1 && Yes y2 = Yes (y1, y2)
+Yes _  && No  n2 = No $ n2 . snd
+No  n1 && _      = No $ n1 . fst

lib/Quox/Syntax/Qty.idr

@@ -1,6 +1,7 @@
 module Quox.Syntax.Qty
 
 import Quox.Pretty
+import public Quox.Decidable
 import Data.DPair
 
 %default total
@@ -13,8 +14,7 @@ commas [x]     = [x]
 commas (x::xs) = (x <+> hl Delim ",") :: commas xs
 
 export %inline
-prettyQtyBinds : Pretty.HasEnv m => PrettyHL q =>
+prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => List q -> m (Doc HL)
-                 List q -> m (Doc HL)
 prettyQtyBinds =
   map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
 
@@ -26,34 +26,34 @@ interface Eq q => IsQty q where
 
   ||| true if bindings of this quantity will be erased
   ||| and must not be runtime relevant
-  IsZero : q -> Type
+  IsZero : Pred q
-  isZero : (pi : q) -> Dec (IsZero pi)
+  isZero : Dec1 IsZero
   zeroIsZero : IsZero zero
 
   ||| true if bindings of this quantity must be linear
   -- [fixme] is this needed for anything?
-  IsOne : q -> Type
+  IsOne : Pred q
-  isOne : (pi : q) -> Dec (IsOne pi)
+  isOne : Dec1 IsOne
   oneIsOne : IsOne one
 
   ||| ``p `Compat` q`` if it is ok for a binding of
   ||| quantity `q` to be used exactly `p` times.
   ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
-  Compat : q -> q -> Type
+  Compat : Rel q
-  compat : (pi, rh : q) -> Dec (pi `Compat` rh)
+  compat : Dec2 Compat
 
   ||| true if it is ok for this quantity to appear for the
   ||| subject of a typing judgement. this is about the
   ||| subject reduction stuff in atkey
-  IsSubj : q -> Type
+  IsSubj : Pred q
-  isSubj : (pi : q) -> Dec (IsSubj pi)
+  isSubj : Dec1 IsSubj
   zeroIsSubj : IsSubj zero
   oneIsSubj  : IsSubj one
 
   ||| true if it is ok for a global definition to have this
   ||| quantity. so not exact usage counts, maybe.
-  IsGlobal : q -> Type
+  IsGlobal : Pred q
-  isGlobal : (pi : q) -> Dec (IsGlobal pi)
+  isGlobal : Dec1 IsGlobal
   zeroIsGlobal : IsGlobal zero
 
 public export

lib/Quox/Syntax/Qty/Three.idr

@@ -39,12 +39,12 @@ times pi   One  = pi
 times Any  Any  = Any
 
 public export
-data Compat3 : Three -> Three -> Type where
+data Compat3 : Rel Three where
-  CmpRefl : Compat3 pi pi
+  CmpRefl : Compat3 rh rh
-  CmpAny  : Compat3 pi Any
+  CmpAny  : Compat3 rh Any
 
 public export
-compat3 : (pi, rh : Three) -> Dec (pi `Compat3` rh)
+compat3 : Dec2 Compat3
 compat3 pi rh with (decEq pi rh)
   compat3 pi pi | Yes Refl = Yes CmpRefl
   compat3 pi rh | No ne with (decEq rh Any)
@@ -55,23 +55,23 @@ compat3 pi rh with (decEq pi rh)
 
 
 public export
-data IsSubj3 : Three -> Type where
+data IsSubj3 : Pred Three where
   SZero : IsSubj3 Zero
   SOne  : IsSubj3 One
 
 public export
-isSubj3 : (pi : Three) -> Dec (IsSubj3 pi)
+isSubj3 : Dec1 IsSubj3
 isSubj3 Zero = Yes SZero
 isSubj3 One  = Yes SOne
 isSubj3 Any  = No $ \case _ impossible
 
 
 public export
-data IsGlobal3 : Three -> Type where
+data IsGlobal3 : Pred Three where
   GZero : IsGlobal3 Zero
   GAny  : IsGlobal3 Any
 
-isGlobal3 : (pi : Three) -> Dec (IsGlobal3 pi)
+isGlobal3 : Dec1 IsGlobal3
 isGlobal3 Zero = Yes GZero
 isGlobal3 One  = No $ \case _ impossible
 isGlobal3 Any  = Yes GAny

lib/Quox/Syntax/Var.idr

@@ -6,8 +6,9 @@ import Quox.Pretty
 
 import Data.Nat
 import Data.List
-import Decidable.Equality
+import public Quox.Decidable
 import Data.Bool.Decidable
+import Data.DPair
 
 %default total
 
@@ -142,14 +143,14 @@ public export FromVar Var where fromVar = id
 
 
 public export
-data LT : Var n -> Var n -> Type where
+data LT : Rel (Var n) where
   LTZ : VZ `LT` VS i
   LTS : i `LT` j -> VS i `LT` VS j
 %builtin Natural Var.LT
 %name Var.LT lt
 
 public export %inline
-GT : Var n -> Var n -> Type
+GT : Rel (Var n)
 i `GT` j = j `LT` i
 
 export
@@ -161,7 +162,7 @@ export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
 export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
 
 export
-isLT : (i, j : Var n) -> Dec (i `LT` j)
+isLT : Dec2 Var.LT
 isLT VZ     VZ     = No uninhabited
 isLT VZ     (VS j) = Yes LTZ
 isLT (VS i) VZ     = No uninhabited
@@ -202,7 +203,7 @@ comparePSelf i = compareSelf {}
 
 
 public export
-data LTE : Var n -> Var n -> Type where
+data LTE : Rel (Var n) where
   LTEZ : VZ `LTE` j
   LTES : i  `LTE` j -> VS i `LTE` VS j
 

lib/quox-lib.ipkg

@@ -9,6 +9,7 @@ depends = base, contrib, elab-util, sop, snocvect
 
 modules =
   Quox.NatExtra,
+  Quox.Decidable,
   -- Quox.Unicode,
   -- Quox.OPE,
   Quox.Pretty,