{- In the context of polarities, we use "recursive" in the sense of
"computable" rather than syntactic recursion. -}

module Polarity where

import Util
import Warshall

import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.List as List

{- 2010-10-09 Fusing polarity and irrelevance

     .      constant (= irrelevant) function
    / \
  ++   |    strictly positive function (types only)
   |   |
   +   -    positive/negative function (types only)
    \ /
     ^      parametric function (lambda cube), default for types
     |
     *      recursive function (pattern matching), default for terms


 Composition (AC)

  . p = .
  * p = *  (p not .)
  ^ p = ^  (p not .,*)
 ++ p = p
  + p = p  (p not ++)
  - - = +

Equality/subtyping <=p

  x <=. y  iff  true
  x <=- y  iff  x >= y
  x <=^ y  iff  x == y
  x <=* y  iff  x == y
 -}

-- polarities and strict positivity ----------------------------------

class Polarity pol where
  erased    :: pol -> Bool
  compose   :: pol -> pol -> pol
  neutral   :: pol                 -- ^ neutral for compose.
  promote   :: pol -> pol
  demote    :: pol -> pol
  hidden    :: pol                 -- ^ corresponding to hidden quantification

type PVarId = Int

data Pol
  = Const -- non-occurring, irrelevant
  | SPos  -- strictly positive
  | Pos   -- positive
  | Neg   -- negative, used internally for contravariance of sized codata
  | Param -- parametric (lambda) function
  | Rec   -- recursive (takes decision)
  | Default     -- no polarity given (for parsing)
  | PVar PVarId -- flexible polarity variable
         deriving (Pol -> Pol -> Bool
(Pol -> Pol -> Bool) -> (Pol -> Pol -> Bool) -> Eq Pol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pol -> Pol -> Bool
== :: Pol -> Pol -> Bool
$c/= :: Pol -> Pol -> Bool
/= :: Pol -> Pol -> Bool
Eq,Eq Pol
Eq Pol =>
(Pol -> Pol -> Ordering)
-> (Pol -> Pol -> Bool)
-> (Pol -> Pol -> Bool)
-> (Pol -> Pol -> Bool)
-> (Pol -> Pol -> Bool)
-> (Pol -> Pol -> Pol)
-> (Pol -> Pol -> Pol)
-> Ord Pol
Pol -> Pol -> Bool
Pol -> Pol -> Ordering
Pol -> Pol -> Pol
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 :: Pol -> Pol -> Ordering
compare :: Pol -> Pol -> Ordering
$c< :: Pol -> Pol -> Bool
< :: Pol -> Pol -> Bool
$c<= :: Pol -> Pol -> Bool
<= :: Pol -> Pol -> Bool
$c> :: Pol -> Pol -> Bool
> :: Pol -> Pol -> Bool
$c>= :: Pol -> Pol -> Bool
>= :: Pol -> Pol -> Bool
$cmax :: Pol -> Pol -> Pol
max :: Pol -> Pol -> Pol
$cmin :: Pol -> Pol -> Pol
min :: Pol -> Pol -> Pol
Ord)

mixed, defaultPol :: Pol
mixed :: Pol
mixed = Pol
Rec
defaultPol :: Pol
defaultPol = Pol
Rec
{-
mixed = Param -- TODO: Rec
defaultPol = Param -- TODO: Rec
-}
instance Polarity Pol where
  erased :: Pol -> Bool
erased  = Pol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
(==) Pol
Const
  compose :: Pol -> Pol -> Pol
compose = Pol -> Pol -> Pol
polComp
  neutral :: Pol
neutral = Pol
SPos
  promote :: Pol -> Pol
promote = Pol -> Pol -> Pol
invComp Pol
Const
  demote :: Pol -> Pol
demote  = Pol -> Pol -> Pol
invComp Pol
Rec
  hidden :: Pol
hidden  = Pol
Const

instance Show Pol where
  show :: Pol -> String
show Pol
Const = String
"."
  show Pol
SPos  = String
"++"
  show Pol
Pos   = String
"+"
  show Pol
Neg   = String
"-"
  show Pol
Param = String
"^"
  show Pol
Rec   = String
"*"
  show Pol
Default = String
"{default polarity}"
  show (PVar PVarId
i) = PVarId -> String
forall a. Show a => a -> String
showPVar PVarId
i

