haskhol-core-1.0.0: src/HaskHOL/Core/Parser/Elab.hs
{-|
Module: HaskHOL.Core.Parser.Elab
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module defines the elaborators for types and terms. These elaborators
convert 'PreType's and 'PreTerm's, as produced by the parsers, into
'HOLType's and 'HOLTerm's accordingly. This conversion includes local type
inference for terms.
-}
module HaskHOL.Core.Parser.Elab
( tyElab -- :: PreType -> HOL cls thry HOLTerm
, elab -- :: PreTerm -> HOL cls thry HOLTerm
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics
import HaskHOL.Core.Parser.Lib hiding ((<?>))
{-
PEnv is an environment that carries an association between system type
variables and their unifiable type. It is defined as a type synonym in case
we ever need to change its implementation for performance reasons.
-}
type PEnv = [(Int, PreType)]
-- utility functions
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]
{-
Used to construct a constant that has one or more instantiations provided for
its type operator variables.
-}
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"
-- Constructs a PreTerm representation of a provided integer.
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
{-
Checks if a unification for a system type variable is trivial, i.e. unifying
with itself or a unification between two system type variables already stored
in the environment.
Also used to check for cyclic occurances, i.e. a system type variable exists
as a sub-term of the provided term.
-}
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
-- system type generation
newTypeVar :: HOL cls thry PreType
newTypeVar = return STyVar <*> tickTypeCounter
-- Turn UType term into a non-UType by adding type applications
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
-- Check where unification of ty with a UType is potentially possible
unifiableWithUType :: PreType -> PEnv -> Bool
unifiableWithUType ty env
| ty == dpty = False
| otherwise =
let tys = solve env ty in
isJust (destPUTy tys) || isJust (destSTV tys)
-- Get a new instance of a constant's generic type modulo interface
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
{-
Pretype substitution based on HOLType substitution.
Note that the PTyCon case is comparatively simpler given the extra work done
in the parser.
-}
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
-- Apply type unifications
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
-- Final type checker for preterms
{-
Local reference that tracks if we invent system type (operator) variables.
Also used to track the smallness constraints of system type variables.
-}
type TypingState = HOLRef TypingRefs
data TypingRefs = TypingRefs
{ stvsTrans :: !Bool
, stovsTrans :: !Bool
, smallSTVS :: ![Int]
}
-- Post typechecking elaboration
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."
-- Alternative way to handle this if we don't want to make it an error,
-- per HOL2P:
{-
tyElabRef ref (PUTy tv@(STyVar n) tbody) =
do modifyHOLRef ref $ \ st -> st { stvsTrans = True }
warn True "tyElab: system type variable in universal type."
let tv' = '?' : show n
tbody' <- tyElabRef ref $ pretypeSubst [(UTyVar True tv' 0, tv)] tbody
liftMaybe "tyElab: universal type - system type variable case" $
do tv'' <- mkSmall $ mkVarType tv'
mkUType tv'' tbody'
-}
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
-- retypecheck
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
-- Give system type vars for all free type vars, except those in tys
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
-- Type constraint specialization by resolving overloadings
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
-- Push specialization throughout a preterm
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
-- Unification of types
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
-- | Elaborator for 'PreType's.
tyElab :: PreType -> HOL cls thry HOLType
tyElab pty =
do ref <- newHOLRef $ TypingRefs False False []
tyElabRef ref pty
-- | Elaborator and type inference for 'PreTerm's.
elab :: PreTerm -> HOL cls thry HOLTerm
elab ptm =
do ref <- newHOLRef $ TypingRefs False False []
tmElab ref =<< preTypeOf ref [] ptm