{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
module Embedder.Atmo.Types
      ( TypeAnnotated (typeOf, tyAnn, setTyAnn), tupleTy
      , arr, intTy, strTy, nilTy, refTy, (|->)
      , rangeTy, sig, flattenSig, pairTy, arrowRight, arrowLeft
      , higherOrder, fundamental, concrete, paramTys
      , finMax, proxyNat, finiteTy, vecSize, vecElemTy, vecTy, evalNat
      , mkArrowTy, mkTyApp, poly, poly', listTy, plusTy, dstPlusTy
      , isReacT, isStateT, ctorNames, resInputTy
      , dstArrow, dstStateT, dstTyApp, dstReacT, proxyTy
      , dstNegTy, negTy, dstPoly1, Poly1, minusP1, zeroP1, pickVar, poly1Ty
      ) where

import ReWire.Annotation (Annote (MsgAnnote), Annotated (ann), noAnn)
import Embedder.Atmo.Syntax (Exp (..), Ty (..), TyBuiltin (..), Poly (Poly), Pat (..))
import Embedder.Builtins (tb2s)
import ReWire.Pretty (Pretty (pretty), Doc, hsep, text, punctuate, parens, showt)

import Data.Containers.ListUtils (nubOrd)
import Data.HashMap.Strict (HashMap)
import Data.Hashable (Hashable (hash))
import Data.List (sortOn)
import Data.Maybe (isJust)
import Data.Ratio (numerator, denominator, (%))
import Numeric.Natural (Natural)

import qualified Data.HashMap.Strict as Map
import Data.Text (Text)

--- TypeAnnotated instances

-- Name Handling:
      -- remove Embed
      -- remove s2n and n2s
      -- Replace bindings with vs and body
      -- fix defs of `poly` and `|->`
      -- define fv for types

class TypeAnnotated a where
      typeOf   :: a -> Maybe Ty
      tyAnn    :: a -> Maybe Poly
      setTyAnn :: Maybe Poly -> a -> a

instance TypeAnnotated Exp where
      typeOf :: Exp -> Maybe Ty
typeOf = \ case
            App Annote
_ Maybe Poly
_ Maybe Ty
t Exp
_ [Exp]
_         -> Maybe Ty
t
            Lam Annote
_ Maybe Poly
_ Maybe Ty
t [Text]
_ Exp
_        -> Maybe Ty
t
            Var Annote
_ Maybe Poly
_ Maybe Ty
t Text
_           -> Maybe Ty
t
            Con Annote
_ Maybe Poly
_ Maybe Ty
t Text
_           -> Maybe Ty
t
            Case Annote
_ Maybe Poly
_ Maybe Ty
t Exp
_ [PatBind]
_        -> Maybe Ty
t
            RWUser Annote
_ Maybe Poly
_ Maybe Ty
t RWUserOp
_        -> Maybe Ty
t
            LitInt Annote
a Maybe Poly
_ Integer
_          -> Ty -> Maybe Ty
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> Maybe Ty) -> Ty -> Maybe Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Ty
intTy Annote
a
            LitStr Annote
a Maybe Poly
_ Text
_          -> Ty -> Maybe Ty
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> Maybe Ty) -> Ty -> Maybe Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Ty
strTy Annote
a
            LitList Annote
_ Maybe Poly
_ Maybe Ty
t [Exp]
_       -> Maybe Ty
t
            LitVec Annote
_ Maybe Poly
_ Maybe Ty
t [Exp]
_        -> Maybe Ty
t
            Tuple Annote
_ Maybe Poly
_ Maybe Ty
t [Exp]
_         -> Maybe Ty
t
            If Annote
_ Maybe Poly
_ Maybe Ty
t Exp
_ Exp
_ Exp
_        -> Maybe Ty
t
            Let Annote
_ Maybe Poly
_ Maybe Ty
t [PatBind]
_ Exp
_         -> Maybe Ty
t
            RecVal Annote
_ Maybe Poly
_ Maybe Ty
t [(Text, Exp)]
_        -> Maybe Ty
t
            RecUpd Annote
_ Maybe Poly
_ Maybe Ty
t Exp
_ [(Text, Exp)]
_      -> Maybe Ty
t
            RecSel Annote
_ Maybe Poly
_ Maybe Ty
t Text
_ Exp
_      -> Maybe Ty
t
      
      tyAnn :: Exp -> Maybe Poly
tyAnn = \ case
            App Annote
_ Maybe Poly
pt Maybe Ty
_ Exp
_ [Exp]
_        -> Maybe Poly
pt
            Lam Annote
_ Maybe Poly
pt Maybe Ty
_ [Text]
_ Exp
_        -> Maybe Poly
pt
            Var Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_          -> Maybe Poly
pt
            Con Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_          -> Maybe Poly
pt
            Case Annote
_ Maybe Poly
pt Maybe Ty
_ Exp
_ [PatBind]
_       -> Maybe Poly
pt
            RWUser Annote
_ Maybe Poly
pt Maybe Ty
_ RWUserOp
_       -> Maybe Poly
pt
            LitInt Annote
_ Maybe Poly
pt Integer
_         -> Maybe Poly
pt
            LitStr Annote
_ Maybe Poly
pt Text
_         -> Maybe Poly
pt
            LitList Annote
_ Maybe Poly
pt Maybe Ty
_ [Exp]
_      -> Maybe Poly
pt
            LitVec Annote
_ Maybe Poly
pt Maybe Ty
_ [Exp]
_       -> Maybe Poly
pt
            Tuple Annote
_ Maybe Poly
pt Maybe Ty
_ [Exp]
_        -> Maybe Poly
pt
            If Annote
_ Maybe Poly
pt Maybe Ty
_ Exp
_ Exp
_ Exp
_       -> Maybe Poly
pt
            Let Annote
_ Maybe Poly
pt Maybe Ty
_ [PatBind]
_ Exp
_        -> Maybe Poly
pt
            RecVal Annote
_ Maybe Poly
pt Maybe Ty
_ [(Text, Exp)]
_       -> Maybe Poly
pt
            RecUpd Annote
_ Maybe Poly
pt Maybe Ty
_ Exp
_ [(Text, Exp)]
_     -> Maybe Poly
pt
            RecSel Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_ Exp
_     -> Maybe Poly
pt
      setTyAnn :: Maybe Poly -> Exp -> Exp
setTyAnn Maybe Poly
pt = \ case
            App Annote
a Maybe Poly
_ Maybe Ty
t Exp
e1 [Exp]
e2       -> Annote -> Maybe Poly -> Maybe Ty -> Exp -> [Exp] -> Exp
App Annote
a Maybe Poly
pt Maybe Ty
t Exp
e1 [Exp]
e2
            Lam Annote