showPVar :: Show a => a -> String
showPVar :: forall a. Show a => a -> String
showPVar a
i = String
"?p" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

isPVar :: Pol -> Bool
isPVar :: Pol -> Bool
isPVar (PVar{}) = Bool
True
isPVar Pol
_ = Bool
False

-- information ordering
leqPol :: Pol -> Pol -> Bool
leqPol :: Pol -> Pol -> Bool
leqPol Pol
_ Pol
Const  = Bool
True   -- Const is top
leqPol Pol
Const Pol
_  = Bool
False
leqPol Pol
Rec Pol
_    = Bool
True   -- Rec is bottom
leqPol Pol
_ Pol
Rec    = Bool
False
leqPol Pol
Param Pol
_  = Bool
True   -- Param is second bottom
leqPol Pol
_ Pol
Param  = Bool
False
leqPol Pol
Pos Pol
SPos = Bool
True
leqPol Pol
x   Pol
y    = Pol
x Pol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
== Pol
y

{- RETIRED
isSPos :: Pol -> Bool
isSPos SPos = True
isSPos Const = True
isSPos _ = False
-}

{- NOT USED
isPos :: Pol -> Bool
isPos Pos = True
isPos x = isSPos x
-}

-- polarity negation
-- used in Eval.hs leqVals' for switching sides
-- this means it is only applied to Pos, Neg, Param,
-- never to SPos, Const, or polarity expressions
polNeg :: Pol -> Pol
polNeg :: Pol -> Pol
polNeg Pol
Const  = Pol
Const
polNeg Pol
SPos  = Pol
Neg
polNeg Pol
Pos   = Pol
Neg
polNeg Pol
Neg   = Pol
Pos
polNeg Pol
Param = Pol
Param
polNeg Pol
Rec   = Pol
Rec
polNeg Pol
_ = Pol
forall a. HasCallStack => a
undefined

-- polarity composition
-- used in Eval.hs leqVals'
polComp :: Pol -> Pol -> Pol
polComp :: Pol -> Pol -> Pol
polComp Pol
Const  Pol
_  = Pol
Const   -- most dominant
polComp Pol
_ Pol
Const   = Pol
Const
polComp Pol
Rec Pol
_     = Pol
Rec  -- dominant except for Const
polComp Pol
_ Pol
Rec     = Pol
Rec
polComp Pol
Param Pol
_   = Pol
Param  -- dominant except for Const, Rec
polComp Pol
_ Pol
Param   = Pol
Param
polComp Pol
SPos  Pol
x   = Pol
x      -- neutral
polComp Pol
x Pol
SPos    = Pol
x
polComp Pol
Pos  Pol
x    = Pol
x      -- neutral except for SPos
polComp Pol
x Pol
Pos     = Pol
x
polComp Pol
Neg Pol
Neg   = Pol
Pos    -- order 2
polComp Pol
_ Pol
_ = Pol
forall a. HasCallStack => a
undefined
{- pol.comp. is ass., comm., with neutral ++, and infinity Const
   cancellation does not hold, since composition with anything by ++ is
   information loss:
     q p <= q p' ==> p <= p'
   only if q = ++ (then it is trivial anyway) -}

-- polarity inverse composition (see Abel, MSCS 2008)
-- invComp p q1 <= q2  <==> q1 <= polComp p q2
-- used in TCM.hs cxtApplyDec
invComp :: Pol -> Pol -> Pol
invComp :: Pol -> Pol -> Pol
invComp Pol
Rec   Pol
Rec   = Pol
Rec       -- in rec. arg. keep only rec. vars
invComp Pol
Rec   Pol
_     = Pol
Const     -- all others are declared unusable
invComp Pol
Param Pol
Param = Pol
Param     -- in parametric mixed arg, keep only mixed vars
invComp Pol
Param Pol
_     = Pol
Const
invComp Pol
Const Pol
_     = Pol
Param     -- a constant function can take any argument
invComp Pol
SPos  Pol
x     = Pol
x         -- SPos is the identity
invComp Pol
_     Pol
SPos  = Pol
Const     -- SPos preserved only under SPos
invComp Pol
Pos   Pol
x     = Pol
x         -- x not SPos
invComp Pol
Neg   Pol
x     = Pol -> Pol
polNeg Pol
x  -- x not SPos
invComp Pol
_ Pol
_ = Pol
forall a. HasCallStack => a
undefined

