/*---------------------------------------------------------------------------
  Copyright 2012-2024, Microsoft Research, Daan Leijen.

  This is free software; you can redistribute it and/or modify it under the
  terms of the Apache License, Version 2.0. A copy of the License can be
  found in the LICENSE file at the root of this distribution.
---------------------------------------------------------------------------*/

// Standard `:order` functions.
module std/core/orderstd/core/order

import std/core/typesstd/core/types
import std/core/intstd/core/int

pub fip fun intstd/core/order/int: (x : order) -> int( xx: order : orderstd/core/types/order: V )result: -> total int : intstd/core/types/int: V
  match xx: order
    Ltstd/core/types/Lt: order -> -1literal: int
dec  = -1
hex8 = 0xFF
bit8 = 0b11111111
    Eqstd/core/types/Eq: order -> 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000
    Gtstd/core/types/Gt: order -> 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001

pub fip fun (==)std/core/order/(==): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int ==std/core/int/(==): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

pub fip fun (!=)std/core/order/(!=): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int !=std/core/int/(!=): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

pub fip fun (>=)std/core/order/(>=): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int >=std/core/int/(>=): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

pub fip fun (<=)std/core/order/(<=): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int <=std/core/int/(<=): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

pub fip fun (>)std/core/order/(>): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int >std/core/int/(>): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

pub fip fun (<)std/core/order/(<): (x : order, y : order) -> bool( xx: order : orderstd/core/types/order: V, yy: order : orderstd/core/types/order: V )result: -> total bool : boolstd/core/types/bool: V
  xx: order.intstd/core/order/int: (x : order) -> int <std/core/int/(<): (x : int, y : int) -> bool yy: order.intstd/core/order/int: (x : order) -> int

// Convert an `:order2` to an `:int` (`-1`, `0`, or `1`)
pub fip fun order2/intstd/core/order/order2/int: forall<a> (x : order2<a>) -> int( xx: order2<$37> : order2std/core/types/order2: V -> V<aa: V> )result: -> total int : intstd/core/types/int: V
  match xx: order2<$37>
    Lt2std/core/types/Lt2: forall<a> (lt : a, gt : a) -> order2<a> -> -1literal: int
dec  = -1
hex8 = 0xFF
bit8 = 0b11111111
    Eq2std/core/types/Eq2: forall<a> (eq : a) -> order2<a> -> 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000
    Gt2std/core/types/Gt2: forall<a> (lt : a, gt : a) -> order2<a> -> 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001

// Given a comparison function, we can order 2 elements.
pub fun order2std/core/order/order2: forall<a> (x : a, y : a, @implicit/cmp : (a, a) -> order) -> order2<a>( xx: $183 : aa: V, yy: $183 : aa: V, ^@implicit/cmp?cmp: ($183, $183) -> order : (aa: V,aa: V) -> orderstd/core/types/order: V )result: -> total order2<223> : order2std/core/types/order2: V -> V<aa: V>
  match cmp?cmp: ($183, $183) -> order(xx: $183,yy: $183)
    Eqstd/core/types/Eq: order -> Eq2std/core/types/Eq2: forall<a> (eq : a) -> order2<a>(xx: $183)
    Ltstd/core/types/Lt: order -> Lt2std/core/types/Lt2: forall<a> (lt : a, gt : a) -> order2<a>(xx: $183,yy: $183)
    Gtstd/core/types/Gt: order -> Gt2std/core/types/Gt2: forall<a> (lt : a, gt : a) -> order2<a>(yy: $183,xx: $183)