{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : OAlg.Entity.Diagram.Proposition
-- Description : propositions on diagrams
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on diagrams on 'Oriented' structures.
module OAlg.Entity.Diagram.Proposition
  (
    -- * Proposition
    prpDiagramOrntSymbol
  , prpCoDiagram

  )
  where

import OAlg.Prelude hiding (T)

import OAlg.Structure.Oriented

import OAlg.Entity.Natural as N hiding ((++))

import OAlg.Entity.Diagram.Definition

--------------------------------------------------------------------------------
-- prpCoDiagram -

-- | the point list is stable under 'coDiagram'.
prpCoDiagram :: Oriented a => Diagram t n m a -> Statement
prpCoDiagram :: forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> Statement
prpCoDiagram Diagram t n m a
d = String -> Label
Prp String
"CoDiagram"
  Label -> Statement -> Statement
:<=>: (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram t n m a
d) forall a. Eq a => a -> a -> Bool
== forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
d) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"d"String -> String -> Parameter
:=forall a. Show a => a -> String
show Diagram t n m a
d]
                  
--------------------------------------------------------------------------------
-- prpDiagramOrntSymbol -

-- | validity of diagrams on 'OAlg.Data.Symbol.Symbol's.
prpDiagramOrntSymbol :: Statement
prpDiagramOrntSymbol :: Statement
prpDiagramOrntSymbol = String -> Label
Prp String
"DiagramOrntSymbol"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeDiagram OS)
xd forall a. Validable a => a -> Statement
valid
            , forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeDiagram OS)
xd (\(SomeDiagram Diagram t n m OS
d) -> forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> Statement
prpCoDiagram Diagram t n m OS
d)
            ] where
  xd :: X (SomeDiagram OS)
  xd :: X (SomeDiagram OS)
xd = forall p.
Entity p =>
X SomeNatural -> X p -> X (SomeDiagram (Orientation p))
xSomeDiagramOrnt X SomeNatural
xn forall x. XStandard x => X x
xStandard

  xn :: X SomeNatural
xn = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 N -> SomeNatural
someNatural forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> N -> X N
xNB N
0 N
20