{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Theory.Lists
(
head, tail, cons, nil
, Head, Tail
, Cons', Nil'
, IsList, IsCons, IsNil
, consIsList, nilIsList, listIsList
, listShapes, consIsCons, headOfCons, tailOfCons
, listInduction
, classify, ListCase (..)
, pattern IsCons, pattern IsNil
, classify', ListCase' (..)
, 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
data IsList xs
data IsCons xs
data IsNil xs
newtype Head xs = Head Defn
type role Head nominal
newtype Tail xs = Tail Defn
type role Tail nominal
data ListCase a xs
= IsCons_ (Proof (IsCons xs)) (a ~~ Head xs) ([a] ~~ Tail xs)
| IsNil_ (Proof (IsNil xs))
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)
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' :: 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_)
head :: Fact (IsCons xs) => ([a] ~~ xs) -> (a ~~ Head xs)
head (The xs) = defn (Prelude.head xs)
tail :: Fact (IsCons xs) => ([a] ~~ xs) -> ([a] ~~ Tail xs)
tail (The xs) = defn (Prelude.tail xs)
cons :: (a ~~ x) -> ([a] ~~ xs) -> ([a] ~~ Cons' x xs)
cons (The x) (The xs) = defn (x:xs)
nil :: ([a] ~~ Nil')
nil = defn []
newtype Cons' x xs = Cons' Defn
type role Cons' nominal nominal
newtype Nil' = Nil' Defn
headOfCons :: Proof (Head (Cons' x xs) == x)
headOfCons = axiom
tailOfCons :: Proof (Tail (Cons' x xs) == xs)
tailOfCons = axiom
consIsCons :: Proof (IsCons (Cons' x xs))
consIsCons = axiom
nilIsNil :: Proof (IsNil Nil')
nilIsNil = axiom
listShapes :: Proof (IsList xs) -> Proof ( (IsNil xs && Not (IsCons xs)) || (IsCons xs && Not (IsNil xs)) )
listShapes _ = axiom
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