{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ViewPatterns #-} -- TEMP
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

{-# OPTIONS_GHC -Wall #-}
-- {-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP

-- {-# LANGUAGE DataKinds #-}  -- TEMP
{-# OPTIONS_GHC -Wno-unused-foralls -Wno-redundant-constraints #-} -- TEMP

-- #define ShowTypes

-- | Syntactic CCC

module ConCat.Syntactic where

import Prelude hiding (id,(.),lookup,const)

import Data.Tree (Tree(..))
import Data.Map (Map,fromList,lookup)
import Data.Foldable (toList)
import Text.PrettyPrint.HughesPJClass hiding (render,first)
import Data.Typeable (Typeable)
import Data.Constraint (Dict(..),(:-)(..))  -- temp
import Data.Key (Zip)
import GHC.TypeLits (KnownNat)

import Data.Functor.Rep (Representable(tabulate))
import qualified Data.Functor.Rep as R
import Data.Vector.Sized (Vector)

import qualified ConCat.Category
import ConCat.AltCat
import ConCat.Misc (Unop)
import ConCat.Additive (Additive)
import ConCat.Rep
-- import ConCat.Finite

#ifdef ShowTypes
import ConCat.Misc (typeR)
#else
import ConCat.Misc (Yes1)
#endif

{--------------------------------------------------------------------
    Untyped S-expression
--------------------------------------------------------------------}

type DocTree = Tree PDoc

-- Using PDoc instead of String allows for complex values that can be
-- pretty-printed and parenthesized in context.
prettyTree :: DocTree -> PDoc
prettyTree :: DocTree -> PDoc
prettyTree (Node PDoc
d [DocTree
u,DocTree
v]) Prec
p | Just (Prec
q,(Prec -> Prec
lf,Prec -> Prec
rf)) <- String -> Map String Fixity -> Maybe Fixity
forall k a. Ord k => k -> Map k a -> Maybe a
lookup String
nm Map String Fixity
fixities =
  Bool -> Doc -> Doc
maybeParens (Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
q) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [DocTree -> PDoc
prettyTree DocTree
u (Prec -> Prec
lf Prec
q) Doc -> Doc -> Doc
<+> String -> Doc
text String
nm, (DocTree -> PDoc
prettyTree DocTree
v) (Prec -> Prec
rf Prec
q)]
 where nm :: String
nm = Doc -> String
forall a. Show a => a -> String
show (PDoc
d Prec
0)
prettyTree (Node PDoc
f [DocTree]
es) Prec
p =
  Bool -> Doc -> Doc
maybeParens (Bool -> Bool
not ([DocTree] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DocTree]
es) Bool -> Bool -> Bool
&& Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
appPrec) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
sep (PDoc
f Prec
appPrec Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (DocTree -> Doc) -> [DocTree] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ DocTree
e -> DocTree -> PDoc
prettyTree DocTree
e (Prec
appPrecPrec -> Prec -> Prec
forall a. Num a => a -> a -> a
+Prec
1)) [DocTree]
es)

fixities :: Map String Fixity
fixities :: Map String Fixity
fixities = [(String, Fixity)] -> Map String Fixity
forall k a. Ord k => [(k, a)] -> Map k a
fromList
  [ (String
"."  , (Prec
9,(Prec -> Prec, Prec -> Prec)
assocRight))
  , (String
"&&&", (Prec
3,(Prec -> Prec, Prec -> Prec)
assocRight))
  , (String
"***", (Prec
3,(Prec -> Prec, Prec -> Prec)
assocRight))
  , (String
"|||", (Prec
2,(Prec -> Prec, Prec -> Prec)
assocRight))
  , (String
"+++", (Prec
2,(Prec -> Prec, Prec -> Prec)
assocRight))
  ]

appt :: String -> [DocTree] -> DocTree
appt :: String -> [DocTree] -> DocTree
appt = PDoc -> [DocTree] -> DocTree
forall a. a -> [Tree a] -> Tree a
Node (PDoc -> [DocTree] -> DocTree)
-> (String -> PDoc) -> String -> [DocTree] -> DocTree
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Doc -> PDoc
forall (k :: * -> * -> *) b a. (ConstCat k b, Ok k a) => b -> k a b
const (Doc -> PDoc) -> (String -> Doc) -> String -> PDoc
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. String -> Doc
text
-- appt s ts = Node (const (text s)) ts

{--------------------------------------------------------------------
    Phantom-typed S-expression
--------------------------------------------------------------------}

newtype Syn a b = Syn DocTree

instance Show2 Syn where
  show2 :: forall a b. Syn a b -> String
show2 = Syn a b -> String
forall a. Show a => a -> String
show

#if 1
-- instance Newtype (Syn a b) where
--   type O (Syn a b) = DocTree
--   pack s = Syn s
--   unpack (Syn s) = s

instance HasRep (Syn a b) where
  type Rep (Syn a b) = DocTree
  abst :: Rep (Syn a b) -> Syn a b
abst Rep (Syn a b)
s = DocTree -> Syn a b
forall a b. DocTree -> Syn a b
Syn Rep (Syn a b)
DocTree
s
  repr :: Syn a b -> Rep (Syn a b)
repr (Syn DocTree
s) = Rep (Syn a b)
DocTree
s

atom :: Pretty a => a -> Syn a b
atom :: forall a b. Pretty a => a -> Syn a b
atom a
a = Rep (Syn a b) -> Syn a b
forall a. HasRep a => Rep a -> a
abst (PDoc -> [DocTree] -> DocTree
forall a. a -> [Tree a] -> Tree a
Node (a -> PDoc
forall a. Pretty a => a -> PDoc
ppretty a
a) [])

app0 :: String -> Syn a b
app0 :: forall a b. String -> Syn a b
app0 String
s = Rep (Syn a b) -> Syn a b
forall a. HasRep a => Rep a -> a
abst (String -> [DocTree] -> DocTree
appt String
s [])

app1 :: String -> Syn a b -> Syn c d
app1 :: forall a b c d. String -> Syn a b -> Syn c d
app1 String
s = (Rep (Syn a b) -> Rep (Syn c d)) -> Syn a b -> Syn c d
forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst (\ Rep (Syn a b)
p -> String -> [DocTree] -> DocTree
appt String
s [Rep (Syn a b)
DocTree
p])

app2 :: String -> Syn a b -> Syn c d -> Syn e f
app2 :: forall a b c d e f. String -> Syn a b -> Syn c d -> Syn e f
app2 String
s = (Rep (Syn a b) -> Rep (Syn c d) -> Rep (Syn e f))
-> Syn a b -> Syn c d -> Syn e f
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 (\ Rep (Syn a b)
p Rep (Syn c d)
q -> String -> [DocTree] -> DocTree
appt String
s [Rep (Syn a b)
DocTree
p,Rep (Syn c d)
DocTree
q])

apps :: (Functor h, Foldable h) => String -> h (Syn a b) -> Syn c d
apps :: forall (h :: * -> *) a b c d.
(Functor h, Foldable h) =>
String -> h (Syn a b) -> Syn c d
apps String
s ((Syn a b -> DocTree) -> h (Syn a b) -> h DocTree
forall a b. (a -> b) -> h a -> h b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Syn a b -> Rep (Syn a b)
Syn a b -> DocTree
forall a. HasRep a => a -> Rep a
repr -> h DocTree
ts) = Rep (Syn c d) -> Syn c d
forall a. HasRep a => Rep a -> a
abst (String -> [DocTree] -> DocTree
appt String
s (h DocTree -> [DocTree]
forall a. h a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList h DocTree
ts))

#else

atom :: Pretty a => a -> Syn a b
atom a = Syn (Node (ppretty a) [])

app0 :: String -> Syn a b
app0 s = Syn (appt s [])

app1 :: String -> Syn a b -> Syn c d
app1 s (Syn p) = Syn (appt s [p])

app2 :: String -> Syn a b -> Syn c d -> Syn e f
app2 s (Syn p) (Syn q) = Syn (appt s [p,q])

unSyn :: Syn a b -> DocTree
unSyn (Syn t) = t

apps :: (Functor h, Foldable h) => String -> h (Syn a b) -> Syn c d
apps s (fmap unSyn -> ts) = Syn (appt s (toList ts))

#endif

instance Show (Syn a b) where show :: Syn a b -> String
show = Syn a b -> String
forall a b. Syn a b -> String
render

render :: Syn a b -> String
render :: forall a b. Syn a b -> String
render (Syn DocTree
synu) = Style -> Doc -> String
renderStyle (Mode -> Int -> Float -> Style
Style Mode
PageMode Int
80 Float
1) (DocTree -> PDoc
prettyTree DocTree
synu Prec
0)
{-# NOINLINE render #-}

-- NOINLINE here avoids the empty-case problem that was plaguing me.
-- Perhaps a strictness-based optimization forced my ccc definition.
-- 
-- I think I've fixed the empty-case issue via ConCat.Misc.oops. I still like
-- the NOINLINE for keeping the generated code simple.

-- #define INLINER(nm) {-# INLINE nm #-}
#define INLINER(nm) {-# NOINLINE nm #-}
-- #define INLINER(nm)

instance Category Syn where
  id :: forall a. Ok Syn a => Syn a a
id  = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"id"
  . :: forall b c a. Ok3 Syn a b c => Syn b c -> Syn a b -> Syn a c
(.) = String -> Syn b c -> Syn a b -> Syn a c
forall a b c d e f. String -> Syn a b -> Syn c d -> Syn e f
app2 String
"."
  INLINER(id)
  INLINER((.))

instance AssociativePCat Syn where
  lassocP :: forall a b c.
Ok3 Syn a b c =>
Syn (Prod Syn a (Prod Syn b c)) (Prod Syn (Prod Syn a b) c)
lassocP = String
-> Syn (Prod Syn a (Prod Syn b c)) (Prod Syn (Prod Syn a b) c)
forall a b. String -> Syn a b
app0 String
"lassocP"
  rassocP :: forall a b c.
Ok3 Syn a b c =>
Syn (Prod Syn (Prod Syn a b) c) (Prod Syn a (Prod Syn b c))
rassocP = String
-> Syn (Prod Syn (Prod Syn a b) c) (Prod Syn a (Prod Syn b c))
forall a b. String -> Syn a b
app0 String
"rassocP"
  INLINER(lassocP)
  INLINER(rassocP)

instance MonoidalPCat Syn where
  *** :: forall a b c d.
Ok4 Syn a b c d =>
Syn a c -> Syn b d -> Syn (Prod Syn a b) (Prod Syn c d)
(***)  = String -> Syn a c -> Syn b d -> Syn (Prod Syn a b) (Prod Syn c d)
forall a b c d e f. String -> Syn a b -> Syn c d -> Syn e f
app2 String
"***"
  first :: forall a a' b.
Ok3 Syn a b a' =>
Syn a a' -> Syn (Prod Syn a b) (Prod Syn a' b)
first  = String -> Syn a a' -> Syn (Prod Syn a b) (Prod Syn a' b)
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"first"
  second :: forall a b b'.
Ok3 Syn a b b' =>
Syn b b' -> Syn (Prod Syn a b) (Prod Syn a b')
second = String -> Syn b b' -> Syn (Prod Syn a b) (Prod Syn a b')
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"second"
  INLINER((***))
  INLINER(first)
  INLINER(second)

