{- |
Module      :  ./HasCASL/DataAna.hs
Description :  analysis of data type declarations
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

analyse alternatives of data types
-}

module HasCASL.DataAna
    ( DataPat (..)
    , toDataPat
    , getConstrScheme
    , getSelScheme
    , anaAlts
    , makeDataSelEqs
    , inductionScheme
    , mkVarDecl
    ) where

import Common.AS_Annotation
import Common.Id
import Common.Result

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.Le
import HasCASL.TypeAna
import HasCASL.Unify

import Control.Monad

import Data.Maybe (mapMaybe)
import qualified Data.Map as Map
import qualified Data.Set as Set

{- | description of polymorphic data types. The top-level identifier is
already renamed according the IdMap. -}
data DataPat = DataPat IdMap Id [TypeArg] RawKind Type

mkVarDecl :: Id -> Type -> VarDecl
mkVarDecl :: Id -> Type -> VarDecl
mkVarDecl i :: Id
i t :: Type
t = Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
i Type
t SeparatorKind
Other Range
nullRange

mkSelId :: Range -> String -> Int -> Int -> Id
mkSelId :: Range -> String -> Int -> Int -> Id
mkSelId p :: Range
p str :: String
str n :: Int
n m :: Int
m = [Token] -> Id
mkId
    [String -> Range -> Token
Token (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then "" else Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m) Range
p]

mkSelVar :: Int -> Int -> Type -> VarDecl
mkSelVar :: Int -> Int -> Type -> VarDecl
mkSelVar n :: Int
n m :: Int
m ty :: Type
ty = Id -> Type -> VarDecl
mkVarDecl (Range -> String -> Int -> Int -> Id
mkSelId (Type -> Range
forall a. GetRange a => a -> Range
getRange Type
ty) "x" Int
n Int
m) Type
ty

