module Std.List

import Std.Foundation

-- Structural lists (Language Platform PRD §28.2 Collections, LP-802).
--
-- This is the small structural sequence: cheap to build, cheap to walk, and
-- shared rather than copied — appending to a list keeps the original intact
-- because the tail is shared, which is the sharing property §28.4 requires.
-- Iteration is deterministic by construction: a list has one order, the one
-- it was built in.
--
-- Asymptotic contract (§28.4 requires it to be explicit):
--   stdListCons     O(1)
--   stdListHead     O(1)
--   stdListLength   O(n)
--   stdListAppend   O(n) in the left list, sharing the right one
--   stdListReverse  O(n)
--   stdListMap      O(n)
--   stdListFold     O(n)
--   stdListIndex    O(i)
family StdList : Type 0
parameter erased stdListElement : Type 0
constructor StdListEmpty
constructor StdListCons
field unrestricted stdListHeadValue : stdListElement
recursive unrestricted stdListTailValue

end-family

-- The number of elements.
def stdListLength =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (eliminate
        StdList
        (lambda unrestricted current : (family StdList element) . Nat)
        values
        (branch StdListEmpty . zero)
        (branch StdListCons head tail induction . (succ induction)))))

-- The first element, or the supplied default for an empty list.
def stdListHeadOr =
  (lambda erased element : Type 0 .
    (lambda unrestricted fallback : element .
      (lambda unrestricted values : (family StdList element) .
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList element) . element)
          values
          (branch StdListEmpty . fallback)
          (branch StdListCons head tail induction . head)))))

-- The first element as an option, so the empty case is visible in the type.
def stdListHead =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (eliminate
        StdList
        (lambda unrestricted current : (family StdList element) . (family StdOption element))
        values
        (branch StdListEmpty . (constructor StdOption StdNone element))
        (branch StdListCons head tail induction . (constructor StdOption StdSome element head)))))

-- Everything after the first element; the empty list has an empty tail.
def stdListTail =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (eliminate
        StdList
        (lambda unrestricted current : (family StdList element) . (family StdList element))
        values
        (branch StdListEmpty . (constructor StdList StdListEmpty element))
        (branch StdListCons head tail induction . tail))))

-- Is the list empty?
def stdListIsEmpty =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (eliminate
        StdList
        (lambda unrestricted current : (family StdList element) . (family StdBool))
        values
        (branch StdListEmpty . (constructor StdBool StdTrue))
        (branch StdListCons head tail induction . (constructor StdBool StdFalse)))))

-- The left list followed by the right one. The right list is SHARED, not
-- copied: only the left spine is rebuilt.
def stdListAppend =
  (lambda erased element : Type 0 .
    (lambda unrestricted left : (family StdList element) .
      (lambda unrestricted right : (family StdList element) .
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList element) . (family StdList element))
          left
          (branch StdListEmpty . right)
          (branch
            StdListCons
            head
            tail
            induction
            .
            (constructor StdList StdListCons element head induction))))))

-- The list in the opposite order.
def stdListReverse =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (app
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList element) .
            (pi unrestricted accumulator : (family StdList element) . (family StdList element)))
          values
          (branch
            StdListEmpty
            .
            (lambda unrestricted accumulator : (family StdList element) . accumulator))
          (branch
            StdListCons
            head
            tail
            induction
            .
            (lambda unrestricted accumulator : (family StdList element) .
              (induction (constructor StdList StdListCons element head accumulator)))))
        (constructor StdList StdListEmpty element))))

-- Every element transformed, in order.
def stdListMap =
  (lambda erased element : Type 0 .
    (lambda erased target : Type 0 .
      (lambda unrestricted transform : (pi unrestricted value : element . target) .
        (lambda unrestricted values : (family StdList element) .
          (eliminate
            StdList
            (lambda unrestricted current : (family StdList element) . (family StdList target))
            values
            (branch StdListEmpty . (constructor StdList StdListEmpty target))
            (branch
              StdListCons
              head
              tail
              induction
              .
              (constructor StdList StdListCons target (transform head) induction)))))))

-- Fold from the right: `stdListFold f z [a, b] = f a (f b z)`.
def stdListFold =
  (lambda erased element : Type 0 .
    (lambda erased accumulator : Type 0 .
      (lambda unrestricted step : (pi unrestricted value : element . (pi unrestricted carried : accumulator . accumulator)) .
        (lambda unrestricted initial : accumulator .
          (lambda unrestricted values : (family StdList element) .
            (eliminate
              StdList
              (lambda unrestricted current : (family StdList element) . accumulator)
              values
              (branch StdListEmpty . initial)
              (branch StdListCons head tail induction . (step head induction))))))))