{- UNUSED
invCompExpr :: Pol -> PExpr -> PExpr
invCompExpr q (PValue p)   = PValue $ invComp q p
invCompExpr q (PExpr q' i) = PExpr (polComp q q') i
-}

-- polarity conjuction (infimum)
-- used in comparing spines
polAnd :: Pol -> Pol -> Pol
polAnd :: Pol -> Pol -> Pol
polAnd Pol
Const Pol
x = Pol
x      -- most information
polAnd Pol
x Pol
Const = Pol
x
polAnd Pol
Rec   Pol
_ = Pol
Rec   -- least information
polAnd Pol
_   Pol
Rec = Pol
Rec
{-
polAnd Param x  = Param   -- 2nd least information
polAnd x Param  = Param
-}
polAnd Pol
x Pol
y | Pol
x Pol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
== Pol
y = Pol
x       -- same information
polAnd Pol
SPos Pol
Pos = Pol
Pos     -- SPos is more informative than Pos
polAnd Pol
Pos Pol
SPos = Pol
Pos
{-
polAnd SPos Neg = Param
polAnd Neg SPos = Param
-}
polAnd Pol
_ Pol
_      = Pol
Param     -- remaining cases: conflicting info or Param

instance SemiRing Pol where
  oplus :: Pol -> Pol -> Pol
oplus  = Pol -> Pol -> Pol
polAnd
  otimes :: Pol -> Pol -> Pol
otimes = Pol -> Pol -> Pol
polComp
  ozero :: Pol
ozero  = Pol
Const    -- dominant for composition, neutral for infimum
  oone :: Pol
oone   = Pol
SPos     -- neutral  for composition

-- computing a relation from <=
relPol :: Pol -> (a -> a -> Bool) -> (a -> a -> Bool)
relPol :: forall a. Pol -> (a -> a -> Bool) -> a -> a -> Bool
relPol Pol
Const a -> a -> Bool
_ a
_ a
_ = Bool
True
relPol Pol
Rec   a -> a -> Bool
r a
a a
b = a -> a -> Bool
r a
a a
b Bool -> Bool -> Bool
&& a -> a -> Bool
r a
b a
a
relPol Pol
Param a -> a -> Bool
r a
a a
b = a -> a -> Bool
r a
a a
b Bool -> Bool -> Bool
&& a -> a -> Bool
r a
b a
a
relPol Pol
Neg   a -> a -> Bool
r a
a a
b = a -> a -> Bool
r a
b a
a
relPol Pol
Pos   a -> a -> Bool
r a
a a
b = a -> a -> Bool
r a
a a
b
relPol Pol
SPos  a -> a -> Bool
r a
a a
b = a -> a -> Bool
r a
a a
b
relPol Pol
_ a -> a -> Bool
_ a
_ a
_ = Bool
forall a. HasCallStack => a
undefined

relPolM :: (Monad m) => Pol -> (a -> a -> m ()) -> (a -> a -> m ())
relPolM :: forall (m :: * -> *) a.
Monad m =>
Pol -> (a -> a -> m ()) -> a -> a -> m ()
relPolM Pol
Const a -> a -> m ()
_ a
_ a
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
relPolM Pol
Rec   a -> a -> m ()
r a
a a
b = a -> a -> m ()
r a
a a
b m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> a -> m ()
r a
b a
a
relPolM Pol
Param a -> a -> m ()
r a
a a
b = a -> a -> m ()
r a
a a
b m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> a -> m ()
r a
b a
a
relPolM Pol
Neg   a -> a -> m ()
r a
a a
b = a -> a -> m ()
r a
b a
a
relPolM Pol
Pos   a -> a -> m ()
r a
a a
b = a -> a -> m ()
r a
a a
b
relPolM Pol
SPos  a -> a -> m ()
r a
a a
b = a -> a -> m ()
r a
a a
b
relPolM Pol
_ a -> a -> m ()
_ a
_ a
_ = m ()
forall a. HasCallStack => a
undefined

-- polarity product (composition of polarities) ----------------------