genTuple :: Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple :: Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple _ _ [] = []
genTuple n :: Int
n m :: Int
m (s :: Selector
s@(Select _ ty :: Type
ty _) : sels :: [Selector]
sels) =
    (Selector
s, Int -> Int -> Type -> VarDecl
mkSelVar Int
n Int
m Type
ty) (Selector, VarDecl)
-> [(Selector, VarDecl)] -> [(Selector, VarDecl)]
forall a. a -> [a] -> [a]
: Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple Int
n (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [Selector]
sels

genSelVars :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVars :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVars n :: Int
n sels :: [[Selector]]
sels = case [[Selector]]
sels of
  [ts :: [Selector]
ts] -> [Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple 0 1 [Selector]
ts]
  _ -> if ([Selector] -> Bool) -> [[Selector]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all [Selector] -> Bool
forall a. [a] -> Bool
isSingle [[Selector]]
sels
       then ((Selector, VarDecl) -> [(Selector, VarDecl)])
-> [(Selector, VarDecl)] -> [[(Selector, VarDecl)]]
forall a b. (a -> b) -> [a] -> [b]
map ((Selector, VarDecl)
-> [(Selector, VarDecl)] -> [(Selector, VarDecl)]
forall a. a -> [a] -> [a]
: []) ([(Selector, VarDecl)] -> [[(Selector, VarDecl)]])
-> [(Selector, VarDecl)] -> [[(Selector, VarDecl)]]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple 0 1 ([Selector] -> [(Selector, VarDecl)])
-> [Selector] -> [(Selector, VarDecl)]
forall a b. (a -> b) -> a -> b
$ ([Selector] -> Selector) -> [[Selector]] -> [Selector]
forall a b. (a -> b) -> [a] -> [b]
map [Selector] -> Selector
forall a. [a] -> a
head [[Selector]]
sels
       else Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVarsAux Int
n [[Selector]]
sels

genSelVarsAux :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVarsAux :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVarsAux _ [] = []
genSelVarsAux n :: Int
n (ts :: [Selector]
ts : sels :: [[Selector]]
sels) =
    Int -> Int -> [Selector] -> [(Selector, VarDecl)]
genTuple Int
n 1 [Selector]
ts [(Selector, VarDecl)]
-> [[(Selector, VarDecl)]] -> [[(Selector, VarDecl)]]
forall a. a -> [a] -> [a]
: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVarsAux (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [[Selector]]
sels

makeSelTupleEqs :: DataPat -> Term -> [(Selector, VarDecl)] -> [Named Term]
makeSelTupleEqs :: DataPat -> Term -> [(Selector, VarDecl)] -> [Named Term]
makeSelTupleEqs dt :: DataPat
dt ct :: Term
ct = ((Selector, VarDecl) -> [Named Term])
-> [(Selector, VarDecl)] -> [Named Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Select mi :: Maybe Id
mi ty :: Type
ty p :: Partiality
p, v :: VarDecl
v) -> case Maybe Id
mi of
     Just i :: Id
i -> let
         sc :: TypeScheme
sc = DataPat -> Partiality -> Type -> TypeScheme
getSelScheme DataPat
dt Partiality
p Type
ty
         eq :: Term
eq = Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
ty Range
nullRange
              (Term -> [Term] -> Term
mkApplTerm (Id -> TypeScheme -> Term
mkOpTerm Id
i TypeScheme
sc) [Term
ct]) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar VarDecl
v
         in [String -> Term -> Named Term
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_select_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i) Term
eq]
     _ -> [])

makeSelEqs :: DataPat -> Term -> [[(Selector, VarDecl)]] -> [Named Term]
makeSelEqs :: DataPat -> Term -> [[(Selector, VarDecl)]] -> [Named Term]
makeSelEqs dt :: DataPat
dt = ([(Selector, VarDecl)] -> [Named Term])
-> [[(Selector, VarDecl)]] -> [Named Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([(Selector, VarDecl)] -> [Named Term])
 -> [[(Selector, VarDecl)]] -> [Named Term])
-> (Term -> [(Selector, VarDecl)] -> [Named Term])
-> Term
-> [[(Selector, VarDecl)]]
-> [Named Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataPat -> Term -> [(Selector, VarDecl)] -> [Named Term]
makeSelTupleEqs DataPat
dt

makeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
makeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
makeAltSelEqs dt :: DataPat
dt@(DataPat _ _ iargs :: [TypeArg]
iargs _ _) (Construct mc :: Maybe Id
mc ts :: [Type]
ts p :: Partiality
p sels :: [[Selector]]
sels) =
    case Maybe Id
mc of
    Nothing -> []
    Just c :: Id
c -> let
      selvars :: [[(Selector, VarDecl)]]
selvars = Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVars 1 [[Selector]]
sels
      vars :: [[VarDecl]]
vars = ([(Selector, VarDecl)] -> [VarDecl])
-> [[(Selector, VarDecl)]] -> [[VarDecl]]
forall a b. (a -> b) -> [a] -> [b]
map (((Selector, VarDecl) -> VarDecl)
-> [(Selector, VarDecl)] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Selector, VarDecl) -> VarDecl
forall a b. (a, b) -> b
snd) [[(Selector, VarDecl)]]
selvars
      ars :: [Term]
ars = [[VarDecl]] -> [Term]
mkSelArgs [[VarDecl]]
vars
      ct :: Term
ct = Term -> [Term] -> Term
mkApplTerm (Id -> TypeScheme -> Term
mkOpTerm Id
c (TypeScheme -> Term) -> TypeScheme -> Term
forall a b. (a -> b) -> a -> b
$ DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme DataPat
dt Partiality
p [Type]
ts) [Term]
ars
      in (Named Term -> Named Term) -> [Named Term] -> [Named Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> Named Term -> Named Term
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ([GenVarDecl] -> Term -> Term
mkForall ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl [TypeArg]
iargs
           [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl ([[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
vars)))) ([Named Term] -> [Named Term]) -> [Named Term] -> [Named Term]
forall a b. (a -> b) -> a -> b
$ DataPat -> Term -> [[(Selector, VarDecl)]] -> [Named Term]
makeSelEqs DataPat
dt Term
ct [[(Selector, VarDecl)]]
selvars

mkSelArgs :: [[VarDecl]] -> [Term]
mkSelArgs :: [[VarDecl]] -> [Term]
mkSelArgs = ([VarDecl] -> Term) -> [[VarDecl]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ vs :: [VarDecl]
vs -> [Term] -> Range -> Term
mkTupleTerm ((VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
vs) Range
nullRange)

getConstrScheme :: DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme :: DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme (DataPat dm :: IdMap
dm _ args :: [TypeArg]
args _ rt :: Type
rt) p :: Partiality
p ts :: [Type]
ts =
  let realTs :: [Type]
realTs = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Type -> Type
mapType IdMap
dm) [Type]
ts
  in [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
args (Type -> Partiality -> [Type] -> Type
getFunType Type
rt Partiality
p [Type]
realTs) Range
nullRange

getSelScheme :: DataPat -> Partiality -> Type -> TypeScheme
getSelScheme :: DataPat -> Partiality -> Type -> TypeScheme
getSelScheme (DataPat dm :: IdMap
dm _ args :: [TypeArg]
args _ rt :: Type
rt) p :: Partiality
p t :: Type
t =
  let realT :: Type
realT = IdMap -> Type -> Type
mapType IdMap
dm Type
t
  in [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
args (Type -> Partiality -> Type -> Type
getSelType Type
rt Partiality
p Type
realT) Range
nullRange

-- | remove variances from generalized type arguments
toDataPat :: DataEntry -> DataPat
toDataPat :: DataEntry -> DataPat
toDataPat (DataEntry im :: IdMap
im i :: Id
i _ args :: [TypeArg]
args rk :: RawKind
rk _) = let j :: Id
j = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i IdMap
im in
  IdMap -> Id -> [TypeArg] -> RawKind -> Type -> DataPat
DataPat IdMap
im Id
j ((TypeArg -> TypeArg) -> [TypeArg] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> TypeArg
nonVarTypeArg [TypeArg]
args) RawKind
rk (Type -> DataPat) -> Type -> DataPat
forall a b. (a -> b) -> a -> b
$ Id -> [TypeArg] -> RawKind -> Type
patToType Id
j [TypeArg]
args RawKind
rk

-- | create selector equations for a data type
makeDataSelEqs :: DataPat -> [AltDefn] -> [Named Sentence]
makeDataSelEqs :: DataPat -> [AltDefn] -> [Named Sentence]
makeDataSelEqs dp :: DataPat
dp = (Named Term -> Named Sentence) -> [Named Term] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Sentence) -> Named Term -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed Term -> Sentence
Formula) ([Named Term] -> [Named Sentence])
-> ([AltDefn] -> [Named Term]) -> [AltDefn] -> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AltDefn -> [Named Term]) -> [AltDefn] -> [Named Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataPat -> AltDefn -> [Named Term]
makeAltSelEqs DataPat
dp)

-- | analyse the alternatives of a data type
anaAlts :: GenKind -> [DataPat] -> DataPat -> [Alternative] -> Env
        -> Result [AltDefn]
anaAlts :: GenKind
-> [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
anaAlts genKind :: GenKind
genKind tys :: [DataPat]
tys dt :: DataPat
dt alts :: [Alternative]
alts te :: Env
te =
    do [AltDefn]
l <- (Alternative -> Result AltDefn)
-> [Alternative] -> Result [AltDefn]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (GenKind
-> [DataPat] -> DataPat -> Env -> Alternative -> Result AltDefn
anaAlt GenKind
genKind [DataPat]
tys DataPat
dt Env
te) [Alternative]
alts
       [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Id] -> [Diagnosis]) -> [Id] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ (AltDefn -> Maybe Id) -> [AltDefn] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ( \ (Construct i :: Maybe Id
i _ _ _) -> Maybe Id
i) [AltDefn]
l)
         (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
       [AltDefn] -> Result [AltDefn]
forall (m :: * -> *) a. Monad m => a -> m a
return [AltDefn]
l

anaAlt :: GenKind -> [DataPat] -> DataPat -> Env -> Alternative
       -> Result AltDefn
anaAlt :: GenKind
-> [DataPat] -> DataPat -> Env -> Alternative -> Result AltDefn
anaAlt _ _ _ te :: Env
te (Subtype ts :: [Type]
ts _) =
    do [((RawKind, Set Kind), Type)]
l <- (Type -> Result ((RawKind, Set Kind), Type))
-> [Type] -> Result [((RawKind, Set Kind), Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Env -> Result ((RawKind, Set Kind), Type)
`anaStarTypeM` Env
te) [Type]
ts
       AltDefn -> Result AltDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (AltDefn -> Result AltDefn) -> AltDefn -> Result AltDefn
forall a b. (a -> b) -> a -> b
$ Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct Maybe Id
forall a. Maybe a
Nothing (Set Type -> [Type]
forall a. Set a -> [a]
Set.toList (Set Type -> [Type]) -> Set Type -> [Type]
forall a b. (a -> b) -> a -> b
$ [Type] -> Set Type
forall a. Ord a => [a] -> Set a
Set.fromList ([Type] -> Set Type) -> [Type] -> Set Type
forall a b. (a -> b) -> a -> b
$ (((RawKind, Set Kind), Type) -> Type)
-> [((RawKind, Set Kind), Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((RawKind, Set Kind), Type) -> Type
forall a b. (a, b) -> b
snd [((RawKind, Set Kind), Type)]
l)
           Partiality
Partial []
anaAlt genKind :: GenKind
genKind tys :: [DataPat]
tys dt :: DataPat
dt te :: Env
te (Constructor i :: Id
i cs :: [[Component]]
cs p :: Partiality
p _) =
    do [(Type, [Selector])]
newCs <- ([Component] -> Result (Type, [Selector]))
-> [[Component]] -> Result [(Type, [Selector])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (GenKind
-> [DataPat]
-> DataPat
-> Env
-> [Component]
-> Result (Type, [Selector])
anaComps GenKind
genKind [DataPat]
tys DataPat
dt Env
te) [[Component]]
cs
       let sels :: [[Selector]]
sels = ((Type, [Selector]) -> [Selector])
-> [(Type, [Selector])] -> [[Selector]]
forall a b. (a -> b) -> [a] -> [b]
map (Type, [Selector]) -> [Selector]
forall a b. (a, b) -> b
snd [(Type, [Selector])]
newCs
       [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Id] -> [Diagnosis])
-> ([Selector] -> [Id]) -> [Selector] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Selector -> Maybe Id) -> [Selector] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ( \ (Select s :: Maybe Id
s _ _) -> Maybe Id
s )
              ([Selector] -> [Diagnosis]) -> [Selector] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ [[Selector]] -> [Selector]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Selector]]
sels) (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
       AltDefn -> Result AltDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (AltDefn -> Result AltDefn) -> AltDefn -> Result AltDefn
forall a b. (a -> b) -> a -> b
$ Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i) (((Type, [Selector]) -> Type) -> [(Type, [Selector])] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, [Selector]) -> Type
forall a b. (a, b) -> a
fst [(Type, [Selector])]
newCs) Partiality
p [[Selector]]
sels

