{-# 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

    prpDiagram, prpDiagramOrntSymbol
  )
  where

import OAlg.Prelude hiding (T)

import OAlg.Structure.Oriented

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

import OAlg.Entity.Diagram.Definition

--------------------------------------------------------------------------------

-- prpDiagramOrntSymbol -


-- | validity of diagrams on 'OAlg.Data.Symbol.Symbol's.

prpDiagramOrntSymbol :: Statement
prpDiagramOrntSymbol :: Statement
prpDiagramOrntSymbol = String -> Label
Prp String
"DiagramOrntSymbol"
  Label -> Statement -> Statement
:<=>: X (SomeDiagram OS) -> (SomeDiagram OS -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeDiagram OS)
xd SomeDiagram OS -> Statement
forall a. Validable a => a -> Statement
valid where
    xd :: X (SomeDiagram OS)
    xd :: X (SomeDiagram OS)
xd = X SomeNatural -> X Symbol -> X (SomeDiagram OS)
forall p.
Entity p =>
X SomeNatural -> X p -> X (SomeDiagram (Orientation p))
xSomeDiagramOrnt X SomeNatural
xn X Symbol
forall x. XStandard x => X x
xStandard

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

--------------------------------------------------------------------------------

-- prpDiagram -


-- | validity for same statements of diagrams.

prpDiagram :: Statement
prpDiagram :: Statement
prpDiagram = String -> Label
Prp String
"Diagram" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ Statement
prpDiagramOrntSymbol
      -- , prpDiagrammatic 10

      ]