module Stdlib.Trait.Ord;

import Stdlib.Data.Fixity open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Trait.Eq open;

type Ordering :=
  | LessThan
  | Equal
  | GreaterThan;

isLessThan (ordering : Ordering) : Bool :=
  case ordering of
    | LessThan := true
    | _ := false;

isEqual (ordering : Ordering) : Bool :=
  case ordering of
    | Equal := true
    | _ := false;

isGreaterThan (ordering : Ordering) : Bool :=
  case ordering of
    | GreaterThan := true
    | _ := false;

instance
orderingEqI : Eq Ordering :=
  mkEq@{
    eq (ordering1 ordering2 : Ordering) : Bool :=
      case ordering2 of
        | LessThan := isLessThan ordering1
        | Equal := isEqual ordering1
        | GreaterThan := isGreaterThan ordering1;
  };

--- A trait for defining a total order
trait
type Ord A := mkOrd@{cmp : A -> A -> Ordering};

syntax operator <= comparison;

--- Returns ;true; iff the first element is less than or equal to the second.
{-# inline: always, isabelle-operator: {name: "\\<le>", prec: 50, assoc: none} #-}
<= {A} {{Ord A}} (x y : A) : Bool :=
  case Ord.cmp x y of
    | Equal := true
    | LessThan := true
    | GreaterThan := false;

syntax operator < comparison;

--- Returns ;true; iff the first element is less than the second.
{-# inline: always, isabelle-operator: {name: "<", prec: 50, assoc: none} #-}
< {A} {{Ord A}} (x y : A) : Bool :=
  case Ord.cmp x y of
    | Equal := false
    | LessThan := true
    | GreaterThan := false;

syntax operator > comparison;

--- Returns ;true; iff the first element is greater than the second.
{-# inline: always, isabelle-operator: {name: ">", prec: 50, assoc: none} #-}
> {A} {{Ord A}} (x y : A) : Bool := y < x;

syntax operator >= comparison;

--- Returns ;true; iff the first element is greater than or equal to the second.
{-# inline: always, isabelle-operator: {name: "\\<ge>", prec: 50, assoc: none} #-}
>= {A} {{Ord A}} (x y : A) : Bool := y <= x;

--- Returns the smaller element.
{-# inline: always #-}
min {A} {{Ord A}} (x y : A) : A :=
  if 
    | x < y := x
    | else := y;

--- Returns the larger element.
{-# inline: always #-}
max {A} {{Ord A}} (x y : A) : A :=
  if 
    | x > y := x
    | else := y;