anaComps :: GenKind -> [DataPat] -> DataPat -> Env -> [Component]
         -> Result (Type, [Selector])
anaComps :: GenKind
-> [DataPat]
-> DataPat
-> Env
-> [Component]
-> Result (Type, [Selector])
anaComps genKind :: GenKind
genKind tys :: [DataPat]
tys rt :: DataPat
rt te :: Env
te cs :: [Component]
cs =
    do [(Type, Selector)]
newCs <- (Component -> Result (Type, Selector))
-> [Component] -> Result [(Type, Selector)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (GenKind
-> [DataPat]
-> DataPat
-> Env
-> Component
-> Result (Type, Selector)
anaComp GenKind
genKind [DataPat]
tys DataPat
rt Env
te) [Component]
cs
       (Type, [Selector]) -> Result (Type, [Selector])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
mkProductType ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ ((Type, Selector) -> Type) -> [(Type, Selector)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Selector) -> Type
forall a b. (a, b) -> a
fst [(Type, Selector)]
newCs, ((Type, Selector) -> Selector) -> [(Type, Selector)] -> [Selector]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Selector) -> Selector
forall a b. (a, b) -> b
snd [(Type, Selector)]
newCs)

isPartialSelector :: Type -> Bool
isPartialSelector :: Type -> Bool
isPartialSelector ty :: Type
ty = case Type
ty of
  TypeAppl (TypeName i :: Id
i _ _) _ -> Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId
  _ -> Bool
