content: {-# LANGUAGE FlexibleContexts    #-}
  {-# LANGUAGE GADTs               #-}
  {-# LANGUAGE LambdaCase          #-}
  {-# LANGUAGE PatternSynonyms     #-}
  {-# LANGUAGE RoleAnnotations     #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators       #-}
  {-# LANGUAGE ViewPatterns        #-}
  
  module Theory.Lists
      ( -- * Basic functions on lists
        head, tail, cons, nil
        -- ** Names for parts of a list
      , Head, Tail
        -- ** Names for basic list operations
      , Cons', Nil'
        -- * Reasoning about lists
        -- ** Predicates about list shapes
      , IsList, IsCons, IsNil
        -- ** Axioms about list shapes
      , consIsList, nilIsList, listIsList
      , listShapes, consIsCons, headOfCons, tailOfCons
        -- ** Induction principle
      , listInduction
        -- * Pattern-matching on lists
        -- ** Decompositions that use explicit evidence-passing
      , classify, ListCase (..)
        -- *** Pattern synonyms
      , pattern IsCons, pattern IsNil
        -- ** Decompositions that use implicit evidence-passing
      , classify', ListCase' (..)
        -- *** Pattern synonyms
      , pattern Cons, pattern Nil
      ) where
  
  import           Prelude             hiding (cons, head, reverse, tail)
  import qualified Prelude
  
  import           Data.The
  import           Logic.Implicit
  import           Logic.Proof
  import           Logic.Propositional
  import           Theory.Equality
  import           Theory.Named
  
  -- | Predicates about the possible shapes of lists.
  data IsList xs
  data IsCons xs
  data IsNil  xs
  
  -- | Names for the parts of a list.
  newtype Head xs = Head Defn
  type role Head nominal
  newtype Tail xs = Tail Defn
  type role Tail nominal
  
  -- | Possible shapes of a list, along with evidence that the list
  --   has the given shape.
  data ListCase a xs
    = IsCons_ (Proof (IsCons xs)) (a ~~ Head xs) ([a] ~~ Tail xs)
    | IsNil_  (Proof (IsNil  xs))
  
  -- | Classify a named list by shape, producing evidence that the
  --   list matches the corresponding case.
  classify :: ([a] ~~ xs) -> ListCase a xs
  classify xs = case the xs of
      (h:t) -> IsCons_ axiom (defn h) (defn t)
      []    -> IsNil_  axiom
  
  pattern IsCons :: Proof (IsCons xs) -> (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)
  pattern IsCons proof hd tl <- (classify -> IsCons_ proof hd tl)
  
  pattern IsNil :: Proof (IsNil xs) -> ([a] ~~ xs)
  pattern IsNil proof <- (classify -> IsNil_ proof)
  
  -- | A variation on @ListCase@ that passes the shape facts implicitly. Pattern-matching on a
  --   constructor of @ListCase'@ will bring a shape proof into the implicit context.
  data ListCase' a xs where
      Cons_ :: Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ListCase' a xs
      Nil_  :: Fact (IsNil  xs) => ListCase' a xs
  
  -- | Classify a named list by shape, producing /implicit/ evidence that the
  --   list matches the corresponding case.
  classify' :: forall a xs. ([a] ~~ xs) -> ListCase' a xs
  classify' xs = case the xs of
      (h:t) -> note (axiom :: Proof (IsCons xs)) (Cons_ (defn h) (defn t))
      []    -> note (axiom :: Proof (IsNil  xs))  Nil_
  
  pattern Cons :: () => Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)
  pattern Cons hd tl <- (classify' -> Cons_ hd tl)
  
  pattern Nil :: () => Fact (IsNil xs) => ([a] ~~ xs)
  pattern Nil <- (classify' -> Nil_)
  
  -- | Extract the first element from a non-empty list.
  head :: Fact (IsCons xs) => ([a] ~~ xs) -> (a ~~ Head xs)
  head (The xs) = defn (Prelude.head xs)
  
  -- | Extract all but the first element from a non-empty list.
  tail :: Fact (IsCons xs) => ([a] ~~ xs) -> ([a] ~~ Tail xs)
  tail (The xs) = defn (Prelude.tail xs)
  
  -- | Construct a list from an element and another list.
  cons :: (a ~~ x) -> ([a] ~~ xs) -> ([a] ~~ Cons' x xs)
  cons (The x) (The xs) = defn (x:xs)
  
  -- | The empty list, named @Nil'@.
  nil :: ([a] ~~ Nil')
  nil = defn []
  
  -- | A name for referring to the result of a @cons@ operation.
  newtype Cons' x xs = Cons' Defn
  type role Cons' nominal nominal
  
  -- | A name for referring to the empty list.
  newtype Nil' = Nil' Defn
  
  -- | Axiom: The @head@ of @cons x y@ is @x@.
  headOfCons :: Proof (Head (Cons' x xs) == x)
  headOfCons = axiom
  
  -- | Axiom: The @tail@ of @cons x y@ is @y@.
  tailOfCons :: Proof (Tail (Cons' x xs) == xs)
  tailOfCons = axiom
  
  -- | Axiom: The result of @cons x y@ satisfies @IsCons@.
  consIsCons :: Proof (IsCons (Cons' x xs))
  consIsCons = axiom
  
  -- | Axiom: The empty list satisfies @IsNil@.
  nilIsNil :: Proof (IsNil Nil')
  nilIsNil = axiom
  
  -- | Axiom: a list @xs@ satisfies exactly one of @IsCons xs@ or @IsNil xs@.
  listShapes :: Proof (IsList xs) -> Proof ( (IsNil xs && Not (IsCons xs)) || (IsCons xs && Not (IsNil xs)) )
  listShapes _ = axiom
  
  -- | Induction principle: If a predicate @P@ is true for the empty list, and
  --   @P@ is true for a list whenever it is true for the tail of the list,
  --   then @P@ is true.
  listInduction :: Proof (IsList xs) -> Proof (p Nil') -> Proof (ForAll ys ((IsList ys && p (Tail ys)) --> p ys)) -> Proof (p xs)
  listInduction _ _ _ = axiom
  
  consIsList :: Proof (IsCons xs) -> Proof (IsList xs)
  consIsList _ = axiom
  
  nilIsList :: Proof (IsNil xs) -> Proof (IsList xs)
  nilIsList _ = axiom
  
  listIsList :: ([a] ~~ xs) -> Proof (IsList xs)
  listIsList _ = axiom
  