instance BraidedPCat Syn where
  swapP :: forall a b. Ok2 Syn a b => Syn (Prod Syn a b) (Prod Syn b a)
swapP = String -> Syn (Prod Syn a b) (Prod Syn b a)
forall a b. String -> Syn a b
app0 String
"swapP"
  INLINER(swapP)

instance ProductCat Syn where
  exl :: forall a b. Ok2 Syn a b => Syn (Prod Syn a b) a
exl = String -> Syn (Prod Syn a b) a
forall a b. String -> Syn a b
app0 String
"exl"
  exr :: forall a b. Ok2 Syn a b => Syn (Prod Syn a b) b
exr = String -> Syn (Prod Syn a b) b
forall a b. String -> Syn a b
app0 String
"exr"
  dup :: forall a. Ok Syn a => Syn a (Prod Syn a a)
dup = String -> Syn a (Prod Syn a a)
forall a b. String -> Syn a b
app0 String
"dup"
  INLINER(exl)
  INLINER(exr)
  INLINER(dup)

instance UnitCat Syn where
  lunit :: forall a. Ok Syn a => Syn a (Prod Syn (Unit Syn) a)
lunit   = String -> Syn a (Prod Syn (Unit Syn) a)
forall a b. String -> Syn a b
app0 String
"lunit"
  runit :: forall a. Ok Syn a => Syn a (Prod Syn a (Unit Syn))