False

anaComp :: GenKind -> [DataPat] -> DataPat -> Env -> Component
        -> Result (Type, Selector)
anaComp :: GenKind
-> [DataPat]
-> DataPat
-> Env
-> Component
-> Result (Type, Selector)
anaComp genKind :: GenKind
genKind tys :: [DataPat]
tys rt :: DataPat
rt te :: Env
te (Selector s :: Id
s _ t :: Type
t _ _) =
    do Type
ct <- GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
anaCompType GenKind
genKind [DataPat]
tys DataPat
rt Type
t Env
te
       let (p :: Partiality
p, nct :: Type
nct) = case Type -> (Type, [Type])
getTypeAppl Type
ct of
             (TypeName i :: Id
i _ _, [lt :: Type
lt]) | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId
                Bool -> Bool -> Bool
&& Type -> Bool
isPartialSelector Type
t -> (Partiality
Partial, Type
lt)
             _ -> (Partiality
Total, Type
ct)
       (Type, Selector) -> Result (Type, Selector)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
nct, Maybe Id -> Type -> Partiality -> Selector
Select (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s) Type
nct Partiality
p)
anaComp genKind :: GenKind
genKind tys :: [DataPat]
tys rt :: DataPat
rt te :: Env
te (NoSelector t :: Type
t) =
    do Type