a Maybe Poly
_ Maybe Ty
t [Text]
v Exp
e         -> Annote -> Maybe Poly -> Maybe Ty -> [Text] -> Exp -> Exp
Lam Annote
a Maybe Poly
pt Maybe Ty
t [Text]
v Exp
e
            Var Annote
a Maybe Poly
_ Maybe Ty
t Text
e           -> Annote -> Maybe Poly -> Maybe Ty -> Text -> Exp
Var Annote
a Maybe Poly
pt Maybe Ty
t Text
e
            Con Annote
a Maybe Poly
_ Maybe Ty
t Text
e           -> Annote -> Maybe Poly -> Maybe Ty -> Text -> Exp
Con Annote
a Maybe Poly
pt Maybe Ty
t Text
e
            Case Annote
a Maybe Poly
_ Maybe Ty
t Exp
e [PatBind]
pbs      -> Annote -> Maybe Poly -> Maybe Ty -> Exp -> [PatBind] -> Exp
Case Annote
a Maybe Poly
pt Maybe Ty
t Exp
e [PatBind]
pbs
            RWUser Annote
a Maybe Poly
_ Maybe Ty
t RWUserOp
b        -> Annote -> Maybe Poly -> Maybe Ty -> RWUserOp -> Exp
RWUser Annote
a Maybe Poly
pt Maybe Ty
t RWUserOp
b
            LitInt Annote
a Maybe Poly
_ Integer
n          -> Annote -> Maybe Poly -> Integer -> Exp
LitInt Annote
a Maybe Poly
pt Integer
n
            LitStr Annote
a Maybe Poly
_ Text
n          -> Annote -> Maybe Poly -> Text -> Exp
LitStr Annote
a Maybe Poly
pt Text
n
            LitList Annote
a Maybe Poly
_ Maybe Ty
t [Exp]
n       -> Annote -> Maybe Poly -> Maybe Ty -> [Exp] -> Exp
LitList Annote
a Maybe Poly
pt Maybe Ty
t [Exp]
n
            LitVec Annote
a Maybe Poly
_ Maybe Ty
t [Exp]
n        -> Annote -> Maybe Poly -> Maybe Ty -> [Exp] -> Exp
LitVec Annote
a Maybe Poly
pt Maybe Ty
t [Exp]
n
            Tuple Annote
a Maybe Poly
_ Maybe Ty
t [Exp]
n         -> Annote -> Maybe Poly -> Maybe Ty -> [Exp] -> Exp
Tuple Annote
a Maybe Poly
pt Maybe Ty
t [Exp]
n
            If Annote
a Maybe Poly
_ Maybe Ty
t Exp
tst Exp
con Exp
alt       -> Annote -> Maybe Poly -> Maybe Ty -> Exp -> Exp -> Exp -> Exp
If Annote
a Maybe Poly
pt Maybe Ty
t Exp
tst Exp
con Exp
alt
            Let Annote
a Maybe Poly
_ Maybe Ty
t [PatBind]
b Exp
e         -> Annote -> Maybe Poly -> Maybe Ty -> [PatBind] -> Exp -> Exp
Let Annote
a Maybe Poly
pt Maybe Ty
t [PatBind]
b Exp
e
            RecVal Annote
a Maybe Poly
_ Maybe Ty
t [(Text, Exp)]
fs       -> Annote -> Maybe Poly -> Maybe Ty -> [(Text, Exp)] -> Exp
RecVal Annote
a Maybe Poly
pt Maybe Ty
t [(Text, Exp)]
fs
            RecUpd Annote
a Maybe Poly
_ Maybe Ty
t Exp
e [(Text, Exp)]
fs     -> Annote -> Maybe Poly -> Maybe Ty -> Exp -> [(Text, Exp)] -> Exp
RecUpd Annote
a Maybe Poly
pt Maybe Ty
t Exp
e [(Text, Exp)]
fs
            RecSel Annote
a Maybe Poly
_ Maybe Ty
t Text
f Exp
e      -> Annote -> Maybe Poly -> Maybe Ty -> Text -> Exp -> Exp
RecSel Annote
a Maybe Poly
pt Maybe Ty
t Text
f Exp
e

instance TypeAnnotated Pat where
      typeOf :: Pat -> Maybe Ty
typeOf = \ case
            PatCon Annote
_ Maybe Poly
_ Maybe Ty
t Text
_ [Pat]
_   -> Maybe Ty
t
            PatVar Annote
_ Maybe Poly
_ Maybe Ty
t Text
_     -> Maybe Ty
t
            PatWildCard Annote
_ Maybe Poly
_ Maybe Ty
t  -> Maybe Ty
t
            PatTuple Annote
_ Maybe Poly
_ Maybe Ty
t [Pat]
_   -> Maybe Ty
t
            PatAs Annote
_ Maybe Poly
_ Maybe Ty
t Text
_ Pat
_    -> Maybe Ty
t
            PatRec Annote
_ Maybe Poly
_ Maybe Ty
t [(Text, Pat)]
_     -> Maybe Ty
t
      tyAnn :: Pat -> Maybe Poly
tyAnn = \ case
            PatCon Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_ [Pat]
_  -> Maybe Poly
pt
            PatVar Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_    -> Maybe Poly
pt
            PatWildCard Annote
_ Maybe Poly
pt Maybe Ty
_ -> Maybe Poly
pt
            PatTuple Annote
_ Maybe Poly
pt Maybe Ty
_ [Pat]
_  -> Maybe Poly
pt
            PatAs Annote
_ Maybe Poly
pt Maybe Ty
_ Text
_ Pat
_   -> Maybe Poly
pt
            PatRec Annote
_ Maybe Poly
pt Maybe Ty
_ [(Text, Pat)]
_    -> Maybe Poly
pt
      setTyAnn :: Maybe Poly -> Pat -> Pat
setTyAnn Maybe Poly
pt = \ case
            PatCon Annote
a Maybe Poly
_ Maybe Ty
t Text
c [Pat]
ps  -> Annote -> Maybe Poly -> Maybe Ty -> Text -> [Pat] -> Pat
PatCon Annote
a Maybe Poly
pt Maybe Ty
t Text
c [Pat]
ps
            PatVar Annote
a Maybe Poly
_ Maybe Ty
t Text
x     -> Annote -> Maybe Poly -> Maybe Ty -> Text -> Pat
PatVar Annote
a Maybe Poly
pt Maybe Ty
t Text
x
            PatWildCard Annote
