{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TemplateHaskell #-}

-- | Internal Syntax.

module Internal where

import Data.Foldable (Foldable)
import Data.Traversable (Traversable)

import Lens

-- | Definition names are strings.

type Id = String

-- | Variables are de Bruijn indices.

newtype Index = Index { Index -> Int
dbIndex :: Int }
  deriving (Index -> Index -> Bool
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
/= :: Index -> Index -> Bool
Eq, Eq Index
Eq Index =>
(Index -> Index -> Ordering)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> Ord Index
Index -> Index -> Bool
Index -> Index -> Ordering
Index -> Index -> Index
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Index -> Index -> Ordering
compare :: Index -> Index -> Ordering
$c< :: Index -> Index -> Bool
< :: Index -> Index -> Bool
$c<= :: Index -> Index -> Bool
<= :: Index -> Index -> Bool
$c> :: Index -> Index -> Bool
> :: Index -> Index -> Bool
$c>= :: Index -> Index -> Bool
>= :: Index -> Index -> Bool
$cmax :: Index -> Index -> Index
max :: Index -> Index -> Index
$cmin :: Index -> Index -> Index
min :: Index -> Index -> Index
Ord, Int -> Index -> ShowS
[Index] -> ShowS
Index -> String
(Int -> Index -> ShowS)
-> (Index -> String) -> ([Index] -> ShowS) -> Show Index
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Index -> ShowS
showsPrec :: Int -> Index -> ShowS
$cshow :: Index -> String
show :: Index -> String
$cshowList :: [Index] -> ShowS
showList :: [Index] -> ShowS
Show, Int -> Index
Index -> Int
Index -> [Index]
Index -> Index
Index -> Index -> [Index]
Index -> Index -> Index -> [Index]
(Index -> Index)
-> (Index -> Index)
-> (Int -> Index)
-> (Index -> Int)
-> (Index -> [Index])
-> (Index -> Index -> [Index])
-> (Index -> Index -> [Index])
-> (Index -> Index -> Index -> [Index])
-> Enum Index
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Index -> Index
succ :: Index -> Index
$cpred :: Index -> Index
pred :: Index -> Index
$ctoEnum :: Int -> Index
toEnum :: Int -> Index
$cfromEnum :: Index -> Int
fromEnum :: Index -> Int
$cenumFrom :: Index -> [Index]
enumFrom :: Index -> [Index]
$cenumFromThen :: Index -> Index -> [Index]
enumFromThen :: Index -> Index -> [Index]
$cenumFromTo :: Index -> Index -> [Index]
enumFromTo :: Index -> Index -> [Index]
$cenumFromThenTo :: Index -> Index -> Index -> [Index]
enumFromThenTo :: Index -> Index -> Index -> [Index]
Enum, Integer -> Index
Index -> Index
Index -> Index -> Index
(Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Integer -> Index)
-> Num Index
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Index -> Index -> Index
+ :: Index -> Index -> Index
$c- :: Index -> Index -> Index
- :: Index -> Index -> Index
$c* :: Index -> Index -> Index
* :: Index -> Index -> Index
$cnegate :: Index -> Index
negate :: Index -> Index
$cabs :: Index -> Index
abs :: Index -> Index
$csignum :: Index -> Index
signum :: Index -> Index
$cfromInteger :: Integer -> Index
fromInteger :: Integer -> Index
Num)

-- | Size expressions.

type Size  = Term
type Level = Size

-- | Terms/types

type Type = Term

data Term
  = -- | Universe with level.
    Type Level
  | -- | Type of sizes (internal use only).
    Size
  | -- | Sized natural number type.
    Nat Size
  | -- | Zero constructor, or zero size (then @Size@ is ignored).
    Zero (Arg Size)
  | -- | Successor constructor, or successor size (then @Size@ is ignored).
    Suc (Arg Size) Term
  | -- | Infinity size.
    Infty
  | -- ^ (Dependent) function type.
    Pi (Dom Type) (Abs Term)
  | -- ^ Lambda abstraction
    Lam ArgInfo (Abs Term)
  | -- ^ Variable.
    Var Index
  | -- ^ Function call.
    Def Id
  | -- ^ Application/eliminiation.
    App Term Elim
  deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Term -> Term -> Ordering
compare :: Term -> Term -> Ordering
$c< :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
>= :: Term -> Term -> Bool
$cmax :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
min :: Term -> Term -> Term
Ord, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Term -> ShowS
showsPrec :: Int -> Term -> ShowS
$cshow :: Term -> String
show :: Term -> String
$cshowList :: [Term] -> ShowS
showList :: [Term] -> ShowS
Show)