-- The first `count` elements (all of them when the list is shorter); the
-- structural recursion is on the count, the list is eliminated one cell at a
-- time under it (Language & Testing Evolution L5: shrinkers halve lists).
def stdListTake =
  (lambda erased element : Type 0 .
    (lambda unrestricted count : Nat .
      (lambda unrestricted values : (family StdList element) .
        (app
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (pi unrestricted remaining : (family StdList element) . (family StdList element)))
            (lambda unrestricted remaining : (family StdList element) .
              (constructor StdList StdListEmpty element))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
                (lambda unrestricted remaining : (family StdList element) .
                  (eliminate
                    StdList
                    (lambda unrestricted current : (family StdList element) .
                      (family StdList element))
                    remaining
                    (branch StdListEmpty . (constructor StdList StdListEmpty element))
                    (branch
                      StdListCons
                      head
                      tail
                      tailInduction
                      .
                      (constructor StdList StdListCons element head (induction tail)))))))
            count)
          values))))

-- Everything after the first `count` elements.
def stdListDrop =
  (lambda erased element : Type 0 .
    (lambda unrestricted count : Nat .
      (lambda unrestricted values : (family StdList element) .
        (app
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (pi unrestricted remaining : (family StdList element) . (family StdList element)))
            (lambda unrestricted remaining : (family StdList element) . remaining)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
                (lambda unrestricted remaining : (family StdList element) .
                  (eliminate
                    StdList
                    (lambda unrestricted current : (family StdList element) .
                      (family StdList element))
                    remaining
                    (branch StdListEmpty . (constructor StdList StdListEmpty element))
                    (branch StdListCons head tail tailInduction . (induction tail))))))
            count)
          values))))

-- The element at a position, as an option: an index past the end is absent,
-- never an error and never a wrong element.
def stdListIndex =
  (lambda erased element : Type 0 .
    (lambda unrestricted values : (family StdList element) .
      (lambda unrestricted position : Nat .
        (app
          (eliminate
            StdList
            (lambda unrestricted current : (family StdList element) .
              (pi unrestricted remaining : Nat . (family StdOption element)))
            values
            (branch
              StdListEmpty
              .
              (lambda unrestricted remaining : Nat . (constructor StdOption StdNone element)))
            (branch
              StdListCons
              head
              tail
              induction
              .
              (lambda unrestricted remaining : Nat .
                (nat-eliminate
                  (lambda unrestricted current : Nat . (family StdOption element))
                  (constructor StdOption StdSome element head)
                  (lambda unrestricted predecessor : Nat .
                    (lambda unrestricted inner : (family StdOption element) .
                      (induction predecessor)))
                  remaining))))
          position))))

-- A list of the naturals below a bound, in increasing order: `[0, 1, ..., n-1]`.
def stdListNaturalsBelow =
  (lambda unrestricted bound : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdList Nat))
      (constructor StdList StdListEmpty Nat)
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdList Nat) .
          (stdListAppend
            Nat
            induction
            (constructor StdList StdListCons Nat predecessor (constructor StdList StdListEmpty Nat)))))
      bound))

-- Structural equality of two lists of naturals: same length, same elements in
-- the same order. The first list is eliminated into a FUNCTION of the second,
-- so the recursion walks both spines together.  A proof about two computed
-- lists states this closed verdict rather than an equation between them: an
-- equation between two lists built by the same builder is compared
-- symbolically first (the builders' element functions, under a binder),
-- which costs far more than computing them (Proof.CheckedHMMATile's instance
-- words: 580 s against 34 s).
def stdListNaturalEqual =
  (lambda unrestricted expected : (family StdList Nat) .
    (lambda unrestricted actual : (family StdList Nat) .
      (app
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList Nat) .
            (pi unrestricted other : (family StdList Nat) . (family StdBool)))
          expected
          (branch
            StdListEmpty
            .
            (lambda unrestricted other : (family StdList Nat) . (stdListIsEmpty Nat other)))
          (branch
            StdListCons
            head
            tail
            induction
            .
            (lambda unrestricted other : (family StdList Nat) .
              (eliminate
                StdList
                (lambda unrestricted current : (family StdList Nat) . (family StdBool))
                other
                (branch StdListEmpty . (constructor StdBool StdFalse))
                (branch
                  StdListCons
                  otherHead
                  otherTail
                  otherInduction
                  .
                  (stdBoolAnd
                    (stdOrderIsEqual (stdOrderCompareNatural head otherHead))
                    (induction otherTail)))))))
        actual)))