runit   = String -> Syn a (Prod Syn a (Unit Syn))
forall a b. String -> Syn a b
app0 String
"runit"
  lcounit :: forall a. Ok Syn a => Syn (Prod Syn (Unit Syn) a) a
lcounit = String -> Syn (Prod Syn (Unit Syn) a) a
forall a b. String -> Syn a b
app0 String
"lcounit"
  rcounit :: forall a. Ok Syn a => Syn (Prod Syn a (Unit Syn)) a
rcounit = String -> Syn (Prod Syn a (Unit Syn)) a
forall a b. String -> Syn a b
app0 String
"rcounit"
  INLINER(lunit)
  INLINER(runit)
  INLINER(lcounit)
  INLINER(rcounit)

instance TerminalCat Syn where
  it :: forall a. Ok Syn a => Syn a (Unit Syn)
it = String -> Syn a (Unit Syn)
forall a b. String -> Syn a b
app0 String
"it"
  INLINER(it)

instance AssociativeSCat Syn where
  lassocS :: forall a b c.
Oks Syn '[a, b, c] =>
Syn (Coprod Syn a (Coprod Syn b c)) (Coprod Syn (Coprod Syn a b) c)
lassocS = String
-> Syn
     (Coprod Syn a (Coprod Syn b c)) (Coprod Syn (Coprod Syn a b) c)