ct <- GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
anaCompType GenKind
genKind [DataPat]
tys DataPat
rt Type
t Env
te
       (Type, Selector) -> Result (Type, Selector)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ct, Maybe Id -> Type -> Partiality -> Selector
Select Maybe Id
forall a. Maybe a
Nothing Type
ct Partiality
Partial)

anaCompType :: GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
anaCompType :: GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
anaCompType genKind :: GenKind
genKind tys :: [DataPat]
tys (DataPat _ _ tArgs :: [TypeArg]
tArgs _ _) t :: Type
t te :: Env
te = do
    (_, ct :: Type
ct) <- Type -> Env -> Result ((RawKind, Set Kind), Type)
anaStarTypeM Type
t Env
te
    let ds :: [Diagnosis]
ds = Bool -> [TypeArg] -> Type -> [Diagnosis]
unboundTypevars Bool
True [TypeArg]
tArgs Type
ct
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe ()
forall a. Maybe a
Nothing
    (DataPat -> Result ()) -> [DataPat] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Type -> Env -> DataPat -> Result ()
checkMonomorphRecursion Type
ct Env
te) [DataPat]
tys
    (DataPat -> Result ()) -> [DataPat] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenKind -> Type -> Env -> DataPat -> Result ()
rejectNegativeOccurrence GenKind
genKind Type
ct Env
te) [DataPat]
tys
    Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Type
generalize [TypeArg]
tArgs Type
ct

checkMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
checkMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
checkMonomorphRecursion t :: Type
t te :: Env
te (DataPat _ i :: Id
i _ _ rt :: Type
rt) =
    case (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ ty :: Type
ty -> Bool -> Bool
not (Env -> Type -> Type -> Bool
lesserType Env
te Type
ty Type
rt Bool -> Bool -> Bool
|| Env -> Type -> Type -> Bool
lesserType Env
te Type
rt Type
ty))
       ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Id -> Bool) -> Id -> Type -> [Type]
findSubTypes (TypeMap -> Id -> Id -> Bool
relatedTypeIds (Env -> TypeMap
typeMap Env
te) Id
i) Id
i Type
t of
      [] -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      ty :: Type
ty : _ -> [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("illegal polymorphic recursion"
                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> Type -> String
forall a. Pretty a => a -> a -> String
expected Type
rt Type
ty) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Type -> Range
forall a. GetRange a => a -> Range
getRange Type
ty] Maybe ()
forall a. Maybe a
Nothing

