module HaskHOL.Core.Parser.Elab
( tyElab
, elab
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics
import HaskHOL.Core.Parser.Lib hiding ((<?>))
type PEnv = [(Int, PreType)]
destSTV :: PreType -> Maybe Int
destSTV (STyVar n) = Just n
destSTV _ = Nothing
destUTy :: PreType -> Maybe String
destUTy (UTyVar _ x _) = Just x
destUTy _ = Nothing
destPUTy :: PreType -> Maybe (PreType, PreType)
destPUTy (PUTy tv ty) = Just (tv, ty)
destPUTy _ = Nothing
freeSTVS0 :: PreType -> [Int]
freeSTVS0 PTyCon{} = []
freeSTVS0 UTyVar{} = []
freeSTVS0 (STyVar n) = [n]
freeSTVS0 (PTyComb _ args) =
foldr (\ x y -> freeSTVS0 x `union` y) [] args
freeSTVS0 (PUTy _ tbody) = freeSTVS0 tbody
utyvars :: PreType -> [PreType]
utyvars PTyCon{} = []
utyvars tv@UTyVar{} = [tv]
utyvars STyVar{} = []
utyvars (PTyComb t args) = foldr (union . utyvars) [] $ t : args
utyvars (PUTy tv tbody) = utyvars tbody \\ [tv]
catUTyVars :: [PreType] -> [PreType]
catUTyVars = foldr (union . utyvars) []
variantUTyVar :: [PreType] -> PreType -> PreType
variantUTyVar avoid tv@(UTyVar f name n)
| tv `elem` avoid = variantUTyVar avoid $ UTyVar f (name ++ "'") n
| otherwise = tv
variantUTyVar _ tv = tv
mkFunPTy :: PreType -> PreType -> PreType
mkFunPTy pty1 pty2 = PTyComb (PTyCon "fun") [pty1, pty2]
mkTIConst :: String -> HOLType -> HOLTypeEnv -> HOL cls thry HOLTerm
mkTIConst c ty subs =
(do cty' <- liftM (typeSubst subs) $ getConstType c
let (mat1Tys, opTys, opOps) = fromJust $ typeMatch cty' ty ([], [], [])
tys' = map (second $ typeSubst mat1Tys) subs ++ mat1Tys
mat2 = (tys', opTys, opOps)
con <- mkConstFull c mat2
if typeOf con == ty
then return con
else mzero)
<?> "mkTIConst"
pmkNumeral :: Integer -> PreTerm
pmkNumeral = PComb numeral . pmkNumeralRec
where numPTy :: PreType
numPTy = PTyComb (PTyCon "num") []
numeral, bit0, bit1, t0 :: PreTerm
numeral = PConst "NUMERAL" $ mkFunPTy numPTy numPTy
bit0 = PConst "BIT0" $ mkFunPTy numPTy numPTy
bit1 = PConst "BIT1" $ mkFunPTy numPTy numPTy
t0 = PConst "_0" numPTy
pmkNumeralRec :: Integer -> PreTerm
pmkNumeralRec 0 = t0
pmkNumeralRec n =
let op = if n `mod` 2 == num0 then bit0 else bit1 in
PComb op . pmkNumeralRec $ n `div` 1
istrivial :: PEnv -> Int -> PreType -> Maybe Bool
istrivial _ _ PTyCon{} = Just False
istrivial env x (STyVar y)
| y == x = Just True
| otherwise =
(istrivial env x =<< lookup y env) <|> return False
istrivial _ _ UTyVar{} = Just False
istrivial env x (PTyComb f args) =
do ys' <- mapM (istrivial env x) $ f : args
if or ys'
then Nothing
else return False
istrivial env x (PUTy _ tbody) =
do tbody' <- istrivial env x tbody
if tbody'
then Nothing
else return False
newTypeVar :: HOL cls thry PreType
newTypeVar = return STyVar <*> tickTypeCounter
addTyApps :: PreTerm -> PreType -> HOL cls thry PreTerm
addTyApps tm ty@(PUTy tv tb) =
do ntv <- newTypeVar
addTyApps (TyPComb tm ty ntv) $ pretypeSubst [(ntv, tv)] tb
addTyApps tm _ = return tm
unifiableWithUType :: PreType -> PEnv -> Bool
unifiableWithUType ty env
| ty == dpty = False
| otherwise =
let tys = solve env ty in
isJust (destPUTy tys) || isJust (destSTV tys)
getGenericType :: String -> HOL cls thry HOLType
getGenericType cname =
do ctxt <- get
case filter (\ (x, _) -> x == cname) $ getInterface ctxt of
((_, (_, ty)):[]) -> return ty
(_:_:_) -> liftMaybe "getGenericType" . assoc cname $ getOverloads ctxt
_ -> getConstType cname
pretypeSubst :: [(PreType, PreType)] -> PreType -> PreType
pretypeSubst _ ty@PTyCon{} = ty
pretypeSubst tyenv ty@UTyVar{} = revAssocd ty tyenv ty
pretypeSubst _ ty@STyVar{} = ty
pretypeSubst tyenv ty@(PTyComb tyop args) =
let tyop' = pretypeSubst tyenv tyop
args' = map (pretypeSubst tyenv) args in
if tyop == tyop' && args == args' then ty
else case tyop' of
PUTy{} -> let (rtvs, rtbody) = splitList destPUTy tyop' in
pretypeSubst (zip args' rtvs) rtbody
_ -> PTyComb tyop' args'
pretypeSubst tyenv ty@(PUTy tv tbody) =
let tyenv' = filter (\ (_, x) -> x /= tv) tyenv in
if null tyenv' then ty
else if any (\ (t, x) -> tv `elem` utyvars t &&
x `elem` utyvars tbody) tyenv'
then let tvbody = utyvars tbody
tvpatts = map snd tyenv'
tvrepls = catUTyVars . map (\ x -> revAssocd x tyenv' x) $
intersect tvbody tvpatts
tv' = variantUTyVar ((tvbody \\ tvpatts) `union` tvrepls) tv in
PUTy tv' $ pretypeSubst ((tv', tv):tyenv') tbody
else PUTy tv $ pretypeSubst tyenv' tbody
solve :: PEnv -> PreType -> PreType
solve _ pty@PTyCon{} = pty
solve _ pty@UTyVar{} = pty
solve env pty@(STyVar i) =
fromMaybe pty . liftM (solve env) $ lookup i env
solve env (PTyComb f args) =
PTyComb (solve env f) $ map (solve env) args
solve env (PUTy tv tbod) =
PUTy tv $ solve env tbod
type TypingState = HOLRef TypingRefs
data TypingRefs = TypingRefs
{ stvsTrans :: !Bool
, stovsTrans :: !Bool
, smallSTVS :: ![Int]
}
tyElabRef :: TypingState -> PreType -> HOL cls thry HOLType
tyElabRef _ (PTyCon s) = mkType s []
tyElabRef ref (PTyComb STyVar{} []) =
do modifyHOLRef ref $ \ st -> st { stvsTrans = True }
fail $ "tyElab: system type variable present in type application of " ++
"null arity"
tyElabRef ref (PTyComb (STyVar n) args) =
do modifyHOLRef ref $ \ st -> st { stovsTrans = True }
mkType ('?' : show n) =<< mapM (tyElabRef ref) args
tyElabRef ref (PTyComb (UTyVar _ v _) args) =
mkType v =<< mapM (tyElabRef ref) args
tyElabRef ref (PTyComb (PTyCon s) args) =
mkType s =<< mapM (tyElabRef ref) args
tyElabRef _ PTyComb{} =
fail "tyElab: unexpected first argument to type combination"
tyElabRef ref (PUTy (UTyVar _ s 0) tbody) =
do tbody' <- tyElabRef ref tbody
liftEither "tyElab: universal type" $
liftM1 mkUType (mkSmall $ mkVarType s) tbody'
tyElabRef ref (PUTy STyVar{} _) =
do modifyHOLRef ref $ \ st -> st { stvsTrans = True }
fail "tyElab: system type variable in universal type."
tyElabRef _ PUTy{} =
fail "tyElab: invalid universal type construction."
tyElabRef ref (STyVar n) =
do modifyHOLRef ref $ \ st -> st { stvsTrans = True }
let tv = mkVarType $ '?' : show n
st <- readHOLRef ref
if n `elem` smallSTVS st
then liftEither "tyElab: small system type variable" $ mkSmall tv
else return tv
tyElabRef _ (UTyVar True v _) =
liftEither "tyElab: small user type variable" . mkSmall $ mkVarType v
tyElabRef _ (UTyVar False v _) = return $! mkVarType v
tmElab :: TypingState -> PreTerm -> HOL cls thry HOLTerm
tmElab ref ptm =
do modifyHOLRef ref $ \ st -> st { stvsTrans = False, stovsTrans = False }
tm <- tmElabRec ptm
st <- readHOLRef ref
flag1 <- getBenignFlag FlagTyInvWarning
flag2 <- getBenignFlag FlagTyOpInvWarning
warn (stvsTrans st && flag1)
"warning: inventing type variables"
warn (stovsTrans st && flag2)
"warning: inventing type operator variables"
return tm
where tmElabRec :: PreTerm -> HOL cls thry HOLTerm
tmElabRec PApp{} =
fail $ "tmElab: type application present outside of type " ++
"combination term"
tmElabRec (PVar s pty) =
liftM (mkVar s) $ tyElabRef ref pty
tmElabRec (PConst s pty) =
mkMConst s =<< tyElabRef ref pty
tmElabRec (PInst tvis (PConst c pty)) =
do tvis' <- mapM (\ (ty, x) -> do ty' <- tyElabRef ref ty
return (mkVarType x, ty')) tvis
pty' <- tyElabRef ref pty
mkTIConst c pty' tvis'
tmElabRec PInst{} =
fail "tmElab: body of TYINST not a constant."
tmElabRec (PComb l r) =
do (l', r') <- pairMapM tmElabRec (l, r)
liftEither "tmElab" $ mkComb l' r'
tmElabRec (PAbs v bod) =
do (v', bod') <- pairMapM tmElabRec (v, bod)
mkGAbs v' bod'
tmElabRec (TyPAbs tv t) =
do tv' <- tyElabRef ref tv
t' <- tmElabRec t
liftEither "tmElab" $ mkTyAbs tv' t'
tmElabRec (TyPComb t _ ti) =
do t' <- tmElabRec t
ti' <- tyElabRef ref ti
liftEither "tmElab" $ mkTyComb t' ti'
tmElabRec (PAs tm _) = tmElabRec tm
preTypeOf :: TypingState -> [(String, PreType)] -> PreTerm ->
HOL cls thry PreTerm
preTypeOf ref senv pretm =
do ty <- newTypeVar
modifyHOLRef ref $ \ st -> st { smallSTVS = [] }
(tm', _, env) <- typify ty (pretm, senv, []) <?>
"typechecking: initial type assignment"
env' <- resolveInterface tm' return env <?>
"typechecking: overload resolution"
solvePreterm env' tm'
where typify :: PreType -> (PreTerm, [(String, PreType)], PEnv) ->
HOL cls thry (PreTerm, [(String, PreType)], PEnv)
typify ty (PVar s _, venv, uenv) =
case lookup s venv of
Just ty' ->
do flag <- getBenignFlag FlagAddTyAppsAuto
let tys = if flag then solve uenv ty' else ty'
if flag && isJust (destPUTy tys) &&
not (unifiableWithUType ty uenv)
then do tys' <- addTyApps (PVar s tys) tys
typify ty (tys', venv, uenv)
else do uenv' <- unify uenv (tys, ty)
return (PVar s tys, [], uenv')
Nothing ->
case numOfString s of
Just s' ->
let t = pmkNumeral s' in
do uenv' <- unify uenv (PTyComb (PTyCon "num") [], ty)
return (t, [], uenv')
Nothing ->
(do s' <- getGenericType s
hidden <- gets getHidden
if s `notElem` hidden
then do flag <- getBenignFlag FlagAddTyAppsAuto
tys <- pretypeInstance s'
if flag && isJust (destPUTy tys) &&
not (unifiableWithUType ty uenv)
then do ty' <- addTyApps (PVar s tys) tys
typify ty (ty', venv, uenv)
else do uenv' <- unify uenv (tys, ty)
return (PConst s tys, [], uenv')
else mzero)
<|> return (PVar s ty, [(s, ty)], uenv)
typify ty (PInst tvis (PVar c _), _, uenv) =
do c' <- getGenericType c <?> ("typify: TYINST can only be " ++
"applied to a constant: " ++ c)
let cty = pretypeOfType c'
let tvs = map snd tvis
rtvs = filter (\ x -> case x of
UTyVar _ x' _ -> x' `elem` tvs
_ -> False) $ utyvars cty
if length rtvs < length tvs
then let rtvNames = fromJust $ mapM destUTy rtvs
(missing:_) = filter (`notElem` rtvNames) tvs in
fail $ "typify: TYINST: type does not contain " ++
"tyvar " ++ missing
else let subs = fromJust $ mapM (\ tv ->
do x <- destUTy tv
x' <- revAssoc x tvis
return (x', tv)) rtvs
tvis' = fromJust $ mapM (\ (t, tv) ->
do x <- destUTy tv
return (t, x)) subs in
do ctyrep <- replaceUtvsWithStvs tvs cty
let cty' = pretypeSubst subs ctyrep
uenv' <- unify uenv (cty', ty)
return (PInst tvis' (PConst c cty'), [], uenv')
typify ty (PComb t (PApp ti), venv, uenv) =
do ntv <- newTypeVar
(t', venv1, uenv1) <- typify ntv (t, venv, uenv)
case solve uenv1 ntv of
ty'@(PUTy ty1 ty2) ->
do uenv1' <- unify uenv1
(ty, pretypeSubst [(ti, ty1)] ty2)
return (TyPComb t' ty' ti, venv1, uenv1')
_ -> fail $ "typify: Type application argument maybe not " ++
"of universal type: " ++ show t
typify ty (PComb f x, venv, uenv) =
do ty'' <- newTypeVar
let ty' = mkFunPTy ty'' ty
(f', venv1, uenv1) <- typify ty' (f, venv, uenv)
(x', venv2, uenv2) <- typify (solve uenv1 ty'')
(x, venv1 ++ venv, uenv1)
return (PComb f' x', venv1 ++ venv2, uenv2)
typify ty (ptm@(PAs tm pty), venv, uenv) =
do flag <- getBenignFlag FlagAddTyAppsAuto
if flag && isJust (destPUTy pty) &&
not (unifiableWithUType ty uenv)
then do ty' <- addTyApps ptm pty
typify ty (ty', venv, uenv)
else do uenv' <- unify uenv (ty, pty)
typify ty (tm, venv, uenv')
typify ty (PAbs v bod, venv, uenv) =
do (ty', ty'') <- case ty of
PTyComb (PTyCon "fun") [ty', ty''] ->
return (ty', ty'')
_ -> do ty1 <- newTypeVar
ty2 <- newTypeVar
return (ty1, ty2)
uenv0 <- unify uenv (mkFunPTy ty' ty'', ty)
(v', venv1, uenv1) <- do (v', venv1, uenv1) <- typify ty'
(v, [], uenv0)
flag <- getBenignFlag
FlagIgnoreConstVarstruct
case v' of
PConst s _ -> return $!
if flag
then (PVar s ty', [(s, ty')], uenv0)
else (v', venv1, uenv1)
_ -> return (v', venv1, uenv1)
(bod', venv2, uenv2) <- typify ty'' (bod, venv1 ++ venv, uenv1)
return (PAbs v' bod', venv2, uenv2)
typify ty (TyPAbs tv bod, venv, uenv) =
do ntv <- newTypeVar
(bod', venv1, uenv1) <- typify ntv (bod, venv, uenv)
uenv2 <- unify uenv1 (PUTy tv $ solve uenv1 ntv, ty)
return (TyPAbs tv bod', venv1, uenv2)
typify ty (TyPComb t (PUTy ty1 ty2) ti, venv, uenv) =
do uenv0 <- unify uenv (pretypeSubst [(ti, ty1)] ty2, ty)
(t', venv1, uenv1) <- typify (PUTy ty1 ty2) (t, venv, uenv0)
return (TyPComb t' (PUTy ty1 ty2) ti, venv1, uenv1)
typify _ (ptm, _, _) =
fail $ "typify: unexpected preterm at this stage: " ++ show ptm
replaceUtvsWithStvs :: [String] -> PreType -> HOL cls thry PreType
replaceUtvsWithStvs tys pty =
do tyvs' <- mapM subsf $ utyvars pty
return $! pretypeSubst tyvs' pty
where subsf :: PreType -> HOL cls thry (PreType, PreType)
subsf tv@(UTyVar f s _) =
if s `elem` tys then return (tv, tv)
else do tv'@(STyVar n) <- newTypeVar
when f $ modifyHOLRef ref
(\ st -> st { smallSTVS = n : smallSTVS st})
return (tv', tv)
subsf _ = fail "replaceUtvsWithStvs"
pretypeInstance :: HOLType -> HOL cls thry PreType
pretypeInstance = replaceUtvsWithStvs [] . pretypeOfType
resolveInterface :: PreTerm -> (PEnv -> HOL cls thry PEnv) -> PEnv ->
HOL cls thry PEnv
resolveInterface PApp{} _ _ =
fail "resolveInterface: type application"
resolveInterface (PComb f x) cont env =
resolveInterface f (resolveInterface x cont) env
resolveInterface (PAbs v bod) cont env =
resolveInterface v (resolveInterface bod cont) env
resolveInterface (TyPAbs _ bod) cont env =
resolveInterface bod cont env
resolveInterface (TyPComb t _ _) cont env =
resolveInterface t cont env
resolveInterface PAs{} _ _ =
fail "resolveInterface: type ascription"
resolveInterface (PInst _ bod) cont env =
resolveInterface bod cont env
resolveInterface PVar{} cont env =
cont env
resolveInterface (PConst s ty) cont env =
do iface <- gets getInterface
let maps = filter (\ (s', _) -> s' == s) iface
if null maps
then cont env
else tryFind (\ (_, (_, ty')) ->
do ty'' <- pretypeInstance ty'
cont =<< unify env (ty'', ty)) maps
solvePreterm :: PEnv -> PreTerm -> HOL cls thry PreTerm
solvePreterm _ PApp{} =
fail "solvePreterm: type application"
solvePreterm env (PVar s ty) = return . PVar s $ solve env ty
solvePreterm env (PComb f x) =
do (f', x') <- pairMapM (solvePreterm env) (f, x)
return $! PComb f' x'
solvePreterm env (PAbs v bod) =
do (v', bod') <- pairMapM (solvePreterm env) (v, bod)
return $! PAbs v' bod'
solvePreterm env (TyPAbs tv bod) =
liftM (TyPAbs tv) $ solvePreterm env bod
solvePreterm env (TyPComb t ty ti) =
let ti' = solve env ti in
do modifyHOLRef ref $
\ st -> st { smallSTVS = smallSTVS st `union` freeSTVS0 ti' }
t' <- solvePreterm env t
return $! TyPComb t' (solve env ty) ti'
solvePreterm env (PInst tys bod) =
liftM (PInst tys) $ solvePreterm env bod
solvePreterm _ PAs{} =
fail "solvePreterm: type ascription"
solvePreterm env (PConst s ty) =
let tys = solve env ty in
(do iface <- gets getInterface
c' <- tryFind (\ (s', (c', ty')) ->
if s == s'
then do ty'' <- pretypeInstance ty'
_ <- unify env (ty'', ty)
return c'
else mzero) iface
pmkCV c' tys)
<|> (return $! PConst s tys)
where pmkCV :: String -> PreType -> HOL cls thry PreTerm
pmkCV name pty =
do cond <- can getConstType name
return $! if cond then PConst name pty
else PVar name pty
unify :: PEnv -> (PreType, PreType) -> HOL cls thry PEnv
unify env (ty1, ty2)
| ty1 == ty2 = return env
| otherwise =
case (ty1, ty2) of
(PTyComb f@STyVar{} fargs, PTyComb g gargs) ->
if length fargs == length gargs
then foldrM (flip unify) env $ (f, g) : zip fargs gargs
else fail $ "unify: " ++ show f ++ " WITH " ++ show g
(PTyComb{}, PTyComb STyVar{} _) ->
unify env (ty2, ty1)
(PTyComb f fargs, PTyComb g gargs) ->
if f == g && length fargs == length gargs
then foldrM (flip unify) env $ zip fargs gargs
else fail $ "unify: " ++ show f ++ " WITH " ++ show g
(PUTy tv1@UTyVar{} tbody1, PUTy tv2@UTyVar{} tbody2) ->
if tv1 == tv2 then unify env (tbody1, tbody2)
else let tv = variantUTyVar (utyvars tbody1 `union`
utyvars tbody2) tv1 in
unify env (pretypeSubst [(tv, tv1)] tbody1,
pretypeSubst [(tv, tv2)] tbody2)
(STyVar x, t) -> handleSTVS x t
(t, STyVar x) -> handleSTVS x t
_ -> fail $ "unify: " ++ show ty1 ++ " WITH " ++ show ty2
where handleSTVS :: Int -> PreType -> HOL cls thry PEnv
handleSTVS x t =
case lookup x env of
Just x' -> unify env (x', t)
_ -> if istrivial env x t == Just True
then return env
else do st <- readHOLRef ref
let t' = destSTV t
when (isJust t' && x `elem` smallSTVS st) $
modifyHOLRef ref $ \ s ->
s { smallSTVS = fromJust t' : smallSTVS s }
return $! insertMap x t env
tyElab :: PreType -> HOL cls thry HOLType
tyElab pty =
do ref <- newHOLRef $ TypingRefs False False []
tyElabRef ref pty
elab :: PreTerm -> HOL cls thry HOLTerm
elab ptm =
do ref <- newHOLRef $ TypingRefs False False []
tmElab ref =<< preTypeOf ref [] ptm