81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : analysis of data type declarations
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional
fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederPortability : portable
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederanalyse alternatives of data types
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder , getConstrScheme
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder , getSelScheme
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , makeDataSelEqs
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder , inductionScheme
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Data.Maybe (mapMaybe)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport qualified Data.Map as Map
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport qualified Data.Set as Set
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder{- | description of polymorphic data types. The top-level identifier is
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederalready renamed according the IdMap. -}
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederdata DataPat = DataPat IdMap Id [TypeArg] RawKind Type
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkVarDecl :: Id -> Type -> VarDecl
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkVarDecl i t = VarDecl i t Other nullRange
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkSelId :: Range -> String -> Int -> Int -> Id
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedermkSelId p str n m = mkId
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder [Token (str ++ "_" ++ (if n < 1 then "" else show n ++ "_") ++ show m) p]
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedermkSelVar :: Int -> Int -> Type -> VarDecl
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkSelVar n m ty = mkVarDecl (mkSelId (getRange ty) "x" n m) ty
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedergenTuple :: Int -> Int -> [Selector] -> [(Selector, VarDecl)]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedergenTuple _ _ [] = []
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedergenTuple n m (s@(Select _ ty _) : sels) =
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder (s, mkSelVar n m ty) : genTuple n (m + 1) sels
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedergenSelVars :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedergenSelVars n sels = case sels of
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder [ts] -> [genTuple 0 1 ts]
4cf9b5b0484a15c0f071ef7898cdcc3a44a15429Christian Maeder _ -> if all isSingle sels
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder then map (: []) $ genTuple 0 1 $ map head sels
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder else genSelVarsAux n sels
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenSelVarsAux :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedergenSelVarsAux _ [] = []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenSelVarsAux n (ts : sels) =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder genTuple n 1 ts : genSelVarsAux (n + 1) sels
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedermakeSelTupleEqs :: DataPat -> Term -> [(Selector, VarDecl)] -> [Named Term]
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedermakeSelTupleEqs dt ct = concatMap (\ (Select mi ty p, v) -> case mi of
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Just i -> let
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder sc = getSelScheme dt p ty
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder eq = mkEqTerm eqId ty nullRange
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder (mkApplTerm (mkOpTerm i sc) [ct]) $ QualVar v
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder in [makeNamed ("ga_select_" ++ show i) eq]
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedermakeSelEqs :: DataPat -> Term -> [[(Selector, VarDecl)]] -> [Named Term]
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermakeSelEqs dt = concatMap . makeSelTupleEqs dt
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedermakeAltSelEqs dt@(DataPat _ _ iargs _ _) (Construct mc ts p sels) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> []
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder Just c -> let
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder selvars = genSelVars 1 sels
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder vars = map (map snd) selvars
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ars = mkSelArgs vars
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ct = mkApplTerm (mkOpTerm c $ getConstrScheme dt p ts) ars
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder in map (mapNamed (mkForall (map GenTypeVarDecl iargs
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder ++ map GenVarDecl (concat vars)))) $ makeSelEqs dt ct selvars
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedermkSelArgs :: [[VarDecl]] -> [Term]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedermkSelArgs = map (\ vs -> mkTupleTerm (map QualVar vs) nullRange)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetConstrScheme :: DataPat -> Partiality -> [Type] -> TypeScheme
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedergetConstrScheme (DataPat dm _ args _ rt) p ts =
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder let realTs = map (mapType dm) ts
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in TypeScheme args (getFunType rt p realTs) nullRange
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetSelScheme :: DataPat -> Partiality -> Type -> TypeScheme
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedergetSelScheme (DataPat dm _ args _ rt) p t =
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder let realT = mapType dm t
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in TypeScheme args (getSelType rt p realT) nullRange
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder-- | remove variances from generalized type arguments
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedertoDataPat :: DataEntry -> DataPat
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian MaedertoDataPat (DataEntry im i _ args rk _) = let j = Map.findWithDefault i i im in
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder DataPat im j (map nonVarTypeArg args) rk $ patToType j args rk
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- | create selector equations for a data type
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedermakeDataSelEqs :: DataPat -> [AltDefn] -> [Named Sentence]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedermakeDataSelEqs dp = map (mapNamed Formula) . concatMap (makeAltSelEqs dp)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- | analyse the alternatives of a data type
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaAlts :: GenKind -> [DataPat] -> DataPat -> [Alternative] -> Env
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder -> Result [AltDefn]
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaAlts genKind tys dt alts te =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do l <- mapM (anaAlt genKind tys dt te) alts
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Result (checkUniqueness $ mapMaybe ( \ (Construct i _ _ _) -> i) l)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaAlt :: GenKind -> [DataPat] -> DataPat -> Env -> Alternative
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder -> Result AltDefn
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaAlt _ _ _ te (Subtype ts _) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do l <- mapM (`anaStarTypeM` te) ts
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder return $ Construct Nothing (Set.toList $ Set.fromList $ map snd l)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaAlt genKind tys dt te (Constructor i cs p _) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do newCs <- mapM (anaComps genKind tys dt te) cs
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let sels = map snd newCs
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Result (checkUniqueness . mapMaybe ( \ (Select s _ _) -> s )
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder $ concat sels) $ Just ()
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return $ Construct (Just i) (map fst newCs) p sels
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaComps :: GenKind -> [DataPat] -> DataPat -> Env -> [Component]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder -> Result (Type, [Selector])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaComps genKind tys rt te cs =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do newCs <- mapM (anaComp genKind tys rt te) cs
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (mkProductType $ map fst newCs, map snd newCs)
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaederisPartialSelector :: Type -> Bool
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaederisPartialSelector ty = case ty of
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder TypeAppl (TypeName i _ _) _ -> i == lazyTypeId
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaComp :: GenKind -> [DataPat] -> DataPat -> Env -> Component
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Result (Type, Selector)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaComp genKind tys rt te (Selector s _ t _ _) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do ct <- anaCompType genKind tys rt t te
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder let (p, nct) = case getTypeAppl ct of
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder (TypeName i _ _, [lt]) | i == lazyTypeId
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder && isPartialSelector t -> (Partial, lt)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> (Total, ct)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder return (nct, Select (Just s) nct p)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaComp genKind tys rt te (NoSelector t) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do ct <- anaCompType genKind tys rt t te
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (ct, Select Nothing ct Partial)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederanaCompType :: GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaederanaCompType genKind tys (DataPat _ _ tArgs _ _) t te = do
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder (_, ct) <- anaStarTypeM t te
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder let ds = unboundTypevars True tArgs ct
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder unless (null ds) $ Result ds Nothing
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder mapM_ (checkMonomorphRecursion ct te) tys
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder mapM_ (rejectNegativeOccurrence genKind ct te) tys
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder return $ generalize tArgs ct
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercheckMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedercheckMonomorphRecursion t te (DataPat _ i _ _ rt) =
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder $ findSubTypes (relatedTypeIds (typeMap te) i) i t of
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder [] -> return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder ++ expected rt ty) $ getRange ty] Nothing
7344fe509f1a733c88a72b05f9beff070af4701aChristian MaederfindSubTypes :: (Id -> Bool) -> Id -> Type -> [Type]
7344fe509f1a733c88a72b05f9beff070af4701aChristian MaederfindSubTypes chk i t = case getTypeAppl t of
7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder (TypeName j _ _, args) -> if chk j then [t]
7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder else concatMap (findSubTypes chk i) args
7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder (topTy, args) -> concatMap (findSubTypes chk i) $ topTy : args
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederrejectNegativeOccurrence :: GenKind -> Type -> Env -> DataPat -> Result ()
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaederrejectNegativeOccurrence genKind t te (DataPat _ i _ _ _) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder case findNegativeOccurrence te i t of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder [] -> return ()
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder ty : _ -> Result [mkDiag (case genKind of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Free -> Error
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder _ -> Hint) "negative datatype occurrence of" ty] $ Just ()
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederfindNegativeOccurrence :: Env -> Id -> Type -> [Type]
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederfindNegativeOccurrence te i t = let tm = typeMap te in case getTypeAppl t of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (TypeName j _ _, _) | relatedTypeIds tm i j ->
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder [] -- positive occurrence
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (topTy, [larg, rarg]) | lesserType te topTy (toFunType PFunArr) ->
7344fe509f1a733c88a72b05f9beff070af4701aChristian Maeder findSubTypes (== i) i larg ++ findNegativeOccurrence te i rarg
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (_, args) -> concatMap (findNegativeOccurrence te i) args
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederrelatedTypeIds :: TypeMap -> Id -> Id -> Bool
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederrelatedTypeIds tm i1 i2 =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederallRelIds :: TypeMap -> Id -> Set.Set Id
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederallRelIds tm i = Set.union (superIds tm i) $ subIds tm i
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedersubIds :: TypeMap -> Id -> Set.Set Id
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedersubIds tm i = foldr ( \ j s ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if Set.member i $ superIds tm j then
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Set.insert j s else s) Set.empty $ Map.keys tm
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPredVar :: DataPat -> VarDecl
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedermkPredVar (DataPat _ i _ _ rt) = let ps = posOfId i in
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder mkVarDecl (if isSimpleId i then mkId [mkSimpleId $ "p_" ++ show i]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder else Id [mkSimpleId "p"] [i] ps) (predType ps rt)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPredAppl :: DataPat -> Term -> Term
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPredAppl dp t = mkApplTerm (QualVar $ mkPredVar dp) [t]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPredToVarAppl :: DataPat -> VarDecl -> Term
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPredToVarAppl dp = mkPredAppl dp . QualVar
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkConclusion :: DataPat -> Term
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedermkConclusion dp@(DataPat _ _ _ _ ty) =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder let v = mkVarDecl (mkId [mkSimpleId "x"]) ty
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder in mkForall [GenVarDecl v] $ mkPredToVarAppl dp v
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPremise :: Map.Map Type DataPat -> DataPat -> AltDefn -> [Term]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPremise m dp (Construct mc ts p sels) =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Nothing -> []
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Just c -> let
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder vars = map (map snd) $ genSelVars 1 sels
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder findHypo vd@(VarDecl _ ty _ _) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fmap (`mkPredToVarAppl` vd) $ Map.lookup ty m
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder flatVars = concat vars
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder indHypos = mapMaybe findHypo flatVars
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder indConcl = mkPredAppl dp
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder $ mkApplTerm (mkOpTerm c $ getConstrScheme dp p ts)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder $ mkSelArgs vars
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder in [mkForall (map GenVarDecl flatVars) $
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder if null indHypos then indConcl else
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder mkLogTerm implId nullRange (mkConjunct indHypos) indConcl]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkConjunct :: [Term] -> Term
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkConjunct ts = if null ts then error "HasCASL.DataAna.mkConjunct" else
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder toBinJunctor andId ts nullRange
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPremises :: Map.Map Type DataPat -> DataEntry -> [Term]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermkPremises m de@(DataEntry _ _ _ _ _ alts) =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder concatMap (mkPremise m $ toDataPat de) $ Set.toList alts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederjoinTypeArgs :: [DataPat] -> Map.Map Id TypeArg
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaederjoinTypeArgs = foldr (\ (DataPat _ _ iargs _ _) m ->
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder foldr (\ ta -> Map.insert (getTypeVar ta) ta) m iargs) Map.empty
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederinductionScheme :: [DataEntry] -> Term
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederinductionScheme des =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder let dps = map toDataPat des
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder m = Map.fromList $ map (\ dp@(DataPat _ _ _ _ ty) -> (ty, dp)) dps
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder in mkForall (map GenTypeVarDecl (Map.elems $ joinTypeArgs dps)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder ++ map (GenVarDecl . mkPredVar) dps)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder $ mkLogTerm implId nullRange
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (mkConjunct $ concatMap (mkPremises m) des)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder $ mkConjunct $ map mkConclusion dps