order.egi

--
--
-- Order
--
--

inductive Ordering := | Less | Equal | Greater

inductive pattern Ordering :=
    | less
    | equal
    | greater

def ordering : Matcher Ordering :=
  algebraicDataMatcher
    | less
    | equal
    | greater

def min {Ord a} (x: a) (y: a) : a := if x < y then x else y
def max {Ord a} (x: a) (y: a) : a := if x > y then x else y

class Ord a extends Eq a where
  compare (x: a) (y: a) : Ordering
  (<) (x: a) (y: a) : Bool
  (<=) (x: a) (y: a) : Bool
  (>) (x: a) (y: a) : Bool
  (>=) (x: a) (y: a) : Bool
  min (x: a) (y: a) : a
  max (x: a) (y: a) : a

-- | Ord instances for basic types
instance Ord Integer where
  compare x y := if i.< x y then Less else if i.> x y then Greater else Equal
  (<) x y := i.< x y
  (<=) x y := i.<= x y
  (>) x y := i.> x y
  (>=) x y := i.>= x y
  min x y := if i.< x y then x else y
  max x y := if i.> x y then x else y

instance Ord Float where
  compare x y := if f.< x y then Less else if f.> x y then Greater else Equal
  (<) x y := f.< x y
  (<=) x y := f.<= x y
  (>) x y := f.> x y
  (>=) x y := f.>= x y
  min x y := if f.< x y then x else y
  max x y := if f.> x y then x else y

instance Ord Char where
  compare x y := if i.< (ctoi x) (ctoi y) then Less else if i.> (ctoi x) (ctoi y) then Greater else Equal
  (<) x y := i.< (ctoi x) (ctoi y)
  (<=) x y := i.<= (ctoi x) (ctoi y)
  (>) x y := i.> (ctoi x) (ctoi y)
  (>=) x y := i.>= (ctoi x) (ctoi y)
  min x y := if i.< (ctoi x) (ctoi y) then x else y
  max x y := if i.> (ctoi x) (ctoi y) then x else y

instance Ord String where
  compare s1 s2 := compare (unpack s1) (unpack s2)
  (<) s1 s2 :=
    match compare s1 s2 as ordering with
      | less -> True
      | _ -> False
  (<=) s1 s2 :=
    match compare s1 s2 as ordering with
      | greater -> False
      | _ -> True
  (>) s1 s2 :=
    match compare s1 s2 as ordering with
      | greater -> True
      | _ -> False
  (>=) s1 s2 :=
    match compare s1 s2 as ordering with
      | less -> False
      | _ -> True
  min s1 s2 :=
    match compare s1 s2 as ordering with
      | less -> s1
      | _ -> s2
  max s1 s2 :=
    match compare s1 s2 as ordering with
      | greater -> s1
      | _ -> s2