forall a b. String -> Syn a b
app0 String
"lassocS"
  rassocS :: forall a b c.
Oks Syn '[a, b, c] =>
Syn (Coprod Syn (Coprod Syn a b) c) (Coprod Syn a (Coprod Syn b c))
rassocS = String
-> Syn
     (Coprod Syn (Coprod Syn a b) c) (Coprod Syn a (Coprod Syn b c))
forall a b. String -> Syn a b
app0 String
"rassocS"
  INLINER(lassocS)
  INLINER(rassocS)

instance BraidedSCat Syn where
  swapS :: forall a b. Ok2 Syn a b => Syn (Coprod Syn a b) (Coprod Syn b a)
swapS   = String -> Syn (Coprod Syn a b) (Coprod Syn b a)
forall a b. String -> Syn a b
app0 String
"swapS"
  INLINER(swapS)

instance MonoidalSCat Syn where
  +++ :: forall a b c d.
Ok4 Syn a b c d =>
Syn c a -> Syn d b -> Syn (Coprod Syn c d) (Coprod Syn a b)
(+++) = String
-> Syn c a -> Syn d b -> Syn (Coprod Syn c d) (Coprod Syn a b)
forall a b c d e f. String -> Syn a b -> Syn c d -> Syn e f
app2 String
"+++"
  left :: forall a a' b.
Oks Syn '[a, b, a'] =>
Syn a a' -> Syn (Coprod Syn a b) (Coprod Syn a' b)
left    = String -> Syn a a' -> Syn (Coprod Syn a b) (Coprod Syn a' b)
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"left"
  right :: forall a b b'.
Oks Syn '[a, b, b'] =>
Syn b b' -> Syn (Coprod Syn a b) (Coprod Syn a b')
right   = String -> Syn b b' -> Syn (Coprod Syn a b) (Coprod Syn a b')
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"right"
  INLINER((+++))
  INLINER(left)
  INLINER(right)

instance CoproductCat Syn where
  inl :: forall a b. Ok2 Syn a b => Syn a (Coprod Syn a b)
inl = String -> Syn a (Coprod Syn a b)
forall a b. String -> Syn a b
app0 String
"inl"
  inr :: forall a b. Ok2 Syn a b => Syn b (Coprod Syn a b)
inr = String -> Syn b (Coprod Syn a b)
forall a b. String -> Syn a b
app0 String
"inr"
  jam :: forall a. Ok Syn a => Syn (Coprod Syn a a) a
jam = String -> Syn (Coprod Syn a a) a
forall a b. String -> Syn a b
app0 String
"jam"
  INLINER(inl)
  INLINER(inr)

instance CoproductPCat Syn where
  inlP :: forall a b. Ok2 Syn a b => Syn a (CoprodP Syn a b)
inlP   = String -> Syn a (CoprodP Syn a b)
forall a b. String -> Syn a b
app0 String
"inlP"
  inrP :: forall a b. Ok2 Syn a b => Syn b (CoprodP Syn a b)
inrP   = String -> Syn b (CoprodP Syn a b)
forall a b. String -> Syn a b
app0 String
"inrP"
  jamP :: forall a. Ok Syn a => Syn (CoprodP Syn a a) a
jamP   = String -> Syn (CoprodP Syn a a) a
forall a b. String -> Syn a b
app0 String
"jamP"
  INLINER(inlP)
  INLINER(inrP)
  INLINER(jamP)
  
instance DistribCat Syn where
  distl :: forall a u v.
Ok3 Syn a u v =>
Syn
  (Prod Syn a (Coprod Syn u v))
  (Coprod Syn (Prod Syn a u) (Prod Syn a v))
distl = String
-> Syn
     (Prod Syn a (Coprod Syn u v))
     (Coprod Syn (Prod Syn a u) (Prod Syn a v))
forall a b. String -> Syn a b
app0 String
"distl"
  distr :: forall u v b.
Ok3 Syn u v b =>
Syn
  (Prod Syn (Coprod Syn u v) b)
  (Coprod Syn (Prod Syn u b) (Prod Syn v b))
distr = String
-> Syn
     (Prod Syn (Coprod Syn u v) b)
     (Coprod Syn (Prod Syn u b) (Prod Syn v b))
forall a b. String -> Syn a b
app0 String
"distr"
  INLINER(distl)
  INLINER(distr)

instance ClosedCat Syn where
  apply :: forall a b. Ok2 Syn a b => Syn (Prod Syn (Exp Syn a b) a) b
apply   = String -> Syn (Prod Syn (Exp Syn a b) a) b
forall a b. String -> Syn a b
app0 String
"apply"
  curry :: forall a b c.