a Maybe Poly
_ Maybe Ty
t  -> Annote -> Maybe Poly -> Maybe Ty -> Pat
PatWildCard Annote
a Maybe Poly
pt Maybe Ty
t
            PatTuple Annote
a Maybe Poly
_ Maybe Ty
t [Pat]
ps  -> Annote -> Maybe Poly -> Maybe Ty -> [Pat] -> Pat
PatTuple Annote
a Maybe Poly
pt Maybe Ty
t [Pat]
ps
            PatAs Annote
a Maybe Poly
_ Maybe Ty
t Text
n Pat
p    -> Annote -> Maybe Poly -> Maybe Ty -> Text -> Pat -> Pat
PatAs Annote
a Maybe Poly
pt Maybe Ty
t Text
n Pat
p
            PatRec Annote
a Maybe Poly
_ Maybe Ty
t [(Text, Pat)]
fs    -> Annote -> Maybe Poly -> Maybe Ty -> [(Text, Pat)] -> Pat
PatRec Annote
a Maybe Poly
pt Maybe Ty
t [(Text, Pat)]
fs

---

intTy :: Annote -> Ty
intTy :: Annote -> Ty
intTy Annote
an = Annote -> Text -> Ty
TyCon Annote
an Text
"Integer"

strTy :: Annote -> Ty
strTy :: Annote -> Ty
strTy Annote
an = Annote -> Text -> Ty
TyCon Annote
an Text
"String"

poly :: [Text] -> Ty -> Poly
poly :: [Text] -> Ty -> Poly
poly = [Text] -> Ty -> Poly
Poly

fv :: Ty -> [Text]
fv :: Ty -> [Text]
fv = \ case
      TyApp Annote
_a Ty
t1 [Ty]
ts -> Ty -> [Text]
fv Ty
t1 [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ (Ty -> [Text]) -> [Ty] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Ty -> [Text]
fv [Ty]
ts
      TyVar Annote
_a Text
n -> [Text
n]
      Ty
_ -> []

poly' :: Ty -> Poly
poly' :: Ty -> Poly
poly' Ty
t = [Text] -> Ty -> Poly
poly ([Text] -> [Text]
forall a. Ord a => [a] -> [a]
nubOrd ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ Ty -> [Text]
fv Ty
t) Ty
t

(|->) :: [Text] -> Ty -> Poly
[Text]
vs |-> :: [Text] -> Ty -> Poly
|-> Ty
t = [Text] -> Ty -> Poly
poly [Text]
vs Ty
t

infix 1 |->

arr :: Ty -> Ty -> Ty
arr :: Ty -> Ty -> Ty
arr Ty
t1 Ty
t2 = Annote -> Ty -> [Ty] -> Ty
TyApp (Ty -> Annote
forall a. Annotated a => a -> Annote
ann Ty
t1) (Annote -> TyBuiltin -> Ty
TyBuiltin (Ty -> Annote
forall a. Annotated a => a -> Annote
ann Ty
t1) TyBuiltin
TyFun) [Ty
t1, Ty
t2]

infixr 1 `arr`

sig :: [Ty] -> Ty -> Ty
sig :: [Ty] -> Ty -> Ty
sig [] Ty
u = Ty
u
sig (Ty
t:[Ty]
ts) Ty
u = Annote -> Ty -> [Ty] -> Ty
TyApp (Ty -> Annote
forall a. Annotated a => a -> Annote
ann Ty
t) (Annote -> TyBuiltin -> Ty
TyBuiltin (Ty -> Annote
forall a. Annotated a => a -> Annote
ann Ty
t) TyBuiltin
TyFun) [Ty
t,[Ty] -> Ty -> Ty
sig [Ty]
ts Ty
u]

flattenSig :: Ty -> ([Ty], Ty)
flattenSig :: Ty -> ([Ty], Ty)
flattenSig = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyFun) [Ty
t1,Ty
t2] -> (Ty
t1 Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: [Ty]
ts, Ty
t)
            where ([Ty]
ts, Ty
t) = Ty -> ([Ty], Ty)
flattenSig Ty
t2
      Ty
t                                               -> ([], Ty
t)

paramTys :: Ty -> [Ty]
paramTys :: Ty -> [Ty]
paramTys = ([Ty], Ty) -> [Ty]
forall a b. (a, b) -> a
fst (([Ty], Ty) -> [Ty]) -> (Ty -> ([Ty], Ty)) -> Ty -> [Ty]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> ([Ty], Ty)
flattenSig

rangeTy :: Ty -> Ty
rangeTy :: Ty -> Ty
rangeTy = ([Ty], Ty) -> Ty
forall a b. (a, b) -> b
snd (([Ty], Ty) -> Ty) -> (Ty -> ([Ty], Ty)) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> ([Ty], Ty)
flattenSig

isArrow :: Ty -> Bool
isArrow :: Ty -> Bool
isArrow = Maybe (Ty, Ty) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Ty, Ty) -> Bool) -> (Ty -> Maybe (Ty, Ty)) -> Ty -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Maybe (Ty, Ty)
dstArrow

dstArrow :: Ty -> Maybe (Ty, Ty)
dstArrow :: Ty -> Maybe (Ty, Ty)
dstArrow = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyFun) [Ty
t1,Ty
t2] -> (Ty, Ty) -> Maybe (Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
t1, Ty
t2)
      Ty
_                                   -> Maybe (Ty, Ty)
forall a. Maybe a
Nothing

-- | Given 'a -> (b -> c)' returns 'b -> c'.
arrowRight :: Ty -> Ty
arrowRight :: Ty -> Ty
arrowRight Ty
t = Ty -> ((Ty, Ty) -> Ty) -> Maybe (Ty, Ty) -> Ty
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ty
t (Ty, Ty) -> Ty
forall a b. (a, b) -> b
snd (Ty -> Maybe (Ty, Ty)
dstArrow Ty
t)

-- | Given 'a -> (b -> c)' returns 'a'.
arrowLeft :: Ty -> Ty
arrowLeft :: Ty -> Ty
arrowLeft Ty
t = Ty -> ((Ty, Ty) -> Ty) -> Maybe (Ty, Ty) -> Ty
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ty
t (Ty, Ty) -> Ty
forall a b. (a, b) -> a
fst (Ty -> Maybe (Ty, Ty)
dstArrow Ty
t)

ctorNames :: Ty -> [Text]
ctorNames :: Ty -> [Text]
ctorNames = \ case
      TyCon Annote
_ Text
n    -> [Text
n]
      TyApp Annote
