module Std.Foundation

-- Foundation of the standard library (Language Platform PRD §28.2, LP-800):
-- booleans, ordering, optional values, results, pairs, and equality helpers.
-- Every type here is an ordinary checked family: the trusted core stays small
-- and usability comes from the library (§28.1).
-- A decision. Distinct from Nat so a decision cannot be mistaken for a count.
family StdBool : Type 0
constructor StdTrue
constructor StdFalse

end-family

-- The result of comparing two values.
family StdOrder : Type 0
constructor StdLess
constructor StdEqual
constructor StdGreater

end-family

-- A value that may be absent. The parameter is the value's type, so
-- `StdOption` is one family used at every element type rather than one family
-- per type.
family StdOption : Type 0
parameter erased stdOptionElement : Type 0
constructor StdNone
constructor StdSome
field unrestricted stdSomeValue : stdOptionElement

end-family

-- Either an error or a value. The error type is a parameter too, so a caller
-- chooses how rich its errors are.
family StdResult : Type 0
parameter erased stdResultError : Type 0
parameter erased stdResultValue : Type 0
constructor StdFailure
field unrestricted stdFailureError : stdResultError
constructor StdSuccess
field unrestricted stdSuccessValue : stdResultValue

end-family

-- An ordinary pair. The dependent pair is `sigma` in the core; this is the
-- non-dependent case, which is what most library code wants.
family StdPair : Type 0
parameter erased stdPairLeftType : Type 0
parameter erased stdPairRightType : Type 0
constructor StdPairOf
field unrestricted stdPairLeft : stdPairLeftType
field unrestricted stdPairRight : stdPairRightType

end-family

-- Negation.
def stdBoolNot =
  (lambda unrestricted value : (family StdBool) .
    (eliminate
      StdBool
      (lambda unrestricted current : (family StdBool) . (family StdBool))
      value
      (branch StdTrue . (constructor StdBool StdFalse))
      (branch StdFalse . (constructor StdBool StdTrue))))

-- Conjunction, evaluating both arguments (there is no short-circuiting to
-- observe: the language is total).
def stdBoolAnd =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) .
      (eliminate
        StdBool
        (lambda unrestricted current : (family StdBool) . (family StdBool))
        left
        (branch StdTrue . right)
        (branch StdFalse . (constructor StdBool StdFalse)))))

-- Disjunction.
def stdBoolOr =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) .
      (eliminate
        StdBool
        (lambda unrestricted current : (family StdBool) . (family StdBool))
        left
        (branch StdTrue . (constructor StdBool StdTrue))
        (branch StdFalse . right))))

-- Exclusive disjunction.
def stdBoolExclusiveOr =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) .
      (eliminate
        StdBool
        (lambda unrestricted current : (family StdBool) . (family StdBool))
        left
        (branch StdTrue . (stdBoolNot right))
        (branch StdFalse . right))))

-- The remaining binary Boolean functions. Together with `stdBoolAnd`,
-- `stdBoolExclusiveOr`, and `stdBoolOr`, these name all sixteen possible
-- truth tables over two decisions; callers never need to encode a table as a
-- numeric flag or duplicate the logic in another package.
def stdBoolFalse =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (constructor StdBool StdFalse)))

def stdBoolLeftAndNotRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolAnd left (stdBoolNot right))))

def stdBoolLeft =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . left))

def stdBoolNotLeftAndRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolAnd (stdBoolNot left) right)))

def stdBoolRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . right))

def stdBoolNor =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolOr left right))))

def stdBoolEquivalent =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolExclusiveOr left right))))

def stdBoolNotRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolNot right)))

def stdBoolLeftOrNotRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolOr left (stdBoolNot right))))

def stdBoolNotLeft =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolNot left)))

def stdBoolNotLeftOrRight =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolOr (stdBoolNot left) right)))

def stdBoolNand =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolAnd left right))))

def stdBoolTrue =
  (lambda unrestricted left : (family StdBool) .
    (lambda unrestricted right : (family StdBool) . (constructor StdBool StdTrue)))

-- A decision as a natural: zero is false, one is true. The conversion is
-- explicit, so a count is never treated as a decision by accident.
def stdBoolToNatural =
  (lambda unrestricted value : (family StdBool) .
    (eliminate
      StdBool
      (lambda unrestricted current : (family StdBool) . Nat)
      value
      (branch StdTrue . (succ zero))
      (branch StdFalse . zero)))

-- Zero is false, every other natural is true.
def stdBoolFromNatural =
  (lambda unrestricted value : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdBool))
      (constructor StdBool StdFalse)
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdBool) . (constructor StdBool StdTrue)))
      value))

-- The opposite comparison: what `stdOrderCompare y x` would say.
def stdOrderReverse =
  (lambda unrestricted value : (family StdOrder) .
    (eliminate
      StdOrder
      (lambda unrestricted current : (family StdOrder) . (family StdOrder))
      value
      (branch StdLess . (constructor StdOrder StdGreater))
      (branch StdEqual . (constructor StdOrder StdEqual))
      (branch StdGreater . (constructor StdOrder StdLess))))

-- Is this comparison equality?
def stdOrderIsEqual =
  (lambda unrestricted value : (family StdOrder) .
    (eliminate
      StdOrder
      (lambda unrestricted current : (family StdOrder) . (family StdBool))
      value
      (branch StdLess . (constructor StdBool StdFalse))
      (branch StdEqual . (constructor StdBool StdTrue))
      (branch StdGreater . (constructor StdBool StdFalse))))