Ok3 Syn a b c =>
Syn (Prod Syn a b) c -> Syn a (Exp Syn b c)
curry   = String -> Syn (Prod Syn a b) c -> Syn a (Exp Syn b c)
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"curry"
  uncurry :: forall a b c.
Ok3 Syn a b c =>
Syn a (Exp Syn b c) -> Syn (Prod Syn a b) c
uncurry = String -> Syn a (Exp Syn b c) -> Syn (Prod Syn a b) c
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"uncurry"
  INLINER(apply)
  INLINER(curry)
  INLINER(uncurry)

#if 1

atomicConst :: Show b => b -> Syn a b
atomicConst :: forall b a. Show b => b -> Syn a b
atomicConst b
b = String -> Syn Any Any -> Syn a b
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"const" (String -> Syn Any Any
forall a b. String -> Syn a b
app0 (b -> String
forall a. Show a => a -> String
show b
b))

#define LitConst(ty) \
instance ConstCat Syn (ty) where { const = atomicConst ; INLINER(const) }

LitConst(())
LitConst(Bool)
LitConst(Int)
LitConst(Integer)
LitConst(Float)
LitConst(Double)

#if 0
LitConst(Finite n)

instance (ConstCat Syn a, Show a, KnownNat n) => ConstCat Syn (Vector n a) where
  const = atomicConst
  INLINER(const)
#else
instance KnownNat n => ConstCat Syn (Finite n) where
  const :: forall a.
Ok Syn a =>
ConstObj Syn (Finite n) -> Syn a (ConstObj Syn (Finite n))
const = ConstObj Syn (Finite n) -> Syn a (ConstObj Syn (Finite n))
forall b a. Show b => b -> Syn a b
atomicConst
  INLINER(const)

instance (ConstCat Syn a, Show a, KnownNat n) => ConstCat Syn (Vector n a) where
  const :: forall a.
Ok Syn a =>
ConstObj Syn (Vector n a) -> Syn a (ConstObj Syn (Vector n a))
const = ConstObj Syn (Vector n a) -> Syn a (ConstObj Syn (Vector n a))
forall b a. Show b => b -> Syn a b
atomicConst
  INLINER(const)
#endif

-- instance Show a => ConstCat Syn (Vector n a) where ...

-- instance (ConstCat Syn a, ConstCat Syn b) => ConstCat Syn (a :* b) where
--   const = pairConst

#else

instance Pretty b => ConstCat Syn b where
  const b = app1 "const" (atom b)
  INLINER(const)
  -- unitArrow b = app1 "unitArrow" (atom (showPrec appPrec b))
  -- INLINER(unitArrow)

#endif

-- Some or all of the methods below are failing to inline

instance FiniteCat Syn where
  unsafeFinite :: forall (n :: Nat). KnownNat n => Syn Int (Finite n)
unsafeFinite = String -> Syn Int (Finite n)
forall a b. String -> Syn a b
app0 String
"unsafeFinite"
  unFinite :: forall (n :: Nat). KnownNat n => Syn (Finite n) Int
unFinite     = String -> Syn (Finite n) Int
forall a b. String -> Syn a b
app0 String
"unFinite"

instance BoolCat Syn where
  notC :: Syn Bool Bool
notC = String -> Syn Bool Bool
forall a b. String -> Syn a b
app0 String
"notC"
  andC :: Syn (Prod Syn Bool Bool) Bool
andC = String -> Syn (Prod Syn Bool Bool) Bool
forall a b. String -> Syn a b
app0 String
"andC"
  orC :: Syn (Prod Syn Bool Bool) Bool
orC  = String -> Syn (Prod Syn Bool Bool) Bool
forall a b. String -> Syn a b
app0 String
"orC"
  xorC :: Syn (Prod Syn Bool Bool) Bool
xorC = String -> Syn (Prod Syn Bool Bool) Bool
forall a b. String -> Syn a b
app0 String
"xorC"
  INLINER(notC)
  INLINER(andC)
  INLINER(orC)
  INLINER(xorC)

instance EqCat Syn a where
  equal :: Syn (Prod Syn a a) Bool
equal    = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"equal"
  notEqual :: Syn (Prod Syn a a) Bool
notEqual = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"notEqual"
  INLINER(equal)
  INLINER(notEqual)

instance Ord a => OrdCat Syn a where
  lessThan :: Syn (Prod Syn a a) Bool
lessThan = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"lessThan"
  greaterThan :: Syn (Prod Syn a a) Bool
greaterThan = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"greaterThan"
  lessThanOrEqual :: Syn (Prod Syn a a) Bool
lessThanOrEqual = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"lessThanOrEqual"
  greaterThanOrEqual :: Syn (Prod Syn a a) Bool