data Multiplicity = POne | PTwo deriving (Multiplicity -> Multiplicity -> Bool
(Multiplicity -> Multiplicity -> Bool)
-> (Multiplicity -> Multiplicity -> Bool) -> Eq Multiplicity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Multiplicity -> Multiplicity -> Bool
== :: Multiplicity -> Multiplicity -> Bool
$c/= :: Multiplicity -> Multiplicity -> Bool
/= :: Multiplicity -> Multiplicity -> Bool
Eq, Eq Multiplicity
Eq Multiplicity =>
(Multiplicity -> Multiplicity -> Ordering)
-> (Multiplicity -> Multiplicity -> Bool)
-> (Multiplicity -> Multiplicity -> Bool)
-> (Multiplicity -> Multiplicity -> Bool)
-> (Multiplicity -> Multiplicity -> Bool)
-> (Multiplicity -> Multiplicity -> Multiplicity)
-> (Multiplicity -> Multiplicity -> Multiplicity)
-> Ord Multiplicity
Multiplicity -> Multiplicity -> Bool
Multiplicity -> Multiplicity -> Ordering
Multiplicity -> Multiplicity -> Multiplicity
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 :: Multiplicity -> Multiplicity -> Ordering
compare :: Multiplicity -> Multiplicity -> Ordering
$c< :: Multiplicity -> Multiplicity -> Bool
< :: Multiplicity -> Multiplicity -> Bool
$c<= :: Multiplicity -> Multiplicity -> Bool
<= :: Multiplicity -> Multiplicity -> Bool
$c> :: Multiplicity -> Multiplicity -> Bool
> :: Multiplicity -> Multiplicity -> Bool
$c>= :: Multiplicity -> Multiplicity -> Bool
>= :: Multiplicity -> Multiplicity -> Bool
$cmax :: Multiplicity -> Multiplicity -> Multiplicity
max :: Multiplicity -> Multiplicity -> Multiplicity
$cmin :: Multiplicity -> Multiplicity -> Multiplicity
min :: Multiplicity -> Multiplicity -> Multiplicity
Ord)

instance Show Multiplicity where
  show :: Multiplicity -> String
show Multiplicity
POne = String
"1"
  show Multiplicity
PTwo = String
"2"

-- addition modulo 2
addMultiplicity :: Multiplicity -> Multiplicity -> Multiplicity
addMultiplicity :: Multiplicity -> Multiplicity -> Multiplicity
addMultiplicity Multiplicity
PTwo Multiplicity
y = Multiplicity
y
addMultiplicity Multiplicity
x Multiplicity
PTwo = Multiplicity
x
addMultiplicity Multiplicity
POne Multiplicity
POne = Multiplicity
PTwo

type VarMults = Map PVarId Multiplicity -- multiplicity of variables (1 or 2)

showMults :: VarMults -> String
showMults :: VarMults -> String
showMults VarMults
mults =
  let ml :: [(PVarId, Multiplicity)]
ml = VarMults -> [(PVarId, Multiplicity)]
forall k a. Map k a -> [(k, a)]
Map.toList VarMults
mults  -- get list of (key,value) pairs
      l :: [PVarId]
l  = [[PVarId]] -> [PVarId]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PVarId]] -> [PVarId]) -> [[PVarId]] -> [PVarId]
forall a b. (a -> b) -> a -> b
$ ((PVarId, Multiplicity) -> [PVarId])
-> [(PVarId, Multiplicity)] -> [[PVarId]]
forall a b. (a -> b) -> [a] -> [b]
map (PVarId, Multiplicity) -> [PVarId]
forall {a}. (a, Multiplicity) -> [a]
f [(PVarId, Multiplicity)]
ml where
             f :: (a, Multiplicity) -> [a]
f (a
k, Multiplicity
POne) = [a
k]
             f (a
k, Multiplicity
PTwo) = [a
k,a
k]
  in String -> (PVarId -> String) -> [PVarId] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"." PVarId -> String
forall a. Show a => a -> String
showPVar [PVarId]
l

multsEmpty :: VarMults
multsEmpty :: VarMults
multsEmpty = VarMults
forall k a. Map k a
Map.empty

multsSingle :: Int -> VarMults
multsSingle :: PVarId -> VarMults
multsSingle PVarId
i = PVarId -> Multiplicity -> VarMults -> VarMults
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert PVarId
i Multiplicity
POne VarMults
multsEmpty