findSubTypes :: (Id -> Bool) -> Id -> Type -> [Type]
findSubTypes :: (Id -> Bool) -> Id -> Type -> [Type]
findSubTypes chk :: Id -> Bool
chk i :: Id
i t :: Type
t = case Type -> (Type, [Type])
getTypeAppl Type
t of
    (TypeName j :: Id
j _ _, args :: [Type]
args) -> if Id -> Bool
chk Id
j then [Type
t]
                              else (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Id -> Bool) -> Id -> Type -> [Type]
findSubTypes Id -> Bool
chk Id
i) [Type]
args
    (topTy :: Type
topTy, args :: [Type]
args) -> (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Id -> Bool) -> Id -> Type -> [Type]
findSubTypes Id -> Bool
chk Id
i) ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Type
topTy Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
args

rejectNegativeOccurrence :: GenKind -> Type -> Env -> DataPat -> Result ()
rejectNegativeOccurrence :: GenKind -> Type -> Env -> DataPat -> Result ()
rejectNegativeOccurrence genKind :: GenKind
genKind t :: Type
t te :: Env
te (DataPat _ i :: Id
i _ _ _) =
    case Env -> Id -> Type -> [Type]
findNegativeOccurrence Env
te Id
i Type
t of
      [] -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      ty :: Type