greaterThanOrEqual = String -> Syn (Prod Syn a a) Bool
forall a b. String -> Syn a b
app0 String
"greaterThanOrEqual"
  INLINER(lessThan)
  INLINER(greaterThan)
  INLINER(lessThanOrEqual)
  INLINER(greaterThanOrEqual)

instance MinMaxCat Syn a where
  minC :: Syn (Prod Syn a a) a
minC = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"minC"
  maxC :: Syn (Prod Syn a a) a
maxC = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"maxC"

instance EnumCat Syn a where
  succC :: Syn a a
succC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"succC"
  predC :: Syn a a
predC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"predC"
  INLINER(succC)
  INLINER(predC)

instance NumCat Syn a where
  negateC :: Syn a a
negateC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"negateC"
  addC :: Syn (Prod Syn a a) a
addC    = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"addC"
  subC :: Syn (Prod Syn a a) a
subC    = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"subC"
  mulC :: Syn (Prod Syn a a) a
mulC    = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"mulC"
  powIC :: Ok Syn Int => Syn (Prod Syn a Int) a
powIC   = String -> Syn (Prod Syn a Int) a
forall a b. String -> Syn a b
app0 String
"powIC"
  INLINER(negateC)
  INLINER(addC)
  INLINER(subC)
  INLINER(mulC)
  INLINER(powIC)

instance IntegralCat Syn a where
  divC :: Syn (Prod Syn a a) a
divC = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"divC"
  modC :: Syn (Prod Syn a a) a
modC = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"modC"
  INLINER(divC)
  INLINER(modC)

instance FractionalCat Syn a where
  recipC :: Syn a a
recipC  = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"recipC"
  divideC :: Syn (Prod Syn a a) a
divideC = String -> Syn (Prod Syn a a) a
forall a b. String -> Syn a b
app0 String
"divideC"
  INLINER(recipC)
  INLINER(divideC)

instance RealFracCat Syn a b where
  floorC :: Syn a b
floorC    = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"floorC"
  ceilingC :: Syn a b
ceilingC  = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"ceilingC"
  truncateC :: Syn a b
truncateC = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"truncateC"
  INLINER(floorC)
  INLINER(ceilingC)
  INLINER(truncateC)

instance FloatingCat Syn a where
  expC :: Syn a a
expC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"expC"
  cosC :: Syn a a
cosC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"cosC"
  sinC :: Syn a a
sinC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"sinC"
  logC :: Syn a a
logC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"logC"
  sqrtC :: Syn a a
sqrtC = String -> Syn a a
forall a b. String -> Syn a b
app0 String
"sqrtC"
  INLINER(expC)
  INLINER(cosC)
  INLINER(sinC)
  INLINER(logC)
  INLINER(sqrtC)

instance FromIntegralCat Syn a b where
  fromIntegralC :: Syn a b
fromIntegralC = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"fromIntegralC"
  INLINER(fromIntegralC)

instance BottomCat Syn a b where
  bottomC :: Syn a b
bottomC = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"bottomC"
  INLINER(bottomC)

#if 1
instance IfCat Syn a where
  ifC :: IfT Syn a
ifC = String -> IfT Syn a
forall a b. String -> Syn a b
app0 String
"ifC"
  INLINER(ifC)
#else

atomicIf :: Syn a b
atomicIf = app0 "ifC"

#define LitIf(ty) \
instance IfCat Syn (ty) where { ifC = atomicIf ; INLINER(ifC) }

-- LitIf(())
LitIf(Bool)
LitIf(Int)
LitIf(Float)
LitIf(Double)

instance IfCat Syn () where ifC = unitIf

instance (IfCat Syn a, IfCat Syn b) => IfCat Syn (a :* b) where
  ifC = prodIf

#define AbstIf(abs) \
instance (IfCat Syn (Rep (abs)), T (abs), T (Rep (abs))) => IfCat Syn (abs) where { ifC = repIf }

AbstIf(Maybe a)
AbstIf((a,b,c))
...

#endif

instance UnknownCat Syn a b where
  unknownC :: Syn a b
unknownC = String -> Syn a b
forall a b. String -> Syn a b
app0 String
"unknownC"
  INLINER(unknownC)

#ifdef ShowTypes
type T a = Typeable a

addTy :: forall t. Typeable t => Unop String
addTy = flip (++) (" :: " ++ show (typeR @t))

#else
type T = Yes1
addTy :: forall t. Unop String
addTy :: forall t. ShowS
addTy = ShowS
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
#endif

app0' :: forall a b. (T a, T b) => String -> Syn a b
app0' :: forall a b. (T a, T b) => String -> Syn a b
app0' = String -> Syn a b
forall a b. String -> Syn a b
app0 (String -> Syn a b) -> ShowS -> String -> Syn a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. forall t. ShowS
addTy @(a -> b)

instance (r ~ Rep a, T a, T r) => RepCat Syn a r where
  reprC :: Syn a r