-- | Eliminations.

type Elims = [ Elim ]
type Elim  = Elim' Term

data Elim' a
  = -- | Function application.
    Apply (Arg a)
  | -- | Case distinction
    Case
    { forall a. Elim' a -> a
caseReturn :: a -- ^ @T : Nat (b + 1) -> Setω@
    , forall a. Elim' a -> a
caseZero   :: a -- ^ @tz : T zero@
    , forall a. Elim' a -> a
caseTySuc  :: a -- ^ Type of @caseSuc@.  Stored here for convenience, must be
                      --        @(t : Nat b) -> T (suc t)@
    , forall a. Elim' a -> a
caseSuc    :: a -- ^ @ts : (t : Nat b) -> T (suc t)@
    }
  | -- | Recursion
    Fix
    { forall a. Elim' a -> a
fixReturn :: a
      -- ^ @T : ..(i : Size) -> Nat i -> Setω@
    , forall a. Elim' a -> a
fixTyBody :: a
      -- ^ Type of @fixBody@.  Stored here for convenience, must be
      -- @.(i : Size) (f : (x : Nat i) -> T i x) (x : Nat (i + 1)) -> T (i + 1) x@.
    , forall a. Elim' a -> a
fixBody   :: a
      -- ^ @t : .(i : Size) (f : (x : Nat i) -> T i x) (x : Nat (i + 1)) -> T (i + 1) x@
    }
  deriving (Elim' a -> Elim' a -> Bool
(Elim' a -> Elim' a -> Bool)
-> (Elim' a -> Elim' a -> Bool) -> Eq (Elim' a)
forall a. Eq a => Elim' a -> Elim' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Elim' a -> Elim' a -> Bool
== :: Elim' a -> Elim' a -> Bool
$c/= :: forall a. Eq a => Elim' a -> Elim' a -> Bool
/= :: Elim' a -> Elim' a -> Bool
Eq, Eq (Elim' a)
Eq (Elim' a) =>
(Elim' a -> Elim' a -> Ordering)
-> (Elim' a -> Elim' a -> Bool)
-> (Elim' a -> Elim' a -> Bool)
-> (Elim' a -> Elim' a -> Bool)
-> (Elim' a -> Elim' a -> Bool)
-> (Elim' a -> Elim' a -> Elim' a)
-> (Elim' a -> Elim' a -> Elim' a)
-> Ord (Elim' a)
Elim' a -> Elim' a -> Bool
Elim' a -> Elim' a -> Ordering
Elim' a -> Elim' a -> Elim' a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Elim' a)
forall a. Ord a => Elim' a -> Elim' a -> Bool
forall a. Ord a => Elim' a -> Elim' a -> Ordering
forall a. Ord a => Elim' a -> Elim' a -> Elim' a
$ccompare :: forall a. Ord a => Elim' a -> Elim' a -> Ordering
compare :: Elim' a -> Elim' a -> Ordering
$c< :: forall a. Ord a => Elim' a -> Elim' a -> Bool
< :: Elim' a -> Elim' a -> Bool
$c<= :: forall a. Ord a => Elim' a -> Elim' a -> Bool
<= :: Elim' a -> Elim' a -> Bool
$c> :: forall a. Ord a => Elim' a -> Elim' a -> Bool
> :: Elim' a -> Elim' a -> Bool
$c>= :: forall a. Ord a => Elim' a -> Elim' a -> Bool
>= :: Elim' a -> Elim' a -> Bool
$cmax :: forall a. Ord a => Elim' a -> Elim' a -> Elim' a
max :: Elim' a -> Elim' a -> Elim' a
$cmin :: forall a. Ord a => Elim' a -> Elim' a -> Elim' a
min :: Elim' a -> Elim' a -> Elim' a
Ord, Int -> Elim' a -> ShowS
[Elim' a] -> ShowS
Elim' a -> String
(Int -> Elim' a -> ShowS)
-> (Elim' a -> String) -> ([Elim' a] -> ShowS) -> Show (Elim' a)
forall a. Show a => Int -> Elim' a -> ShowS
forall a. Show a => [Elim' a] -> ShowS
forall a. Show a => Elim' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Elim' a -> ShowS
showsPrec :: Int -> Elim' a -> ShowS
$cshow :: forall a. Show a => Elim' a -> String
show :: Elim' a -> String
$cshowList :: forall a. Show a => [Elim' a] -> ShowS
showList :: [Elim' a] -> ShowS
Show, (forall a b. (a -> b) -> Elim' a -> Elim' b)
-> (forall a b. a -> Elim' b -> Elim' a) -> Functor Elim'
forall a b. a -> Elim' b -> Elim' a
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
fmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
$c<$ :: forall a b. a -> Elim' b -> Elim' a
<$ :: forall a b. a -> Elim' b -> Elim' a
Functor, (forall m. Monoid m => Elim' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Elim' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Elim' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Elim' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Elim' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Elim' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Elim' a -> b)
-> (forall a. (a -> a -> a) -> Elim' a -> a)
-> (forall a. (a -> a -> a) -> Elim' a -> a)
-> (forall a. Elim' a -> [a])
-> (forall a. Elim' a -> Bool)
-> (forall a. Elim' a -> Int)
-> (forall a. Eq a => a -> Elim' a -> Bool)
-> (forall a. Ord a => Elim' a -> a)
-> (forall a. Ord a => Elim' a -> a)
-> (forall a. Num a => Elim' a -> a)
-> (forall a. Num a => Elim' a -> a)
-> Foldable Elim'
forall a. Eq a => a -> Elim' a -> Bool
forall a. Num a => Elim' a -> a
forall a. Ord a => Elim' a -> a
forall m. Monoid m => Elim' m -> m
forall a. Elim' a -> Bool
forall a. Elim' a -> Int
forall a. Elim' a -> [a]
forall a. (a -> a -> a) -> Elim' a -> a
forall m a. Monoid m => (a -> m) -> Elim' a -> m
forall b a. (b -> a -> b) -> b -> Elim' a -> b
forall a b. (a -> b -> b) -> b -> Elim' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Elim' m -> m
fold :: forall m. Monoid m => Elim' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
foldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
foldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
$ctoList :: forall a. Elim' a -> [a]
toList :: forall a. Elim' a -> [a]
$cnull :: forall a. Elim' a -> Bool
null :: forall a. Elim' a -> Bool
$clength :: forall a. Elim' a -> Int
length :: forall a. Elim' a -> Int
$celem :: forall a. Eq a => a -> Elim' a -> Bool
elem :: forall a. Eq a => a -> Elim' a -> Bool
$cmaximum :: forall a. Ord a => Elim' a -> a
maximum :: forall a. Ord a => Elim' a -> a
$cminimum :: forall a. Ord a => Elim' a -> a
minimum :: forall a. Ord a => Elim' a -> a
$csum :: forall a. Num a => Elim' a -> a
sum :: forall a. Num a => Elim' a -> a
$cproduct :: forall a. Num a => Elim' a -> a
product :: forall a. Num a => Elim' a -> a
Foldable, Functor Elim'
Foldable Elim'
(Functor Elim', Foldable Elim') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Elim' a -> f (Elim' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Elim' (f a) -> f (Elim' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b))
-> (forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a))
-> Traversable Elim'
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Elim' a -> m (Elim' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Elim' a -> m (Elim' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Elim' a -> m (Elim' b)
$csequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
sequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
Traversable)

-- | Abstraction.

type AbsName = String

data Abs a
  = -- | Actual abstraction (body contains one more index).
    Abs   { forall a. Abs a -> String
absName :: AbsName, forall a. Abs a -> a
absBody :: a }
  | -- | No abstraction (argument will be ignored).
    NoAbs { absName :: AbsName, absBody :: a }
  deriving (Abs a -> Abs a -> Bool
(Abs a -> Abs a -> Bool) -> (Abs a -> Abs a -> Bool) -> Eq (Abs a)
forall a. Eq a => Abs a -> Abs a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Abs a -> Abs a -> Bool
== :: Abs a -> Abs a -> Bool
$c/= :: forall a. Eq a => Abs a -> Abs a -> Bool
/= :: Abs a -> Abs a -> Bool
Eq, Eq (Abs a)
Eq (Abs a) =>
(Abs a -> Abs a -> Ordering)
-> (Abs a -> Abs a -> Bool)
-> (Abs a -> Abs a -> Bool)
-> (Abs a -> Abs a -> Bool)
-> (Abs a -> Abs a -> Bool)
-> (Abs a -> Abs a -> Abs a)
-> (Abs a -> Abs a -> Abs a)
-> Ord (Abs a)
Abs a -> Abs a -> Bool
Abs a -> Abs a -> Ordering
Abs a -> Abs a -> Abs a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Abs a)
forall a. Ord a => Abs a -> Abs a -> Bool
forall a. Ord a => Abs a -> Abs a -> Ordering
forall a. Ord a => Abs a -> Abs a -> Abs a
$ccompare :: forall a. Ord a => Abs a -> Abs a -> Ordering
compare :: Abs a -> Abs a -> Ordering
$c< :: forall a. Ord a => Abs a -> Abs a -> Bool
< :: Abs a -> Abs a -> Bool
$c<= :: forall a. Ord a => Abs a -> Abs a -> Bool
<= :: Abs a -> Abs a -> Bool
$c> :: forall a. Ord a => Abs a -> Abs a -> Bool
> :: Abs a -> Abs a -> Bool
$c>= :: forall a. Ord a => Abs a -> Abs a -> Bool
>= :: Abs a -> Abs a -> Bool
$cmax :: forall a. Ord a => Abs a -> Abs a -> Abs a
max :: Abs a -> Abs a -> Abs a
$cmin :: forall a. Ord a => Abs a -> Abs a -> Abs a
min :: Abs a -> Abs a -> Abs a
Ord, Int -> Abs a -> ShowS
[Abs a] -> ShowS
Abs a -> String
(Int -> Abs a -> ShowS)
-> (Abs a -> String) -> ([Abs a] -> ShowS) -> Show (Abs a)
forall a. Show a => Int -> Abs a -> ShowS
forall a. Show a => [Abs a] -> ShowS
forall a. Show a => Abs a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Abs a -> ShowS
showsPrec :: Int -> Abs a -> ShowS
$cshow :: forall a. Show a => Abs a -> String
show :: Abs a -> String
$cshowList :: forall a. Show a => [Abs a] -> ShowS
showList :: [Abs a] -> ShowS
Show)

-- | Function domain decoration.

data Dom a = Dom { forall a. Dom a -> ArgInfo
_domInfo :: ArgInfo, forall a. Dom a -> a
unDom :: a }
  deriving (Dom a -> Dom a -> Bool
(Dom a -> Dom a -> Bool) -> (Dom a -> Dom a -> Bool) -> Eq (Dom a)
forall a. Eq a => Dom a -> Dom a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Dom a -> Dom a -> Bool
== :: Dom a -> Dom a -> Bool
$c/= :: forall a. Eq a => Dom a -> Dom a -> Bool
/= :: Dom a -> Dom a -> Bool
Eq, Eq (Dom a)
Eq (Dom a) =>
(Dom a -> Dom a -> Ordering)
-> (Dom a -> Dom a -> Bool)
-> (Dom a -> Dom a -> Bool)
-> (Dom a -> Dom a -> Bool)
-> (Dom a -> Dom a -> Bool)
-> (Dom a -> Dom a -> Dom a)
-> (Dom a -> Dom a -> Dom a)
-> Ord (Dom a)
Dom a -> Dom a -> Bool
Dom a -> Dom a -> Ordering
Dom a -> Dom a -> Dom a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Dom a)
forall a. Ord a => Dom a -> Dom a -> Bool
forall a. Ord a => Dom a -> Dom a -> Ordering
forall a. Ord a => Dom a -> Dom a -> Dom a
$ccompare :: forall a. Ord a => Dom a -> Dom a -> Ordering
compare :: Dom a -> Dom a -> Ordering
$c< :: forall a. Ord a => Dom a -> Dom a -> Bool
< :: Dom a -> Dom a -> Bool
$c<= :: forall a. Ord a => Dom a -> Dom a -> Bool
<= :: Dom a -> Dom a -> Bool
$c> :: forall a. Ord a => Dom a -> Dom a -> Bool
> :: Dom a -> Dom a -> Bool
$c>= :: forall a. Ord a => Dom a -> Dom a -> Bool
>= :: Dom a -> Dom a -> Bool
$cmax :: forall a. Ord a => Dom a -> Dom a -> Dom a
max :: Dom a -> Dom a -> Dom a
$cmin :: forall a. Ord a => Dom a -> Dom a -> Dom a
min :: Dom a -> Dom a -> Dom a
Ord, Int -> Dom a -> ShowS
[Dom a] -> ShowS
Dom a -> String
(Int -> Dom a -> ShowS)
-> (Dom a -> String) -> ([Dom a] -> ShowS) -> Show (Dom a)
forall a. Show a => Int -> Dom a -> ShowS
forall a. Show a => [Dom a] -> ShowS
forall a. Show a => Dom a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Dom a -> ShowS
showsPrec :: Int -> Dom a -> ShowS
$cshow :: forall a. Show a => Dom a -> String
show :: Dom a -> String
$cshowList :: forall a. Show a => [Dom a] -> ShowS
showList :: [Dom a] -> ShowS
Show, (forall a b. (a -> b) -> Dom a -> Dom b)
-> (forall a b. a -> Dom b -> Dom a) -> Functor Dom
forall a b. a -> Dom b -> Dom a
forall a b. (a -> b) -> Dom a -> Dom b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Dom a -> Dom b
fmap :: forall a b. (a -> b) -> Dom a -> Dom b
$c<$ :: forall a b. a -> Dom b -> Dom a
<$ :: forall a b. a -> Dom b -> Dom a
Functor, (forall m. Monoid m => Dom m -> m)
-> (forall m a. Monoid m => (a -> m) -> Dom a -> m)
-> (forall m a. Monoid m => (a -> m) -> Dom a -> m)
-> (forall a b. (a -> b -> b) -> b -> Dom a -> b)
-> (forall a b. (a -> b -> b) -> b -> Dom a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dom a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dom a -> b)
-> (forall a. (a -> a -> a) -> Dom a -> a)
-> (forall a. (a -> a -> a) -> Dom a -> a)
-> (forall a. Dom a -> [a])
-> (forall a. Dom a -> Bool)
-> (forall a. Dom a -> Int)
-> (forall a. Eq a => a -> Dom a -> Bool)
-> (forall a. Ord a => Dom a -> a)
-> (forall a. Ord a => Dom a -> a)
-> (forall a. Num a => Dom a -> a)
-> (forall a. Num a => Dom a -> a)
-> Foldable Dom
forall a. Eq a => a -> Dom a -> Bool
forall a. Num a => Dom a -> a
forall a. Ord a => Dom a -> a
forall m. Monoid m => Dom m -> m
forall a. Dom a -> Bool
forall a. Dom a -> Int
forall a. Dom a -> [a]
forall a. (a -> a -> a) -> Dom a -> a
forall m a. Monoid m => (a -> m) -> Dom a -> m
forall b a. (b -> a -> b) -> b -> Dom a -> b
forall a b. (a -> b -> b) -> b -> Dom a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Dom m -> m
fold :: forall m. Monoid m => Dom m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Dom a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Dom a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Dom a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Dom a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Dom a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Dom a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Dom a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Dom a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Dom a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Dom a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Dom a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Dom a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Dom a -> a
foldr1 :: forall a. (a -> a -> a) -> Dom a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Dom a -> a
foldl1 :: forall a. (a -> a -> a) -> Dom a -> a
$ctoList :: forall a. Dom a -> [a]
toList :: forall a. Dom a -> [a]
$cnull :: forall a. Dom a -> Bool
null :: forall a. Dom a -> Bool
$clength :: forall a. Dom a -> Int
length :: forall a. Dom a -> Int
$celem :: forall a. Eq a => a -> Dom a -> Bool
elem :: forall a. Eq a => a -> Dom a -> Bool
$cmaximum :: forall a. Ord a => Dom a -> a
maximum :: forall a. Ord a => Dom a -> a
$cminimum :: forall a. Ord a => Dom a -> a
minimum :: forall a. Ord a => Dom a -> a
$csum :: forall a. Num a => Dom a -> a
sum :: forall a. Num a => Dom a -> a
$cproduct :: forall a. Num a => Dom a -> a
product :: forall a. Num a => Dom a -> a
Foldable, Functor Dom
Foldable Dom
(Functor Dom, Foldable Dom) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Dom a -> f (Dom b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Dom (f a) -> f (Dom a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom a -> m (Dom b))
-> (forall (m :: * -> *) a. Monad m => Dom (m a) -> m (Dom a))
-> Traversable Dom
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Dom (m a) -> m (Dom a)
forall (f :: * -> *) a. Applicative f => Dom (f a) -> f (Dom a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Dom (f a) -> f (Dom a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Dom (f a) -> f (Dom a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
$csequence :: forall (m :: * -> *) a. Monad m => Dom (m a) -> m (Dom a)
sequence :: forall (m :: * -> *) a. Monad m => Dom (m a) -> m (Dom a)
Traversable)

-- | Argument decoration.

data Arg a = Arg { forall a. Arg a -> ArgInfo
argInfo :: ArgInfo, forall a. Arg a -> a
unArg :: a }
  deriving (Eq (Arg a)
Eq (Arg a) =>
(Arg a -> Arg a -> Ordering)
-> (Arg a -> Arg a -> Bool)
-> (Arg a -> Arg a -> Bool)
-> (Arg a -> Arg a -> Bool)
-> (Arg a -> Arg a -> Bool)
-> (Arg a -> Arg a -> Arg a)
-> (Arg a -> Arg a -> Arg a)
-> Ord (Arg a)
Arg a -> Arg a -> Bool
Arg a -> Arg a -> Ordering
Arg a -> Arg a -> Arg a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Arg a)
forall a. Ord a => Arg a -> Arg a -> Bool
forall a. Ord a => Arg a -> Arg a -> Ordering
forall a. Ord a => Arg a -> Arg a -> Arg a
$ccompare :: forall a. Ord a => Arg a -> Arg a -> Ordering
compare :: Arg a -> Arg a -> Ordering
$c< :: forall a. Ord a => Arg a -> Arg a -> Bool
< :: Arg a -> Arg a -> Bool
$c<= :: forall a. Ord a => Arg a -> Arg a -> Bool
<= :: Arg a -> Arg a -> Bool
$c> :: forall a. Ord a => Arg a -> Arg a -> Bool
> :: Arg a -> Arg a -> Bool
$c>= :: forall a. Ord a => Arg a -> Arg a -> Bool
>= :: Arg a -> Arg a -> Bool
$cmax :: forall a. Ord a => Arg a -> Arg a -> Arg a
max :: Arg a -> Arg a -> Arg a
$cmin :: forall a. Ord a => Arg a -> Arg a -> Arg a
min :: Arg a -> Arg a -> Arg a
Ord, Int -> Arg a -> ShowS
[Arg a] -> ShowS
Arg a -> String
(Int -> Arg a -> ShowS)
-> (Arg a -> String) -> ([Arg a] -> ShowS) -> Show (Arg a)
forall a. Show a => Int -> Arg a -> ShowS
forall a. Show a => [Arg a] -> ShowS
forall a. Show a => Arg a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Arg a -> ShowS
showsPrec :: Int -> Arg a -> ShowS
$cshow :: forall a. Show a => Arg a -> String
show :: Arg a -> String
$cshowList :: forall a. Show a => [Arg a] -> ShowS
showList :: [Arg a] -> ShowS
Show, (forall a b. (a -> b) -> Arg a -> Arg b)
-> (forall a b. a -> Arg b -> Arg a) -> Functor Arg
forall a b. a -> Arg b -> Arg a
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Arg a -> Arg b
fmap :: forall a b. (a -> b) -> Arg a -> Arg b
$c<$ :: forall a b. a -> Arg b -> Arg a
<$ :: forall a b. a -> Arg b -> Arg a
Functor, (forall m. Monoid m => Arg m -> m)
-> (forall m a. Monoid m => (a -> m) -> Arg a -> m)
-> (forall m a. Monoid m => (a -> m) -> Arg a -> m)
-> (forall a b. (a -> b -> b) -> b -> Arg a -> b)
-> (forall a b. (a -> b -> b) -> b -> Arg a -> b)
-> (forall b a. (b -> a -> b) -> b -> Arg a -> b)
-> (forall b a. (b -> a -> b) -> b -> Arg a -> b)
-> (forall a. (a -> a -> a) -> Arg a -> a)
-> (forall a. (a -> a -> a) -> Arg a -> a)
-> (forall a. Arg a -> [a])
-> (forall a. Arg a -> Bool)
-> (forall a. Arg a -> Int)
-> (forall a. Eq a => a -> Arg a -> Bool)
-> (forall a. Ord a => Arg a -> a)
-> (forall a. Ord a => Arg a -> a)
-> (forall a. Num a => Arg a -> a)
-> (forall a. Num a => Arg a -> a)
-> Foldable Arg
forall a. Eq a => a -> Arg a -> Bool
forall a. Num a => Arg a -> a
forall a. Ord a => Arg a -> a
forall m. Monoid m => Arg m -> m
forall a. Arg a -> Bool
forall a. Arg a -> Int
forall a. Arg a -> [a]
forall a. (a -> a -> a) -> Arg a -> a
forall m a. Monoid m => (a -> m) -> Arg a -> m
forall b a. (b -> a -> b) -> b -> Arg a -> b
forall a b. (a -> b -> b) -> b -> Arg a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Arg m -> m
fold :: forall m. Monoid m => Arg m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Arg a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Arg a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Arg a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Arg a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Arg a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Arg a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Arg a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Arg a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Arg a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Arg a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Arg a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Arg a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Arg a -> a
foldr1 :: forall a. (a -> a -> a) -> Arg a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Arg a -> a
foldl1 :: forall a. (a -> a -> a) -> Arg a -> a
$ctoList :: forall a. Arg a -> [a]
toList :: forall a. Arg a -> [a]
$cnull :: forall a. Arg a -> Bool
null :: forall a. Arg a -> Bool
$clength :: forall a. Arg a -> Int
length :: forall a. Arg a -> Int
$celem :: forall a. Eq a => a -> Arg a -> Bool
elem :: forall a. Eq a => a -> Arg a -> Bool
$cmaximum :: forall a. Ord a => Arg a -> a
maximum :: forall a. Ord a => Arg a -> a
$cminimum :: forall a. Ord a => Arg a -> a
minimum :: forall a. Ord a => Arg a -> a
$csum :: forall a. Num a => Arg a -> a
sum :: forall a. Num a => Arg a -> a
$cproduct :: forall a. Num a => Arg a -> a
product :: forall a. Num a => Arg a -> a
Foldable, Functor Arg
Foldable Arg
(Functor Arg, Foldable Arg) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Arg a -> f (Arg b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Arg (f a) -> f (Arg a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Arg a -> m (Arg b))
-> (forall (m :: * -> *) a. Monad m => Arg (m a) -> m (Arg a))
-> Traversable Arg
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Arg (m a) -> m (Arg a)
forall (f :: * -> *) a. Applicative f => Arg (f a) -> f (Arg a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Arg a -> m (Arg b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Arg (f a) -> f (Arg a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Arg (f a) -> f (Arg a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Arg a -> m (Arg b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Arg a -> m (Arg b)
$csequence :: forall (m :: * -> *) a. Monad m => Arg (m a) -> m (Arg a)
sequence :: forall (m :: * -> *) a. Monad m => Arg (m a) -> m (Arg a)
Traversable)

instance Eq a => Eq (Arg a) where
   Arg ArgInfo
Irrelevant a
_ == :: Arg a -> Arg a -> Bool
== Arg ArgInfo
Irrelevant a
_ = Bool
True
   Arg ArgInfo
r a
a == Arg ArgInfo
r' a
a' = ArgInfo
r ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
r' Bool -> Bool -> Bool
&& a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a'

type ArgInfo = Relevance

-- | Relevance lattice (order matters)
data Relevance
  = Relevant
  | ShapeIrr
  | Irrelevant
  deriving (ArgInfo -> ArgInfo -> Bool
(ArgInfo -> ArgInfo -> Bool)
-> (ArgInfo -> ArgInfo -> Bool) -> Eq ArgInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ArgInfo -> ArgInfo -> Bool
== :: ArgInfo -> ArgInfo -> Bool
$c/= :: ArgInfo -> ArgInfo -> Bool
/= :: ArgInfo -> ArgInfo -> Bool
Eq, Eq ArgInfo
Eq ArgInfo =>
(ArgInfo -> ArgInfo -> Ordering)
-> (ArgInfo -> ArgInfo -> Bool)
-> (ArgInfo -> ArgInfo -> Bool)
-> (ArgInfo -> ArgInfo -> Bool)
-> (ArgInfo -> ArgInfo -> Bool)
-> (ArgInfo -> ArgInfo -> ArgInfo)
-> (ArgInfo -> ArgInfo -> ArgInfo)
-> Ord ArgInfo
ArgInfo -> ArgInfo -> Bool
ArgInfo -> ArgInfo -> Ordering
ArgInfo -> ArgInfo -> ArgInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ArgInfo -> ArgInfo -> Ordering
compare :: ArgInfo -> ArgInfo -> Ordering
$c< :: ArgInfo -> ArgInfo -> Bool
< :: ArgInfo -> ArgInfo -> Bool
$c<= :: ArgInfo -> ArgInfo -> Bool
<= :: ArgInfo -> ArgInfo -> Bool
$c> :: ArgInfo -> ArgInfo -> Bool
> :: ArgInfo -> ArgInfo -> Bool
$c>= :: ArgInfo -> ArgInfo -> Bool
>= :: ArgInfo -> ArgInfo -> Bool
$cmax :: ArgInfo -> ArgInfo -> ArgInfo
max :: ArgInfo -> ArgInfo -> ArgInfo
$cmin :: ArgInfo -> ArgInfo -> ArgInfo
min :: ArgInfo -> ArgInfo -> ArgInfo
Ord, Int -> ArgInfo -> ShowS
[ArgInfo] -> ShowS
ArgInfo -> String
(Int -> ArgInfo -> ShowS)
-> (ArgInfo -> String) -> ([ArgInfo] -> ShowS) -> Show ArgInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ArgInfo -> ShowS
showsPrec :: Int -> ArgInfo -> ShowS
$cshow :: ArgInfo -> String
show :: ArgInfo -> String
$cshowList :: [ArgInfo] -> ShowS
showList :: [ArgInfo] -> ShowS
Show)

makeLens ''Dom

-- * Smart constructor.

zero :: Size -> Term
zero :: Term -> Term
zero = Arg Term -> Term
Zero (Arg Term -> Term) -> (Term -> Arg Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Irrelevant

suc :: Size -> Term -> Term
suc :: Term -> Term -> Term
suc = Arg Term -> Term -> Term
Suc (Arg Term -> Term -> Term)
-> (Term -> Arg Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Irrelevant

defaultArg :: a -> Arg a
defaultArg :: forall a. a -> Arg a
defaultArg = ArgInfo -> a -> Arg a
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant

defaultDom :: a -> Dom a
defaultDom :: forall a. a -> Dom a
defaultDom = ArgInfo -> a -> Dom a
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant

-- | Zero size.

sZero :: Term
sZero :: Term
sZero = Term -> Term
zero Term
Infty

-- | Successor size.

sSuc  :: Term -> Term
sSuc :: Term -> Term
sSuc  = Term -> Term -> Term
suc Term
Infty

-- | Size increment.

sPlus :: Term -> Integer -> Term
sPlus :: Term -> Integer -> Term
sPlus Term
t Integer
n = (Term -> Term) -> Term -> [Term]
forall a. (a -> a) -> a -> [a]
iterate Term -> Term
sSuc Term
t [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n

-- | @fixKind = ..(i : Size) -> Nat i -> Setω@

fixKind :: Type
fixKind :: Term
fixKind =
  Dom Term -> Abs Term -> Term
Pi (ArgInfo -> Term -> Dom Term
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
ShapeIrr Term
Size) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
    Dom Term -> Abs Term -> Term
Pi (ArgInfo -> Term -> Dom Term
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant (Term -> Term
Nat (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Index -> Term
Var Index
0)) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"x" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
      Term -> Term
Type Term
Infty