9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{- |

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederModule : $Header$

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeCopyright : (c) Christian Maeder and Uni Bremen 2003

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicence : All rights reserved.

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeMaintainer : hets@tzi.de

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability : experimental

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : portable

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maedertype inference

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-}

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkemodule HasCASL.TypeCheck where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.Unify

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.VarDecl

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.As

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.AsUtils

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.Le

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.MixAna

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Common.Lib.Map as Map

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Common.Id

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Common.Result

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Common.GlobalAnnotations

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Common.Lib.State

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Data.Maybe

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaVar :: Id

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaVar = simpleIdToId $ mkSimpleId "a"

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaType :: Type

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaType = TypeName aVar star 1

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkebindA :: Type -> TypeScheme

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkebindA ty = TypeScheme [TypeArg aVar star Other []] ([] :=> ty) []

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeeqType, logType, defType, notType, ifType :: TypeScheme

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeeqType = bindA $

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke FunType (ProductType [aType, aType] [])

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke PFunArr logicalType []

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkelogType = simpleTypeScheme $

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke FunType (ProductType [logicalType, logicalType] [])

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke PFunArr logicalType []

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederdefType = bindA $ FunType aType PFunArr logicalType []

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedernotType = simpleTypeScheme $ FunType logicalType PFunArr logicalType []

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederifType = bindA $

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder FunType (ProductType [logicalType, aType, aType] [])

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder PFunArr aType []

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkebList :: [(Id, TypeScheme)]

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkebList = (defId, defType) : (notId, notType) : (ifThenElse, ifType) :

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke map ( \ e -> (e, eqType)) [eqId, exEq] ++

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke map ( \ o -> (o, logType)) [andId, orId, eqvId, implId]

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaddUnit :: TypeMap -> TypeMap

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeaddUnit = let TypeName i k _ = logicalType in

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Map.insertWith ( \ _ old -> old) i

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (TypeInfo k [] [] NoTypeDefn)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederaddOps :: Assumps -> Assumps

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeaddOps as = foldr ( \ (i, sc) m ->

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Map.insertWith ( \ _ old -> old) i

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (OpInfos [OpInfo sc [] NoOpDefn]) m) as bList

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeresolveTerm :: GlobalAnnos -> Maybe Type -> Term -> State Env (Maybe Term)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeresolveTerm ga mt trm = do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke mtrm <- resolve ga trm

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case mtrm of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Nothing -> return Nothing

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just t -> typeCheck mt t

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkemUnifySc :: Maybe Type -> OpInfo

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> State Env (Maybe (Subst, Type, OpInfo))

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkemUnifySc mt oi = do

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tm <- gets typeMap

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ty <- toEnvState $ freshInst $ opType oi

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke let Result ds ms = mUnify tm mt ty

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke addDiags ds

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case ms of Nothing -> return Nothing

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder Just s -> return $ Just (s, subst s ty, oi)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercheckList :: [Type] -> [Term] -> State Env [(Subst, [Type], [Term])]

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercheckList [] [] = return [(eps, [], [])]

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercheckList (ty : rty) (trm : rt) = do

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder fts <- infer (Just ty) trm

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder combs <- mapM ( \ (sf, tyf, tf) -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke rts <- checkList (map (subst sf) rty) rt

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke mapM ( \ (sr, tys, tts) ->

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return (compSubst sf sr,

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke subst sr tyf : tys,

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tf : tts)) rts) fts

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return $ concat combs

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecheckList _ _ = error "checkList"

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedertypeCheck :: Maybe Type -> Term -> State Env (Maybe Term)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedertypeCheck mt trm =

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder do alts <- infer mt trm

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder if null alts then

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder do addDiags [mkDiag Error "no typing for" trm]

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return Nothing

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke else if null $ tail alts then

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke let (_,_,t) = head alts in

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return $ Just t

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder else do addDiags [Diag Error

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ("ambiguous typings \n\t" ++

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke showSepList (showString "\n\t")

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke showPretty (take 5 $ map ( \ (_,_,t) -> t) alts) "")

$ posOfTerm trm]

return Nothing

freshTypeVar :: State Env Type

freshTypeVar = do var <- toEnvState freshVar

return $ TypeName var star 1