data PProd = PProd
  { PProd -> Pol
coeff    :: Pol      -- a coefficient, excluding PVar
  , PProd -> VarMults
varMults :: VarMults -- multiplicity of variables (1 or 2)
  } deriving (PProd -> PProd -> Bool
(PProd -> PProd -> Bool) -> (PProd -> PProd -> Bool) -> Eq PProd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PProd -> PProd -> Bool
== :: PProd -> PProd -> Bool
$c/= :: PProd -> PProd -> Bool
/= :: PProd -> PProd -> Bool
Eq,Eq PProd
Eq PProd =>
(PProd -> PProd -> Ordering)
-> (PProd -> PProd -> Bool)
-> (PProd -> PProd -> Bool)
-> (PProd -> PProd -> Bool)
-> (PProd -> PProd -> Bool)
-> (PProd -> PProd -> PProd)
-> (PProd -> PProd -> PProd)
-> Ord PProd
PProd -> PProd -> Bool
PProd -> PProd -> Ordering
PProd -> PProd -> PProd
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 :: PProd -> PProd -> Ordering
compare :: PProd -> PProd -> Ordering
$c< :: PProd -> PProd -> Bool
< :: PProd -> PProd -> Bool
$c<= :: PProd -> PProd -> Bool
<= :: PProd -> PProd -> Bool
$c> :: PProd -> PProd -> Bool
> :: PProd -> PProd -> Bool
$c>= :: PProd -> PProd -> Bool
>= :: PProd -> PProd -> Bool
$cmax :: PProd -> PProd -> PProd
max :: PProd -> PProd -> PProd
$cmin :: PProd -> PProd -> PProd
min :: PProd -> PProd -> PProd
Ord)

instance Polarity PProd where
  erased :: PProd -> Bool
erased  = Pol -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Pol -> Bool) -> (PProd -> Pol) -> PProd -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PProd -> Pol
coeff
  compose :: PProd -> PProd -> PProd
compose = PProd -> PProd -> PProd
polProd
  neutral :: PProd
neutral = Pol -> VarMults -> PProd
PProd Pol
SPos VarMults
multsEmpty
  demote :: PProd -> PProd
demote  = PProd -> PProd
forall a. HasCallStack => a
undefined
  promote :: PProd -> PProd
promote = PProd -> PProd
forall a. HasCallStack => a
undefined
  hidden :: PProd
hidden  = Pol -> VarMults -> PProd
PProd Pol
forall pol. Polarity pol => pol
hidden VarMults
multsEmpty

instance Show PProd where
  show :: PProd -> String
show (PProd Pol
Const VarMults
_) = Pol -> String
forall a. Show a => a -> String
show Pol
Const
  show (PProd Pol
SPos VarMults
m) = if VarMults -> Bool
forall k a. Map k a -> Bool
Map.null VarMults
m then Pol -> String
forall a. Show a => a -> String
show Pol
SPos else VarMults -> String
showMults VarMults
m
  show (PProd Pol
q VarMults
m) = String -> String -> ShowS
separate String
"." (Pol -> String
forall a. Show a => a -> String
show Pol
q) (VarMults -> String
showMults VarMults
m)

pprod :: Pol -> PProd
pprod :: Pol -> PProd
pprod (PVar PVarId
i) = Pol -> VarMults -> PProd
PProd Pol
SPos (PVarId -> VarMults
multsSingle PVarId
i)
pprod Pol
q = Pol -> VarMults -> PProd
PProd Pol
q VarMults
multsEmpty

-- | fails if not a simple polarity
fromPProd :: PProd -> Maybe Pol
fromPProd :: PProd -> Maybe Pol
fromPProd (PProd Pol
Const VarMults
_)          = Pol -> Maybe Pol
forall a. a -> Maybe a
Just Pol
Const
fromPProd (PProd Pol
p VarMults
m) | VarMults -> Bool
forall k a. Map k a -> Bool
Map.null VarMults
m = Pol -> Maybe Pol
forall a. a -> Maybe a
Just Pol
p
fromPProd PProd
_                        = Maybe Pol
forall a. Maybe a
Nothing

isSPos :: PProd -> Bool
isSPos :: PProd -> Bool
isSPos (PProd Pol
Const VarMults
_) = Bool
True
isSPos (PProd Pol
SPos VarMults
m) = VarMults -> Bool
forall k a. Map k a -> Bool
Map.null VarMults
m
isSPos PProd
_ = Bool
False