_ Ty
t [Ty]
ts -> Ty -> [Text]
ctorNames Ty
t [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (Ty -> [Text]) -> [Ty] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Ty -> [Text]
ctorNames [Ty]
ts
      Ty
_            -> []

unop :: TyBuiltin -> Annote -> Ty -> Ty
unop :: TyBuiltin -> Annote -> Ty -> Ty
unop TyBuiltin
tb Annote
a Ty
b = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
a (Annote -> TyBuiltin -> Ty
TyBuiltin Annote
a TyBuiltin
tb) [Ty
b]

binop :: TyBuiltin -> Annote -> Ty -> Ty -> Ty
binop :: TyBuiltin -> Annote -> Ty -> Ty -> Ty
binop TyBuiltin
tb Annote
a Ty
b Ty
c = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
a (Annote -> TyBuiltin -> Ty
TyBuiltin Annote
a TyBuiltin
tb) [Ty
b,Ty
c]


listTy :: Annote -> Ty -> Ty
listTy :: Annote -> Ty -> Ty
listTy = TyBuiltin -> Annote -> Ty -> Ty
unop TyBuiltin
TyList

refTy :: Annote -> Ty -> Ty
refTy :: Annote -> Ty -> Ty
refTy = TyBuiltin -> Annote -> Ty -> Ty
unop TyBuiltin
TyRef

vecTy :: Annote -> Ty -> Ty -> Ty
vecTy :: Annote -> Ty -> Ty -> Ty
vecTy = TyBuiltin -> Annote -> Ty -> Ty -> Ty
binop TyBuiltin
TyVec

vecElemTy :: Ty -> Maybe Ty
vecElemTy :: Ty -> Maybe Ty
vecElemTy = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyVec) [Ty
_, Ty
c] -> Ty -> Maybe Ty
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
c
      Ty
_                                  -> Maybe Ty
forall a. Maybe a
Nothing

vecSize :: Ty -> Maybe Natural
vecSize :: Ty -> Maybe Natural
vecSize = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyVec) [Ty
n, Ty
_] -> Ty -> Maybe Natural
evalNat Ty
n
      Ty
_                                  -> Maybe Natural
forall a. Maybe a
Nothing

proxyNat :: Ty -> Maybe Natural
proxyNat :: Ty -> Maybe Natural
proxyNat = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyProxy) [Ty
n] -> Ty -> Maybe Natural
evalNat Ty
n
      Ty
_                                 -> Maybe Natural
forall a. Maybe a
Nothing

finMax :: Ty -> Maybe Natural
finMax :: Ty -> Maybe Natural
finMax = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyFin) [Ty
n] -> Ty -> Maybe Natural
evalNat Ty
n
      Ty
_                               -> Maybe Natural
forall a. Maybe a
Nothing

proxyTy :: Annote -> Natural -> Ty
proxyTy :: Annote -> Natural -> Ty
proxyTy Annote
an Natural
n = TyBuiltin -> Annote -> Ty -> Ty
unop TyBuiltin
TyProxy Annote
an (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Natural -> Ty
TyNat Annote
an Natural
n

finiteTy :: Annote -> Natural -> Ty
finiteTy :: Annote -> Natural -> Ty
finiteTy Annote
an Natural
n = TyBuiltin -> Annote -> Ty -> Ty
unop TyBuiltin
TyFin Annote
an (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Natural -> Ty
TyNat Annote
an Natural
n

plusTy' :: Annote -> Ty -> Ty -> Ty
plusTy' :: Annote -> Ty -> Ty -> Ty
plusTy' = TyBuiltin -> Annote -> Ty -> Ty -> Ty
binop TyBuiltin
TyPlus

plusTy :: Annote -> Natural -> Natural -> Ty
plusTy :: Annote -> Natural -> Natural -> Ty
plusTy Annote
an Natural
m Natural
n = Annote -> Ty -> Ty -> Ty
plusTy' Annote
an (Annote -> Natural -> Ty
TyNat Annote
an Natural
m) (Annote -> Natural -> Ty
TyNat Annote
an Natural
n)

dstPlusTy :: Ty -> Maybe (Ty, Ty)
dstPlusTy :: Ty -> Maybe (Ty, Ty)
dstPlusTy = \ case
      TyApp Annote
_ Ty
c [Ty
t1,Ty
t2] | Ty -> Bool
isPlus Ty
c -> (Ty, Ty) -> Maybe (Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
t1, Ty
t2)
      Ty
_                                    -> Maybe (Ty, Ty)
forall a. Maybe a
Nothing
      where isPlus :: Ty -> Bool
            isPlus :: Ty -> Bool
isPlus = \ case
                  TyCon Annote
_ Text
"+" -> Bool
True
                  TyBuiltin Annote
_ TyBuiltin
TyPlus -> Bool
True
                  Ty
_                    -> Bool
False

negTy :: Annote -> Ty -> Ty
negTy :: Annote -> Ty -> Ty
negTy Annote
an Ty
t = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"-") [Ty
t]

dstNegTy :: Ty -> Maybe Ty
dstNegTy :: Ty -> Maybe Ty
dstNegTy = \ case
      TyApp Annote
_ Ty
c [Ty
t] | Ty -> Bool
isNeg Ty
c -> Ty -> Maybe Ty
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      Ty
_                     -> Maybe Ty
forall a. Maybe a
Nothing
      where isNeg :: Ty -> Bool
            isNeg :: Ty -> Bool
isNeg = \ case
                  TyCon Annote
_ Text
"-" -> Bool
True
                  Ty
_                    -> Bool
False



evalNat :: Ty -> Maybe Natural
evalNat :: Ty -> Maybe Natural
evalNat Ty
t | Just (Poly1 Rational
r HashMap Text Rational
cs) <- Ty -> Maybe Poly1
dstPoly1 Ty
t
          , Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
0, Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1, HashMap Text Rational
cs HashMap Text Rational -> HashMap Text Rational -> Bool
forall a. Eq a => a -> a -> Bool
== HashMap Text Rational
forall a. Monoid a => a
mempty = Natural -> Maybe Natural
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> Maybe Natural) -> Natural -> Maybe Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
          | Bool
otherwise                                = Maybe Natural
forall a. Maybe a
Nothing

-- | Takes [T1, ..., Tn-1] Tn and returns (T1 -> (T2 -> ... (T(n-1) -> Tn) ...))
mkArrowTy :: [Ty] -> Ty -> Ty
mkArrowTy :: [Ty] -> Ty -> Ty
mkArrowTy [Ty]
ps = (Ty -> Ty -> Ty) -> [Ty] -> Ty
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Ty -> Ty -> Ty
arr ([Ty] -> Ty) -> (Ty -> [Ty]) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Ty]
ps [Ty] -> [Ty] -> [Ty]
forall a. [a] -> [a] -> [a]
++) ([Ty] -> [Ty]) -> (Ty -> [Ty]) -> Ty -> [Ty]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: [])

