content: {- 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 (Eq,Ord)
  
  mixed, defaultPol :: Pol
  mixed = Rec
  defaultPol = Rec
  {-
  mixed = Param -- TODO: Rec
  defaultPol = Param -- TODO: Rec
  -}
  instance Polarity Pol where
    erased  = (==) Const
    compose = polComp
    neutral = SPos
    promote = invComp Const
    demote  = invComp Rec
    hidden  = Const
  
  instance Show Pol where
    show Const = "."
    show SPos  = "++"
    show Pos   = "+"
    show Neg   = "-"
    show Param = "^"
    show Rec   = "*"
    show Default = "{default polarity}"
    show (PVar i) = showPVar i
  
  showPVar :: Show a => a -> String
  showPVar i = "?p" ++ show i
  
  isPVar :: Pol -> Bool
  isPVar (PVar{}) = True
  isPVar _ = False
  
  -- information ordering
  leqPol :: Pol -> Pol -> Bool
  leqPol _ Const  = True   -- Const is top
  leqPol Const _  = False
  leqPol Rec _    = True   -- Rec is bottom
  leqPol _ Rec    = False
  leqPol Param _  = True   -- Param is second bottom
  leqPol _ Param  = False
  leqPol Pos SPos = True
  leqPol x   y    = x == 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 Const  = Const
  polNeg SPos  = Neg
  polNeg Pos   = Neg
  polNeg Neg   = Pos
  polNeg Param = Param
  polNeg Rec   = Rec
  polNeg _ = undefined
  
  -- polarity composition
  -- used in Eval.hs leqVals'
  polComp :: Pol -> Pol -> Pol
  polComp Const  _  = Const   -- most dominant
  polComp _ Const   = Const
  polComp Rec _     = Rec  -- dominant except for Const
  polComp _ Rec     = Rec
  polComp Param _   = Param  -- dominant except for Const, Rec
  polComp _ Param   = Param
  polComp SPos  x   = x      -- neutral
  polComp x SPos    = x
  polComp Pos  x    = x      -- neutral except for SPos
  polComp x Pos     = x
  polComp Neg Neg   = Pos    -- order 2
  polComp _ _ = 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 Rec   Rec   = Rec       -- in rec. arg. keep only rec. vars
  invComp Rec   _     = Const     -- all others are declared unusable
  invComp Param Param = Param     -- in parametric mixed arg, keep only mixed vars
  invComp Param _     = Const
  invComp Const _     = Param     -- a constant function can take any argument
  invComp SPos  x     = x         -- SPos is the identity
  invComp _     SPos  = Const     -- SPos preserved only under SPos
  invComp Pos   x     = x         -- x not SPos
  invComp Neg   x     = polNeg x  -- x not SPos
  invComp _ _ = 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 Const x = x      -- most information
  polAnd x Const = x
  polAnd Rec   _ = Rec   -- least information
  polAnd _   Rec = Rec
  {-
  polAnd Param x  = Param   -- 2nd least information
  polAnd x Param  = Param
  -}
  polAnd x y | x == y = x       -- same information
  polAnd SPos Pos = Pos     -- SPos is more informative than Pos
  polAnd Pos SPos = Pos
  {-
  polAnd SPos Neg = Param
  polAnd Neg SPos = Param
  -}
  polAnd _ _      = Param     -- remaining cases: conflicting info or Param
  
  instance SemiRing Pol where
    oplus  = polAnd
    otimes = polComp
    ozero  = Const    -- dominant for composition, neutral for infimum
    oone   = SPos     -- neutral  for composition
  
  -- computing a relation from <=
  relPol :: Pol -> (a -> a -> Bool) -> (a -> a -> Bool)
  relPol Const _ _ _ = True
  relPol Rec   r a b = r a b && r b a
  relPol Param r a b = r a b && r b a
  relPol Neg   r a b = r b a
  relPol Pos   r a b = r a b
  relPol SPos  r a b = r a b
  relPol _ _ _ _ = undefined
  
  relPolM :: (Monad m) => Pol -> (a -> a -> m ()) -> (a -> a -> m ())
  relPolM Const _ _ _ = return ()
  relPolM Rec   r a b = r a b >> r b a
  relPolM Param r a b = r a b >> r b a
  relPolM Neg   r a b = r b a
  relPolM Pos   r a b = r a b
  relPolM SPos  r a b = r a b
  relPolM _ _ _ _ = undefined
  
  -- polarity product (composition of polarities) ----------------------
  
  data Multiplicity = POne | PTwo deriving (Eq, Ord)
  
  instance Show Multiplicity where
    show POne = "1"
    show PTwo = "2"
  
  -- addition modulo 2
  addMultiplicity :: Multiplicity -> Multiplicity -> Multiplicity
  addMultiplicity PTwo y = y
  addMultiplicity x PTwo = x
  addMultiplicity POne POne = PTwo
  
  type VarMults = Map PVarId Multiplicity -- multiplicity of variables (1 or 2)
  
  showMults :: VarMults -> String
  showMults mults =
    let ml = Map.toList mults  -- get list of (key,value) pairs
        l  = concat $ map f ml where
               f (k, POne) = [k]
               f (k, PTwo) = [k,k]
    in Util.showList "." showPVar l
  
  multsEmpty :: VarMults
  multsEmpty = Map.empty
  
  multsSingle :: Int -> VarMults
  multsSingle i = Map.insert i POne multsEmpty
  
  
  data PProd = PProd
    { coeff    :: Pol      -- a coefficient, excluding PVar
    , varMults :: VarMults -- multiplicity of variables (1 or 2)
    } deriving (Eq,Ord)
  
  instance Polarity PProd where
    erased  = erased . coeff
    compose = polProd
    neutral = PProd SPos multsEmpty
    demote  = undefined
    promote = undefined
    hidden  = PProd hidden multsEmpty
  
  instance Show PProd where
    show (PProd Const _) = show Const
    show (PProd SPos m) = if Map.null m then show SPos else showMults m
    show (PProd q m) = separate "." (show q) (showMults m)
  
  pprod :: Pol -> PProd
  pprod (PVar i) = PProd SPos (multsSingle i)
  pprod q = PProd q multsEmpty
  
  -- | fails if not a simple polarity
  fromPProd :: PProd -> Maybe Pol
  fromPProd (PProd Const _)          = Just Const
  fromPProd (PProd p m) | Map.null m = Just p
  fromPProd _                        = Nothing
  
  isSPos :: PProd -> Bool
  isSPos (PProd Const _) = True
  isSPos (PProd SPos m) = Map.null m
  isSPos _ = False
  
  -- multiply two products
  
  polProd :: PProd -> PProd -> PProd
  polProd (PProd q1 m1) (PProd q2 m2) = PProd (polComp q1 q2) $
    Map.unionWith addMultiplicity m1 m2
  
  -- polarity expressions are polynomials ------------------------------
  
  data PPoly = PPoly { monomials :: [PProd] } deriving (Eq,Ord)
  
  instance Show PPoly where
    show (PPoly []) = show Const
    show (PPoly [m]) = show m
    show (PPoly l)   = Util.showList "/\\" show l
  
  ppoly :: PProd -> PPoly
  ppoly (PProd Const _) = PPoly []
  ppoly pp = PPoly [pp]
  
  polSum :: PPoly -> PPoly -> PPoly
  polSum (PPoly x) (PPoly y) = PPoly $ List.nub $ x ++ y
  
  polProduct :: PPoly -> PPoly -> PPoly
  polProduct (PPoly l1) (PPoly l2) =
    let ps = [ polProd x y | x <- l1, y <- l2]
    in PPoly $ List.nub $ ps
  
  instance SemiRing PPoly where
    oplus  = polSum
    otimes = polProduct
    ozero  = PPoly []
    oone   = PPoly [PProd SPos 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
  -}
  