-- multiply two products

polProd :: PProd -> PProd -> PProd
polProd :: PProd -> PProd -> PProd
polProd (PProd Pol
q1 VarMults
m1) (PProd Pol
q2 VarMults
m2) = Pol -> VarMults -> PProd
PProd (Pol -> Pol -> Pol
polComp Pol
q1 Pol
q2) (VarMults -> PProd) -> VarMults -> PProd
forall a b. (a -> b) -> a -> b
$
  (Multiplicity -> Multiplicity -> Multiplicity)
-> VarMults -> VarMults -> VarMults
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Multiplicity -> Multiplicity -> Multiplicity
addMultiplicity VarMults
m1 VarMults
m2

-- polarity expressions are polynomials ------------------------------

data PPoly = PPoly { PPoly -> [PProd]
monomials :: [PProd] } deriving (PPoly -> PPoly -> Bool
(PPoly -> PPoly -> Bool) -> (PPoly -> PPoly -> Bool) -> Eq PPoly
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PPoly -> PPoly -> Bool
== :: PPoly -> PPoly -> Bool
$c/= :: PPoly -> PPoly -> Bool
/= :: PPoly -> PPoly -> Bool
Eq,Eq PPoly
Eq PPoly =>
(PPoly -> PPoly -> Ordering)
-> (PPoly -> PPoly -> Bool)
-> (PPoly -> PPoly -> Bool)
-> (PPoly -> PPoly -> Bool)
-> (PPoly -> PPoly -> Bool)
-> (PPoly -> PPoly -> PPoly)
-> (PPoly -> PPoly -> PPoly)
-> Ord PPoly
PPoly -> PPoly -> Bool
PPoly -> PPoly -> Ordering
PPoly -> PPoly -> PPoly
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 :: PPoly -> PPoly -> Ordering
compare :: PPoly -> PPoly -> Ordering
$c< :: PPoly -> PPoly -> Bool
< :: PPoly -> PPoly -> Bool
$c<= :: PPoly -> PPoly -> Bool
<= :: PPoly -> PPoly -> Bool
$c> :: PPoly -> PPoly -> Bool
> :: PPoly -> PPoly -> Bool
$c>= :: PPoly -> PPoly -> Bool
>= :: PPoly -> PPoly -> Bool
$cmax :: PPoly -> PPoly -> PPoly
max :: PPoly -> PPoly -> PPoly
$cmin :: PPoly -> PPoly -> PPoly
min :: PPoly -> PPoly -> PPoly
Ord)

instance Show PPoly where
  show :: PPoly -> String
show (PPoly []) = Pol -> String
forall a. Show a => a -> String
show Pol
Const
  show (PPoly [PProd
m]) = PProd -> String
forall a. Show a => a -> String
show PProd
m
  show (PPoly [PProd]
l)   = String -> (PProd -> String) -> [PProd] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"/\\" PProd -> String
forall a. Show a => a -> String
show [PProd]
l

ppoly :: PProd -> PPoly
ppoly :: PProd -> PPoly
ppoly (PProd Pol
Const VarMults
_) = [PProd] -> PPoly
PPoly []
ppoly PProd
pp = [PProd] -> PPoly
PPoly [PProd
pp]

polSum :: PPoly -> PPoly -> PPoly
polSum :: PPoly -> PPoly -> PPoly
polSum (PPoly [PProd]
x) (PPoly [PProd]
y) = [PProd] -> PPoly
PPoly ([PProd] -> PPoly) -> [PProd] -> PPoly
forall a b. (a -> b) -> a -> b
$ [PProd] -> [PProd]
forall a. Eq a => [a] -> [a]
List.nub ([PProd] -> [PProd]) -> [PProd] -> [PProd]
forall a b. (a -> b) -> a -> b
$ [PProd]
x [PProd] -> [PProd] -> [PProd]
forall a. [a] -> [a] -> [a]
++ [PProd]
y

polProduct :: PPoly -> PPoly -> PPoly
polProduct :: PPoly -> PPoly -> PPoly
polProduct (PPoly [PProd]
l1) (PPoly [PProd]
l2) =
  let ps :: [PProd]
ps = [ PProd -> PProd -> PProd
polProd PProd
x PProd
y | PProd
x <- [PProd]
l1, PProd
y <- [PProd]
l2]
  in [PProd] -> PPoly