mkTyApp :: Annote -> Ty -> [Ty] -> Ty
mkTyApp :: Annote -> Ty -> [Ty] -> Ty
mkTyApp Annote
_ Ty
f []     = Ty
f
mkTyApp Annote
ann Ty
f [Ty]
args = (Ty -> Ty -> Ty) -> Ty -> [Ty] -> Ty
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Ty
acc Ty
x -> Annote -> Ty -> [Ty] -> Ty
TyApp Annote
ann Ty
acc [Ty
x]) Ty
f [Ty]
args

nilTy :: Ty
nilTy :: Ty
nilTy = Annote -> TyBuiltin -> Ty
TyBuiltin (Text -> Annote
MsgAnnote Text
"nilTy") TyBuiltin
TyUnit

pairTy :: Annote -> Ty -> Ty -> Ty
pairTy :: Annote -> Ty -> Ty -> Ty
pairTy Annote
an Ty
t1 Ty
t2 = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an (Annote -> TyBuiltin -> Ty
TyBuiltin Annote
an TyBuiltin
TyProd) [Ty
t1,Ty
t2]

tupleTy :: Annote -> [Ty] -> Ty
tupleTy :: Annote -> [Ty] -> Ty
tupleTy = Annote -> [Ty] -> Ty
TyTuple

isReacT :: Ty -> Bool
isReacT :: Ty -> Bool
isReacT = Maybe (Ty, Ty, [Ty], Ty) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Ty, Ty, [Ty], Ty) -> Bool)
-> (Ty -> Maybe (Ty, Ty, [Ty], Ty)) -> Ty -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Maybe (Ty, Ty, [Ty], Ty)
dstReacT (Ty -> Maybe (Ty, Ty, [Ty], Ty))
-> (Ty -> Ty) -> Ty -> Maybe (Ty, Ty, [Ty], Ty)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Ty
rangeTy

resInputTy :: Ty -> Maybe Ty
resInputTy :: Ty -> Maybe Ty
resInputTy Ty
ty = case Ty -> Ty
rangeTy Ty
ty of
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyReacT) (Ty
i : [Ty]
_) -> Ty -> Maybe Ty
forall a. a -> Maybe a
Just Ty
i
      Ty
_                                     -> Maybe Ty
forall a. Maybe a
Nothing

isStateT :: Ty -> Bool
isStateT :: Ty -> Bool
isStateT Ty
ty = case Ty -> Ty
rangeTy Ty
ty of
      TyApp Annote
an (TyBuiltin Annote
_ TyBuiltin
TyStateT) [Ty
_,Ty
m,Ty
a] -> Ty -> Bool
isStateT (Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an Ty
m [Ty
a])
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyIdentity) [Ty]
_      -> Bool
True
      Ty
_                                       -> Bool
False

-- | This takes a type of the form
--
-- >  StateT S1 (StateT S2 (... (StateT Sm I)))
--
-- and returns
--
-- >  [S1, ..., Sm]
dstStateT :: Ty -> Maybe [Ty]
dstStateT :: Ty -> Maybe [Ty]
dstStateT = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyStateT) (Ty
s:Ty
m:[Ty]
_) -> (Ty
s Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
:) ([Ty] -> [Ty]) -> Maybe [Ty] -> Maybe [Ty]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe [Ty]
dstStateT Ty
m
      TyBuiltin Annote
_ TyBuiltin
TyIdentity                 -> [Ty] -> Maybe [Ty]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      Ty
_                                      -> Maybe [Ty]
forall a. Maybe a
Nothing

-- | This takes a type of the form
--
-- >  m a
--
-- and returns
--
-- >  Just (m, a)
dstTyApp :: Ty -> Maybe (Ty, Ty)
dstTyApp :: Ty -> Maybe (Ty, Ty)
dstTyApp = \ case
      TyApp Annote
_ Ty
m [Ty
a]     -> (Ty, Ty) -> Maybe (Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
m,Ty
a)
      TyApp Annote
an Ty
m (Ty
a:[Ty]
as) -> (Ty, Ty) -> Maybe (Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
m,Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an Ty
a [Ty]
as)
      Ty
_                 -> Maybe (Ty, Ty)
forall a. Maybe a
Nothing

dstTyBinOp :: Ty -> Maybe (Text, Ty, Ty)
dstTyBinOp :: Ty -> Maybe (Text, Ty, Ty)
dstTyBinOp = \ case
      TyApp Annote
_ (TyCon Annote
_ Text
op) [Ty
t1,Ty
t2]         -> (Text, Ty, Ty) -> Maybe (Text, Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
op, Ty
t1, Ty
t2)
      TyApp Annote
an (TyCon Annote
_ Text
op) (Ty
t1:Ty
t2:[Ty]
ts)     -> (Text, Ty, Ty) -> Maybe (Text, Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
op, Ty
t1, Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an Ty
t2 [Ty]
ts)
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
op) [Ty
t1,Ty
t2]     -> (Text, Ty, Ty) -> Maybe (Text, Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyBuiltin -> Text
tb2s TyBuiltin
op, Ty
t1, Ty
t2)
      TyApp Annote
an (TyBuiltin Annote
_ TyBuiltin
op) (Ty
t1:Ty
t2:[Ty]
ts) -> (Text, Ty, Ty) -> Maybe (Text, Ty, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyBuiltin -> Text
tb2s TyBuiltin
op, Ty
t1, Annote -> Ty -> [Ty] -> Ty
TyApp Annote
an Ty
t2 [Ty]
ts)
      Ty
_                                    -> Maybe (Text, Ty, Ty)
forall a. Maybe a
Nothing

-- | This takes a type of the form
--
-- >  ReacT In Out (StateT S1 (StateT S2 (... (StateT Sm I)))) T
--
-- and returns
--
-- >  (In, Out, [S1, ..., Sm], T)
dstReacT :: Ty -> Maybe (Ty, Ty, [Ty], Ty)
dstReacT :: Ty -> Maybe (Ty, Ty, [Ty], Ty)
dstReacT = \ case
      TyApp Annote
_ (TyBuiltin Annote
_ TyBuiltin
TyReacT) [Ty
i, Ty
o, Ty
m, Ty
a] -> Ty -> Maybe [Ty]
dstStateT Ty
m Maybe [Ty]
-> ([Ty] -> Maybe (Ty, Ty, [Ty], Ty)) -> Maybe (Ty, Ty, [Ty], Ty)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [Ty]
ms -> (Ty, Ty, [Ty], Ty) -> Maybe (Ty, Ty, [Ty], Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
i, Ty
o, [Ty]
ms, Ty
a)
      Ty