reprC = String -> Syn a r
forall a b. (T a, T b) => String -> Syn a b
app0' String
"repr"
  abstC :: Syn r a
abstC = String -> Syn r a
forall a b. (T a, T b) => String -> Syn a b
app0' String
"abst"
  INLINER(reprC)
  INLINER(abstC)

instance (Typeable a, Typeable b) => CoerceCat Syn a b where
  coerceC :: Syn a b
coerceC = String -> Syn a b
forall a b. (T a, T b) => String -> Syn a b
app0' String
"coerce"
  INLINER(coerceC)

instance OkIxProd Syn h where okIxProd :: forall a. Ok' Syn a |- Ok' Syn (h a)
okIxProd = (Con (Sat Yes1 a) :- Con (Sat Yes1 (h a)))
-> Sat Yes1 a |- Sat Yes1 (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((Yes1 a => Dict (Yes1 (h a))) -> Yes1 a :- Yes1 (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (Yes1 (h a))
Yes1 a => Dict (Yes1 (h a))
forall (a :: Constraint). a => Dict a
Dict)

instance (Functor h, Foldable h
          {- OkIxProd Syn h, Representable h, Foldable h, Show (R.Rep h) -})
      => IxMonoidalPCat Syn h where
  crossF :: forall a b. Ok2 Syn a b => h (a `Syn` b) -> (h a `Syn` h b)
  crossF :: forall a b. Ok2 Syn a b => h (Syn a b) -> Syn (h a) (h b)
crossF = String -> h (Syn a b) -> Syn (h a) (h b)
forall (h :: * -> *) a b c d.
(Functor h, Foldable h) =>
String -> h (Syn a b) -> Syn c d
apps String
"crossF"

instance (OkIxProd Syn h, Representable h, Foldable h, Show (R.Rep h))
      => IxProductCat Syn h where
  exF :: forall a . Ok Syn a => h (h a `Syn` a)
  exF :: forall a. Ok Syn a => h (Syn (h a) a)
exF = (Rep h -> Syn (h a) a) -> h (Syn (h a) a)
forall a. (Rep h -> a) -> h a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate ((Rep h -> Syn (h a) a) -> h (Syn (h a) a))
-> (Rep h -> Syn (h a) a) -> h (Syn (h a) a)
forall a b. (a -> b) -> a -> b
$ \ Rep h
i -> String -> Syn (h a) a
forall a b. String -> Syn a b
app0 (String
"ex " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Rep h -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Rep h
i String
"")
  replF :: forall a . Ok Syn a => a `Syn` h a
  replF :: forall a. Ok Syn a => Syn a (h a)
replF = String -> Syn a (h a)
forall a b. String -> Syn a b
app0 String
"replF"

instance (OkIxProd Syn h, Representable h, Zip h, Traversable h, Show (R.Rep h))
      => IxCoproductPCat Syn h where
  inPF :: forall a. Ok Syn a => h (a `Syn` h a)
  inPF :: forall a. Ok Syn a => h (Syn a (h a))
inPF = (Rep h -> Syn a (h a)) -> h (Syn a (h a))
forall a. (Rep h -> a) -> h a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate ((Rep h -> Syn a (h a)) -> h (Syn a (h a)))
-> (Rep h -> Syn a (h a)) -> h (Syn a (h a))
forall a b. (a -> b) -> a -> b
$ \ Rep h
i -> String -> Syn a (h a)
forall a b. String -> Syn a b
app0 (String
"inP " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Rep h -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Rep h
i String
"")
  jamPF :: forall a. Ok Syn a => h a `Syn` a
  jamPF :: forall a. Ok Syn a => Syn (h a) a
jamPF = String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"jamPF"
  -- plusPF :: forall a b. Ok2 Syn a b => h (a `Syn` b) -> (h a `Syn` h b)
  -- plusPF = crossF

instance OkFunctor Syn h where okFunctor :: forall a. Ok' Syn a |- Ok' Syn (h a)
okFunctor = (Con (Sat Yes1 a) :- Con (Sat Yes1 (h a)))
-> Sat Yes1 a |- Sat Yes1 (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((Yes1 a => Dict (Yes1 (h a))) -> Yes1 a :- Yes1 (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (Yes1 (h a))
Yes1 a => Dict (Yes1 (h a))
forall (a :: Constraint). a => Dict a
Dict)

instance Functor h => FunctorCat Syn h where
  fmapC :: forall a b. Ok2 Syn a b => Syn a b -> Syn (h a) (h b)
fmapC  = String -> Syn a b -> Syn (h a) (h b)
forall a b c d. String -> Syn a b -> Syn c d
app1 String
"fmap"
  unzipC :: forall a b. Ok2 Syn a b => Syn (h (a :* b)) (h a :* h b)
unzipC = String -> Syn (h (a :* b)) (h a :* h b)
forall a b. String -> Syn a b
app0 String
"unzipC"
  INLINER(fmapC)
  INLINER(unzipC)

instance Zip h => ZipCat Syn h where
  zipC :: forall a b. Ok2 Syn a b => Syn (h a :* h b) (h (a :* b))
zipC = String -> Syn (h a :* h b) (h (a :* b))
forall a b. String -> Syn a b
app0 String
"zipC"
  INLINER(zipC)
  -- zipWithC = app0 "zipWithC"
  -- INLINER(zipWithC)

-- class OkFunctor k h => ZapCat k h where
--   zapC :: Ok2 k a b => h (a `k` b) -> (h a `k` h b)

-- instance ZapCat Syn h where
--   zapC = app0 "zapC"

instance {- Pointed h => -} PointedCat Syn h a where
  pointC :: Syn a (h a)
pointC = String -> Syn a (h a)
forall a b. String -> Syn a b
app0 String
"pointC"
  INLINER(pointC)

instance (Foldable h, Additive a) => AddCat Syn h a where
  sumAC :: Syn (h a) a
sumAC = String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"sumAC"
  INLINER(sumAC)

instance (Foldable h, Ord a) => MinMaxFunctorCat Syn h a where
  minimumC :: Syn (h a) a
minimumC = String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"minimumC"
  INLINER(minimumC)
  maximumC :: Syn (h a) a
maximumC = String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"maximumC"
  INLINER(maximumC)

instance (Foldable h, Ord a) => MinMaxFFunctorCat Syn h a where
  minimumCF :: h a -> a :* Syn (h a) a
minimumCF h a
h = (h a -> a
forall a. Ord a => h a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum h a
h, String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"minimumCF")
  maximumCF :: h a -> a :* Syn (h a) a
maximumCF h a
h = (h a -> a
forall a. Ord a => h a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum h a
h, String -> Syn (h a) a
forall a b. String -> Syn a b
app0 String
"maximumCF")
  
-- instance Functor h => Strong Syn h where
--   strength = app0 "strength"
--   INLINER(strength)

instance DistributiveCat Syn g f where
  distributeC :: forall a. Ok Syn a => Syn (f (g a)) (g (f a))
distributeC = String -> Syn (f (g a)) (g (f a))
forall a b. String -> Syn a b
app0 String
"distributeC"
  INLINER(distributeC)

instance RepresentableCat Syn g where
  indexC :: forall a. Ok Syn a => Syn (g a) (Rep g -> a)
indexC    = String -> Syn (g a) (Rep g -> a)
forall a b. String -> Syn a b
app0 String
"indexC"
  tabulateC :: forall a. Ok Syn a => Syn (Rep g -> a) (g a)
tabulateC = String -> Syn (Rep g -> a) (g a)
forall a b. String -> Syn a b
app0 String
"tabulateC"
  INLINER(indexC)
  INLINER(tabulateC)

{--------------------------------------------------------------------
    Pretty-printing utilities
--------------------------------------------------------------------}

type Prec   = Rational
type Fixity = (Prec,Assoc)
type Assoc = (Prec -> Prec, Prec -> Prec)

assocLeft, assocRight, assocNone :: Assoc
assocLeft :: (Prec -> Prec, Prec -> Prec)
assocLeft  = (Prec -> Prec
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id,Prec -> Prec
forall a. Enum a => a -> a
succ)
assocRight :: (Prec -> Prec, Prec -> Prec)
assocRight = (Prec -> Prec
forall a. Enum a => a -> a
succ,Prec -> Prec
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id)
assocNone :: (Prec -> Prec, Prec -> Prec)
assocNone  = (Prec -> Prec
forall a. Enum a => a -> a
succ,Prec -> Prec
forall a. Enum a => a -> a
succ)

-- Doc in a binding precedence context.
type PDoc = Prec -> Doc

-- Pretty-print with normal PrettyLevel.
-- We could include the PrettyLevel in PDoc instead.
ppretty :: Pretty a => a -> PDoc
ppretty :: forall a. Pretty a => a -> PDoc
ppretty a
a Prec
p = PrettyLevel -> Prec -> a -> Doc
forall a. Pretty a => PrettyLevel -> Prec -> a -> Doc
pPrintPrec PrettyLevel
prettyNormal Prec
p a
a

-- showPDoc :: Rational -> PDoc -> String
-- showPDoc p d = show (d p)

-- Precedence of function application.
-- Hack: use 11 instead of 10 to avoid extraneous parens when a function
-- application is the left argument of a function composition.
appPrec :: Prec
appPrec :: Prec
appPrec = Prec
11 -- was 10
-- Revisit