freshVars :: [a] -> State Env [Type]

freshVars l = mapM (const freshTypeVar) l

infer :: Maybe Type -> Term -> State Env [(Subst, Type, Term)]

infer mt trm = do

tm <- gets typeMap

as <- gets assumps

case trm of

QualVar v t ps -> do

let Result ds ms = mUnify tm mt t

addDiags ds

case ms of

Nothing -> return []

Just s -> let ty = (subst s t) in

return [(s, ty, QualVar v ty ps)]

QualOp io sc ps -> do

ty <- toEnvState $ freshInst sc

let Result ds ms = mUnify tm mt ty

addDiags ds

case ms of

Nothing -> return []

Just s -> return [(s, subst s ty, QualOp io sc ps)]

ResolvedMixTerm i ts ps ->

if null ts then do

let ois = opInfos $ Map.findWithDefault (OpInfos []) i as

mls <- mapM (mUnifySc mt) ois

let ls = catMaybes mls

if null ls then do addDiags [mkDiag Error "no match for" i]

return []

else return $ map ( \ (s, ty, oi) ->

case opDefn oi of

VarDefn -> (s, ty, QualVar i ty ps)

_ -> (s, ty, QualOp (InstOpId i [] [])

(opType oi) ps)) ls

else infer mt $ ApplTerm (ResolvedMixTerm i [] ps)

(if isSingle ts then head ts else TupleTerm ts ps) ps

ApplTerm t1 t2 ps -> do

aty <- freshTypeVar

rty <- case mt of

Nothing -> freshTypeVar

Just ty -> return ty

ops <- infer (Just $ FunType aty PFunArr rty []) t1

combs <- mapM ( \ (sf, _, tf) -> do

args <- infer (Just $ subst sf aty) t2

return $ map ( \ (sa, _, ta) ->

(compSubst sf sa,

subst sa (subst sf rty),

ApplTerm tf ta ps)) args) ops

let res = concat combs

if null res then

do addDiags [mkDiag Error "no type match for" trm]

return res

else return res

TupleTerm ts ps -> do

vs <- freshVars ts

let pt = ProductType vs []

Result ds ms = mUnify tm mt pt

addDiags ds

case ms of

Nothing -> return []

Just s -> do

ls <- checkList (subst s vs) ts

return $ map ( \ (su, tys, trms) ->

(compSubst s su, ProductType tys ps,

TupleTerm trms ps)) ls

TypedTerm t qual ty ps -> do

case qual of

OfType -> do

let Result ds ms = mUnify tm mt ty

addDiags ds

case ms of

Nothing -> return []

Just s -> do

rs <- infer (Just $ subst s ty) t

return $ map ( \ (s2, typ, tr) ->

(compSubst s s2, typ,

TypedTerm tr qual ty ps)) rs

InType -> do

let Result ds ms = mUnify tm mt logicalType

addDiags ds

case ms of

Nothing -> return []

Just s -> do

rs <- infer Nothing t

return $ map ( \ (s2, _, tr) ->

(compSubst s s2, logicalType,

TypedTerm tr qual ty ps)) rs

AsType -> do

let Result ds ms = mUnify tm mt ty

addDiags ds

case ms of

Nothing -> return []

Just s -> do

rs <- infer Nothing t

return $ map ( \ (s2, _, tr) ->

(compSubst s s2, subst s2 ty,

TypedTerm tr qual ty ps)) rs

QuantifiedTerm quant decls t ps -> do

mapM_ addGenVarDecl decls

let Result ds ms = mUnify tm mt logicalType

addDiags ds

case ms of

Nothing -> return []

Just _ -> do

rs <- infer (Just logicalType) t

putAssumps as

return $ map ( \ (s, typ, tr) ->

(s, typ, QuantifiedTerm quant decls tr ps)) rs

_ -> do ty <- freshTypeVar

return [(eps, ty, trm)]

{-

Quantifier [GenVarDecl] Term [Pos]

-- pos quantifier, ";"s, dot

-- only "forall" may have a TypeVarDecl

| LambdaTerm [Pattern] Partiality Term [Pos]

-- pos "\", dot (plus "!")

| CaseTerm Term [ProgEq] [Pos]

-- pos "case", "of", "|"s

| LetTerm [ProgEq] Term [Pos]

-}