-- Is the left value the smaller one?
def stdOrderIsLess =
  (lambda unrestricted value : (family StdOrder) .
    (eliminate
      StdOrder
      (lambda unrestricted current : (family StdOrder) . (family StdBool))
      value
      (branch StdLess . (constructor StdBool StdTrue))
      (branch StdEqual . (constructor StdBool StdFalse))
      (branch StdGreater . (constructor StdBool StdFalse))))

-- Compare two naturals, answering with an order rather than a flag.
def stdOrderCompareNatural =
  (lambda unrestricted left : Nat .
    (lambda unrestricted right : Nat .
      (eliminate
        StdBool
        (lambda unrestricted current : (family StdBool) . (family StdOrder))
        (stdBoolFromNatural (nat-less-than left right))
        (branch StdTrue . (constructor StdOrder StdLess))
        (branch
          StdFalse
          .
          (eliminate
            StdBool
            (lambda unrestricted current : (family StdBool) . (family StdOrder))
            (stdBoolFromNatural (nat-less-than right left))
            (branch StdTrue . (constructor StdOrder StdGreater))
            (branch StdFalse . (constructor StdOrder StdEqual)))))))

-- The value an option holds, or the supplied default. The element type is
-- explicit, because the library never guesses a type.
def stdOptionValueOr =
  (lambda erased element : Type 0 .
    (lambda unrestricted fallback : element .
      (lambda unrestricted value : (family StdOption element) .
        (eliminate
          StdOption
          (lambda unrestricted current : (family StdOption element) . element)
          value
          (branch StdNone . fallback)
          (branch StdSome held . held)))))

-- Does this option hold a value?
def stdOptionIsSome =
  (lambda erased element : Type 0 .
    (lambda unrestricted value : (family StdOption element) .
      (eliminate
        StdOption
        (lambda unrestricted current : (family StdOption element) . (family StdBool))
        value
        (branch StdNone . (constructor StdBool StdFalse))
        (branch StdSome held . (constructor StdBool StdTrue)))))

-- The value a result holds, or the supplied default.
def stdResultValueOr =
  (lambda erased errorType : Type 0 .
    (lambda erased valueType : Type 0 .
      (lambda unrestricted fallback : valueType .
        (lambda unrestricted value : (family StdResult errorType valueType) .
          (eliminate
            StdResult
            (lambda unrestricted current : (family StdResult errorType valueType) . valueType)
            value
            (branch StdFailure held . fallback)
            (branch StdSuccess held . held))))))

-- Did this result succeed?
def stdResultIsSuccess =
  (lambda erased errorType : Type 0 .
    (lambda erased valueType : Type 0 .
      (lambda unrestricted value : (family StdResult errorType valueType) .
        (eliminate
          StdResult
          (lambda unrestricted current : (family StdResult errorType valueType) . (family StdBool))
          value
          (branch StdFailure held . (constructor StdBool StdFalse))
          (branch StdSuccess held . (constructor StdBool StdTrue))))))

-- Compose checked operations without replacing an earlier error with a later
-- default. The continuation receives a value only in the success branch.
def stdResultBind =
  (lambda erased errorType : Type 0 .
    (lambda erased inputType : Type 0 .
      (lambda erased outputType : Type 0 .
        (lambda unrestricted input : (family StdResult errorType inputType) .
          (lambda unrestricted next : (pi unrestricted value : inputType . (family StdResult errorType outputType)) .
            (eliminate StdResult
              (lambda unrestricted current : (family StdResult errorType inputType) . (family StdResult errorType outputType)) input
              (branch StdFailure error . (constructor StdResult StdFailure errorType outputType error))
              (branch StdSuccess value . (next value))))))))

-- A result as an option, dropping the error.
def stdResultToOption =
  (lambda erased errorType : Type 0 .
    (lambda erased valueType : Type 0 .
      (lambda unrestricted value : (family StdResult errorType valueType) .
        (eliminate
          StdResult
          (lambda unrestricted current : (family StdResult errorType valueType) .
            (family StdOption valueType))
          value
          (branch StdFailure held . (constructor StdOption StdNone valueType))
          (branch StdSuccess held . (constructor StdOption StdSome valueType held))))))

-- The left component of a pair.
def stdPairLeftOf =
  (lambda erased leftType : Type 0 .
    (lambda erased rightType : Type 0 .
      (lambda unrestricted value : (family StdPair leftType rightType) .
        (eliminate
          StdPair
          (lambda unrestricted current : (family StdPair leftType rightType) . leftType)
          value
          (branch StdPairOf left right . left)))))

-- The right component of a pair.
def stdPairRightOf =
  (lambda erased leftType : Type 0 .
    (lambda erased rightType : Type 0 .
      (lambda unrestricted value : (family StdPair leftType rightType) .
        (eliminate
          StdPair
          (lambda unrestricted current : (family StdPair leftType rightType) . rightType)
          value
          (branch StdPairOf left right . right)))))

-- Equality is reflexive by construction: this is the proof that a value
-- equals itself, named so library code can pass it around.
def stdEqualReflexive =
  (lambda erased element : Type 0 . (lambda unrestricted value : element . (refl element value)))