ty : _ -> [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag (case GenKind
genKind of
             Free -> DiagKind
Error
             _ -> DiagKind
Hint) "negative datatype occurrence of" Type
ty] (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()

findNegativeOccurrence :: Env -> Id -> Type -> [Type]
findNegativeOccurrence :: Env -> Id -> Type -> [Type]
findNegativeOccurrence te :: Env
te i :: Id
i t :: Type
t = let tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
te in case Type -> (Type, [Type])
getTypeAppl Type
t of
    (TypeName j :: Id
j _ _, _) | TypeMap -> Id -> Id -> Bool
relatedTypeIds TypeMap
tm Id
i Id
j ->
      [] -- positive occurrence
    (topTy :: Type
topTy, [larg :: Type
larg, rarg :: Type
rarg]) | Env -> Type -> Type -> Bool
lesserType Env
te Type
topTy (Arrow -> Type
toFunType Arrow
PFunArr) ->
       (Id -> Bool) -> Id -> Type -> [Type]
findSubTypes (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i) Id
i Type
larg [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ Env -> Id -> Type -> [Type]
findNegativeOccurrence Env
te Id
i Type
rarg
    (_, args :: [Type]
args) -> (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env -> Id -> Type -> [Type]
findNegativeOccurrence Env
te Id
i) [Type]
args

relatedTypeIds :: TypeMap -> Id -> Id -> Bool
relatedTypeIds :: TypeMap -> Id -> Id -> Bool
relatedTypeIds tm :: TypeMap
tm i1 :: Id
i1 i2 :: Id
i2 =
    Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Id -> Bool
forall a. Set a -> Bool
Set.null (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (TypeMap -> Id -> Set Id
allRelIds TypeMap
tm Id
i1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeMap -> Id -> Set Id
allRelIds TypeMap
tm Id
i2

allRelIds :: TypeMap -> Id -> Set.Set Id
allRelIds :: TypeMap -> Id -> Set Id
allRelIds tm :: TypeMap
tm i :: Id
i = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TypeMap -> Id -> Set Id
superIds TypeMap
tm Id
i) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeMap -> Id -> Set Id
subIds TypeMap
tm Id
i

subIds :: TypeMap -> Id -> Set.Set Id
subIds :: TypeMap -> Id -> Set Id
subIds tm :: TypeMap
tm i :: Id
i = (Id -> Set Id -> Set Id) -> Set Id -> [Id] -> Set Id
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ j :: Id
j s :: Set Id
s ->
                 if Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ TypeMap -> Id -> Set Id
superIds TypeMap
tm Id
j then
                      Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
j Set Id
s else Set Id
s) Set Id
forall a. Set a
Set.empty ([Id] -> Set Id) -> [Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeMap -> [Id]
forall k a. Map k a -> [k]
Map.keys TypeMap
tm

mkPredVar :: DataPat -> VarDecl
mkPredVar :: DataPat -> VarDecl
mkPredVar (DataPat _ i :: Id
i _ _ rt :: Type
rt) = let ps :: Range
ps = Id -> Range
posOfId Id
i in
  Id -> Type -> VarDecl
mkVarDecl (if Id -> Bool
isSimpleId Id
i then [Token] -> Id
mkId [String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ "p_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i]
             else [Token] -> [Id] -> Range -> Id
Id [String -> Token
mkSimpleId "p"] [Id
i] Range
ps) (Range -> Type -> Type
predType Range
ps Type
rt)

mkPredAppl :: DataPat -> Term -> Term
mkPredAppl :: DataPat -> Term -> Term
mkPredAppl dp :: DataPat
dp t :: Term
t = Term -> [Term] -> Term
mkApplTerm (VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ DataPat -> VarDecl
mkPredVar DataPat
dp) [Term
t]

mkPredToVarAppl :: DataPat -> VarDecl -> Term
mkPredToVarAppl :: DataPat -> VarDecl -> Term
mkPredToVarAppl dp :: DataPat
dp = DataPat -> Term -> Term
mkPredAppl DataPat
dp (Term -> Term) -> (VarDecl -> Term) -> VarDecl -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl -> Term
QualVar

mkConclusion :: DataPat -> Term
mkConclusion :: DataPat -> Term
mkConclusion dp :: DataPat
dp@(DataPat _ _ _ _ ty :: Type
ty) =
  let v :: VarDecl
v = Id -> Type -> VarDecl
mkVarDecl ([Token] -> Id
mkId [String -> Token
mkSimpleId "x"]) Type
ty
  in [GenVarDecl] -> Term -> Term
mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
v] (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ DataPat -> VarDecl -> Term
mkPredToVarAppl DataPat
dp VarDecl
v

mkPremise :: Map.Map Type DataPat -> DataPat -> AltDefn -> [Term]
mkPremise :: Map Type DataPat -> DataPat -> AltDefn -> [Term]
mkPremise m :: Map Type DataPat
m dp :: DataPat
dp (Construct mc :: Maybe Id
mc ts :: [Type]
ts p :: Partiality
p sels :: [[Selector]]
sels) =
    case Maybe Id
mc of
    Nothing -> []
    Just c :: Id
c -> let
      vars :: [[VarDecl]]
vars = ([(Selector, VarDecl)] -> [VarDecl])
-> [[(Selector, VarDecl)]] -> [[VarDecl]]
forall a b. (a -> b) -> [a] -> [b]
map (((Selector, VarDecl) -> VarDecl)
-> [(Selector, VarDecl)] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Selector, VarDecl) -> VarDecl
forall a b. (a, b) -> b
snd) ([[(Selector, VarDecl)]] -> [[VarDecl]])
-> [[(Selector, VarDecl)]] -> [[VarDecl]]
forall a b. (a -> b) -> a -> b
$ Int -> [[Selector]] -> [[(Selector, VarDecl)]]
genSelVars 1 [[Selector]]
sels
      findHypo :: VarDecl -> Maybe Term
findHypo vd :: VarDecl
vd@(VarDecl _ ty :: Type
ty _ _) =
        (DataPat -> Term) -> Maybe DataPat -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DataPat -> VarDecl -> Term
`mkPredToVarAppl` VarDecl
vd) (Maybe DataPat -> Maybe Term) -> Maybe DataPat -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Type -> Map Type DataPat -> Maybe DataPat
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Type
ty Map Type DataPat
m
      flatVars :: [VarDecl]
flatVars = [[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
vars
      indHypos :: [Term]
indHypos = (VarDecl -> Maybe Term) -> [VarDecl] -> [Term]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VarDecl -> Maybe Term
findHypo [VarDecl]
flatVars
      indConcl :: Term
indConcl = DataPat -> Term -> Term
mkPredAppl DataPat
dp
        (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (Id -> TypeScheme -> Term
mkOpTerm Id
c (TypeScheme -> Term) -> TypeScheme -> Term
forall a b. (a -> b) -> a -> b
$ DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme DataPat
dp Partiality
p [Type]
ts)
        ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [[VarDecl]] -> [Term]
mkSelArgs [[VarDecl]]
vars
      in [[GenVarDecl] -> Term -> Term
mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
flatVars) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
          if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
indHypos then Term
indConcl else
           Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nullRange ([Term] -> Term
mkConjunct [Term]
indHypos) Term
indConcl]

mkConjunct :: [Term] -> Term
mkConjunct :: [Term] -> Term
mkConjunct ts :: [Term]
ts = if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts then String -> Term
forall a. HasCallStack => String -> a
error "HasCASL.DataAna.mkConjunct" else
  Id -> [Term] -> Range -> Term
toBinJunctor Id
andId [Term]
ts Range
nullRange

mkPremises :: Map.Map Type DataPat -> DataEntry -> [Term]
mkPremises :: Map Type DataPat -> DataEntry -> [Term]
mkPremises m :: Map Type DataPat
m de :: DataEntry
de@(DataEntry _ _ _ _ _ alts :: Set AltDefn
alts) =
    (AltDefn -> [Term]) -> [AltDefn] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Map Type DataPat -> DataPat -> AltDefn -> [Term]
mkPremise Map Type DataPat
m (DataPat -> AltDefn -> [Term]) -> DataPat -> AltDefn -> [Term]
forall a b. (a -> b) -> a -> b
$ DataEntry -> DataPat
toDataPat DataEntry
de) ([AltDefn] -> [Term]) -> [AltDefn] -> [Term]
forall a b. (a -> b) -> a -> b
$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
alts

joinTypeArgs :: [DataPat] -> Map.Map Id TypeArg
joinTypeArgs :: [DataPat] -> Map Id TypeArg
joinTypeArgs = (DataPat -> Map Id TypeArg -> Map Id TypeArg)
-> Map Id TypeArg -> [DataPat] -> Map Id TypeArg
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (DataPat _ _ iargs :: [TypeArg]
iargs _ _) m :: Map Id TypeArg
m ->
   (TypeArg -> Map Id TypeArg -> Map Id TypeArg)
-> Map Id TypeArg -> [TypeArg] -> Map Id TypeArg
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ta :: TypeArg
ta -> Id -> TypeArg -> Map Id TypeArg -> Map Id TypeArg
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TypeArg -> Id
getTypeVar TypeArg
ta) TypeArg
ta) Map Id TypeArg
m [TypeArg]
iargs) Map Id TypeArg
forall k a. Map k a
Map.empty

