----------------------------------------------------------------------
-- |
-- Module      : Macros
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 16:38:00 $
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.24 $
--
-- Macros for constructing and analysing source code terms.
--
-- operations on terms and types not involving lookup in or reference to grammars
--
-- AR 7\/12\/1999 - 9\/5\/2000 -- 4\/6\/2001
-----------------------------------------------------------------------------

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

-- ** Functions for constructing and analysing source code terms.

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 --- not optimal to do in this way
  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 -- thus recursivity on Cat level
  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  -- pessimistic choice
  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

--eqIdent :: Ident -> Ident -> Bool
--eqIdent = (==)

uType :: Type
uType :: Type
uType = Ident -> Type
Cn Ident
cUndefinedType

-- *** Assignment

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)

-- *** Records

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))


-- *** Types

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

-- *** Terms

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 [] -- nondep prod

--plusRecType :: Type -> Type -> Err Type
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 :: Term -> Term -> Err Term
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) | -- overshadowing of old fields
                              (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)

-- | default linearization type
defLinType :: Type
defLinType :: Type
defLinType = [(Label, Type)] -> Type
RecType [(Label
theLinLabel,  Type
typeStr)]

-- | refreshing variables
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)

-- | trying to preserve a given symbol
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]]

-- | quick hack for refining with var in editor
freshAsTerm :: String -> Term
freshAsTerm :: [Char] -> Type
freshAsTerm [Char]
s = Ident -> Type
Vr (Int -> Ident
varX ([Char] -> Int
readIntArg [Char]
s))

-- | create a terminal for concrete syntax
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

-- | create a terminal from identifier
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] -- default lintype {s :: Str}

linAsStr :: String -> Term
linAsStr :: [Char] -> Type
linAsStr [Char]
s = (Int -> Label) -> [Type] -> Type
mkRecord Int -> Label
linLabel [[Char] -> Type
K [Char]
s] -- default linearization {s = s}

-- *** Term and pattern conversion

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

--- encodings due to excessive use of term-patt convs. AR 7/1/2005
  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             --- not parsable, should not occur
  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]            --- an encoding
  Patt
PChar     -> Ident -> [Type] -> Type
appCons Ident
cChar  []                             --- an encoding
  PChars [Char]
s  -> Ident -> [Type] -> Type
appCons Ident
cChars [[Char] -> Type
K [Char]
s]                          --- an encoding
  PSeq Patt
a Patt
b  -> Ident -> [Type] -> Type
appCons Ident
cSeq   [(Patt -> Type
patt2term Patt
a), (Patt -> Type
patt2term Patt
b)] --- an encoding
  PAlt Patt
a Patt
b  -> Ident -> [Type] -> Type
appCons Ident
cAlt   [(Patt -> Type
patt2term Patt
a), (Patt -> Type
patt2term Patt
b)] --- an encoding
  PRep Patt
a    -> Ident -> [Type] -> Type
appCons Ident
cRep   [(Patt -> Type
patt2term Patt
a)]                --- an encoding
  PNeg Patt
a    -> Ident -> [Type] -> Type
appCons Ident
cNeg   [(Patt -> Type
patt2term Patt
a)]                --- an encoding


-- *** Almost compositional

-- | to define compositional term functions
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)

-- | to define compositional term functions
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 -- covers K, Vr, Cn, Sort, EPatt

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) -- information loss
    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 -- covers cases without subpatterns

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 -- not from patterns --- nor from type annot
  V Type
_ [Type]
cc       -> (Type -> m) -> [Type] -> m
forall c a. Monoid c => (a -> c) -> [a] -> c
mconcatMap Type -> m
co         [Type]
cc --- nor from type annot
  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 -- covers K, Vr, Cn, Sort

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
_               -> []     -- covers cases without subpatterns


-- *** Misc

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

-- | to gather ultimate cases in a table; preserves pattern list
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)]

-- | to get a string from a term that represents a sequence of terminals
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
  --let vs' = zip v0 c0
    [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

-- | to find the word items in a term
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]

-- | normalize records and record types; put s first

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

-- *** Dependencies

-- | dependency check, detecting circularities and returning topo-sorted list

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]  ---- (Maybe (Ident,(Context,Type))
      AbsFun Maybe (L Type)
pty Maybe Int
_ Maybe [L ([Patt], Type)]
ptr Maybe Bool
_ -> [Maybe (L Type)
pty] --- ptr is def, which can be mutual
      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]