module GF.Grammar.Macros where
import GF.Data.Operations
import GF.Data.Str
import GF.Infra.Ident
import GF.Grammar.Grammar
import GF.Grammar.Predef
import GF.Grammar.Printer
import Control.Monad.Identity(Identity(..))
import qualified Data.Traversable as T(mapM)
import qualified Data.Map as Map
import Control.Monad (liftM, liftM2, liftM3)
import Data.List (sortBy,nub)
import Data.Monoid
import GF.Text.Pretty(render,(<+>),hsep,fsep)
import qualified Control.Monad.Fail as Fail
typeForm :: Type -> (Context, Cat, [Term])
typeForm :: Type -> (Context, Cat, [Type])
typeForm Type
t =
case Type
t of
Prod BindType
b Ident
x Type
a Type
t ->
let (Context
x', Cat
cat, [Type]
args) = Type -> (Context, Cat, [Type])
typeForm Type
t
in ((BindType
b,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
x', Cat
cat, [Type]
args)
App Type
c Type
a ->
let (Context
_, Cat
cat, [Type]
args) = Type -> (Context, Cat, [Type])
typeForm Type
c
in ([],Cat
cat,[Type]
args [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
a])
Q Cat
c -> ([],Cat
c,[])
QC Cat
c -> ([],Cat
c,[])
Sort Ident
c -> ([],(Ident -> ModuleName
MN Ident
identW, Ident
c),[])
Type
_ -> [Char] -> (Context, Cat, [Type])
forall a. HasCallStack => [Char] -> a
error (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"no normal form of type" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t))
typeFormCnc :: Type -> (Context, Type)
typeFormCnc :: Type -> (Context, Type)
typeFormCnc Type
t =
case Type
t of
Prod BindType
b Ident
x Type
a Type
t -> let (Context
x', Type
v) = Type -> (Context, Type)
typeFormCnc Type
t
in ((BindType
b,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
x',Type
v)
Type
_ -> ([],Type
t)
valCat :: Type -> Cat
valCat :: Type -> Cat
valCat Type
typ =
let (Context
_,Cat
cat,[Type]
_) = Type -> (Context, Cat, [Type])
typeForm Type
typ
in Cat
cat
valType :: Type -> Type
valType :: Type -> Type
valType Type
typ =
let (Context
_,Cat
cat,[Type]
xx) = Type -> (Context, Cat, [Type])
typeForm Type
typ
in Type -> [Type] -> Type
mkApp (Cat -> Type
Q Cat
cat) [Type]
xx
valTypeCnc :: Type -> Type
valTypeCnc :: Type -> Type
valTypeCnc Type
typ = (Context, Type) -> Type
forall a b. (a, b) -> b
snd (Type -> (Context, Type)
typeFormCnc Type
typ)
typeSkeleton :: Type -> ([(Int,Cat)],Cat)
typeSkeleton :: Type -> ([(Int, Cat)], Cat)
typeSkeleton Type
typ =
let (Context
ctxt,Cat
cat,[Type]
_) = Type -> (Context, Cat, [Type])
typeForm Type
typ
in ([([(Int, Cat)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, Cat)]
c, Cat
v) | (BindType
b,Ident
x,Type
t) <- Context
ctxt, let ([(Int, Cat)]
c,Cat
v) = Type -> ([(Int, Cat)], Cat)
typeSkeleton Type
t], Cat
cat)
catSkeleton :: Type -> ([Cat],Cat)
catSkeleton :: Type -> ([Cat], Cat)
catSkeleton Type
typ =
let ([(Int, Cat)]
args,Cat
val) = Type -> ([(Int, Cat)], Cat)
typeSkeleton Type
typ
in (((Int, Cat) -> Cat) -> [(Int, Cat)] -> [Cat]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Cat) -> Cat
forall a b. (a, b) -> b
snd [(Int, Cat)]
args, Cat
val)
funsToAndFrom :: Type -> (Cat, [(Cat,[Int])])
funsToAndFrom :: Type -> (Cat, [(Cat, [Int])])
funsToAndFrom Type
t =
let ([Cat]
cs,Cat
v) = Type -> ([Cat], Cat)
catSkeleton Type
t
cis :: [(Cat, Int)]
cis = [Cat] -> [Int] -> [(Cat, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Cat]
cs [Int
0..]
in (Cat
v, [(Cat
c,[Int
i | (Cat
c',Int
i) <- [(Cat, Int)]
cis, Cat
c' Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
c]) | Cat
c <- [Cat]
cs])
isRecursiveType :: Type -> Bool
isRecursiveType :: Type -> Bool
isRecursiveType Type
t =
let ([Cat]
cc,Cat
c) = Type -> ([Cat], Cat)
catSkeleton Type
t
in (Cat -> Bool) -> [Cat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
c) [Cat]
cc
isHigherOrderType :: Type -> Bool
isHigherOrderType :: Type -> Bool
isHigherOrderType Type
t = Bool -> Err Bool -> Bool
forall a. a -> Err a -> a
fromErr Bool
True (Err Bool -> Bool) -> Err Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
Context
co <- Type -> Err Context
forall (m :: * -> *). Monad m => Type -> m Context
contextOfType Type
t
Bool -> Err Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Err Bool) -> Bool -> Err Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Ident] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ident
x | (BindType
_,Ident
x,Prod BindType
_ Ident
_ Type
_ Type
_) <- Context
co]
contextOfType :: Monad m => Type -> m Context
contextOfType :: Type -> m Context
contextOfType Type
typ = case Type
typ of
Prod BindType
b Ident
x Type
a Type
t -> (Context -> Context) -> m Context -> m Context
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((BindType
b,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:) (m Context -> m Context) -> m Context -> m Context
forall a b. (a -> b) -> a -> b
$ Type -> m Context
forall (m :: * -> *). Monad m => Type -> m Context
contextOfType Type
t
Type
_ -> Context -> m Context
forall (m :: * -> *) a. Monad m => a -> m a
return []
termForm :: Monad m => Term -> m ([(BindType,Ident)], Term, [Term])
termForm :: Type -> m ([(BindType, Ident)], Type, [Type])
termForm Type
t = case Type
t of
Abs BindType
b Ident
x Type
t ->
do ([(BindType, Ident)]
x', Type
fun, [Type]
args) <- Type -> m ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *).
Monad m =>
Type -> m ([(BindType, Ident)], Type, [Type])
termForm Type
t
([(BindType, Ident)], Type, [Type])
-> m ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ((BindType
b,Ident
x)(BindType, Ident) -> [(BindType, Ident)] -> [(BindType, Ident)]
forall a. a -> [a] -> [a]
:[(BindType, Ident)]
x', Type
fun, [Type]
args)
App Type
c Type
a ->
do ([(BindType, Ident)]
_,Type
fun, [Type]
args) <- Type -> m ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *).
Monad m =>
Type -> m ([(BindType, Ident)], Type, [Type])
termForm Type
c
([(BindType, Ident)], Type, [Type])
-> m ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Type
fun,[Type]
args [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
a])
Type
_ ->
([(BindType, Ident)], Type, [Type])
-> m ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Type
t,[])
termFormCnc :: Term -> ([(BindType,Ident)], Term)
termFormCnc :: Type -> ([(BindType, Ident)], Type)
termFormCnc Type
t = case Type
t of
Abs BindType
b Ident
x Type
t -> ((BindType
b,Ident
x)(BindType, Ident) -> [(BindType, Ident)] -> [(BindType, Ident)]
forall a. a -> [a] -> [a]
:[(BindType, Ident)]
xs, Type
t') where ([(BindType, Ident)]
xs,Type
t') = Type -> ([(BindType, Ident)], Type)
termFormCnc Type
t
Type
_ -> ([],Type
t)
appForm :: Term -> (Term, [Term])
appForm :: Type -> (Type, [Type])
appForm Type
t = case Type
t of
App Type
c Type
a -> (Type
fun, [Type]
args [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
a]) where (Type
fun, [Type]
args) = Type -> (Type, [Type])
appForm Type
c
Typed Type
t Type
_ -> Type -> (Type, [Type])
appForm Type
t
Type
_ -> (Type
t,[])
mkProdSimple :: Context -> Term -> Term
mkProdSimple :: Context -> Type -> Type
mkProdSimple Context
c Type
t = Context -> Type -> [Type] -> Type
mkProd Context
c Type
t []
mkProd :: Context -> Term -> [Term] -> Term
mkProd :: Context -> Type -> [Type] -> Type
mkProd [] Type
typ [Type]
args = Type -> [Type] -> Type
mkApp Type
typ [Type]
args
mkProd ((BindType
b,Ident
x,Type
a):Context
dd) Type
typ [Type]
args = BindType -> Ident -> Type -> Type -> Type
Prod BindType
b Ident
x Type
a (Context -> Type -> [Type] -> Type
mkProd Context
dd Type
typ [Type]
args)
mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
mkTerm :: ([(BindType, Ident)], Type, [Type]) -> Type
mkTerm ([(BindType, Ident)]
xx,Type
t,[Type]
aa) = [(BindType, Ident)] -> Type -> Type
mkAbs [(BindType, Ident)]
xx (Type -> [Type] -> Type
mkApp Type
t [Type]
aa)
mkApp :: Term -> [Term] -> Term
mkApp :: Type -> [Type] -> Type
mkApp = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
App
mkAbs :: [(BindType,Ident)] -> Term -> Term
mkAbs :: [(BindType, Ident)] -> Type -> Type
mkAbs [(BindType, Ident)]
xx Type
t = ((BindType, Ident) -> Type -> Type)
-> Type -> [(BindType, Ident)] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((BindType -> Ident -> Type -> Type)
-> (BindType, Ident) -> Type -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry BindType -> Ident -> Type -> Type
Abs) Type
t [(BindType, Ident)]
xx
appCons :: Ident -> [Term] -> Term
appCons :: Ident -> [Type] -> Type
appCons = Type -> [Type] -> Type
mkApp (Type -> [Type] -> Type)
-> (Ident -> Type) -> Ident -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident -> Type
Cn
mkLet :: [LocalDef] -> Term -> Term
mkLet :: [LocalDef] -> Type -> Type
mkLet [LocalDef]
defs Type
t = (LocalDef -> Type -> Type) -> Type -> [LocalDef] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr LocalDef -> Type -> Type
Let Type
t [LocalDef]
defs
mkLetUntyped :: Context -> Term -> Term
mkLetUntyped :: Context -> Type -> Type
mkLetUntyped Context
defs = [LocalDef] -> Type -> Type
mkLet [(Ident
x,(Maybe Type
forall a. Maybe a
Nothing,Type
t)) | (BindType
_,Ident
x,Type
t) <- Context
defs]
isVariable :: Term -> Bool
isVariable :: Type -> Bool
isVariable (Vr Ident
_ ) = Bool
True
isVariable Type
_ = Bool
False
uType :: Type
uType :: Type
uType = Ident -> Type
Cn Ident
cUndefinedType
assign :: Label -> Term -> Assign
assign :: Label -> Type -> Assign
assign Label
l Type
t = (Label
l,(Maybe Type
forall a. Maybe a
Nothing,Type
t))
assignT :: Label -> Type -> Term -> Assign
assignT :: Label -> Type -> Type -> Assign
assignT Label
l Type
a Type
t = (Label
l,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
a,Type
t))
unzipR :: [Assign] -> ([Label],[Term])
unzipR :: [Assign] -> ([Label], [Type])
unzipR [Assign]
r = ([Label]
ls, ((Maybe Type, Type) -> Type) -> [(Maybe Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type, Type) -> Type
forall a b. (a, b) -> b
snd [(Maybe Type, Type)]
ts) where ([Label]
ls,[(Maybe Type, Type)]
ts) = [Assign] -> ([Label], [(Maybe Type, Type)])
forall a b. [(a, b)] -> ([a], [b])
unzip [Assign]
r
mkAssign :: [(Label,Term)] -> [Assign]
mkAssign :: [(Label, Type)] -> [Assign]
mkAssign [(Label, Type)]
lts = [Label -> Type -> Assign
assign Label
l Type
t | (Label
l,Type
t) <- [(Label, Type)]
lts]
projectRec :: Label -> [Assign] -> Term
projectRec :: Label -> [Assign] -> Type
projectRec Label
l [Assign]
rs =
case Label -> [Assign] -> Maybe (Maybe Type, Type)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Assign]
rs of
Just (Maybe Type
_,Type
t) -> Type
t
Maybe (Maybe Type, Type)
Nothing -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"no value for label" [Char] -> Label -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Label
l))
zipAssign :: [Label] -> [Term] -> [Assign]
zipAssign :: [Label] -> [Type] -> [Assign]
zipAssign [Label]
ls [Type]
ts = [Label -> Type -> Assign
assign Label
l Type
t | (Label
l,Type
t) <- [Label] -> [Type] -> [(Label, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ls [Type]
ts]
mapAssignM :: Monad m => (Term -> m c) -> [Assign] -> m [(Label,(Maybe c,c))]
mapAssignM :: (Type -> m c) -> [Assign] -> m [(Label, (Maybe c, c))]
mapAssignM Type -> m c
f = (Assign -> m (Label, (Maybe c, c)))
-> [Assign] -> m [(Label, (Maybe c, c))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Label
ls,(Maybe Type, Type)
tv) -> ((Maybe c, c) -> (Label, (Maybe c, c)))
-> m (Maybe c, c) -> m (Label, (Maybe c, c))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((,) Label
ls) ((Maybe Type, Type) -> m (Maybe c, c)
g (Maybe Type, Type)
tv))
where g :: (Maybe Type, Type) -> m (Maybe c, c)
g (Maybe Type
t,Type
v) = (Maybe c -> c -> (Maybe c, c))
-> m (Maybe c) -> m c -> m (Maybe c, c)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (m (Maybe c) -> (Type -> m (Maybe c)) -> Maybe Type -> m (Maybe c)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe c -> m (Maybe c)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe c
forall a. Maybe a
Nothing) ((c -> Maybe c) -> m c -> m (Maybe c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM c -> Maybe c
forall a. a -> Maybe a
Just (m c -> m (Maybe c)) -> (Type -> m c) -> Type -> m (Maybe c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> m c
f) Maybe Type
t) (Type -> m c
f Type
v)
mkRecordN :: Int -> (Int -> Label) -> [Term] -> Term
mkRecordN :: Int -> (Int -> Label) -> [Type] -> Type
mkRecordN Int
int Int -> Label
lab [Type]
typs = [Assign] -> Type
R [ Label -> Type -> Assign
assign (Int -> Label
lab Int
i) Type
t | (Int
i,Type
t) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
int..] [Type]
typs]
mkRecord :: (Int -> Label) -> [Term] -> Term
mkRecord :: (Int -> Label) -> [Type] -> Type
mkRecord = Int -> (Int -> Label) -> [Type] -> Type
mkRecordN Int
0
mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type
mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type
mkRecTypeN Int
int Int -> Label
lab [Type]
typs = [(Label, Type)] -> Type
RecType [ (Int -> Label
lab Int
i, Type
t) | (Int
i,Type
t) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
int..] [Type]
typs]
mkRecType :: (Int -> Label) -> [Type] -> Type
mkRecType :: (Int -> Label) -> [Type] -> Type
mkRecType = Int -> (Int -> Label) -> [Type] -> Type
mkRecTypeN Int
0
record2subst :: Term -> Err Substitution
record2subst :: Type -> Err Substitution
record2subst Type
t = case Type
t of
R [Assign]
fs -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawIdent -> Ident
identC RawIdent
x, Type
t) | (LIdent RawIdent
x,(Maybe Type
_,Type
t)) <- [Assign]
fs]
Type
_ -> [Char] -> Err Substitution
forall a. [Char] -> Err a
Bad (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"record expected, found" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t))
typeType, typePType, typeStr, typeTok, typeStrs :: Type
typeType :: Type
typeType = Ident -> Type
Sort Ident
cType
typePType :: Type
typePType = Ident -> Type
Sort Ident
cPType
typeStr :: Type
typeStr = Ident -> Type
Sort Ident
cStr
typeTok :: Type
typeTok = Ident -> Type
Sort Ident
cTok
typeStrs :: Type
typeStrs = Ident -> Type
Sort Ident
cStrs
typeString, typeFloat, typeInt :: Type
typeInts :: Int -> Type
typePBool :: Type
typeError :: Type
typeString :: Type
typeString = Ident -> Type
cnPredef Ident
cString
typeInt :: Type
typeInt = Ident -> Type
cnPredef Ident
cInt
typeFloat :: Type
typeFloat = Ident -> Type
cnPredef Ident
cFloat
typeInts :: Int -> Type
typeInts Int
i = Type -> Type -> Type
App (Ident -> Type
cnPredef Ident
cInts) (Int -> Type
EInt Int
i)
typePBool :: Type
typePBool = Ident -> Type
cnPredef Ident
cPBool
typeError :: Type
typeError = Ident -> Type
cnPredef Ident
cErrorType
isTypeInts :: Type -> Maybe Int
isTypeInts :: Type -> Maybe Int
isTypeInts (App Type
c (EInt Int
i)) | Type
c Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Ident -> Type
cnPredef Ident
cInts = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
isTypeInts Type
_ = Maybe Int
forall a. Maybe a
Nothing
isPredefConstant :: Term -> Bool
isPredefConstant :: Type -> Bool
isPredefConstant Type
t = case Type
t of
Q (ModuleName
mod,Ident
_) | ModuleName
mod ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredef Bool -> Bool -> Bool
|| ModuleName
mod ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredefAbs -> Bool
True
Type
_ -> Bool
False
checkPredefError :: Fail.MonadFail m => Term -> m Term
checkPredefError :: Type -> m Type
checkPredefError Type
t =
case Type
t of
Error [Char]
s -> [Char] -> m Type
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Error: "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
s)
Type
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
cnPredef :: Ident -> Term
cnPredef :: Ident -> Type
cnPredef Ident
f = Cat -> Type
Q (ModuleName
cPredef,Ident
f)
mkSelects :: Term -> [Term] -> Term
mkSelects :: Type -> [Type] -> Type
mkSelects Type
t [Type]
tt = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
S Type
t [Type]
tt
mkTable :: [Term] -> Term -> Term
mkTable :: [Type] -> Type -> Type
mkTable [Type]
tt Type
t = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
Table Type
t [Type]
tt
mkCTable :: [(BindType,Ident)] -> Term -> Term
mkCTable :: [(BindType, Ident)] -> Type -> Type
mkCTable [(BindType, Ident)]
ids Type
v = ((BindType, Ident) -> Type -> Type)
-> Type -> [(BindType, Ident)] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (BindType, Ident) -> Type -> Type
forall a. (a, Ident) -> Type -> Type
ccase Type
v [(BindType, Ident)]
ids where
ccase :: (a, Ident) -> Type -> Type
ccase (a
_,Ident
x) Type
t = TInfo -> [Case] -> Type
T TInfo
TRaw [(Ident -> Patt
PV Ident
x,Type
t)]
mkHypo :: Term -> Hypo
mkHypo :: Type -> (BindType, Ident, Type)
mkHypo Type
typ = (BindType
Explicit,Ident
identW, Type
typ)
eqStrIdent :: Ident -> Ident -> Bool
eqStrIdent :: Ident -> Ident -> Bool
eqStrIdent = Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
(==)
tuple2record :: [Term] -> [Assign]
tuple2record :: [Type] -> [Assign]
tuple2record [Type]
ts = [Label -> Type -> Assign
assign (Int -> Label
tupleLabel Int
i) Type
t | (Int
i,Type
t) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Type]
ts]
tuple2recordType :: [Term] -> [Labelling]
tuple2recordType :: [Type] -> [(Label, Type)]
tuple2recordType [Type]
ts = [(Int -> Label
tupleLabel Int
i, Type
t) | (Int
i,Type
t) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Type]
ts]
tuple2recordPatt :: [Patt] -> [(Label,Patt)]
tuple2recordPatt :: [Patt] -> [(Label, Patt)]
tuple2recordPatt [Patt]
ts = [(Int -> Label
tupleLabel Int
i, Patt
t) | (Int
i,Patt
t) <- [Int] -> [Patt] -> [(Int, Patt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Patt]
ts]
mkCases :: Ident -> Term -> Term
mkCases :: Ident -> Type -> Type
mkCases Ident
x Type
t = TInfo -> [Case] -> Type
T TInfo
TRaw [(Ident -> Patt
PV Ident
x, Type
t)]
mkWildCases :: Term -> Term
mkWildCases :: Type -> Type
mkWildCases = Ident -> Type -> Type
mkCases Ident
identW
mkFunType :: [Type] -> Type -> Type
mkFunType :: [Type] -> Type -> Type
mkFunType [Type]
tt Type
t = Context -> Type -> [Type] -> Type
mkProd [(BindType
Explicit,Ident
identW, Type
ty) | Type
ty <- [Type]
tt] Type
t []
plusRecType :: Type -> Type -> m Type
plusRecType Type
t1 Type
t2 = case (Type
t1, Type
t2) of
(RecType [(Label, Type)]
r1, RecType [(Label, Type)]
r2) -> case
(Label -> Bool) -> [Label] -> [Label]
forall a. (a -> Bool) -> [a] -> [a]
filter (Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (((Label, Type) -> Label) -> [(Label, Type)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Type) -> Label
forall a b. (a, b) -> a
fst [(Label, Type)]
r1)) (((Label, Type) -> Label) -> [(Label, Type)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Type) -> Label
forall a b. (a, b) -> a
fst [(Label, Type)]
r2) of
[] -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Label, Type)] -> Type
RecType ([(Label, Type)]
r1 [(Label, Type)] -> [(Label, Type)] -> [(Label, Type)]
forall a. [a] -> [a] -> [a]
++ [(Label, Type)]
r2))
[Label]
ls -> [Char] -> m Type
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise ([Char] -> m Type) -> [Char] -> m Type
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"clashing labels" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Label] -> Doc
forall a. Pretty a => [a] -> Doc
hsep [Label]
ls)
(Type, Type)
_ -> [Char] -> m Type
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise ([Char] -> m Type) -> [Char] -> m Type
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"cannot add record types" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t1 Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"and" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t2)
plusRecord :: Type -> Type -> m Type
plusRecord Type
t1 Type
t2 =
case (Type
t1,Type
t2) of
(R [Assign]
r1, R [Assign]
r2 ) -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Assign] -> Type
R ([(Label
l,(Maybe Type, Type)
v) |
(Label
l,(Maybe Type, Type)
v) <- [Assign]
r1, Bool -> Bool
not (Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Label
l ((Assign -> Label) -> [Assign] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Assign -> Label
forall a b. (a, b) -> a
fst [Assign]
r2)) ] [Assign] -> [Assign] -> [Assign]
forall a. [a] -> [a] -> [a]
++ [Assign]
r2))
(Type
_, FV [Type]
rs) -> (Type -> m Type) -> [Type] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Type -> m Type
plusRecord Type
t1) [Type]
rs m [Type] -> ([Type] -> m Type) -> m Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> ([Type] -> Type) -> [Type] -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
FV
(FV [Type]
rs,Type
_ ) -> (Type -> m Type) -> [Type] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Type -> m Type
`plusRecord` Type
t2) [Type]
rs m [Type] -> ([Type] -> m Type) -> m Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> ([Type] -> Type) -> [Type] -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
FV
(Type, Type)
_ -> [Char] -> m Type
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise ([Char] -> m Type) -> [Char] -> m Type
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"cannot add records" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t1 Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"and" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t2)
defLinType :: Type
defLinType :: Type
defLinType = [(Label, Type)] -> Type
RecType [(Label
theLinLabel, Type
typeStr)]
mkFreshVar :: [Ident] -> Ident
mkFreshVar :: [Ident] -> Ident
mkFreshVar [Ident]
olds = Int -> Ident
varX ([Ident] -> Int
maxVarIndex [Ident]
olds Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
mkFreshVarX :: [Ident] -> Ident -> Ident
mkFreshVarX :: [Ident] -> Ident -> Ident
mkFreshVarX [Ident]
olds Ident
x = if (Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Ident
x [Ident]
olds) then (Int -> Ident
varX ([Ident] -> Int
maxVarIndex [Ident]
olds Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) else Ident
x
maxVarIndex :: [Ident] -> Int
maxVarIndex :: [Ident] -> Int
maxVarIndex = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> ([Ident] -> [Int]) -> [Ident] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((-Int
1)Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:) ([Int] -> [Int]) -> ([Ident] -> [Int]) -> [Ident] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident -> Int) -> [Ident] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Int
varIndex
mkFreshVars :: Int -> [Ident] -> [Ident]
mkFreshVars :: Int -> [Ident] -> [Ident]
mkFreshVars Int
n [Ident]
olds = [Int -> Ident
varX ([Ident] -> Int
maxVarIndex [Ident]
olds Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) | Int
i <- [Int
1..Int
n]]
freshAsTerm :: String -> Term
freshAsTerm :: [Char] -> Type
freshAsTerm [Char]
s = Ident -> Type
Vr (Int -> Ident
varX ([Char] -> Int
readIntArg [Char]
s))
string2term :: String -> Term
string2term :: [Char] -> Type
string2term = [Char] -> Type
K
int2term :: Int -> Term
int2term :: Int -> Type
int2term = Int -> Type
EInt
float2term :: Double -> Term
float2term :: Double -> Type
float2term = Double -> Type
EFloat
ident2terminal :: Ident -> Term
ident2terminal :: Ident -> Type
ident2terminal = [Char] -> Type
K ([Char] -> Type) -> (Ident -> [Char]) -> Ident -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident -> [Char]
showIdent
symbolOfIdent :: Ident -> String
symbolOfIdent :: Ident -> [Char]
symbolOfIdent = Ident -> [Char]
showIdent
symid :: Ident -> String
symid :: Ident -> [Char]
symid = Ident -> [Char]
symbolOfIdent
justIdentOf :: Term -> Maybe Ident
justIdentOf :: Type -> Maybe Ident
justIdentOf (Vr Ident
x) = Ident -> Maybe Ident
forall a. a -> Maybe a
Just Ident
x
justIdentOf (Cn Ident
x) = Ident -> Maybe Ident
forall a. a -> Maybe a
Just Ident
x
justIdentOf Type
_ = Maybe Ident
forall a. Maybe a
Nothing
linTypeStr :: Type
linTypeStr :: Type
linTypeStr = (Int -> Label) -> [Type] -> Type
mkRecType Int -> Label
linLabel [Type
typeStr]
linAsStr :: String -> Term
linAsStr :: [Char] -> Type
linAsStr [Char]
s = (Int -> Label) -> [Type] -> Type
mkRecord Int -> Label
linLabel [[Char] -> Type
K [Char]
s]
term2patt :: Term -> Err Patt
term2patt :: Type -> Err Patt
term2patt Type
trm = case Type -> Err ([(BindType, Ident)], Type, [Type])
forall (m :: * -> *).
Monad m =>
Type -> m ([(BindType, Ident)], Type, [Type])
termForm Type
trm of
Ok ([], Vr Ident
x, []) | Ident
x Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
identW -> Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return Patt
PW
| Bool
otherwise -> Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> Patt
PV Ident
x)
Ok ([], Con Ident
c, [Type]
aa) -> do
[Patt]
aa' <- (Type -> Err Patt) -> [Type] -> Err [Patt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err Patt
term2patt [Type]
aa
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> [Patt] -> Patt
PC Ident
c [Patt]
aa')
Ok ([], QC Cat
c, [Type]
aa) -> do
[Patt]
aa' <- (Type -> Err Patt) -> [Type] -> Err [Patt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err Patt
term2patt [Type]
aa
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Cat -> [Patt] -> Patt
PP Cat
c [Patt]
aa')
Ok ([], Q Cat
c, []) -> do
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Cat -> Patt
PM Cat
c)
Ok ([], R [Assign]
r, []) -> do
let ([Label]
ll,[Type]
aa) = [Assign] -> ([Label], [Type])
unzipR [Assign]
r
[Patt]
aa' <- (Type -> Err Patt) -> [Type] -> Err [Patt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err Patt
term2patt [Type]
aa
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Label, Patt)] -> Patt
PR ([Label] -> [Patt] -> [(Label, Patt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ll [Patt]
aa'))
Ok ([],EInt Int
i,[]) -> Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Err Patt) -> Patt -> Err Patt
forall a b. (a -> b) -> a -> b
$ Int -> Patt
PInt Int
i
Ok ([],EFloat Double
i,[]) -> Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Err Patt) -> Patt -> Err Patt
forall a b. (a -> b) -> a -> b
$ Double -> Patt
PFloat Double
i
Ok ([],K [Char]
s, []) -> Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Err Patt) -> Patt -> Err Patt
forall a b. (a -> b) -> a -> b
$ [Char] -> Patt
PString [Char]
s
Ok ([], Cn Ident
id, [Vr Ident
a,Type
b]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cAs -> do
Patt
b' <- Type -> Err Patt
term2patt Type
b
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> Patt -> Patt
PAs Ident
a Patt
b')
Ok ([], Cn Ident
id, [Type
a]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cNeg -> do
Patt
a' <- Type -> Err Patt
term2patt Type
a
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt
PNeg Patt
a')
Ok ([], Cn Ident
id, [Type
a]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cRep -> do
Patt
a' <- Type -> Err Patt
term2patt Type
a
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt
PRep Patt
a')
Ok ([], Cn Ident
id, []) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cRep -> do
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return Patt
PChar
Ok ([], Cn Ident
id,[K [Char]
s]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cChars -> do
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Err Patt) -> Patt -> Err Patt
forall a b. (a -> b) -> a -> b
$ [Char] -> Patt
PChars [Char]
s
Ok ([], Cn Ident
id, [Type
a,Type
b]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cSeq -> do
Patt
a' <- Type -> Err Patt
term2patt Type
a
Patt
b' <- Type -> Err Patt
term2patt Type
b
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt -> Patt
PSeq Patt
a' Patt
b')
Ok ([], Cn Ident
id, [Type
a,Type
b]) | Ident
id Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cAlt -> do
Patt
a' <- Type -> Err Patt
term2patt Type
a
Patt
b' <- Type -> Err Patt
term2patt Type
b
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt -> Patt
PAlt Patt
a' Patt
b')
Ok ([], Cn Ident
c, []) -> do
Patt -> Err Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> Patt
PMacro Ident
c)
Err ([(BindType, Ident)], Type, [Type])
_ -> [Char] -> Err Patt
forall a. [Char] -> Err a
Bad ([Char] -> Err Patt) -> [Char] -> Err Patt
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"no pattern corresponds to term" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
patt2term :: Patt -> Term
patt2term :: Patt -> Type
patt2term Patt
pt = case Patt
pt of
PV Ident
x -> Ident -> Type
Vr Ident
x
Patt
PW -> Ident -> Type
Vr Ident
identW
PMacro Ident
c -> Ident -> Type
Cn Ident
c
PM Cat
c -> Cat -> Type
Q Cat
c
PC Ident
c [Patt]
pp -> Type -> [Type] -> Type
mkApp (Ident -> Type
Con Ident
c) ((Patt -> Type) -> [Patt] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Patt -> Type
patt2term [Patt]
pp)
PP Cat
c [Patt]
pp -> Type -> [Type] -> Type
mkApp (Cat -> Type
QC Cat
c) ((Patt -> Type) -> [Patt] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Patt -> Type
patt2term [Patt]
pp)
PR [(Label, Patt)]
r -> [Assign] -> Type
R [Label -> Type -> Assign
assign Label
l (Patt -> Type
patt2term Patt
p) | (Label
l,Patt
p) <- [(Label, Patt)]
r]
PT Type
_ Patt
p -> Patt -> Type
patt2term Patt
p
PInt Int
i -> Int -> Type
EInt Int
i
PFloat Double
i -> Double -> Type
EFloat Double
i
PString [Char]
s -> [Char] -> Type
K [Char]
s
PAs Ident
x Patt
p -> Ident -> [Type] -> Type
appCons Ident
cAs [Ident -> Type
Vr Ident
x, Patt -> Type
patt2term Patt
p]
Patt
PChar -> Ident -> [Type] -> Type
appCons Ident
cChar []
PChars [Char]
s -> Ident -> [Type] -> Type
appCons Ident
cChars [[Char] -> Type
K [Char]
s]
PSeq Patt
a Patt
b -> Ident -> [Type] -> Type
appCons Ident
cSeq [(Patt -> Type
patt2term Patt
a), (Patt -> Type
patt2term Patt
b)]
PAlt Patt
a Patt
b -> Ident -> [Type] -> Type
appCons Ident
cAlt [(Patt -> Type
patt2term Patt
a), (Patt -> Type
patt2term Patt
b)]
PRep Patt
a -> Ident -> [Type] -> Type
appCons Ident
cRep [(Patt -> Type
patt2term Patt
a)]
PNeg Patt
a -> Ident -> [Type] -> Type
appCons Ident
cNeg [(Patt -> Type
patt2term Patt
a)]
composSafeOp :: (Term -> Term) -> Term -> Term
composSafeOp :: (Type -> Type) -> Type -> Type
composSafeOp Type -> Type
op = Identity Type -> Type
forall a. Identity a -> a
runIdentity (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Identity Type) -> Type -> Identity Type
forall (m :: * -> *). Monad m => (Type -> m Type) -> Type -> m Type
composOp (Type -> Identity Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Identity Type) -> (Type -> Type) -> Type -> Identity Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
op)
composOp :: Monad m => (Term -> m Term) -> Term -> m Term
composOp :: (Type -> m Type) -> Type -> m Type
composOp Type -> m Type
co Type
trm =
case Type
trm of
App Type
c Type
a -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
App (Type -> m Type
co Type
c) (Type -> m Type
co Type
a)
Abs BindType
b Ident
x Type
t -> (Type -> Type) -> m Type -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (BindType -> Ident -> Type -> Type
Abs BindType
b Ident
x) (Type -> m Type
co Type
t)
Prod BindType
b Ident
x Type
a Type
t -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (BindType -> Ident -> Type -> Type -> Type
Prod BindType
b Ident
x) (Type -> m Type
co Type
a) (Type -> m Type
co Type
t)
S Type
c Type
a -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
S (Type -> m Type
co Type
c) (Type -> m Type
co Type
a)
Table Type
a Type
c -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
Table (Type -> m Type
co Type
a) (Type -> m Type
co Type
c)
R [Assign]
r -> ([Assign] -> Type) -> m [Assign] -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Assign] -> Type
R ((Type -> m Type) -> [Assign] -> m [Assign]
forall (m :: * -> *) c.
Monad m =>
(Type -> m c) -> [Assign] -> m [(Label, (Maybe c, c))]
mapAssignM Type -> m Type
co [Assign]
r)
RecType [(Label, Type)]
r -> ([(Label, Type)] -> Type) -> m [(Label, Type)] -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Label, Type)] -> Type
RecType ((Type -> m Type) -> [(Label, Type)] -> m [(Label, Type)]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM Type -> m Type
co [(Label, Type)]
r)
P Type
t Label
i -> (Type -> Label -> Type) -> m Type -> m Label -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Label -> Type
P (Type -> m Type
co Type
t) (Label -> m Label
forall (m :: * -> *) a. Monad m => a -> m a
return Label
i)
ExtR Type
a Type
c -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
ExtR (Type -> m Type
co Type
a) (Type -> m Type
co Type
c)
T TInfo
i [Case]
cc -> ([Case] -> TInfo -> Type) -> m [Case] -> m TInfo -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 ((TInfo -> [Case] -> Type) -> [Case] -> TInfo -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip TInfo -> [Case] -> Type
T) ((Type -> m Type) -> [Case] -> m [Case]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM Type -> m Type
co [Case]
cc) ((Type -> m Type) -> TInfo -> m TInfo
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> TInfo -> m TInfo
changeTableType Type -> m Type
co TInfo
i)
V Type
ty [Type]
vs -> (Type -> [Type] -> Type) -> m Type -> m [Type] -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> [Type] -> Type
V (Type -> m Type
co Type
ty) ((Type -> m Type) -> [Type] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> m Type
co [Type]
vs)
Let (Ident
x,(Maybe Type
mt,Type
a)) Type
b -> (Type -> Maybe Type -> Type -> Type)
-> m Type -> m (Maybe Type) -> m Type -> m Type
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 Type -> Maybe Type -> Type -> Type
let' (Type -> m Type
co Type
a) ((Type -> m Type) -> Maybe Type -> m (Maybe Type)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM Type -> m Type
co Maybe Type
mt) (Type -> m Type
co Type
b)
where let' :: Type -> Maybe Type -> Type -> Type
let' Type
a' Maybe Type
mt' Type
b' = LocalDef -> Type -> Type
Let (Ident
x,(Maybe Type
mt',Type
a')) Type
b'
C Type
s1 Type
s2 -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
C (Type -> m Type
co Type
s1) (Type -> m Type
co Type
s2)
Glue Type
s1 Type
s2 -> (Type -> Type -> Type) -> m Type -> m Type -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
Glue (Type -> m Type
co Type
s1) (Type -> m Type
co Type
s2)
Alts Type
t [(Type, Type)]
aa -> (Type -> [(Type, Type)] -> Type)
-> m Type -> m [(Type, Type)] -> m Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> [(Type, Type)] -> Type
Alts (Type -> m Type
co Type
t) (((Type, Type) -> m (Type, Type))
-> [(Type, Type)] -> m [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> m Type) -> (Type, Type) -> m (Type, Type)
forall (m :: * -> *) b c.
Monad m =>
(b -> m c) -> (b, b) -> m (c, c)
pairM Type -> m Type
co) [(Type, Type)]
aa)
FV [Type]
ts -> ([Type] -> Type) -> m [Type] -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Type] -> Type
FV ((Type -> m Type) -> [Type] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> m Type
co [Type]
ts)
Strs [Type]
tt -> ([Type] -> Type) -> m [Type] -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Type] -> Type
Strs ((Type -> m Type) -> [Type] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> m Type
co [Type]
tt)
EPattType Type
ty -> (Type -> Type) -> m Type -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Type -> Type
EPattType (Type -> m Type
co Type
ty)
ELincat Ident
c Type
ty -> (Type -> Type) -> m Type -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Ident -> Type -> Type
ELincat Ident
c) (Type -> m Type
co Type
ty)
ELin Ident
c Type
ty -> (Type -> Type) -> m Type -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Ident -> Type -> Type
ELin Ident
c) (Type -> m Type
co Type
ty)
ImplArg Type
t -> (Type -> Type) -> m Type -> m Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Type -> Type
ImplArg (Type -> m Type
co Type
t)
Type
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
trm
composSafePattOp :: (Patt -> Patt) -> Patt -> Patt
composSafePattOp Patt -> Patt
op = Identity Patt -> Patt
forall a. Identity a -> a
runIdentity (Identity Patt -> Patt) -> (Patt -> Identity Patt) -> Patt -> Patt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Patt -> Identity Patt) -> Patt -> Identity Patt
forall (m :: * -> *). Monad m => (Patt -> m Patt) -> Patt -> m Patt
composPattOp (Patt -> Identity Patt
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Identity Patt) -> (Patt -> Patt) -> Patt -> Identity Patt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Patt -> Patt
op)
composPattOp :: Monad m => (Patt -> m Patt) -> Patt -> m Patt
composPattOp :: (Patt -> m Patt) -> Patt -> m Patt
composPattOp Patt -> m Patt
op Patt
patt =
case Patt
patt of
PC Ident
c [Patt]
ps -> ([Patt] -> Patt) -> m [Patt] -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Ident -> [Patt] -> Patt
PC Ident
c) ((Patt -> m Patt) -> [Patt] -> m [Patt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Patt -> m Patt
op [Patt]
ps)
PP Cat
qc [Patt]
ps -> ([Patt] -> Patt) -> m [Patt] -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Cat -> [Patt] -> Patt
PP Cat
qc) ((Patt -> m Patt) -> [Patt] -> m [Patt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Patt -> m Patt
op [Patt]
ps)
PR [(Label, Patt)]
as -> ([(Label, Patt)] -> Patt) -> m [(Label, Patt)] -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Label, Patt)] -> Patt
PR ((Patt -> m Patt) -> [(Label, Patt)] -> m [(Label, Patt)]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM Patt -> m Patt
op [(Label, Patt)]
as)
PT Type
ty Patt
p -> (Patt -> Patt) -> m Patt -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Type -> Patt -> Patt
PT Type
ty) (Patt -> m Patt
op Patt
p)
PAs Ident
x Patt
p -> (Patt -> Patt) -> m Patt -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Ident -> Patt -> Patt
PAs Ident
x) (Patt -> m Patt
op Patt
p)
PImplArg Patt
p -> (Patt -> Patt) -> m Patt -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Patt -> Patt
PImplArg (Patt -> m Patt
op Patt
p)
PNeg Patt
p -> (Patt -> Patt) -> m Patt -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Patt -> Patt
PNeg (Patt -> m Patt
op Patt
p)
PAlt Patt
p1 Patt
p2 -> (Patt -> Patt -> Patt) -> m Patt -> m Patt -> m Patt
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Patt -> Patt -> Patt
PAlt (Patt -> m Patt
op Patt
p1) (Patt -> m Patt
op Patt
p2)
PSeq Patt
p1 Patt
p2 -> (Patt -> Patt -> Patt) -> m Patt -> m Patt -> m Patt
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Patt -> Patt -> Patt
PSeq (Patt -> m Patt
op Patt
p1) (Patt -> m Patt
op Patt
p2)
PMSeq ((Int, Int)
_,Patt
p1) ((Int, Int)
_,Patt
p2) -> (Patt -> Patt -> Patt) -> m Patt -> m Patt -> m Patt
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Patt -> Patt -> Patt
PSeq (Patt -> m Patt
op Patt
p1) (Patt -> m Patt
op Patt
p2)
PRep Patt
p -> (Patt -> Patt) -> m Patt -> m Patt
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Patt -> Patt
PRep (Patt -> m Patt
op Patt
p)
Patt
_ -> Patt -> m Patt
forall (m :: * -> *) a. Monad m => a -> m a
return Patt
patt
collectOp :: Monoid m => (Term -> m) -> Term -> m
collectOp :: (Type -> m) -> Type -> m
collectOp Type -> m
co Type
trm = case Type
trm of
App Type
c Type
a -> Type -> m
co Type
c m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
a
Abs BindType
_ Ident
_ Type
b -> Type -> m
co Type
b
Prod BindType
_ Ident
_ Type
a Type
b -> Type -> m
co Type
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
b
S Type
c Type
a -> Type -> m
co Type
c m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
a
Table Type
a Type
c -> Type -> m
co Type
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
c
ExtR Type
a Type
c -> Type -> m
co Type
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
c
R [Assign]
r -> (Assign -> m) -> [Assign] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap (\ (Label
_,(Maybe Type
mt,Type
a)) -> m -> (Type -> m) -> Maybe Type -> m
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m
forall a. Monoid a => a
mempty Type -> m
co Maybe Type
mt m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
a) [Assign]
r
RecType [(Label, Type)]
r -> ((Label, Type) -> m) -> [(Label, Type)] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap (Type -> m
co (Type -> m) -> ((Label, Type) -> Type) -> (Label, Type) -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Label, Type) -> Type
forall a b. (a, b) -> b
snd) [(Label, Type)]
r
P Type
t Label
i -> Type -> m
co Type
t
T TInfo
_ [Case]
cc -> (Case -> m) -> [Case] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap (Type -> m
co (Type -> m) -> (Case -> Type) -> Case -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> Type
forall a b. (a, b) -> b
snd) [Case]
cc
V Type
_ [Type]
cc -> (Type -> m) -> [Type] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap Type -> m
co [Type]
cc
Let (Ident
x,(Maybe Type
mt,Type
a)) Type
b -> m -> (Type -> m) -> Maybe Type -> m
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m
forall a. Monoid a => a
mempty Type -> m
co Maybe Type
mt m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
b
C Type
s1 Type
s2 -> Type -> m
co Type
s1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
s2
Glue Type
s1 Type
s2 -> Type -> m
co Type
s1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> Type -> m
co Type
s2
Alts Type
t [(Type, Type)]
aa -> let ([Type]
x,[Type]
y) = [(Type, Type)] -> ([Type], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, Type)]
aa in Type -> m
co Type
t m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (Type -> m) -> [Type] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap Type -> m
co ([Type]
x [Type] -> [Type] -> [Type]
forall a. Semigroup a => a -> a -> a
<> [Type]
y)
FV [Type]
ts -> (Type -> m) -> [Type] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap Type -> m
co [Type]
ts
Strs [Type]
tt -> (Type -> m) -> [Type] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap Type -> m
co [Type]
tt
Type
_ -> m
forall a. Monoid a => a
mempty
mconcatMap :: (a -> c) -> [a] -> c
mconcatMap a -> c
f = [c] -> c
forall a. Monoid a => [a] -> a
mconcat ([c] -> c) -> ([a] -> [c]) -> [a] -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c) -> [a] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map a -> c
f
collectPattOp :: (Patt -> [a]) -> Patt -> [a]
collectPattOp :: (Patt -> [a]) -> Patt -> [a]
collectPattOp Patt -> [a]
op Patt
patt =
case Patt
patt of
PC Ident
c [Patt]
ps -> (Patt -> [a]) -> [Patt] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Patt -> [a]
op [Patt]
ps
PP Cat
qc [Patt]
ps -> (Patt -> [a]) -> [Patt] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Patt -> [a]
op [Patt]
ps
PR [(Label, Patt)]
as -> ((Label, Patt) -> [a]) -> [(Label, Patt)] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Patt -> [a]
op(Patt -> [a]) -> ((Label, Patt) -> Patt) -> (Label, Patt) -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Label, Patt) -> Patt
forall a b. (a, b) -> b
snd) [(Label, Patt)]
as
PT Type
ty Patt
p -> Patt -> [a]
op Patt
p
PAs Ident
x Patt
p -> Patt -> [a]
op Patt
p
PImplArg Patt
p -> Patt -> [a]
op Patt
p
PNeg Patt
p -> Patt -> [a]
op Patt
p
PAlt Patt
p1 Patt
p2 -> Patt -> [a]
op Patt
p1[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++Patt -> [a]
op Patt
p2
PSeq Patt
p1 Patt
p2 -> Patt -> [a]
op Patt
p1[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++Patt -> [a]
op Patt
p2
PMSeq ((Int, Int)
_,Patt
p1) ((Int, Int)
_,Patt
p2) -> Patt -> [a]
op Patt
p1[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++Patt -> [a]
op Patt
p2
PRep Patt
p -> Patt -> [a]
op Patt
p
Patt
_ -> []
redirectTerm :: ModuleName -> Term -> Term
redirectTerm :: ModuleName -> Type -> Type
redirectTerm ModuleName
n Type
t = case Type
t of
QC (ModuleName
_,Ident
f) -> Cat -> Type
QC (ModuleName
n,Ident
f)
Q (ModuleName
_,Ident
f) -> Cat -> Type
Q (ModuleName
n,Ident
f)
Type
_ -> (Type -> Type) -> Type -> Type
composSafeOp (ModuleName -> Type -> Type
redirectTerm ModuleName
n) Type
t
allCaseValues :: Term -> [([Patt],Term)]
allCaseValues :: Type -> [([Patt], Type)]
allCaseValues Type
trm = case Type
trm of
T TInfo
_ [Case]
cs -> [(Patt
pPatt -> [Patt] -> [Patt]
forall a. a -> [a] -> [a]
:[Patt]
ps, Type
t) | (Patt
p,Type
t0) <- [Case]
cs, ([Patt]
ps,Type
t) <- Type -> [([Patt], Type)]
allCaseValues Type
t0]
Type
_ -> [([],Type
trm)]
strsFromTerm :: Term -> Err [Str]
strsFromTerm :: Type -> Err [Str]
strsFromTerm Type
t = case Type
t of
K [Char]
s -> [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Char] -> Str
str [Char]
s]
Type
Empty -> [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Char] -> Str
str []]
C Type
s Type
t -> do
[Str]
s' <- Type -> Err [Str]
strsFromTerm Type
s
[Str]
t' <- Type -> Err [Str]
strsFromTerm Type
t
[Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [Str -> Str -> Str
plusStr Str
x Str
y | Str
x <- [Str]
s', Str
y <- [Str]
t']
Glue Type
s Type
t -> do
[Str]
s' <- Type -> Err [Str]
strsFromTerm Type
s
[Str]
t' <- Type -> Err [Str]
strsFromTerm Type
t
[Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [Str -> Str -> Str
glueStr Str
x Str
y | Str
x <- [Str]
s', Str
y <- [Str]
t']
Alts Type
d [(Type, Type)]
vs -> do
[Str]
d0 <- Type -> Err [Str]
strsFromTerm Type
d
[[Str]]
v0 <- ((Type, Type) -> Err [Str]) -> [(Type, Type)] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Err [Str]
strsFromTerm (Type -> Err [Str])
-> ((Type, Type) -> Type) -> (Type, Type) -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst) [(Type, Type)]
vs
[[Str]]
c0 <- ((Type, Type) -> Err [Str]) -> [(Type, Type)] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Err [Str]
strsFromTerm (Type -> Err [Str])
-> ((Type, Type) -> Type) -> (Type, Type) -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> b
snd) [(Type, Type)]
vs
[Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [Ss -> [(Ss, Ss)] -> Str
strTok (Str -> Ss
str2strings Str
def) [(Ss, Ss)]
vars |
Str
def <- [Str]
d0,
[(Ss, Ss)]
vars <- [[(Str -> Ss
str2strings Str
v, (Str -> [Char]) -> [Str] -> Ss
forall a b. (a -> b) -> [a] -> [b]
map Str -> [Char]
sstr [Str]
c) | (Str
v,[Str]
c) <- [Str] -> [[Str]] -> [(Str, [Str])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Str]
vv [[Str]]
c0] |
[Str]
vv <- [[Str]] -> [[Str]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Str]]
v0]
]
FV [Type]
ts -> (Type -> Err [Str]) -> [Type] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err [Str]
strsFromTerm [Type]
ts Err [[Str]] -> ([[Str]] -> Err [Str]) -> Err [Str]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Str] -> Err [Str]) -> ([[Str]] -> [Str]) -> [[Str]] -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Str]] -> [Str]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
Strs [Type]
ts -> (Type -> Err [Str]) -> [Type] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err [Str]
strsFromTerm [Type]
ts Err [[Str]] -> ([[Str]] -> Err [Str]) -> Err [Str]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Str] -> Err [Str]) -> ([[Str]] -> [Str]) -> [[Str]] -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Str]] -> [Str]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
Type
_ -> [Char] -> Err [Str]
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"cannot get Str from term" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t))
getTableType :: TInfo -> Err Type
getTableType :: TInfo -> Err Type
getTableType TInfo
i = case TInfo
i of
TTyped Type
ty -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
TComp Type
ty -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
TWild Type
ty -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
TInfo
_ -> [Char] -> Err Type
forall a. [Char] -> Err a
Bad [Char]
"the table is untyped"
changeTableType :: Monad m => (Type -> m Type) -> TInfo -> m TInfo
changeTableType :: (Type -> m Type) -> TInfo -> m TInfo
changeTableType Type -> m Type
co TInfo
i = case TInfo
i of
TTyped Type
ty -> Type -> m Type
co Type
ty m Type -> (Type -> m TInfo) -> m TInfo
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TInfo -> m TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> m TInfo) -> (Type -> TInfo) -> Type -> m TInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TInfo
TTyped
TComp Type
ty -> Type -> m Type
co Type
ty m Type -> (Type -> m TInfo) -> m TInfo
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TInfo -> m TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> m TInfo) -> (Type -> TInfo) -> Type -> m TInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TInfo
TComp
TWild Type
ty -> Type -> m Type
co Type
ty m Type -> (Type -> m TInfo) -> m TInfo
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TInfo -> m TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> m TInfo) -> (Type -> TInfo) -> Type -> m TInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TInfo
TWild
TInfo
_ -> TInfo -> m TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return TInfo
i
wordsInTerm :: Term -> [String]
wordsInTerm :: Type -> Ss
wordsInTerm Type
trm = ([Char] -> Bool) -> Ss -> Ss
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Char] -> Bool) -> [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Ss -> Ss) -> Ss -> Ss
forall a b. (a -> b) -> a -> b
$ case Type
trm of
K [Char]
s -> [[Char]
s]
S Type
c Type
_ -> Type -> Ss
wo Type
c
Alts Type
t [(Type, Type)]
aa -> Type -> Ss
wo Type
t Ss -> Ss -> Ss
forall a. [a] -> [a] -> [a]
++ ((Type, Type) -> Ss) -> [(Type, Type)] -> Ss
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type -> Ss
wo (Type -> Ss) -> ((Type, Type) -> Type) -> (Type, Type) -> Ss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst) [(Type, Type)]
aa
Type
_ -> (Type -> Ss) -> Type -> Ss
forall m. Monoid m => (Type -> m) -> Type -> m
collectOp Type -> Ss
wo Type
trm
where wo :: Type -> Ss
wo = Type -> Ss
wordsInTerm
noExist :: Term
noExist :: Type
noExist = [Type] -> Type
FV []
defaultLinType :: Type
defaultLinType :: Type
defaultLinType = (Int -> Label) -> [Type] -> Type
mkRecType Int -> Label
linLabel [Type
typeStr]
sortRec :: [(Label,a)] -> [(Label,a)]
sortRec :: [(Label, a)] -> [(Label, a)]
sortRec = ((Label, a) -> (Label, a) -> Ordering)
-> [(Label, a)] -> [(Label, a)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Label, a) -> (Label, a) -> Ordering
forall b b. (Label, b) -> (Label, b) -> Ordering
ordLabel where
ordLabel :: (Label, b) -> (Label, b) -> Ordering
ordLabel (Label
r1,b
_) (Label
r2,b
_) =
case (Ident -> [Char]
showIdent (Label -> Ident
label2ident Label
r1), Ident -> [Char]
showIdent (Label -> Ident
label2ident Label
r2)) of
([Char]
"s",[Char]
_) -> Ordering
LT
([Char]
_,[Char]
"s") -> Ordering
GT
([Char]
s1,[Char]
s2) -> [Char] -> [Char] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Char]
s1 [Char]
s2
allDependencies :: (ModuleName -> Bool) -> Map.Map Ident Info -> [(Ident,[Ident])]
allDependencies :: (ModuleName -> Bool) -> Map Ident Info -> [(Ident, [Ident])]
allDependencies ModuleName -> Bool
ism Map Ident Info
b =
[(Ident
f, [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub ((Maybe (L Type) -> [Ident]) -> [Maybe (L Type)] -> [Ident]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Maybe (L Type) -> [Ident]
opty (Info -> [Maybe (L Type)]
pts Info
i))) | (Ident
f,Info
i) <- Map Ident Info -> [(Ident, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Ident Info
b]
where
opersIn :: Type -> [Ident]
opersIn Type
t = case Type
t of
Q (ModuleName
n,Ident
c) | ModuleName -> Bool
ism ModuleName
n -> [Ident
c]
QC (ModuleName
n,Ident
c) | ModuleName -> Bool
ism ModuleName
n -> [Ident
c]
Type
_ -> (Type -> [Ident]) -> Type -> [Ident]
forall m. Monoid m => (Type -> m) -> Type -> m
collectOp Type -> [Ident]
opersIn Type
t
opty :: Maybe (L Type) -> [Ident]
opty (Just (L Location
_ Type
ty)) = Type -> [Ident]
opersIn Type
ty
opty Maybe (L Type)
_ = []
pts :: Info -> [Maybe (L Type)]
pts Info
i = case Info
i of
ResOper Maybe (L Type)
pty Maybe (L Type)
pt -> [Maybe (L Type)
pty,Maybe (L Type)
pt]
ResOverload [ModuleName]
_ [(L Type, L Type)]
tyts -> [[Maybe (L Type)]] -> [Maybe (L Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just L Type
ty, L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just L Type
tr] | (L Type
ty,L Type
tr) <- [(L Type, L Type)]
tyts]
ResParam (Just (L Location
loc [Param]
ps)) Maybe [Type]
_ -> [L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
t) | (Ident
_,Context
cont) <- [Param]
ps, (BindType
_,Ident
_,Type
t) <- Context
cont]
CncCat Maybe (L Type)
pty Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> [Maybe (L Type)
pty]
CncFun Maybe (Ident, Context, Type)
_ Maybe (L Type)
pt Maybe (L Type)
_ Maybe PMCFG
_ -> [Maybe (L Type)
pt]
AbsFun Maybe (L Type)
pty Maybe Int
_ Maybe [L ([Patt], Type)]
ptr Maybe Bool
_ -> [Maybe (L Type)
pty]
AbsCat (Just (L Location
loc Context
co)) -> [L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
ty) | (BindType
_,Ident
_,Type
ty) <- Context
co]
Info
_ -> []
topoSortJments :: ErrorMonad m => SourceModule -> m [(Ident,Info)]
topoSortJments :: SourceModule -> m [(Ident, Info)]
topoSortJments (ModuleName
m,ModuleInfo
mi) = do
[Ident]
is <- ([Ident] -> m [Ident])
-> ([[Ident]] -> m [Ident])
-> Either [Ident] [[Ident]]
-> m [Ident]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
[Ident] -> m [Ident]
forall (m :: * -> *) a. Monad m => a -> m a
return
(\[[Ident]]
cyc -> [Char] -> m [Ident]
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"circular definitions:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Ident] -> Doc
forall a. Pretty a => [a] -> Doc
fsep ([[Ident]] -> [Ident]
forall a. [a] -> a
head [[Ident]]
cyc))))
([(Ident, [Ident])] -> Either [Ident] [[Ident]]
forall a. Ord a => [(a, [a])] -> Either [a] [[a]]
topoTest ((ModuleName -> Bool) -> Map Ident Info -> [(Ident, [Ident])]
allDependencies (ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
==ModuleName
m) (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)))
[(Ident, Info)] -> m [(Ident, Info)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Ident, Info)] -> [(Ident, Info)]
forall a. [a] -> [a]
reverse [(Ident
i,Info
info) | Ident
i <- [Ident]
is, Just Info
info <- [Ident -> Map Ident Info -> Maybe Info
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)]])
topoSortJments2 :: ErrorMonad m => SourceModule -> m [[(Ident,Info)]]
topoSortJments2 :: SourceModule -> m [[(Ident, Info)]]
topoSortJments2 (ModuleName
m,ModuleInfo
mi) = do
[[Ident]]
iss <- ([[Ident]] -> m [[Ident]])
-> ([[Ident]] -> m [[Ident]])
-> Either [[Ident]] [[Ident]]
-> m [[Ident]]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
[[Ident]] -> m [[Ident]]
forall (m :: * -> *) a. Monad m => a -> m a
return
(\[[Ident]]
cyc -> [Char] -> m [[Ident]]
forall (m :: * -> *) a. ErrorMonad m => [Char] -> m a
raise (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"circular definitions:"
[Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Ident] -> Doc
forall a. Pretty a => [a] -> Doc
fsep ([[Ident]] -> [Ident]
forall a. [a] -> a
head [[Ident]]
cyc))))
([(Ident, [Ident])] -> Either [[Ident]] [[Ident]]
forall a. Ord a => [(a, [a])] -> Either [[a]] [[a]]
topoTest2 ((ModuleName -> Bool) -> Map Ident Info -> [(Ident, [Ident])]
allDependencies (ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
==ModuleName
m) (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)))
[[(Ident, Info)]] -> m [[(Ident, Info)]]
forall (m :: * -> *) a. Monad m => a -> m a
return
[[(Ident
i,Info
info) | Ident
i<-[Ident]
is,Just Info
info<-[Ident -> Map Ident Info -> Maybe Info
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)]] | [Ident]
is<-[[Ident]]
iss]