PPoly ([PProd] -> PPoly) -> [PProd] -> PPoly
forall a b. (a -> b) -> a -> b
$ [PProd] -> [PProd]
forall a. Eq a => [a] -> [a]
List.nub ([PProd] -> [PProd]) -> [PProd] -> [PProd]
forall a b. (a -> b) -> a -> b
$ [PProd]
ps

instance SemiRing PPoly where
  oplus :: PPoly -> PPoly -> PPoly
oplus  = PPoly -> PPoly -> PPoly
polSum
  otimes :: PPoly -> PPoly -> PPoly
otimes = PPoly -> PPoly -> PPoly
polProduct
  ozero :: PPoly
ozero  = [PProd] -> PPoly
PPoly []
  oone :: PPoly
oone   = [PProd] -> PPoly
PPoly [Pol -> VarMults -> PProd
PProd Pol
SPos VarMults
forall k a. Map k a
Map.empty]

{-
data PExpr
  = PValue Pol     -- constant polarity
  | PExpr Pol Int  -- PExpr q pi means q^_1 pi  (pi is the number of the var)

-- a polarity variable
pvar :: Int -> PExpr
pvar = PExpr SPos  -- ++ is the neutral element of inverse polarity composition

instance Show PExpr where
  show (PValue p) = show p
  show (PExpr SPos i) = "?p" ++ show i
  show (PExpr q i) = show q ++ "^-1(?p" ++ show i ++ ")"
-}


{- ML-style Polarity inference

Preliminaries:
1. constructor types are mixed-variant function types only
2. matching is only allowed on mixed-variant arguments
  1+2 are both consequences that only type-valued functions have variance
  and 1. data constructors are not types, 2. types are not matched on

Concrete syntax

  f : (xs : As) -> C   (C not a Pi-type)
  f = t

is parsed as abstract syntax

  f : pis(xs : As) -> C
  f = t

where pi_1..n are fresh polarity variables

Then t is type-checked to infer the polarity variables, e.g.

  f xs = t

  pis(xs : As) |- t : C

Now what can happen?

Variable:  t = x_i.  Then we add a constraint  pi_i <= ++

Application t = u v  where u : q(x:B) -> D

  q^-1(pis(xs: As)) |- v : B

  A term q^-1 pi arises where q is a polarity constant (!, ML-inference)
  or a polarity variable (recursion!, e.g. u = f)
  and pi is a polarity expression

In the context, keep SOLL and HABEN

  SOLL  is the original polarity (variable or constant)
  HABEN is a (ordered) list of pol.vars. and a pol.const. (default: ++)

Variable   : add constraint SOLL <= HABEN
Application: add q to HABEN by polarity multiplication (q is a var or const)
Abstraction: \xt : q(x:A) -> B:  continue with x (SOLL = q, HABEN = ++)

What kind of constraints do arise
1) q  <= pi    [ from variables , pi is a Pol-product ]
2) ++ <= pis  [ from positivity graph, pis is a sum of Pol-products ]
   this means ++ <= pi for all pi in pis

Solving constraints

- discard  o <= pi  and q <= /  (do not even need to add them)
- all pvars which are not bounded below (appearing in one q in 1)
  can be instantiated to /  which will remove some constraints


-}

{- Mutual recursion

In mutual declarations, use the following Ansatz:  data/codata ++, functions o

  A = B -> A
  B = A -> B

A (B) is positive in its own body and negative in the body of B (A)

  F A B = B -> A   F(-,++)
  G A B = A -> B   G(-,++)

  F A B = G A B -> F A B
  G A B = F A B -> G A B

  Polarities:
  F : fa * -> fb * -> *
  G : ga * -> gb * -> *

  A : -fa, B : -fb |- G A B : *  ==> -fa <= ga, -fb <= gb
  A : -ga, B : -gb |- F A B : *  ==> -ga <= fa, -gb <= fb

-}

{- Pure polarity inference

Judgement:  pis(xs:As) |- t : B ---> C

Variable:   pis(xs:As) |- xi : Ai ---> pi_i <= ++

Application: Delta |- u : q(x:A) -> B ---> C1
             Delta |- v : A           ---> C2
             --------------------------------------------------
             Delta |- u v : B[u/x] ---> C1,C2,q(Delta) <= Delta
-}