_                                          -> Maybe (Ty, Ty, [Ty], Ty)
forall a. Maybe a
Nothing


-- | Types containing no type variables (or blanks).
concrete :: Ty -> Bool
concrete :: Ty -> Bool
concrete = \ case
      TyVar {}    -> Bool
False
      TyCon {}    -> Bool
True
      TyBuiltin {} -> Bool
True
      TyNat {}    -> Bool
True
      TyTuple Annote
_ [Ty]
ts -> (Ty -> Bool) -> [Ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ty -> Bool
concrete [Ty]
ts
      TyApp Annote
_ Ty
a [Ty]
bs -> Ty -> Bool
concrete Ty
a Bool -> Bool -> Bool
&& (Ty -> Bool) -> [Ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ty -> Bool
concrete [Ty]
bs

-- | Types with no built-ins (Strings, Integers, lists).
fundamental :: Ty -> Bool
fundamental :: Ty -> Bool
fundamental = \ case
      TyBuiltin Annote
_ TyBuiltin
TyString  -> Bool
False
      TyBuiltin Annote
_ TyBuiltin
TyInteger -> Bool
False
      TyBuiltin Annote
_ TyBuiltin
TyList    -> Bool
False
      TyNat {}              -> Bool
True
      TyCon {}              -> Bool
True
      TyBuiltin {}          -> Bool
True
      TyVar {}              -> Bool
True
      TyTuple Annote
_ [Ty]
ts          -> (Ty -> Bool) -> [Ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ty -> Bool
fundamental [Ty]
ts
      TyApp Annote
_ Ty
a [Ty]
bs          -> Ty -> Bool
fundamental Ty
a Bool -> Bool -> Bool
&& (Ty -> Bool) -> [Ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ty -> Bool
fundamental [Ty]
bs

higherOrder :: Ty -> Bool
higherOrder :: Ty -> Bool
higherOrder (Ty -> ([Ty], Ty)
flattenSig -> ([Ty]
ats, Ty
rt)) = (Ty -> Bool) -> [Ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Ty -> Bool
isArrow ([Ty] -> Bool) -> [Ty] -> Bool
forall a b. (a -> b) -> a -> b
$ Ty
rt Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: [Ty]
ats

-- | Degree-1 polynomial with rational coefficients.
data Poly1 = Poly1 Rational (HashMap Text Rational)
      deriving (Int -> Poly1 -> ShowS
[Poly1] -> ShowS
Poly1 -> String
(Int -> Poly1 -> ShowS)
-> (Poly1 -> String) -> ([Poly1] -> ShowS) -> Show Poly1
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Poly1 -> ShowS
showsPrec :: Int -> Poly1 -> ShowS
$cshow :: Poly1 -> String
show :: Poly1 -> String
$cshowList :: [Poly1] -> ShowS
showList :: [Poly1] -> ShowS
Show)

instance Eq Poly1 where
      (Poly1 -> Poly1
normP1 -> Poly1 Rational
r HashMap Text Rational
cs) == :: Poly1 -> Poly1 -> Bool
== (Poly1 -> Poly1
normP1 -> Poly1 Rational
r' HashMap Text Rational
cs') = Rational
r Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
r' Bool -> Bool -> Bool
&& HashMap Text Rational
cs HashMap Text Rational -> HashMap Text Rational -> Bool
forall a. Eq a => a -> a -> Bool
== HashMap Text Rational
cs'

instance Pretty Poly1 where
      pretty :: forall ann. Poly1 -> Doc ann
pretty = \ case
            (Poly1 -> Poly1
normP1 -> Poly1 Rational
r (HashMap Text Rational -> [(Text, Rational)]
forall k v. HashMap k v -> [(k, v)]
Map.toList -> [(Text, Rational)]
cs)) | Rational
r Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
" +") ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ ((Text, Rational) -> Doc ann) -> [(Text, Rational)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Rational) -> Doc ann
forall a. (Text, Rational) -> Doc a
pretty' [(Text, Rational)]
cs
            (Poly1 -> Poly1
normP1 -> Poly1 Rational
r (HashMap Text Rational -> [(Text, Rational)]
forall k v. HashMap k v -> [(k, v)]
Map.toList -> [(Text, Rational)]
cs))          -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
" +") ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Rational -> Doc ann
forall a. Rational -> Doc a
rat Rational
r Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: ((Text, Rational) -> Doc ann) -> [(Text, Rational)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Rational) -> Doc ann
forall a. (Text, Rational) -> Doc a
pretty' [(Text, Rational)]
cs
            where pretty' :: (Text, Rational) -> Doc a
                  pretty' :: forall a. (Text, Rational) -> Doc a
pretty' (Text
x, Rational
cx) | Rational
cx Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
1   = Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty Text
x
                                  | Bool
otherwise = Rational -> Doc a
forall a. Rational -> Doc a
rat Rational
cx Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty Text
x

                  rat :: Rational -> Doc a
                  rat :: forall a. Rational -> Doc a
rat Rational
r | Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = Text -> Doc a
forall ann. Text -> Doc ann
text (Text -> Doc a) -> Text -> Doc a
forall a b. (a -> b) -> a -> b
$ Integer -> Text
forall a. TextShow a => a -> Text
showt (Integer -> Text) -> Integer -> Text
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
                        | Bool
otherwise          = Doc a -> Doc a
forall ann. Doc ann -> Doc ann
parens (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ Text -> Doc a
forall ann. Text -> Doc ann
text (Text -> Doc a) -> Text -> Doc a
forall a b. (a -> b) -> a -> b
$ Rational -> Text
forall a. TextShow a => a -> Text
showt Rational
r

zeroP1 :: Poly1
zeroP1 :: Poly1
zeroP1 = Rational -> HashMap Text Rational -> Poly1
Poly1 Rational
0 HashMap Text Rational
forall a. Monoid a => a
mempty

normP1 :: Poly1 -> Poly1
normP1 :: Poly1 -> Poly1
normP1 (Poly1 Rational
r HashMap Text Rational
cs) = Rational -> HashMap Text Rational -> Poly1
Poly1 Rational
r (HashMap Text Rational -> Poly1) -> HashMap Text Rational -> Poly1
forall a b. (a -> b) -> a -> b
$ (Rational -> Bool)
-> HashMap Text Rational -> HashMap Text Rational
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
Map.filter (Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0) HashMap Text Rational
cs

monoP1 :: Rational -> Maybe Text -> Poly1
monoP1 :: Rational -> Maybe Text -> Poly1
monoP1 Rational
r = \ case
      Just Text
x  -> Rational -> HashMap Text Rational -> Poly1
Poly1 Rational
0 (HashMap Text Rational -> Poly1) -> HashMap Text Rational -> Poly1
forall a b. (a -> b) -> a -> b
$ Text -> Rational -> HashMap Text Rational
forall k v. Hashable k => k -> v -> HashMap k v
Map.singleton Text
x Rational
r
      Maybe Text
Nothing -> Rational -> HashMap Text Rational -> Poly1
Poly1 Rational
r HashMap Text Rational
forall a. Monoid a => a
mempty

minusP1 :: Poly1 -> Poly1 -> Poly1
minusP1 :: Poly1 -> Poly1 -> Poly1
minusP1 Poly1
p1 Poly1
p2 = Poly1 -> Poly1 -> Poly1
plusP1 Poly1
p1 (Poly1 -> Poly1) -> Poly1 -> Poly1
forall a b. (a -> b) -> a -> b
$ Rational -> Poly1 -> Poly1
multP1 (-Rational
1) Poly1
p2

plusP1 :: Poly1 -> Poly1 -> Poly1
plusP1 :: Poly1 -> Poly1 -> Poly1
plusP1 (Poly1 Rational
r HashMap Text Rational
cs) (Poly1 Rational
r' HashMap Text Rational
cs') = Poly1 -> Poly1
normP1 (Poly1 -> Poly1) -> Poly1 -> Poly1
forall a b. (a -> b) -> a -> b
$ Rational -> HashMap Text Rational -> Poly1
Poly1 (Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
r') (HashMap Text Rational -> Poly1) -> HashMap Text Rational -> Poly1
forall a b. (a -> b) -> a -> b
$ (Rational -> Rational -> Rational)
-> HashMap Text Rational
-> HashMap Text Rational
-> HashMap Text Rational
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
Map.unionWith Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+) HashMap Text Rational
cs HashMap Text Rational
cs'

multP1 :: Rational -> Poly1 -> Poly1
multP1 :: Rational -> Poly1 -> Poly1
multP1 Rational
r' (Poly1 Rational
r HashMap Text Rational
cs) = Rational -> HashMap Text Rational -> Poly1
Poly1 (Rational
r' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
r) (HashMap Text Rational -> Poly1) -> HashMap Text Rational -> Poly1
forall a b. (a -> b) -> a -> b
$ (Rational -> Rational)
-> HashMap Text Rational -> HashMap Text Rational
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
Map.map (Rational
r' Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
*) HashMap Text Rational
cs

pickVar :: Poly1 -> Maybe (Text, Poly1)
pickVar :: Poly1 -> Maybe (Text, Poly1)
pickVar = Poly1 -> Maybe (Text, Poly1)
pickVar' (Poly1 -> Maybe (Text, Poly1))
-> (Poly1 -> Poly1) -> Poly1 -> Maybe (Text, Poly1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly1 -> Poly1
normP1
      where pickVar' :: Poly1 -> Maybe (Text, Poly1)
            pickVar' :: Poly1 -> Maybe (Text, Poly1)
pickVar' Poly1
p | ((Text
x, Rational
cx) : [(Text, Rational)]
cs) <- Poly1 -> [(Text, Rational)]
vars Poly1
p = (Text, Poly1) -> Maybe (Text, Poly1)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
x, Rational -> Poly1 -> Poly1
multP1 ((-Rational
1) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
cx) (Poly1 -> Poly1) -> Poly1 -> Poly1
forall a b. (a -> b) -> a -> b
$ HashMap Text Rational -> Poly1 -> Poly1
setCoeffs ([(Text, Rational)] -> HashMap Text Rational
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [(Text, Rational)]
cs) Poly1
p)
                       | Bool
otherwise                = Maybe (Text, Poly1)
forall a. Maybe a
Nothing

            vars :: Poly1 -> [(Text, Rational)]
            vars :: Poly1 -> [(Text, Rational)]
vars (Poly1 Rational
_ HashMap Text Rational
cs) = [(Text, Rational)] -> [(Text, Rational)]
sort' ([(Text, Rational)] -> [(Text, Rational)])
-> [(Text, Rational)] -> [(Text, Rational)]
forall a b. (a -> b) -> a -> b
$ HashMap Text Rational -> [(Text, Rational)]
forall k v. HashMap k v -> [(k, v)]
Map.toList HashMap Text Rational
cs

            setCoeffs :: HashMap Text Rational -> Poly1 -> Poly1
            setCoeffs :: HashMap Text Rational -> Poly1 -> Poly1
setCoeffs HashMap Text Rational
cs (Poly1 Rational
r HashMap Text Rational
_) = Rational -> HashMap Text Rational -> Poly1
Poly1 Rational
r HashMap Text Rational
cs

            sort' :: [(Text, Rational)] -> [(Text, Rational)]
            sort' :: [(Text, Rational)] -> [(Text, Rational)]
sort' = ((Text, Rational) -> Int)
-> [(Text, Rational)] -> [(Text, Rational)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (String -> Int
forall a. Hashable a => a -> Int
hash (String -> Int)
-> ((Text, Rational) -> String) -> (Text, Rational) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. Show a => a -> String
show (Text -> String)
-> ((Text, Rational) -> Text) -> (Text, Rational) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Rational) -> Text
forall a b. (a, b) -> a
fst)

poly1Ty :: Poly1 -> Ty
poly1Ty :: Poly1 -> Ty
poly1Ty (Poly1 Rational
r HashMap Text Rational
cs) | ((Text, Rational)
c : [(Text, Rational)]
cs') <- HashMap Text Rational -> [(Text, Rational)]
forall k v. HashMap k v -> [(k, v)]
Map.toList HashMap Text Rational
cs, Rational
r Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 = ((Text, Rational) -> Ty -> Ty) -> Ty -> [(Text, Rational)] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Ty -> Ty -> Ty
plus' (Ty -> Ty -> Ty)
-> ((Text, Rational) -> Ty) -> (Text, Rational) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Rational) -> Ty
mono) ((Text, Rational) -> Ty
mono (Text, Rational)
c) [(Text, Rational)]
cs'
                     | ((Text, Rational)
c : [(Text, Rational)]
cs') <- HashMap Text Rational -> [(Text, Rational)]
forall k v. HashMap k v -> [(k, v)]
Map.toList HashMap Text Rational
cs         = Rational -> Ty
ratTy Rational
r Ty -> Ty -> Ty
`plus'` ((Text, Rational) -> Ty -> Ty) -> Ty -> [(Text, Rational)] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Ty -> Ty -> Ty
plus' (Ty -> Ty -> Ty)
-> ((Text, Rational) -> Ty) -> (Text, Rational) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Rational) -> Ty
mono) ((Text, Rational) -> Ty
mono (Text, Rational)
c) [(Text, Rational)]
cs'
                     | Bool
otherwise                          = Rational -> Ty
ratTy Rational
r
      where mono :: (Text, Rational) -> Ty
            mono :: (Text, Rational) -> Ty
mono (Text
x, Rational
cx) | Rational
cx Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
1   = Text -> Ty
tyVar Text
x
                         | Bool
otherwise = Rational -> Ty -> Ty
multTy Rational
cx (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Text -> Ty
tyVar Text
x

            plus' :: Ty -> Ty -> Ty
            plus' :: Ty -> Ty -> Ty
plus' = Annote -> Ty -> Ty -> Ty
plusTy' Annote
noAnn

            tyVar :: Text -> Ty
            tyVar :: Text -> Ty
tyVar = Annote -> Text -> Ty
TyVar Annote
noAnn

ratTy :: Rational -> Ty
ratTy :: Rational -> Ty
ratTy Rational
r | Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0              = Annote -> Ty -> Ty
negTy Annote
noAnn (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Rational -> Ty
posRatTy (-Rational
r)
        | Bool
otherwise          = Rational -> Ty
posRatTy Rational
r
      where posRatTy :: Rational -> Ty
            posRatTy :: Rational -> Ty
posRatTy Rational
r' | Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = Annote -> Natural -> Ty
TyNat Annote
noAnn (Natural -> Ty) -> Natural -> Ty
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r'
                        | Bool
otherwise           = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
noAnn (Annote -> Text -> Ty
TyCon Annote
noAnn Text
"/") 
                                                  [Annote -> Natural -> Ty
TyNat Annote
noAnn (Natural -> Ty) -> Natural -> Ty
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r'
                                                  , Annote -> Natural -> Ty
TyNat Annote
noAnn (Natural -> Ty) -> Natural -> Ty
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r']

multTy :: Rational -> Ty -> Ty
multTy :: Rational -> Ty -> Ty
multTy Rational
r Ty
t = Annote -> Ty -> [Ty] -> Ty
TyApp Annote
noAnn (Annote -> Text -> Ty
TyCon Annote
noAnn Text
"*") [Rational -> Ty
ratTy Rational
r,Ty
t]

dstRat :: Ty -> Maybe Rational
dstRat :: Ty -> Maybe Rational
dstRat = \ case
      TyNat Annote
_ Natural
n             -> Rational -> Maybe Rational
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n
      (Ty -> Maybe Ty
dstNegTy -> Just Ty
t') -> ((-Rational
1) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
*) (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe Rational
dstRat Ty
t'
      (Ty -> Maybe (Text, Ty, Ty)
dstTyBinOp -> Just (Text
"/", TyNat Annote
_ Natural
a, TyNat Annote
_ Natural
b))
                            -> Rational -> Maybe Rational
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
b
      Ty
_                     -> Maybe Rational
forall a. Maybe a
Nothing

dstPoly1 :: Ty -> Maybe Poly1
dstPoly1 :: Ty -> Maybe Poly1
dstPoly1 = \ case
      TyNat Annote
_ Natural
n               -> Poly1 -> Maybe Poly1
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Poly1 -> Maybe Poly1) -> Poly1 -> Maybe Poly1
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Text -> Poly1
monoP1 (Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) Maybe Text
forall a. Maybe a
Nothing
      TyVar Annote
_ Text
x             -> Poly1 -> Maybe Poly1
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Poly1 -> Maybe Poly1) -> Poly1 -> Maybe Poly1
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Text -> Poly1
monoP1 Rational
1 (Maybe Text -> Poly1) -> Maybe Text -> Poly1
forall a b. (a -> b) -> a -> b
$ Text -> Maybe Text
forall a. a -> Maybe a
Just Text
x
      (Ty -> Maybe Ty
dstNegTy -> Just Ty
t)    -> Rational -> Poly1 -> Poly1
multP1 (-Rational
1) (Poly1 -> Poly1) -> Maybe Poly1 -> Maybe Poly1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe Poly1
dstPoly1 Ty
t
      (Ty -> Maybe (Ty, Ty)
dstPlusTy -> Just (Ty
t1, Ty
t2)) -> Poly1 -> Poly1 -> Poly1
plusP1 (Poly1 -> Poly1 -> Poly1) -> Maybe Poly1 -> Maybe (Poly1 -> Poly1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe Poly1
dstPoly1 Ty
t1 Maybe (Poly1 -> Poly1) -> Maybe Poly1 -> Maybe Poly1
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ty -> Maybe Poly1
dstPoly1 Ty
t2
      (Ty -> Maybe (Rational, Ty)
rmult -> Just (Rational
r, Ty
t))  -> Rational -> Poly1 -> Poly1
multP1 Rational
r (Poly1 -> Poly1) -> Maybe Poly1 -> Maybe Poly1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe Poly1
dstPoly1 Ty
t
      (Ty -> Maybe (Ty, Rational)
rdiv -> Just (Ty
t, Rational
r))   -> Rational -> Poly1 -> Poly1
multP1 (Rational
1Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/Rational
r) (Poly1 -> Poly1) -> Maybe Poly1 -> Maybe Poly1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ty -> Maybe Poly1
dstPoly1 Ty
t
      Ty
_                       -> Maybe Poly1
forall a. Maybe a
Nothing
      where rmult :: Ty -> Maybe (Rational, Ty)
            rmult :: Ty -> Maybe (Rational, Ty)
rmult = \ case
                  (Ty -> Maybe (Text, Ty, Ty)
dstTyBinOp -> Just (Text
"*", Ty -> Maybe Rational
dstRat -> Just Rational
r, Ty
t)) -> (Rational, Ty) -> Maybe (Rational, Ty)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational
r, Ty
t)
                  Ty
_                                                      -> Maybe (Rational, Ty)
forall a. Maybe a
Nothing

            rdiv :: Ty -> Maybe (Ty, Rational)
            rdiv :: Ty -> Maybe (Ty, Rational)
rdiv = \ case
                  (Ty -> Maybe (Text, Ty, Ty)
dstTyBinOp -> Just (Text
"/", Ty
t, Ty -> Maybe Rational
dstRat -> Just Rational
r)) -> (Ty, Rational) -> Maybe (Ty, Rational)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty
t, Rational
r)
                  Ty
_                                                      -> Maybe (Ty, Rational)
forall a. Maybe a
Nothing