inductionScheme :: [DataEntry] -> Term
inductionScheme :: [DataEntry] -> Term
inductionScheme des :: [DataEntry]
des =
    let dps :: [DataPat]
dps = (DataEntry -> DataPat) -> [DataEntry] -> [DataPat]
forall a b. (a -> b) -> [a] -> [b]
map DataEntry -> DataPat
toDataPat [DataEntry]
des
        m :: Map Type DataPat
m = [(Type, DataPat)] -> Map Type DataPat
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Type, DataPat)] -> Map Type DataPat)
-> [(Type, DataPat)] -> Map Type DataPat
forall a b. (a -> b) -> a -> b
$ (DataPat -> (Type, DataPat)) -> [DataPat] -> [(Type, DataPat)]
forall a b. (a -> b) -> [a] -> [b]
map (\ dp :: DataPat
dp@(DataPat _ _ _ _ ty :: Type
ty) -> (Type
ty, DataPat
dp)) [DataPat]
dps
    in [GenVarDecl] -> Term -> Term
mkForall ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl (Map Id TypeArg -> [TypeArg]
forall k a. Map k a -> [a]
Map.elems (Map Id TypeArg -> [TypeArg]) -> Map Id TypeArg -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ [DataPat] -> Map Id TypeArg
joinTypeArgs [DataPat]
dps)
                 [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (DataPat -> GenVarDecl) -> [DataPat] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl)
-> (DataPat -> VarDecl) -> DataPat -> GenVarDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataPat -> VarDecl
mkPredVar) [DataPat]
dps)
       (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nullRange
         ([Term] -> Term
mkConjunct ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (DataEntry -> [Term]) -> [DataEntry] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Map Type DataPat -> DataEntry -> [Term]
mkPremises Map Type DataPat
m) [DataEntry]
des)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkConjunct ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (DataPat -> Term) -> [DataPat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map DataPat -> Term
mkConclusion [DataPat]
dps