diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index 2ef833a5c..33badb3ea 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -20,7 +20,7 @@ import GF.Grammar.ShowTerm import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.Compute.Concrete2(normalForm,normalFlatForm,Globals(..),stdPredef) -import GF.Compile.TypeCheck.ConcreteNew as TC(inferLType) +import GF.Compile.TypeCheck.Concrete as TC(inferLType) import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts) import GF.Command.CommandInfo diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index 9003a3485..b366b55d6 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -27,8 +27,7 @@ import GF.Infra.Ident import GF.Infra.Option import GF.Compile.TypeCheck.Abstract -import GF.Compile.TypeCheck.Concrete(ppType) -import GF.Compile.TypeCheck.ConcreteNew(checkLType,inferLType) +import GF.Compile.TypeCheck.Concrete(checkLType,inferLType) import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef) import GF.Grammar @@ -265,7 +264,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do checkUniq xss = case xss of x:y:xs | x == y -> checkError $ "ambiguous for type" <+> - ppType (mkFunType (tail x) (head x)) + ppTerm Terse 0 (mkFunType (tail x) (head x)) | otherwise -> checkUniq $ y:xs _ -> return () diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs index fd06bb8cd..7c952cd9e 100644 --- a/src/compiler/api/GF/Compile/Repl.hs +++ b/src/compiler/api/GF/Compile/Repl.hs @@ -32,7 +32,7 @@ import GF.Compile.Compute.Concrete2 , ppValue ) import GF.Compile.Rename (renameSourceTerm) -import GF.Compile.TypeCheck.ConcreteNew (inferLType) +import GF.Compile.TypeCheck.Concrete (inferLType) import GF.Data.ErrM (Err(..)) import GF.Data.Utilities (maybeAt, orLeft) import GF.Grammar.Grammar diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs index 9c2f88443..ce9ea1add 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs @@ -1,843 +1,1309 @@ -{-# LANGUAGE PatternGuards #-} -module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where -import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint +{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} +module GF.Compile.TypeCheck.Concrete ( checkLType, checkLType', inferLType, inferLType' ) where -import GF.Infra.CheckM -import GF.Data.Operations +-- The code here is based on the paper: +-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. +-- Practical type inference for arbitrary-rank types. +-- 14 September 2011 -import GF.Grammar +import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) import GF.Grammar.Lookup import GF.Grammar.Predef -import GF.Grammar.PatternMatch -import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord) -import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) - -import Data.List -import Data.Maybe(fromMaybe,isJust,isNothing) -import Control.Monad +import GF.Grammar.Lockfield +import GF.Compile.Compute.Concrete2 +import GF.Infra.CheckM +import GF.Data.ErrM ( Err(Ok, Bad) ) +import Control.Applicative(Applicative(..)) +import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) +import Control.Monad.ST import GF.Text.Pretty - -computeLType :: SourceGrammar -> Context -> Type -> Check Type -computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t - where - comp g ty = case ty of - _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed - | isPredefConstant ty -> return ty ---- shouldn't be needed - - Q (m,ident) -> checkIn ("module" <+> m) $ do - ty' <- lookupResDef gr (m,ident) - if ty' == ty then return ty else comp g ty' --- is this necessary to test? - - AdHocOverload ts -> do - over <- getOverload gr g (Just typeType) t - case over of - Just (tr,_) -> return tr - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t) - - Vr ident -> checkLookup ident g -- never needed to compute! - - App f a -> do - f' <- comp g f - a' <- comp g a - case f' of - Abs b x t -> comp ((b,x,a'):g) t - _ -> return $ App f' a' - - Prod bt x a b -> do - a' <- comp g a - b' <- comp ((bt,x,Vr x) : g) b - return $ Prod bt x a' b' - - Abs bt x b -> do - b' <- comp ((bt,x,Vr x):g) b - return $ Abs bt x b' - - Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b - - ExtR r s -> do - r' <- comp g r - s' <- comp g s - case (r',s') of - (RecType rs, RecType ss) -> plusRecType r' s' >>= comp g - _ -> return $ ExtR r' s' - - RecType fs -> do - let fs' = sortRec fs - liftM RecType $ mapPairsM (comp g) fs' - - ELincat c t -> do - t' <- comp g t - lockRecType c t' ---- locking to be removed AR 20/6/2009 - - _ | ty == typeTok -> return typeStr - - _ -> composOp (comp g) ty - --- the underlying algorithms - -inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type) -inferLType gr g trm = case trm of - - Q ident -> checks [ - termWith trm $ lookupResType gr ident >>= computeLType gr g - , - lookupResDef gr ident >>= inferLType gr g - , - checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm) - ] - - QC ident -> checks [ - termWith trm $ lookupResType gr ident >>= computeLType gr g - , - lookupResDef gr ident >>= inferLType gr g - , - checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm) - ] - - Vr ident -> termWith trm $ checkLookup ident g - - Typed e t -> do - t' <- computeLType gr g t - checkLType gr g e t' - - AdHocOverload ts -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) - - App f a -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> do - (f',fty) <- inferLType gr g f - fty' <- computeLType gr g fty - case fty' of - Prod bt z arg val -> do - a' <- justCheck g a arg - ty <- if z == identW - then return val - else substituteLType [(bt,z,a')] val - return (App f' a',ty) - _ -> - let term = ppTerm Unqualified 0 f - funName = pp . head . words .render $ term - in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$ - "\n ** Maybe you gave too many arguments to" <+> funName <+> "\n") - - S f x -> do - (f', fty) <- inferLType gr g f - case fty of - Table arg val -> do - x'<- justCheck g x arg - return (S f' x', val) - _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm)) - - P t i -> do - (t',ty) <- inferLType gr g t --- ?? - ty' <- computeLType gr g ty - let tr2 = P t' i - termWith tr2 $ case ty' of - RecType ts -> case lookup i ts of - Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty')) - Just x -> return x - _ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$ - " instead of the inferred:" <+> ppTerm Unqualified 0 ty') - - R r -> do - let (ls,fs) = unzip r - fsts <- mapM inferM fs - let ts = [ty | (Just ty,_) <- fsts] - checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts) - return $ (R (zip ls fsts), RecType (zip ls ts)) - - T (TTyped arg) pts -> do - (_,val) <- checks $ map (inferCase (Just arg)) pts - checkLType gr g trm (Table arg val) - T (TComp arg) pts -> do - (_,val) <- checks $ map (inferCase (Just arg)) pts - checkLType gr g trm (Table arg val) - T ti pts -> do -- tries to guess: good in oper type inference - let pts' = [pt | pt@(p,_) <- pts, isConstPatt p] - case pts' of - [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm) ----- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] - _ -> do - (arg,val) <- checks $ map (inferCase Nothing) pts' - checkLType gr g trm (Table arg val) - V arg pts -> do - (_,val) <- checks $ map (inferLType gr g) pts --- return (trm, Table arg val) -- old, caused issue 68 - checkLType gr g trm (Table arg val) - - K s -> - let trm' = case words s of - [] -> Empty - [w] -> K w - (w:ws) -> foldl (\t -> C t . K) (K w) ws - in return (trm', typeStr) - - EInt i -> return (trm, typeInt) - - EFloat i -> return (trm, typeFloat) - - Empty -> return (trm, typeStr) - - C s1 s2 -> - check2 (flip (justCheck g) typeStr) C s1 s2 typeStr - - Glue s1 s2 -> - check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok - ----- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007 - Strs (Cn c : ts) | c == cConflict -> do - checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts)) - inferLType gr g (head ts) - - Strs ts -> do - ts' <- mapM (\t -> justCheck g t typeStr) ts - return (Strs ts', typeStrs) - - Alts t aa -> do - t' <- justCheck g t typeStr - aa' <- flip mapM aa (\ (c,v) -> do - c' <- justCheck g c typeStr - v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr] - v' <- case v' of - Q q -> do t <- lookupResDef gr q - t <- normalForm (Gl gr stdPredef) t - case t of - EPatt _ _ p -> mkStrs p - _ -> return v' - _ -> return v' - return (c',v')) - return (Alts t' aa', typeStr) - - RecType r -> do - let (ls,ts) = unzip r - ts' <- mapM (flip (justCheck g) typeType) ts - return (RecType (zip ls ts'), typeType) - - ExtR r s -> do - (r',rT) <- inferLType gr g r - rT' <- computeLType gr g rT - - (s',sT) <- inferLType gr g s - sT' <- computeLType gr g sT - - let trm' = ExtR r' s' - case (rT', sT') of - (RecType rs, RecType ss) -> do - let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields - checkLType gr g trm' rt ---- return (trm', rt) - _ | rT' == typeType && sT' == typeType -> do - return (trm', typeType) - _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm) - - Sort _ -> - termWith trm $ return typeType - - Prod bt x a b -> do - a' <- justCheck g a typeType - b' <- justCheck ((bt,x,a'):g) b typeType - return (Prod bt x a' b', typeType) - - Table p t -> do - p' <- justCheck g p typeType --- check p partype! - t' <- justCheck g t typeType - return $ (Table p' t', typeType) - - FV vs -> do - (_,ty) <- checks $ map (inferLType gr g) vs ---- checkIfComplexVariantType trm ty - checkLType gr g trm ty - - EPattType ty -> do - ty' <- justCheck g ty typeType - return (EPattType ty',typeType) - EPatt _ _ p -> do - ty <- inferPatt p - (minp,maxp,p') <- measurePatt gr p - return (EPatt minp maxp p', EPattType ty) - - ELin c trm -> do - (trm',ty) <- inferLType gr g trm - ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009 - return $ (ELin c trm', ty') - - _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm) - - where - isPredef m = elem m [cPredef,cPredefAbs] - - justCheck g ty te = checkLType gr g ty te >>= return . fst - - -- for record fields, which may be typed - inferM (mty, t) = do - (t', ty') <- case mty of - Just ty -> checkLType gr g t ty - _ -> inferLType gr g t - return (Just ty',t') - - inferCase mty (patt,term) = do - arg <- maybe (inferPatt patt) return mty - cont <- pattContext gr g arg patt - (term',val) <- inferLType gr (reverse cont ++ g) term - return (arg,val) - isConstPatt p = case p of - PC _ ps -> True --- all isConstPatt ps - PP _ ps -> True --- all isConstPatt ps - PR ps -> all (isConstPatt . snd) ps - PT _ p -> isConstPatt p - PString _ -> True - PInt _ -> True - PFloat _ -> True - PChar -> True - PChars _ -> True - PSeq _ _ p _ _ q -> isConstPatt p && isConstPatt q - PAlt p q -> isConstPatt p && isConstPatt q - PRep _ _ p -> isConstPatt p - PNeg p -> isConstPatt p - PAs _ p -> isConstPatt p - _ -> False - - inferPatt p = case p of - PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c)) - PAs _ p -> inferPatt p - PNeg p -> inferPatt p - PAlt p q -> checks [inferPatt p, inferPatt q] - PSeq _ _ _ _ _ _ -> return $ typeStr - PRep _ _ _ -> return $ typeStr - PChar -> return $ typeStr - PChars _ -> return $ typeStr - _ -> inferLType gr g (patt2term p) >>= return . snd - -measurePatt gr p = - case p of - PM q -> do t <- lookupResDef gr q - t <- normalForm (Gl gr stdPredef) t - case t of - EPatt minp maxp _ -> return (minp,maxp,p) - _ -> checkError ("Expected pattern macro, but found:" $$ nest 2 (pp t)) - PR ass -> do ass <- mapM (\(lbl,p) -> measurePatt gr p >>= \(_,_,p') -> return (lbl,p')) ass - return (0,Nothing,PR ass) - PString s -> do let len=length s - return (len,Just len,p) - PT t p -> do (min,max,p') <- measurePatt gr p - return (min,max,PT t p') - PAs x p -> do (min,max,p) <- measurePatt gr p - case p of - PW -> return (0,Nothing,PV x) - _ -> return (min,max,PAs x p) - PImplArg p -> do (min,max,p') <- measurePatt gr p - return (min,max,PImplArg p') - PNeg p -> do (_,_,p') <- measurePatt gr p - return (0,Nothing,PNeg p') - PAlt p1 p2 -> do (min1,max1,p1) <- measurePatt gr p1 - (min2,max2,p2) <- measurePatt gr p2 - case (p1,p2) of - (PString [c1],PString [c2]) -> return (1,Just 1,PChars [c1,c2]) - (PString [c], PChars cs) -> return (1,Just 1,PChars ([c]++cs)) - (PChars cs, PString [c]) -> return (1,Just 1,PChars (cs++[c])) - (PChars cs1, PChars cs2) -> return (1,Just 1,PChars (cs1++cs2)) - _ -> return (min min1 min2,liftM2 max max1 max2,PAlt p1 p2) - PSeq _ _ p1 _ _ p2 - -> do (min1,max1,p1) <- measurePatt gr p1 - (min2,max2,p2) <- measurePatt gr p2 - case (p1,p2) of - (PW, PW ) -> return (0,Nothing,PW) - (PString s1,PString s2) -> return (min1+min2,liftM2 (+) max1 max2,PString (s1++s2)) - _ -> return (min1+min2,liftM2 (+) max1 max2,PSeq min1 max1 p1 min2 max2 p2) - PRep _ _ p -> do (minp,maxp,p) <- measurePatt gr p - case p of - PW -> return (0,Nothing,PW) - PChar -> return (0,Nothing,PW) - _ -> return (0,Nothing,PRep minp maxp p) - PChar -> return (1,Just 1,p) - PChars _ -> return (1,Just 1,p) - _ -> return (0,Nothing,p) - --- type inference: Nothing, type checking: Just t --- the latter permits matching with value type -getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type)) -getOverload gr g mt ot = case appForm ot of - (f@(Q c), ts) -> case lookupOverload gr c of - Ok typs -> do - ttys <- mapM (inferLType gr g) ts - v <- matchOverload f typs ttys - return $ Just v - _ -> return Nothing - (AdHocOverload cs@(f:_), ts) -> do --- the function name f is only used in error messages - let typs = concatMap collectOverloads cs - ttys <- mapM (inferLType gr g) ts - v <- matchOverload f typs ttys - return $ Just v - _ -> return Nothing - - where - collectOverloads tr@(Q c) = case lookupOverload gr c of - Ok typs -> typs - _ -> case lookupResType gr c of - Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))] - _ -> [] - collectOverloads _ = [] --- constructors QC - - matchOverload f typs ttys = do - let (tts,tys) = unzip ttys - let vfs = lookupOverloadInstance tys typs - let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v] - let showTypes ty = hsep (map ppType ty) - - - let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs]) - - -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013 - let (stysError,stypsError) = if elem (render stys) (map render styps) - then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs]) - else (stys,styps) - - case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of - ([(_,val,fun)],_) -> return (mkApp fun tts, val) - ([],[(pre,val,fun)]) -> do - checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$ - "for" $$ - nest 2 (showTypes tys) $$ - "using" $$ - nest 2 (showTypes pre) - return (mkApp fun tts, val) - ([],[]) -> do - checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$ - maybe empty (\x -> "with value type" <+> ppType x) mt $$ - "for argument list" $$ - nest 2 stysError $$ - "among alternatives" $$ - nest 2 (vcat stypsError) - - - (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of - ([(val,fun)],_) -> do - return (mkApp fun tts, val) - ([],[(val,fun)]) -> do - checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) - return (mkApp fun tts, val) - ------ unsafely exclude irritating warning AR 24/5/2008 ------ checkWarn $ "overloading of" +++ prt f +++ ------ "resolved by excluding partial applications:" ++++ ------ unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)] - ---- now forgiving ambiguity with a warning AR 1/2/2014 --- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before. --- But it also gives a chance to ambiguous overloadings that were banned before. - (nps1,nps2) -> do - checkWarn $ "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+> - ---- "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$ - "resolved by selecting the first of the alternatives" $$ - nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []]) - case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of - [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f - h:_ -> return h - - matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)] - - unlocked v = case v of - RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs) - _ -> v - ---- TODO: accept subtypes - ---- TODO: use a trie - lookupOverloadInstance tys typs = - [((pre,mkFunType rest val, t),isExact) | - let lt = length tys, - (ty,(val,t)) <- typs, length ty >= lt, - let (pre,rest) = splitAt lt ty, - let isExact = pre == tys, - isExact || map unlocked pre == map unlocked tys - ] - - noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v] - - noProd ty = case ty of - Prod _ _ _ _ -> False - _ -> True - -checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type) -checkLType gr g trm typ0 = do - typ <- computeLType gr g typ0 - - case trm of - - Abs bt x c -> do - case typ of - Prod bt' z a b -> do - (c',b') <- if z == identW - then checkLType gr ((bt,x,a):g) c b - else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b - checkLType gr ((bt,x,a):g) c b' - return $ (Abs bt x c', Prod bt' z a b') - _ -> checkError $ "function type expected instead of" <+> ppType typ $$ - "\n ** Double-check that the type signature of the operation" $$ - "matches the number of arguments given to it.\n" - - App f a -> do - over <- getOverload gr g (Just typ) trm - case over of - Just trty -> return trty - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - - AdHocOverload ts -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) - - Q _ -> do - over <- getOverload gr g (Just typ) trm - case over of - Just trty -> return trty - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - - T _ [] -> - checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ) - T _ cs -> case typ of - Table arg val -> do - case allParamValues gr arg of - Ok vs -> do - let ps0 = map fst cs - ps <- testOvershadow ps0 vs - if null ps - then return () - else checkWarn ("patterns never reached:" $$ - nest 2 (vcat (map (ppPatt Unqualified 0) ps))) - _ -> return () -- happens with variable types - cs' <- mapM (checkCase arg val) cs - return (T (TTyped arg) cs', typ) - _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ) - V arg0 vs -> - case typ of - Table arg1 val -> - do arg' <- checkEqLType gr g arg0 arg1 trm - vs1 <- allParamValues gr arg1 - if length vs1 == length vs - then return () - else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm - vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs] - return (V arg' vs',typ) - - R r -> case typ of --- why needed? because inference may be too difficult - RecType rr -> do - --let (ls,_) = unzip rr -- labels of expected type - fsts <- mapM (checkM r) rr -- check that they are found in the record - return $ (R fsts, typ) -- normalize record - - _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ)) - - ExtR r s -> case typ of - _ | typ == typeType -> do - trm' <- computeLType gr g trm - case trm' of - RecType _ -> termWith trm' $ return typeType - ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType - -- ext t = t ** ... - _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm)) - - RecType rr -> do - - (fields1,fields2) <- case s of - R ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr) - _ -> do - (s',typ2) <- inferLType gr g s - case typ2 of - RecType ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr) - _ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2)) - - (r',_) <- checkLType gr g r (RecType fields1) - (s',_) <- checkLType gr g s (RecType fields2) - - let withProjection t fields g f = - case t of - R rs -> f g (\l -> case lookup l rs of - Just (_,t) -> t - Nothing -> error (render ("no value for label" <+> l))) - QC _ -> f g (\l -> P t l) - Vr _ -> f g (\l -> P t l) - _ -> if length fields == 1 - then f g (\l -> P t l) - else let x = mkFreshVar (map (\(_,x,_) -> x) g) (identS "x") - in Let (x, (Nothing, t)) (f ((Explicit,x,RecType fields):g) (\l -> P (Vr x) l)) - - rec = withProjection r' fields1 g $ \g p_r' -> - withProjection s' fields2 g $ \g p_s' -> - R ([(l,(Nothing,p_r' l)) | (l,_) <- fields1] ++ [(l,(Nothing,p_s' l)) | (l,_) <- fields2]) - return (rec, typ) - - ExtR ty ex -> do - r' <- justCheck g r ty - s' <- justCheck g s ex - return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ - - _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ) - - FV vs -> do - ttys <- mapM (flip (checkLType gr g) typ) vs ---- checkIfComplexVariantType trm typ - return (FV (map fst ttys), typ) --- typ' ? - - S tab arg -> checks [ do - (tab',ty) <- inferLType gr g tab - ty' <- computeLType gr g ty - case ty' of - Table p t -> do - (arg',val) <- checkLType gr g arg p - checkEqLType gr g typ t trm - return (S tab' arg', t) - _ -> checkError ("table type expected for applied table instead of" <+> ppType ty') - , do - (arg',ty) <- inferLType gr g arg - ty' <- computeLType gr g ty - (tab',_) <- checkLType gr g tab (Table ty' typ) - return (S tab' arg', typ) - ] - Let (x,(mty,def)) body -> case mty of - Just ty -> do - (ty0,_) <- checkLType gr g ty typeType - (def',ty') <- checkLType gr g def ty0 - body' <- justCheck ((Explicit,x,ty'):g) body typ - return (Let (x,(Just ty',def')) body', typ) - _ -> do - (def',ty) <- inferLType gr g def -- tries to infer type of local constant - checkLType gr g (Let (x,(Just ty,def')) body) typ - - ELin c tr -> do - tr1 <- unlockRecord c tr - checkLType gr g tr1 typ - - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - where - justCheck g ty te = checkLType gr g ty te >>= return . fst -{- - recParts rr t = (RecType rr1,RecType rr2) where - (rr1,rr2) = partition (flip elem (map fst t) . fst) rr --} - checkM rms (l,ty) = case lookup l rms of - Just (Just ty0,t) -> do - checkEqLType gr g ty ty0 t - (t',ty') <- checkLType gr g t ty - return (l,(Just ty',t')) - Just (_,t) -> do - (t',ty') <- checkLType gr g t ty - return (l,(Just ty',t')) - _ -> checkError $ - if isLockLabel l - then let cat = drop 5 (showIdent (label2ident l)) - in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <> - "; try wrapping it with lin" <+> cat - else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms) - - checkCase arg val (p,t) = do - cont <- pattContext gr g arg p - t' <- justCheck (reverse cont ++ g) t val - (_,_,p') <- measurePatt gr p - return (p',t') - -pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context -pattContext env g typ p = case p of - PV x -> return [(Explicit,x,typ)] - PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 - t <- lookupResType env (q,c) - let (cont,v) = typeFormCnc t - checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) - (length cont == length ps) - checkEqLType env g typ v (patt2term p) - mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat - PR r -> do - typ' <- computeLType env g typ - case typ' of - RecType t -> do - let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]] - ----- checkWarn $ prt p ++++ show pts ----- debug - mapM (uncurry (pattContext env g)) pts >>= return . concat - _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ') - PT t p' -> do - checkEqLType env g typ t (patt2term p') - pattContext env g typ p' - - PAs x p -> do - g' <- pattContext env g typ p - return ((Explicit,x,typ):g') - - PAlt p' q -> do - g1 <- pattContext env g typ p' - g2 <- pattContext env g typ q - let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1]) - checkCond - ("incompatible bindings of" <+> - fsep pts <+> - "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) - return g1 -- must be g1 == g2 - PSeq _ _ p _ _ q -> do - g1 <- pattContext env g typ p - g2 <- pattContext env g typ q - return $ g1 ++ g2 - PRep _ _ p' -> noBind typeStr p' - PNeg p' -> noBind typ p' - - _ -> return [] ---- check types! - where - noBind typ p' = do - co <- pattContext env g typ p' - if not (null co) - then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p) - >> return [] - else return [] - -checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type -checkEqLType gr g t u trm = do - (b,t',u',s) <- checkIfEqLType gr g t u trm - case b of - True -> return t' - False -> - let inferredType = ppTerm Qualified 0 u - expectedType = ppTerm Qualified 0 t - term = ppTerm Unqualified 0 trm - funName = pp . head . words .render $ term - helpfulMsg = - case (arrows inferredType, arrows expectedType) of - (0,0) -> pp "" -- None of the types is a function - _ -> "\n **" <+> - if expectedType `isLessApplied` inferredType - then "Maybe you gave too few arguments to" <+> funName - else pp "Double-check that type signature and number of arguments match." - in checkError $ s <+> "type of" <+> term $$ - "expected:" <+> expectedType $$ -- ppqType t u $$ - "inferred:" <+> inferredType $$ -- ppqType u t - helpfulMsg +import Data.STRef +import Data.List (nub, (\\), tails) +import qualified Data.Map as Map +import Data.Maybe(fromMaybe,isNothing,mapMaybe) +import Data.Bifunctor(second) +import Data.Functor((<&>)) +import qualified Control.Monad.Fail as Fail + +checkLType :: Globals -> Term -> Type -> Check (Term, Type) +checkLType globals t ty = do + res <- runEvalM globals $ do + let (c1,c2) = split unit + (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") + +checkLType' :: Choice -> Term -> Constraint -> EvalM (Term, Constraint) +checkLType' c t vty = do + (t,vty) <- tcRho [] c t (Just vty) + t <- zonkTerm [] t + return (t,vty) + +inferLType :: Globals -> Term -> Check (Term, Type) +inferLType globals t = do + res <- runEvalM globals $ do + (t,vty) <- inferLType' t + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") + +inferLType' :: Term -> EvalM (Term, Constraint) +inferLType' t = do + (t,vty) <- inferSigma [] unit t + t <- zonkTerm [] t + return (t,vty) + +inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma) +inferSigma scope s t = do -- GEN1 + (t,ty) <- tcRho scope s t Nothing + env_tvs <- getMetaVars (scopeTypes scope) + res_tvs <- getMetaVars [(scope,ty)] + let forall_tvs = res_tvs \\ env_tvs + quantify scope t forall_tvs ty + +vtypeInt = VApp poison (cPredef,cInt) [] +vtypeFloat = VApp poison (cPredef,cFloat) [] +vtypeInts i= VApp poison (cPredef,cInts) [VInt i] +vtypeStr = VSort cStr +vtypeStrs = VSort cStrs +vtypeType = VSort cType +vtypePType = VSort cPType +vtypeMarkup= VApp poison (cPredef,cMarkup) [] + +tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho) +tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT +tcRho scope s t@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT +tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR +tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty +tcRho scope s t@(Vr v) mb_ty = do -- VAR + case lookup v scope of + Just v_sigma -> instSigma scope s t v_sigma mb_ty + Nothing -> evalError ("Unknown variable" <+> v) +tcRho scope c t@(Q id) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c t@(QC id) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c t@(App fun arg) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c (Abs bt var body) Nothing = do -- ABS1 + i <- newResiduation scope + let arg_ty = VMeta i [] + (body,body_ty) <- tcRho ((var,arg_ty):scope) c body Nothing + let m = length scope + n = m+1 + (b,used_bndrs) <- check m n (False,[]) body_ty + if b + then let v = head (allBinders \\ used_bndrs) + in return (Abs bt var body, (VProd bt v arg_ty body_ty)) + else return (Abs bt var body, (VProd bt identW arg_ty body_ty)) where - -- count the number of arrows in the prettyprinted term - arrows :: Doc -> Int - arrows = length . filter (=="->") . words . render + check m n st (VApp c f vs) = foldM (check m n) st vs + check m n st (VMeta i vs) = do + state <- getMeta i + case state of + Bound _ v -> do g <- globals + check m n st (apply g v vs) + _ -> foldM (check m n) st vs + check m n st@(b,xs) (VGen i vs) + | i == m = return (True, xs) + | otherwise = return st + check m n st (VClosure env c (Abs bt x t)) = do + g <- globals + check m (n+1) st (eval g ((x,VGen n []):env) c t []) + check m n st (VProd _ x v1 v2) = do + st@(b,xs) <- check m n st v1 + case v2 of + VClosure env c t -> do g <- globals + check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t []) + v2 -> check m n st v2 + check m n st (VRecType as) = foldM (\st (l,_,v) -> check m n st v) st as + check m n st (VR as) = + foldM (\st (lbl,tnk) -> check m n st tnk) st as + check m n st (VP v l vs) = + check m n st v >>= \st -> foldM (check m n) st vs + check m n st (VExtR v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VTable v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VT ty env c cs) = + check m n st ty -- Traverse cs as well + check m n st (VV ty cs) = + check m n st ty >>= \st -> foldM (check m n) st cs + check m n st (VS v1 tnk vs) = do + st <- check m n st v1 + st <- check m n st tnk + foldM (check m n) st vs + check m n st (VSort _) = return st + check m n st (VInt _) = return st + check m n st (VFlt _) = return st + check m n st (VStr _) = return st + check m n st VEmpty = return st + check m n st (VC v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VGlue v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VPatt _ _ _) = return st + check m n st (VPattType v) = check m n st v + check m n st (VAlts v vs) = do + st <- check m n st v + foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs + check m n st (VStrs vs) = + foldM (check m n) st vs +tcRho scope c t@(Abs Implicit var body) (Just ty) = do -- ABS2 + (bt, x, var_ty, body_ty) <- unifyFun scope ty + if bt == Implicit + then return () + else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") + body_ty <- evalCodomain x (VGen (length scope) []) body_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) + return (Abs Implicit var body,ty) +tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3 + (scope,f,ty') <- skolemise scope ty + (_,x,var_ty,body_ty) <- unifyFun scope ty' + body_ty <- evalCodomain x (VGen (length scope) []) body_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) + return (f (Abs Explicit var body),ty) +tcRho scope c (Meta _) mb_ty = do + i <- newResiduation scope + ty <- case mb_ty of + Just ty -> return ty + Nothing -> do j <- newResiduation scope + return (VMeta j []) + return (Meta i, ty) +tcRho scope c (Let (var, (Nothing, rhs)) body) mb_ty = do -- LET + let (c1,c2) = split c + (rhs,var_ty) <- tcRho scope c1 rhs Nothing + (body, body_ty) <- tcRho ((var,var_ty):scope) c2 body mb_ty + var_ty <- value2termM True (scopeVars scope) var_ty + return (Let (var, (Just var_ty, rhs)) body, body_ty) +tcRho scope c (Let (var, (Just ann_ty, rhs)) body) mb_ty = do -- LET + let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (rhs,_) <- tcRho scope c3 rhs (Just v_ann_ty) + (body, body_ty) <- tcRho ((var,v_ann_ty):scope) c4 body mb_ty + var_ty <- value2termM True (scopeVars scope) v_ann_ty + return (Let (var, (Just var_ty, rhs)) body, body_ty) +tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT + let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (body,_) <- tcRho scope c3 body (Just v_ann_ty) + instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty +tcRho scope c (FV ts) mb_ty = do + (ts,ty) <- tcUnifying scope c ts mb_ty + return (FV ts, ty) +tcRho scope s t@(Sort _) mb_ty = do + instSigma scope s t vtypeType mb_ty +tcRho scope c t@(RecType rs) Nothing = do + (rs,mb_ty) <- tcRecTypeFields scope c rs Nothing + return (RecType rs,fromMaybe vtypePType mb_ty) +tcRho scope c t@(RecType rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty + case ty' of + VSort s + | s == cType -> return () + | s == cPType -> return () + VMeta i vs-> case rs of + [] -> unifyVar scope i vs vtypePType + _ -> return () + ty -> do ty <- value2termM False (scopeVars scope) ty + evalError ("The record type" <+> ppTerm Unqualified 0 t $$ + "cannot be of type" <+> ppTerm Unqualified 0 ty) + (rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty') + return (f (RecType rs),ty) +tcRho scope s t@(Table p res) mb_ty = do + let (s1,s23) = split s + (s2,s3) = split s23 + (p, p_ty) <- tcRho scope s1 p (Just vtypePType) + (res,res_ty) <- tcRho scope s2 res (Just vtypeType) + instSigma scope s3 (Table p res) vtypeType mb_ty +tcRho scope c (Prod bt x ty1 ty2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (ty1,ty1_ty) <- tcRho scope c1 ty1 (Just vtypeType) + g <- globals + (ty2,ty2_ty) <- tcRho ((x,eval g (scopeEnv scope) c2 ty1 []):scope) c3 ty2 (Just vtypeType) + instSigma scope c4 (Prod bt x ty1 ty2) vtypeType mb_ty +tcRho scope c (S t p) mb_ty = do + let (c1,c2) = split c + let mk_val i = VMeta i [] + p_ty <- fmap mk_val $ newResiduation scope + res_ty <- case mb_ty of + Nothing -> fmap mk_val $ newResiduation scope + Just ty -> return ty + let t_ty = VTable p_ty res_ty + (t,t_ty) <- tcRho scope c1 t (Just t_ty) + (p,_) <- tcRho scope c2 p (Just p_ty) + return (S t p, res_ty) +tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables + let (c1,c2) = split c + let mk_val i = VMeta i [] + p_ty <- case tt of + TRaw -> fmap mk_val $ newResiduation scope + TTyped ty -> do let (c3,c4) = split c1 + (ty, _) <- tcRho scope c3 ty (Just vtypeType) + g <- globals + return (eval g (scopeEnv scope) c4 ty []) + res_ty <- fmap mk_val $ newResiduation scope + ps <- tcCases scope c2 ps p_ty res_ty + p_ty_t <- value2termM True [] p_ty + return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) +tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables + let (c12,c34) = split c + (c3,c4) = split c34 + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' + case tt of + TRaw -> return () + TTyped ty -> do let (c1,c2) = split c12 + (ty, _) <- tcRho scope c1 ty (Just vtypeType) + g <- globals + unify scope (eval g (scopeEnv scope) c2 ty []) p_ty + ps <- tcCases scope c3 ps p_ty res_ty + p_ty_t <- value2termM True (scopeVars scope) p_ty + return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) +tcRho scope c (V p_ty ts) Nothing = do + let (c1,c2,c3,c4) = split4 c + (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType) + i <- newResiduation scope + let res_ty = VMeta i [] - -- If prettyprinted type t has fewer arrows then prettyprinted type u, - -- then t is "less applied", and we can print out more helpful error msg. - isLessApplied :: Doc -> Doc -> Bool - isLessApplied t u = arrows t < arrows u + let go c t = do (t, ty) <- tcRho scope c t Nothing + subsCheckRho scope t ty res_ty -checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String) -checkIfEqLType gr g t u trm = do - t' <- computeLType gr g t - u' <- computeLType gr g u - case t' == u' || alpha [] t' u' of - True -> return (True,t',u',[]) - -- forgive missing lock fields by only generating a warning. - --- better: use a flag to forgive? (AR 31/1/2006) - _ -> case missingLock [] t' u' of - Ok lo -> do - checkWarn $ "missing lock field" <+> fsep lo - return (True,t',u',[]) - Bad s -> return (False,t',u',s) + ts <- mapCM go c2 ts + g <- globals + return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty) +tcRho scope c (V p_ty0 ts) (Just ty) = do + let (c1,c2,c3,c4) = split4 c + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' + (p_ty0, _) <- tcRho scope c1 p_ty0 (Just vtypeType) + g <- globals + let p_vty0 = eval g (scopeEnv scope) c2 p_ty0 [] + unify scope p_ty p_vty0 + ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts + return (V p_ty0 ts, VTable p_ty res_ty) +tcRho scope c (R rs) Nothing = do + lttys <- inferRecFields scope c rs + rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + return (R rs, + VRecType [(l,True,ty) | (l,t,ty) <- lttys] + ) +tcRho scope c (R rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty + case ty' of + (VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys + rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + return ((f . R) rs, + VRecType [(l,True,ty) | (l,t,ty) <- lttys] + ) + ty -> do lttys <- inferRecFields scope c rs + t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys] + t <- subsCheckRho scope t ty' ty + return (t, ty') +tcRho scope c (P t l) mb_ty = do + l_ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newResiduation scope + return (VMeta i []) + (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)])) + return (P t l,l_ty) +tcRho scope c (C t1 t2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) + instSigma scope c3 (C t1 t2) vtypeStr mb_ty +tcRho scope c (Glue t1 t2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) + instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty +tcRho scope c t@(ExtR t1 t2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 Nothing + (t2,t2_ty) <- tcRho scope c2 t2 Nothing + case (t1_ty,t2_ty) of + (VSort s1,VSort s2) + | (s1 == cType || s1 == cPType) && + (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType + | otherwise = cType + in instSigma scope c3 (ExtR t1 t2) (VSort sort) mb_ty + (VRecType rs1, VRecType rs2) -> instSigma scope c3 (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty + _ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t) +tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope c (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho scope c (Alts t ss) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t,_) <- tcRho scope c1 t (Just vtypeStr) + ss <- mapCM (\c (t1,t2) -> do + let (c1,c2) = split c + (t1,_) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,_) <- tcRho scope c2 t2 (Just vtypeStrs) + return (t1,t2)) + c2 ss + instSigma scope c3 (Alts t ss) vtypeStr mb_ty +tcRho scope c (Strs ss) mb_ty = do + let (c1,c2) = split c + ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr) + return t) + c1 ss + instSigma scope c2 (Strs ss) vtypeStrs mb_ty +tcRho scope c (EPattType ty) mb_ty = do + let (c1,c2) = split c + (ty, _) <- tcRho scope c1 ty (Just vtypeType) + instSigma scope c2 (EPattType ty) vtypeType mb_ty +tcRho scope c t@(EPatt min max p) mb_ty = do + (scope,f,ty) <- case mb_ty of + Nothing -> do i <- newResiduation scope + return (scope,id,VMeta i []) + Just ty -> do (scope,f,ty) <- skolemise scope ty + case ty of + VPattType ty -> return (scope,f,ty) + _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") + tcPatt scope c p ty + return (f (EPatt min max p), ty) +tcRho scope c (Markup tag attrs children) mb_ty = do + let (c1,c2,c3,c4) = split4 c + attrs <- mapCM (\c (id,t) -> do + (t,_) <- tcRho scope c t Nothing + return (id,t)) + c1 attrs + res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children + instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty +tcRho scope c (Reset ctl mb_ct t qid) mb_ty + | ctl == cConcat = do + let (c1,c23) = split c + (c2,c3 ) = split c23 + (t,_) <- tcRho scope c1 t Nothing + mb_ct <- case mb_ct of + Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt) + return (Just ct) + Nothing -> return Nothing + instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty + | ctl == cOne = do + let (c1,c2) = split c + (t,ty) <- tcRho scope c1 t mb_ty + (mb_ct,ty) <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) + return (Just ct,ty) + Nothing -> return (Nothing,ty) + return (Reset ctl mb_ct t qid,ty) + | ctl == cDefault = do + let (c1,c2) = split c + (t,ty) <- tcRho scope c1 t mb_ty + (mb_ct,ty) <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) + return (Just ct,ty) + Nothing -> evalError (pp "[list: .. | ..] requires an argument") + return (Reset ctl mb_ct t qid,ty) + | ctl == cList = do + do let (c1,c2) = split c + mb_ct <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing + return (Just ct) + Nothing -> evalError (pp "[list: .. | ..] requires an argument") + (t,ty) <- tcRho scope c2 t mb_ty + case ty of + VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) + _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) + | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") +tcRho scope s (Opts n cs) mb_ty = do + let (s1,s2,s3) = split3 s + (n,_) <- tcRho scope s1 n Nothing + (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing + (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty + return (Opts n (zip ls ts), ty) +tcRho scope s t _ = unimplemented ("tcRho "++show t) +evalCodomain :: Ident -> Value -> Value -> EvalM Value +evalCodomain x v (VClosure env c ty) = do + g <- globals + return (eval g ((x,v):env) c ty []) +evalCodomain x _ ty = return ty + +tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint) +tcUnifying scope c ts mb_ty = do + (ty,subsume) <- + case mb_ty of + Just ty -> do return (ty, \t ty' -> return t) + Nothing -> do i <- newResiduation scope + let ty = VMeta i [] + return (ty, \t ty' -> subsCheckRho scope t ty' ty) + + let go c t = do (t, ty) <- tcRho scope c t mb_ty + subsume t ty + + ts <- mapCM go c ts + return (ts,ty) + +tcCases scope c [] p_ty res_ty = return [] +tcCases scope c ((p,t):cs) p_ty res_ty = do + let (c1,c2,c3,c4) = split4 c + scope' <- tcPatt scope c1 p p_ty + (t,_) <- tcRho scope' c2 t (Just res_ty) + cs <- tcCases scope c3 cs p_ty res_ty + return ((p,t):cs) + +tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP +tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) +tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) +tcApp scope c t0 t args mb_ty = do + let (c1,c23) = split c + let (c2,c3) = split c23 + (t,ty) <- tcRho scope c1 t Nothing + (t,ty) <- reapply1 scope c2 t ty args + instSigma scope c3 t ty mb_ty + +reapply1 :: Scope -> Choice -> Term -> Value -> [Term] -> EvalM (Term,Rho) +reapply1 scope c fun fun_ty [] = return (fun,fun_ty) +reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case + let (c1,c2,c3,c4) = split4 c + (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty + unless (bt == Implicit) $ + evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") + (arg,_) <- tcRho scope c1 arg (Just arg_ty) + g <- globals + res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty + reapply1 scope c3 (App fun (ImplArg arg)) res_ty args +reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case + let (c1,c2,c3,c4) = split4 c + (fun,fun_ty) <- instantiate scope fun fun_ty + (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty + (arg,_) <- tcRho scope c1 arg (Just arg_ty) + g <- globals + res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty + reapply1 scope c3 (App fun arg) res_ty args + +resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) +resolveOverloads scope c t0 q args mb_ty = do + g@(Gl gr _) <- globals + case lookupOverloadTypes gr q of + Bad msg -> evalError (pp msg) + Ok [(t,ty)] -> do let (c1,c23) = split c + (c2,c3) = split c23 + (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args + instSigma scope c3 t ty mb_ty + Ok ttys -> do let (c1,c23) = split c + (c2,c3) = split c23 + arg_tys <- mapCM (checkArg g) c1 args + let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys + try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) + (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys))) + v_ttys where + checkArg g c (ImplArg arg) = do + let (c1,c2) = split c + (arg,arg_ty) <- tcRho scope c1 arg Nothing + let v = eval g (scopeEnv scope) c2 arg [] + return (ImplArg arg,v,arg_ty) + checkArg g c arg = do + let (c1,c2) = split c + (arg,arg_ty) <- tcRho scope c1 arg Nothing + let v = eval g (scopeEnv scope) c2 arg [] + return (arg,v,arg_ty) - -- check that u is a subtype of t - --- quick hack version of TC.eqVal - alpha g t u = case (t,u) of + mkFV [t] = t + mkFV ts = FV ts - -- error (the empty type!) is subtype of any other type - (_,u) | u == typeError -> True + minimum g [] = (maxBound,err) + where + err = evalError (pp "Overload resolution failed") + minimum g (tty@((t,ty),state):ttys) = + let ty' = zonk ty + a = arity ty' + (a',res) = minimum g ttys + in case compare a a' of + GT -> (a',res) + EQ -> (a',join t ty' state res) + LT -> (a ,one t ty' state) + where + arity :: Value -> Int + arity (VProd _ _ _ ty) = 1 + arity ty + arity _ = 0 - -- contravariance - (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d + zonk :: Value -> Value + zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2) + zonk (VMeta i vs) = + case Map.lookup i (metaVars state) of + Just (Bound _ v) -> zonk (apply g v vs) + Just (Residuation _ (Just v)) -> zonk (apply g v vs) + _ -> VMeta i (map zonk vs) + zonk (VSusp i k vs) = + case Map.lookup i (metaVars state) of + Just (Bound _ v) -> zonk (apply g (k v) vs) + Just (Residuation _ (Just v)) -> zonk (apply g (k v) vs) + _ -> VSusp i k (map zonk vs) + zonk v = v - -- record subtyping - (RecType rs, RecType ts) -> all (\ (l,a) -> - any (\ (k,b) -> l == k && alpha g a b) ts) rs - (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s' - (ExtR r s, t) -> alpha g r t || alpha g s t + one t ty state = do + t <- withState state (zonkTerm [] t) + return ([t],ty) - -- the following say that Ints n is a subset of Int and of Ints m >= n - -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04 - (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n - | Just _ <- isTypeInts t, u == typeInt -> True ---- check size! - | t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005 + join t ty state res = do + t <- withState state (zonkTerm [] t) + (ts,ty') <- res + ty <- supertype scope (Just ty) ty' + return (t:ts,ty) - ---- this should be made in Rename - (Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - || m == n --- for Predef - (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - (QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - (Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) +reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) +reapply2 scope c fun fun_ty [] mb_ty = instSigma scope c fun fun_ty mb_ty +reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case + (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty + unless (bt == Implicit) $ + evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") + arg <- subsCheckRho scope arg arg_ty' arg_ty + res_ty <- evalCodomain x arg_v res_ty + reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty +reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case + (fun,fun_ty) <- instantiate scope fun fun_ty + (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty + arg <- subsCheckRho scope arg arg_ty arg_ty' + res_ty <- evalCodomain x arg_v res_ty + reapply2 scope c (App fun arg) res_ty args mb_ty - -- contravariance - (Table a b, Table c d) -> alpha g c a && alpha g b d - (Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g - _ -> t == u - --- the following should be one-way coercions only. AR 4/1/2001 - || elem t sTypes && elem u sTypes - || (t == typeType && u == typePType) - || (u == typeType && t == typePType) +tcPatt scope c PW ty0 = + return scope +tcPatt scope c (PV x) ty0 = + return ((x,ty0):scope) +tcPatt scope c (PP q ps) ty0 = do + g@(Gl gr _) <- globals + ty <- case lookupResType gr q of + Ok ty -> return ty + Bad msg -> evalError (pp msg) + let go scope c ty [] = return (scope,ty) + go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty + let (c1,c2) = split c + scope <- tcPatt scope c1 p arg_ty + go scope c2 res_ty ps + let (c1,c2) = split c + (scope,ty) <- go scope c1 (eval g [] c2 ty []) ps + unify scope ty0 ty + return scope +tcPatt scope c (PInt i) ty0 = do + subsCheckRho scope (EInt i) (vtypeInts i) ty0 + return scope +tcPatt scope c (PString s) ty0 = do + unify scope ty0 vtypeStr + return scope +tcPatt scope c PChar ty0 = do + unify scope ty0 vtypeStr + return scope +tcPatt scope c (PChars cs) ty0 = do + unify scope ty0 vtypeStr + return scope +tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do + unify scope ty0 vtypeStr + let (c1,c2) = split c + scope <- tcPatt scope c1 p1 vtypeStr + scope <- tcPatt scope c2 p2 vtypeStr + return scope +tcPatt scope c (PRep _ _ p) ty0 = do + unify scope ty0 vtypeStr + tcPatt scope c p vtypeStr +tcPatt scope c (PAs x p) ty0 = do + tcPatt ((x,ty0):scope) c p ty0 +tcPatt scope c (PR rs) ty0 = do + let mk_ltys [] = return [] + mk_ltys ((l,p):rs) = do i <- newResiduation scope + ltys <- mk_ltys rs + return ((l,p,VMeta i []) : ltys) + go scope c [] = return scope + go scope c ((l,p,ty):rs) = do let (c1,c2) = split c + scope <- tcPatt scope c1 p ty + go scope c2 rs + ltys <- mk_ltys rs + subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,True,ty) | (l,p,ty) <- ltys]) ty0 + go scope c ltys +tcPatt scope c (PAlt p1 p2) ty0 = do + let (c1,c2) = split c + tcPatt scope c1 p1 ty0 + tcPatt scope c2 p2 ty0 + return scope +tcPatt scope c (PM q) ty0 = do + g@(Gl gr _) <- globals + ty <- case lookupResType gr q of + Ok ty -> return ty + Bad msg -> evalError (pp msg) + case ty of + EPattType ty + -> do unify scope ty0 (eval g [] c ty []) + return scope + ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") +tcPatt scope c p ty = unimplemented ("tcPatt "++show p) - missingLock g t u = case (t,u) of - (RecType rs, RecType ts) -> - let - ls = [l | (l,a) <- rs, - not (any (\ (k,b) -> alpha g a b && l == k) ts)] - (locks,others) = partition isLockLabel ls - in case others of - _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others))) - _ -> return locks - -- contravariance - (Prod _ x a b, Prod _ y c d) -> do - ls1 <- missingLock g c a - ls2 <- missingLock g b d - return $ ls1 ++ ls2 +inferRecFields scope c rs = + mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs - _ -> Bad "" +checkRecFields scope c [] ltys + | null ltys = return [] + | otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys]) +checkRecFields scope c ((l,t):lts) ltys = + case takeIt l ltys of + (Just ty,ltys) -> do let (c1,c2) = split c + ltty <- tcRecField scope c1 l t (Just ty) + lttys <- checkRecFields scope c2 lts ltys + return (ltty : lttys) + (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) + lttys <- checkRecFields scope c lts ltys + return lttys -- ignore the field + where + takeIt l1 [] = (Nothing, []) + takeIt l1 (lty@(l2,_,ty):ltys) + | l1 == l2 = (Just ty,ltys) + | otherwise = let (mb_ty,ltys') = takeIt l1 ltys + in (mb_ty,lty:ltys') - sTypes = [typeStr, typeTok, typeString] +tcRecField scope c l (mb_ann_ty,t) mb_ty = do + (t,ty) <- case mb_ann_ty of + Just ann_ty -> do let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (t,_) <- tcRho scope c3 t (Just v_ann_ty) + instSigma scope c4 t v_ann_ty mb_ty + Nothing -> tcRho scope c t mb_ty + return (l,t,ty) --- auxiliaries +tcRecTypeFields scope c [] mb_ty = return ([],mb_ty) +tcRecTypeFields scope c ((l,ty):rs) mb_ty = do + let (c1,c2) = split c + (ty,sort) <- tcRho scope c1 ty mb_ty + mb_ty <- case sort of + VSort s + | s == cType -> return (Just sort) + | s == cPType -> return mb_ty + VMeta _ _ -> return mb_ty + _ -> do sort <- value2termM False (scopeVars scope) sort + evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ + "cannot be of type" <+> ppTerm Unqualified 0 sort) + (rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty + return ((l,ty):rs,mb_ty) --- | light-weight substitution for dep. types -substituteLType :: Context -> Type -> Check Type -substituteLType g t = case t of - Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g] - _ -> composOp (substituteLType g) t +-- | Invariant: if the third argument is (Just rho), +-- then rho is in weak-prenex form +instSigma :: Scope -> Choice -> Term -> Sigma -> Maybe Rho -> EvalM (Term, Rho) +instSigma scope s t ty1 Nothing = return (t,ty1) -- INST1 +instSigma scope s t ty1 (Just ty2) = do -- INST2 + t <- subsCheckRho scope t ty1 ty2 + return (t,ty2) -termWith :: Term -> Check Type -> Check (Term, Type) -termWith t ct = do - ty <- ct +-- | Invariant: the second argument is in weak-prenex form +subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM Term +subsCheckRho scope t (VMeta i vs1) (VMeta j vs2) + | i == j = do sequence_ (zipWith (unify scope) vs1 vs2) + return t + | otherwise = do + mv <- getMeta i + case mv of + Bound _ v1 -> do + g <- globals + subsCheckRho scope t (apply g v1 vs1) (VMeta j vs2) + Residuation scope1 (Just ctr1) -> do + g <- globals + subsCheckRho scope t (apply g ctr1 vs1) (VMeta j vs2) + Residuation scope1 Nothing -> do + mv <- getMeta j + case mv of + Bound _ v2 -> do + g <- globals + subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2) + Residuation scope2 ctr2 + | m > n -> do setMeta i (Bound scope1 (VMeta j vs2)) + return t + | otherwise -> case ctr2 of + Nothing -> do setMeta j (Bound scope2 (VMeta i vs2)) + return t + Just ctr2 -> do g <- globals + subsCheckRho scope t (VMeta i vs1) (apply g ctr2 vs2) + where + m = length scope1 + n = length scope2 +subsCheckRho scope t ty1@(VMeta i vs) ty2 = do + mv <- getMeta i + case mv of + Bound _ ty1 -> do + g <- globals + subsCheckRho scope t (apply g ty1 vs) ty2 + Residuation scope' ctr -> do + occursCheck scope' i scope ty2 + ctr <- subtype scope ctr ty2 + setMeta i (Residuation scope' (Just ctr)) + return t +subsCheckRho scope t ty1 ty2@(VMeta i vs) = do + mv <- getMeta i + case mv of + Bound _ ty2 -> do + g <- globals + subsCheckRho scope t ty1 (apply g ty2 vs) + Residuation scope' ctr -> do + occursCheck scope' i scope ty1 + ctr <- supertype scope ctr ty1 + setMeta i (Residuation scope' (Just ctr)) + return t +subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC + i <- newResiduation scope + g <- globals + let ty2' = case ty2 of + VClosure env c ty2 -> eval g ((x,VMeta i []):env) c ty2 [] + ty2 -> ty2 + subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2 +subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL + let v = newVar scope + ty2 <- evalCodomain x (VGen (length scope) []) ty2 + t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 + return (Abs Implicit v t) +subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN + (_,_,a1,r1) <- unifyFun scope rho1 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t (VProd Explicit _ a1 r1) rho2 = do -- Rule FUN + (_,_,a2,r2) <- unifyFun scope rho2 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t rho1 (VTable p2 r2) = do -- Rule TABLE + (p1,r1) <- unifyTbl scope rho1 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE + (p2,r2) <- unifyTbl scope rho2 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE + | s1 == cPType && s2 == cType = return t +subsCheckRho scope t (VApp _ p1 []) rho2 -- for backwards compatibility + | p1 == (cPredef,cErrorType) = return t +subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- This is not correct but there is in the RGL nextPrec relies on it. + | p1 == (cPredef,cInt) && p2 == (cPredef,cInts) = return t -- Should be only a temporary hack. +subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1 + | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t +subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2 + | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do + if i <= j + then return t + else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) +subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC + let mkAccess scope t = + case t of + ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 + (scope,mkProj2,mkWrap2) <- mkAccess scope t2 + return (scope + ,\l -> mkProj2 l `mplus` mkProj1 l + ,mkWrap1 . mkWrap2 + ) + R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] + return (scope + ,\l -> lookup l rs + ,id + ) + Vr x -> do return (scope + ,\l -> do VRecType rs <- lookup x scope + ty <- lookup3 l rs + return (Nothing,P t l) + ,id + ) + t -> let x = newVar scope + in return (((x,ty1):scope) + ,\l -> return (Nothing,P (Vr x) l) + ,Let (x, (Nothing, t)) + ) + + mkField scope l (mb_ty,t) ty1 ty2 = do + t <- subsCheckRho scope t ty1 ty2 + return (l, (mb_ty,t)) + + lookup3 l [] = Nothing + lookup3 l ((l',_,v):rs) + | l == l' = Just v + | otherwise = lookup3 l rs + + (scope,mkProj,mkWrap) <- mkAccess scope t + + let fields = [(l,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2] + case [l | (l,_,Nothing) <- fields, not (isLockLabel l)] of + [] -> return () + missing -> evalError ("In the term" <+> pp t $$ + "there are no values for fields:" <+> hsep missing) + rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] + return (mkWrap (R (rs++[(l, (Just (RecType []),R [])) | (l,_,Nothing) <- fields, isLockLabel l]))) +subsCheckRho scope t tau1 (VFV c (VarFree vs)) = do + tau2 <- variants c vs + subsCheckRho scope t tau1 tau2 +subsCheckRho scope t (VFV c (VarFree vs)) tau2 = do + tau1 <- variants c vs + subsCheckRho scope t tau1 tau2 +subsCheckRho scope t tau1 tau2 = do -- Rule EQ + unify scope tau1 tau2 -- Revert to ordinary unification + return t + +subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM Term +subsCheckFun scope t a1 r1 a2 r2 = do + let v = newVar scope + vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 + g <- globals + let r1' = case r1 of + VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 [] + r1 -> r1 + r2' = case r2 of + VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 [] + r2 -> r2 + t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2' + return (Abs Explicit v t) + +subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term +subsCheckTbl scope t p1 r1 p2 r2 = do + let x = newVar scope + xt <- subsCheckRho ((x,p2):scope) (Vr x) p2 p1 + t <- subsCheckRho ((x,p2):scope) (S t xt) r1 r2 + p2 <- value2termM True (scopeVars scope) p2 + return (T (TTyped p2) [(PV x,t)]) + +subtype scope Nothing (VApp c p [VInt i]) + | p == (cPredef,cInts) = do + return (VInts Nothing (Just i)) +subtype scope (Just (VInts i j)) (VApp c p [VInt k]) + | p == (cPredef,cInts) = do + return (VInts j (Just (maybe k (min k) i))) +subtype scope Nothing (VRecType ltys) = do + lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys + return (VRecType lctrs) +subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do + lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2 + return (VRecType lctrs) + where + union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1 + return [(l,True,ctr)] + union l o1 ctr1 ((l',o2,ctr2):lctrs) + | l == l' = do ctr <- subtype scope (Just ctr1) ctr2 + return ((l,o1||o2,ctr):lctrs) + | otherwise = do lctrs <- union l o1 ctr1 lctrs + return ((l',o2,ctr2):lctrs) +subtype scope (Just (VTable a1 r1)) (VTable a2 r2) = do + a <- supertype scope (Just a1) a2 + r <- subtype scope (Just r1) r2 + return (VTable a r) +subtype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) + | x == identW && y == identW = do + a <- supertype scope (Just a1) a2 + r <- subtype scope (Just r1) r2 + return (VProd Explicit identW a r) +subtype scope Nothing ty = return ty +subtype scope (Just ctr) ty = do + unify scope ctr ty + return ty + +supertype scope Nothing (VApp c p [VInt i]) + | p == (cPredef,cInts) = do + return (VInts (Just i) Nothing) +supertype scope (Just (VInts i j)) (VApp c p [VInt k]) + | p == (cPredef,cInts) = do + return (VInts (Just (maybe k (max k) i)) j) +supertype scope Nothing (VRecType ltys) = do + lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys + return (VRecType lctrs) +supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do + lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1 + return (VRecType lctrs) + where + intersect l o1 ctr1 lctrs [] = return lctrs + intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2) + | l == l' = do ctr <- supertype scope (Just ctr1) ctr2 + return ((l,o1 && o2,ctr):lctrs) + | otherwise = do intersect l o1 ctr1 lctrs lctrs2 +supertype scope (Just (VTable a1 r1)) (VTable a2 r2) = do + a <- subtype scope (Just a1) a2 + r <- supertype scope (Just r1) r2 + return (VTable a r) +supertype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) + | x == identW && y == identW = do + a <- subtype scope (Just a1) a2 + r <- supertype scope (Just r1) r2 + return (VProd Explicit identW a r) +supertype scope Nothing ty = return ty +supertype scope (Just ctr) ty = do + unify scope ctr ty + return ty + +----------------------------------------------------------------------- +-- Unification +----------------------------------------------------------------------- + +unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho) +unifyFun scope (VProd bt x arg res) = + return (bt,x,arg,res) +unifyFun scope (VFV c (VarFree vs)) = do + res <- mapM (unifyFun scope) vs + return + ( Explicit + , identW + , VFV c (VarFree [sigma | (_,_,sigma,rho) <- res]) + , VFV c (VarFree [rho | (_,_,sigma,rho) <- res]) + ) +unifyFun scope tau = do + let mk_val i = VMeta i [] + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope + let bt = Explicit + unify scope tau (VProd bt identW arg res) + return (bt,identW,arg,res) + +unifyTbl :: Scope -> Rho -> EvalM (Sigma, Rho) +unifyTbl scope (VTable arg res) = + return (arg,res) +unifyTbl scope tau = do + let mk_val i = VMeta i [] + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope + unify scope tau (VTable arg res) + return (arg,res) + +unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2) + | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) +unify scope (VMeta i vs1) (VMeta j vs2) + | i == j = sequence_ (zipWith (unify scope) vs1 vs2) + | otherwise = do + mv <- getMeta i + case mv of + Bound _ v1 -> do + g <- globals + unify scope (apply g v1 vs1) (VMeta j vs2) + Residuation scope1 _ -> do + mv <- getMeta j + case mv of + Bound _ v2 -> do + g <- globals + unify scope (VMeta i vs1) (apply g v2 vs2) + Residuation scope2 _ + | m > n -> setMeta i (Bound scope1 (VMeta j vs2)) + | otherwise -> setMeta j (Bound scope2 (VMeta i vs2)) + where + m = length scope1 + n = length scope2 +unify scope (VMeta i vs) v = unifyVar scope i vs v +unify scope v (VMeta i vs) = unifyVar scope i vs v +unify scope (VGen i vs1) (VGen j vs2) + | i == j = sequence_ (zipWith (unify scope) vs1 vs2) +unify scope (VProd b x d cod) (VProd b' x' d' cod') + | b == b' = do + unify scope d d' + cod <- evalCodomain x (VGen (length scope) []) cod + cod' <- evalCodomain x' (VGen (length scope) []) cod' + unify scope cod cod' +unify scope (VTable p1 res1) (VTable p2 res2) = do + unify scope p2 p1 + unify scope res1 res2 +unify scope (VSort s1) (VSort s2) + | s1 == s2 = return () +unify scope (VInt i) (VInt j) + | i == j = return () +unify scope (VFlt x) (VFlt y) + | x == y = return () +unify scope (VStr s1) (VStr s2) + | s1 == s2 = return () +unify scope VEmpty VEmpty = return () +unify scope v1 v2 = do + t1 <- value2termM False (scopeVars scope) v1 + t2 <- value2termM False (scopeVars scope) v2 + evalError ("Cannot unify:" <+> ppTerm Terse 0 t1 $$ + " with:" <+> ppTerm Terse 0 t2) + + +-- | Invariant: tv1 is a flexible type variable +unifyVar :: Scope -> MetaId -> [Value] -> Tau -> EvalM () +unifyVar scope metaid vs ty2 = do -- Check whether i is bound + mv <- getMeta metaid + case mv of + Bound _ ty1 -> do g <- globals + unify scope (apply g ty1 vs) ty2 + Residuation scope' _ -> do occursCheck scope' metaid scope ty2 + setMeta metaid (Bound scope' ty2) + +occursCheck scope' i0 scope v = + let m = length scope' + n = length scope + in check m n v + where + check m n (VApp c f vs) = mapM_ (check m n) vs + check m n (VMeta i vs) + | i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs) + ty2 <- value2termM False (scopeVars scope) v + evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2)) + | otherwise = do + s <- getMeta i + case s of + Bound _ v -> do g <- globals + check m n (apply g v vs) + _ -> mapM_ (check m n) vs + check m n (VGen i vs) + | i > m = let (v,_) = reverse scope !! i + in evalError ("Variable" <+> pp v <+> "has escaped") + | otherwise = mapM_ (check m n) vs + check m n (VClosure env c (Abs bt x t)) = do + g <- globals + check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) + check m n (VProd bt x ty1 ty2) = do + check m n ty1 + case ty2 of + VClosure env c t -> do g <- globals + check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) + _ -> check m n ty2 + check m n (VRecType as) = + mapM_ (\(_,_,v) -> check m n v) as + check m n (VR as) = + mapM_ (\(lbl,v) -> check m n v) as + check m n (VP v l vs) = + check m n v >> mapM_ (check m n) vs + check m n (VExtR v1 v2) = + check m n v1 >> check m n v2 + check m n (VTable v1 v2) = + check m n v1 >> check m n v2 + check m n (VT ty env c cs) = + check m n ty -- Traverse cs as well + check m n (VV ty cs) = + check m n ty >> mapM_ (check m n) cs + check m n (VS v1 v2 vs) = + check m n v1 >> check m n v2 >> mapM_ (check m n) vs + check m n (VSort _) = return () + check m n (VInt _) = return () + check m n (VFlt _) = return () + check m n (VStr _) = return () + check m n VEmpty = return () + check m n (VC v1 v2) = + check m n v1 >> check m n v2 + check m n (VGlue v1 v2) = + check m n v1 >> check m n v2 + check m n (VPatt _ _ _) = return () + check m n (VPattType v) = + check m n v + check m n (VFV c vs) = + mapM_ (check m n) (unvariants vs) + check m n (VAlts v vs) = + check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs + check m n (VStrs vs) = + mapM_ (check m n) vs + check m n (VInts _ _) = return () + +----------------------------------------------------------------------- +-- Instantiation and quantification +----------------------------------------------------------------------- + +-- | Instantiate the topmost implicit arguments with metavariables +instantiate :: Scope -> Term -> Sigma -> EvalM (Term,Rho) +instantiate scope t (VProd Implicit x ty1 ty2) = do + i <- newResiduation scope + ty2 <- case ty2 of + VClosure env c ty2 -> do g <- globals + return (eval g ((x,VMeta i []):env) c ty2 []) + ty2 -> return ty2 + instantiate scope (App t (ImplArg (Meta i))) ty2 +instantiate scope t ty@(VMeta i args) = getMeta i >>= \case + Bound _ v -> instantiate scope t v + Residuation _ (Just v) -> instantiate scope t v + _ -> return (t,ty) -- We don't have enough information to try any instantiation +instantiate scope t ty = do return (t,ty) --- | compositional check\/infer of binary operations -check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> - Term -> Term -> Type -> Check (Term,Type) -check2 chk con a b t = do - a' <- chk a - b' <- chk b - return (con a' b', t) +-- | Build fresh lambda abstractions for the topmost implicit arguments +skolemise :: Scope -> Sigma -> EvalM (Scope, Term->Term, Rho) +skolemise scope ty@(VMeta i vs) = do + mv <- getMeta i + case mv of + Residuation _ _ -> return (scope,id,ty) -- guarded constant? + Bound _ ty -> do g <- globals + skolemise scope (apply g ty vs) +skolemise scope (VProd Implicit x ty1 ty2) = do + let v = newVar scope + ty2 <- evalCodomain x (VGen (length scope) []) ty2 + (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 + return (scope,Abs Implicit v . f,ty2) +skolemise scope ty = do + return (scope,id,ty) --- printing a type with a lock field lock_C as C -ppType :: Type -> Doc -ppType ty = - case ty of - RecType fs -> case filter isLockLabel $ map fst fs of - [lock] -> pp (drop 5 (showIdent (label2ident lock))) - _ -> ppTerm Unqualified 0 ty - Prod _ x a b -> ppType a <+> "->" <+> ppType b - _ -> ppTerm Unqualified 0 ty +-- | Quantify over the specified type variables (all flexible) +quantify :: Scope -> Term -> [MetaId] -> Rho -> EvalM (Term,Sigma) +quantify scope t tvs ty = do + let m = length tvs + n = length scope + (used_bndrs,ty) <- check m n [] ty + let new_bndrs = take m (allBinders \\ used_bndrs) + mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs) + let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs + return (foldr (Abs Implicit) t new_bndrs,ty') + where + bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i [])) -checkLookup :: Ident -> Context -> Check Type -checkLookup x g = - case [ty | (b,y,ty) <- g, x == y] of - [] -> checkError ("unknown variable" <+> x) - (ty:_) -> return ty + check m n xs (VApp c f vs) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VApp c f vs) + check m n xs (VMeta i vs) = do + s <- getMeta i + case s of + Bound _ v -> do g <- globals + check m n xs (apply g v vs) + _ -> do (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VMeta i vs) + check m n st (VGen i vs)= do + (st,vs) <- mapAccumM (check m n) st vs + return (st, VGen (m+i) vs) + check m n st (VClosure env c (Abs bt x t)) = do + (st,env) <- mapAccumM (\st (x,v) -> check m n st v >>= \(st,v) -> return (st,(x,v))) st env + return (st,VClosure env c (Abs bt x t)) + check m n xs (VProd bt x v1 v2) = do + (xs,v1) <- check m n xs v1 + case v2 of + VClosure env c t -> do (st,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (x:xs,VProd bt x v1 (VClosure env c t)) + v2 -> do (xs,v2) <- check m (n+1) xs v2 + return (x:xs,VProd bt x v1 v2) + check m n xs (VRecType as) = do + (xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,v))) xs as + return (xs,VRecType as) + check m n xs (VR as) = do + (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as + return (xs,VR as) + check m n xs (VP v l vs) = do + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VP v l vs) + check m n xs (VExtR v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VExtR v1 v2) + check m n xs (VTable v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VTable v1 v2) + check m n xs (VT ty env c cs) = do + (xs,ty) <- check m n xs ty + (xs,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (xs,VT ty env c cs) + check m n xs (VV ty cs) = do + (xs,ty) <- check m n xs ty + (xs,cs) <- mapAccumM (check m n) xs cs + return (xs,VV ty cs) + check m n xs (VS v1 tnk vs) = do + (xs,v1) <- check m n xs v1 + (xs,tnk) <- check m n xs tnk + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VS v1 tnk vs) + check m n xs v@(VSort _) = return (xs,v) + check m n xs v@(VInt _) = return (xs,v) + check m n xs v@(VFlt _) = return (xs,v) + check m n xs v@(VStr _) = return (xs,v) + check m n xs v@VEmpty = return (xs,v) + check m n xs (VC v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VC v1 v2) + check m n xs (VGlue v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VGlue v1 v2) + check m n xs v@(VPatt _ _ _) = return (xs,v) + check m n xs (VPattType v) = do + (xs,v) <- check m n xs v + return (xs,VPattType v) + check m n xs (VFV c (VarFree vs)) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VFV c (VarFree vs)) + check m n xs (VFV c (VarOpts name os)) = do + (xs,os) <- mapAccumM (\acc (l,v) -> second (l,) <$> check m n acc v) xs os + return (xs,VFV c (VarOpts name os)) + check m n xs (VAlts v vs) = do + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,(v1,v2))) + xs vs + return (xs,VAlts v vs) + check m n xs (VStrs vs) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VStrs vs) + check m n xs v = unimplemented ("check "++show (ppValue Unqualified 5 v)) + + mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c]) + mapAccumM f s [] = return (s,[]) + mapAccumM f s (x:xs) = do + (s,y) <- f s x + (s,ys) <- mapAccumM f s xs + return (s,y:ys) + +allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... +allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ + [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] + +----------------------------------------------------------------------- +-- Helpers +----------------------------------------------------------------------- + +type Sigma = Value +type Rho = Value -- No top-level ForAll +type Tau = Value -- No ForAlls anywhere + +unimplemented str = fail ("Unimplemented: "++str) + +newVar :: Scope -> Ident +newVar scope = head [x | i <- [1..], + let x = identS ('v':show i), + isFree scope x] + where + isFree [] x = True + isFree ((y,_):scope) x = x /= y && isFree scope x + +scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] +scopeVars scope = map fst scope +scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) + +-- | This function takes account of zonking, and returns a set +-- (no duplicates) of unbound meta-type variables +getMetaVars :: [(Scope,Sigma)] -> EvalM [MetaId] +getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys + where + -- Get the MetaIds from a term; no duplicates in result + go acc (VGen i args) = foldM go acc args + go acc (VSort s) = return acc + go acc (VInt _) = return acc + go acc (VRecType vs) = foldM (\acc (lbl,_,v) -> go acc v) acc vs + go acc (VClosure _ _ _) = return acc + go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1 + go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1 + go acc (VMeta m args) + | m `elem` acc = return acc + | otherwise = do res <- getMeta m + case res of + Bound _ v -> go acc v + Residuation _ Nothing -> foldM go (m:acc) args + Residuation _ (Just v) -> go acc v + _ -> return acc + go acc (VApp c f args) = foldM go acc args + go acc (VFV c vs) = foldM go acc (unvariants vs) + go acc (VInts _ _) = return acc + go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) + +-- | Eliminate any substitutions in a term +zonkTerm :: [Ident] -> Term -> EvalM Term +zonkTerm xs (Abs b x t) = do + t <- zonkTerm (x:xs) t + return (Abs b x t) +zonkTerm xs (Prod b x t1 t2) = do + t1 <- zonkTerm xs t1 + t2 <- zonkTerm xs' t2 + return (Prod b x t1 t2) + where + xs' | x == identW = xs + | otherwise = x:xs +zonkTerm xs (Meta i) = do + st <- getMeta i + case st of + Bound _ v -> zonkTerm xs =<< value2termM False xs v + Residuation scope v -> case v of + Just v -> zonkTerm xs =<< value2termM False (map fst scope) v + Nothing -> return (Meta i) + Narrowing _ -> return (Meta i) +zonkTerm xs t = composOp (zonkTerm xs) t diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs deleted file mode 100644 index 9a0452ac1..000000000 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ /dev/null @@ -1,1309 +0,0 @@ -{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} -module GF.Compile.TypeCheck.ConcreteNew ( checkLType, checkLType', inferLType, inferLType' ) where - --- The code here is based on the paper: --- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. --- Practical type inference for arbitrary-rank types. --- 14 September 2011 - -import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) -import GF.Grammar.Lookup -import GF.Grammar.Predef -import GF.Grammar.Lockfield -import GF.Compile.Compute.Concrete2 -import GF.Infra.CheckM -import GF.Data.ErrM ( Err(Ok, Bad) ) -import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) -import Control.Monad.ST -import GF.Text.Pretty -import Data.STRef -import Data.List (nub, (\\), tails) -import qualified Data.Map as Map -import Data.Maybe(fromMaybe,isNothing,mapMaybe) -import Data.Bifunctor(second) -import Data.Functor((<&>)) -import qualified Control.Monad.Fail as Fail - -checkLType :: Globals -> Term -> Type -> Check (Term, Type) -checkLType globals t ty = do - res <- runEvalM globals $ do - let (c1,c2) = split unit - (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) - ty <- value2termM True [] vty - return (t,ty) - case res of - [tty] -> return tty - _ -> checkError (pp "Encountered variants while type checking") - -checkLType' :: Choice -> Term -> Constraint -> EvalM (Term, Constraint) -checkLType' c t vty = do - (t,vty) <- tcRho [] c t (Just vty) - t <- zonkTerm [] t - return (t,vty) - -inferLType :: Globals -> Term -> Check (Term, Type) -inferLType globals t = do - res <- runEvalM globals $ do - (t,vty) <- inferLType' t - ty <- value2termM True [] vty - return (t,ty) - case res of - [tty] -> return tty - _ -> checkError (pp "Encountered variants while type checking") - -inferLType' :: Term -> EvalM (Term, Constraint) -inferLType' t = do - (t,vty) <- inferSigma [] unit t - t <- zonkTerm [] t - return (t,vty) - -inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma) -inferSigma scope s t = do -- GEN1 - (t,ty) <- tcRho scope s t Nothing - env_tvs <- getMetaVars (scopeTypes scope) - res_tvs <- getMetaVars [(scope,ty)] - let forall_tvs = res_tvs \\ env_tvs - quantify scope t forall_tvs ty - -vtypeInt = VApp poison (cPredef,cInt) [] -vtypeFloat = VApp poison (cPredef,cFloat) [] -vtypeInts i= VApp poison (cPredef,cInts) [VInt i] -vtypeStr = VSort cStr -vtypeStrs = VSort cStrs -vtypeType = VSort cType -vtypePType = VSort cPType -vtypeMarkup= VApp poison (cPredef,cMarkup) [] - -tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho) -tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT -tcRho scope s t@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT -tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR -tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty -tcRho scope s t@(Vr v) mb_ty = do -- VAR - case lookup v scope of - Just v_sigma -> instSigma scope s t v_sigma mb_ty - Nothing -> evalError ("Unknown variable" <+> v) -tcRho scope c t@(Q id) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c t@(QC id) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c t@(App fun arg) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c (Abs bt var body) Nothing = do -- ABS1 - i <- newResiduation scope - let arg_ty = VMeta i [] - (body,body_ty) <- tcRho ((var,arg_ty):scope) c body Nothing - let m = length scope - n = m+1 - (b,used_bndrs) <- check m n (False,[]) body_ty - if b - then let v = head (allBinders \\ used_bndrs) - in return (Abs bt var body, (VProd bt v arg_ty body_ty)) - else return (Abs bt var body, (VProd bt identW arg_ty body_ty)) - where - check m n st (VApp c f vs) = foldM (check m n) st vs - check m n st (VMeta i vs) = do - state <- getMeta i - case state of - Bound _ v -> do g <- globals - check m n st (apply g v vs) - _ -> foldM (check m n) st vs - check m n st@(b,xs) (VGen i vs) - | i == m = return (True, xs) - | otherwise = return st - check m n st (VClosure env c (Abs bt x t)) = do - g <- globals - check m (n+1) st (eval g ((x,VGen n []):env) c t []) - check m n st (VProd _ x v1 v2) = do - st@(b,xs) <- check m n st v1 - case v2 of - VClosure env c t -> do g <- globals - check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t []) - v2 -> check m n st v2 - check m n st (VRecType as) = foldM (\st (l,_,v) -> check m n st v) st as - check m n st (VR as) = - foldM (\st (lbl,tnk) -> check m n st tnk) st as - check m n st (VP v l vs) = - check m n st v >>= \st -> foldM (check m n) st vs - check m n st (VExtR v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VTable v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VT ty env c cs) = - check m n st ty -- Traverse cs as well - check m n st (VV ty cs) = - check m n st ty >>= \st -> foldM (check m n) st cs - check m n st (VS v1 tnk vs) = do - st <- check m n st v1 - st <- check m n st tnk - foldM (check m n) st vs - check m n st (VSort _) = return st - check m n st (VInt _) = return st - check m n st (VFlt _) = return st - check m n st (VStr _) = return st - check m n st VEmpty = return st - check m n st (VC v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VGlue v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VPatt _ _ _) = return st - check m n st (VPattType v) = check m n st v - check m n st (VAlts v vs) = do - st <- check m n st v - foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs - check m n st (VStrs vs) = - foldM (check m n) st vs -tcRho scope c t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, x, var_ty, body_ty) <- unifyFun scope ty - if bt == Implicit - then return () - else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") - body_ty <- evalCodomain x (VGen (length scope) []) body_ty - (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) - return (Abs Implicit var body,ty) -tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3 - (scope,f,ty') <- skolemise scope ty - (_,x,var_ty,body_ty) <- unifyFun scope ty' - body_ty <- evalCodomain x (VGen (length scope) []) body_ty - (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) - return (f (Abs Explicit var body),ty) -tcRho scope c (Meta _) mb_ty = do - i <- newResiduation scope - ty <- case mb_ty of - Just ty -> return ty - Nothing -> do j <- newResiduation scope - return (VMeta j []) - return (Meta i, ty) -tcRho scope c (Let (var, (Nothing, rhs)) body) mb_ty = do -- LET - let (c1,c2) = split c - (rhs,var_ty) <- tcRho scope c1 rhs Nothing - (body, body_ty) <- tcRho ((var,var_ty):scope) c2 body mb_ty - var_ty <- value2termM True (scopeVars scope) var_ty - return (Let (var, (Just var_ty, rhs)) body, body_ty) -tcRho scope c (Let (var, (Just ann_ty, rhs)) body) mb_ty = do -- LET - let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (rhs,_) <- tcRho scope c3 rhs (Just v_ann_ty) - (body, body_ty) <- tcRho ((var,v_ann_ty):scope) c4 body mb_ty - var_ty <- value2termM True (scopeVars scope) v_ann_ty - return (Let (var, (Just var_ty, rhs)) body, body_ty) -tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT - let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (body,_) <- tcRho scope c3 body (Just v_ann_ty) - instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty -tcRho scope c (FV ts) mb_ty = do - (ts,ty) <- tcUnifying scope c ts mb_ty - return (FV ts, ty) -tcRho scope s t@(Sort _) mb_ty = do - instSigma scope s t vtypeType mb_ty -tcRho scope c t@(RecType rs) Nothing = do - (rs,mb_ty) <- tcRecTypeFields scope c rs Nothing - return (RecType rs,fromMaybe vtypePType mb_ty) -tcRho scope c t@(RecType rs) (Just ty) = do - (scope,f,ty') <- skolemise scope ty - case ty' of - VSort s - | s == cType -> return () - | s == cPType -> return () - VMeta i vs-> case rs of - [] -> unifyVar scope i vs vtypePType - _ -> return () - ty -> do ty <- value2termM False (scopeVars scope) ty - evalError ("The record type" <+> ppTerm Unqualified 0 t $$ - "cannot be of type" <+> ppTerm Unqualified 0 ty) - (rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty') - return (f (RecType rs),ty) -tcRho scope s t@(Table p res) mb_ty = do - let (s1,s23) = split s - (s2,s3) = split s23 - (p, p_ty) <- tcRho scope s1 p (Just vtypePType) - (res,res_ty) <- tcRho scope s2 res (Just vtypeType) - instSigma scope s3 (Table p res) vtypeType mb_ty -tcRho scope c (Prod bt x ty1 ty2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (ty1,ty1_ty) <- tcRho scope c1 ty1 (Just vtypeType) - g <- globals - (ty2,ty2_ty) <- tcRho ((x,eval g (scopeEnv scope) c2 ty1 []):scope) c3 ty2 (Just vtypeType) - instSigma scope c4 (Prod bt x ty1 ty2) vtypeType mb_ty -tcRho scope c (S t p) mb_ty = do - let (c1,c2) = split c - let mk_val i = VMeta i [] - p_ty <- fmap mk_val $ newResiduation scope - res_ty <- case mb_ty of - Nothing -> fmap mk_val $ newResiduation scope - Just ty -> return ty - let t_ty = VTable p_ty res_ty - (t,t_ty) <- tcRho scope c1 t (Just t_ty) - (p,_) <- tcRho scope c2 p (Just p_ty) - return (S t p, res_ty) -tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables - let (c1,c2) = split c - let mk_val i = VMeta i [] - p_ty <- case tt of - TRaw -> fmap mk_val $ newResiduation scope - TTyped ty -> do let (c3,c4) = split c1 - (ty, _) <- tcRho scope c3 ty (Just vtypeType) - g <- globals - return (eval g (scopeEnv scope) c4 ty []) - res_ty <- fmap mk_val $ newResiduation scope - ps <- tcCases scope c2 ps p_ty res_ty - p_ty_t <- value2termM True [] p_ty - return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) -tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables - let (c12,c34) = split c - (c3,c4) = split c34 - (scope,f,ty') <- skolemise scope ty - (p_ty, res_ty) <- unifyTbl scope ty' - case tt of - TRaw -> return () - TTyped ty -> do let (c1,c2) = split c12 - (ty, _) <- tcRho scope c1 ty (Just vtypeType) - g <- globals - unify scope (eval g (scopeEnv scope) c2 ty []) p_ty - ps <- tcCases scope c3 ps p_ty res_ty - p_ty_t <- value2termM True (scopeVars scope) p_ty - return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) -tcRho scope c (V p_ty ts) Nothing = do - let (c1,c2,c3,c4) = split4 c - (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType) - i <- newResiduation scope - let res_ty = VMeta i [] - - let go c t = do (t, ty) <- tcRho scope c t Nothing - subsCheckRho scope t ty res_ty - - ts <- mapCM go c2 ts - g <- globals - return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty) -tcRho scope c (V p_ty0 ts) (Just ty) = do - let (c1,c2,c3,c4) = split4 c - (scope,f,ty') <- skolemise scope ty - (p_ty, res_ty) <- unifyTbl scope ty' - (p_ty0, _) <- tcRho scope c1 p_ty0 (Just vtypeType) - g <- globals - let p_vty0 = eval g (scopeEnv scope) c2 p_ty0 [] - unify scope p_ty p_vty0 - ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts - return (V p_ty0 ts, VTable p_ty res_ty) -tcRho scope c (R rs) Nothing = do - lttys <- inferRecFields scope c rs - rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys - return (R rs, - VRecType [(l,True,ty) | (l,t,ty) <- lttys] - ) -tcRho scope c (R rs) (Just ty) = do - (scope,f,ty') <- skolemise scope ty - case ty' of - (VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys - rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys - return ((f . R) rs, - VRecType [(l,True,ty) | (l,t,ty) <- lttys] - ) - ty -> do lttys <- inferRecFields scope c rs - t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) - let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys] - t <- subsCheckRho scope t ty' ty - return (t, ty') -tcRho scope c (P t l) mb_ty = do - l_ty <- case mb_ty of - Just ty -> return ty - Nothing -> do i <- newResiduation scope - return (VMeta i []) - (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)])) - return (P t l,l_ty) -tcRho scope c (C t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) - instSigma scope c3 (C t1 t2) vtypeStr mb_ty -tcRho scope c (Glue t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) - instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty -tcRho scope c t@(ExtR t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 Nothing - (t2,t2_ty) <- tcRho scope c2 t2 Nothing - case (t1_ty,t2_ty) of - (VSort s1,VSort s2) - | (s1 == cType || s1 == cPType) && - (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType - | otherwise = cType - in instSigma scope c3 (ExtR t1 t2) (VSort sort) mb_ty - (VRecType rs1, VRecType rs2) -> instSigma scope c3 (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty - _ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t) -tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty -tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho scope c (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty -tcRho scope c (Alts t ss) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t,_) <- tcRho scope c1 t (Just vtypeStr) - ss <- mapCM (\c (t1,t2) -> do - let (c1,c2) = split c - (t1,_) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,_) <- tcRho scope c2 t2 (Just vtypeStrs) - return (t1,t2)) - c2 ss - instSigma scope c3 (Alts t ss) vtypeStr mb_ty -tcRho scope c (Strs ss) mb_ty = do - let (c1,c2) = split c - ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr) - return t) - c1 ss - instSigma scope c2 (Strs ss) vtypeStrs mb_ty -tcRho scope c (EPattType ty) mb_ty = do - let (c1,c2) = split c - (ty, _) <- tcRho scope c1 ty (Just vtypeType) - instSigma scope c2 (EPattType ty) vtypeType mb_ty -tcRho scope c t@(EPatt min max p) mb_ty = do - (scope,f,ty) <- case mb_ty of - Nothing -> do i <- newResiduation scope - return (scope,id,VMeta i []) - Just ty -> do (scope,f,ty) <- skolemise scope ty - case ty of - VPattType ty -> return (scope,f,ty) - _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") - tcPatt scope c p ty - return (f (EPatt min max p), ty) -tcRho scope c (Markup tag attrs children) mb_ty = do - let (c1,c2,c3,c4) = split4 c - attrs <- mapCM (\c (id,t) -> do - (t,_) <- tcRho scope c t Nothing - return (id,t)) - c1 attrs - res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children - instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty -tcRho scope c (Reset ctl mb_ct t qid) mb_ty - | ctl == cConcat = do - let (c1,c23) = split c - (c2,c3 ) = split c23 - (t,_) <- tcRho scope c1 t Nothing - mb_ct <- case mb_ct of - Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt) - return (Just ct) - Nothing -> return Nothing - instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty - | ctl == cOne = do - let (c1,c2) = split c - (t,ty) <- tcRho scope c1 t mb_ty - (mb_ct,ty) <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) - return (Just ct,ty) - Nothing -> return (Nothing,ty) - return (Reset ctl mb_ct t qid,ty) - | ctl == cDefault = do - let (c1,c2) = split c - (t,ty) <- tcRho scope c1 t mb_ty - (mb_ct,ty) <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) - return (Just ct,ty) - Nothing -> evalError (pp "[list: .. | ..] requires an argument") - return (Reset ctl mb_ct t qid,ty) - | ctl == cList = do - do let (c1,c2) = split c - mb_ct <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing - return (Just ct) - Nothing -> evalError (pp "[list: .. | ..] requires an argument") - (t,ty) <- tcRho scope c2 t mb_ty - case ty of - VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) - _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) - | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") -tcRho scope s (Opts n cs) mb_ty = do - let (s1,s2,s3) = split3 s - (n,_) <- tcRho scope s1 n Nothing - (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing - (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty - return (Opts n (zip ls ts), ty) -tcRho scope s t _ = unimplemented ("tcRho "++show t) - -evalCodomain :: Ident -> Value -> Value -> EvalM Value -evalCodomain x v (VClosure env c ty) = do - g <- globals - return (eval g ((x,v):env) c ty []) -evalCodomain x _ ty = return ty - -tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint) -tcUnifying scope c ts mb_ty = do - (ty,subsume) <- - case mb_ty of - Just ty -> do return (ty, \t ty' -> return t) - Nothing -> do i <- newResiduation scope - let ty = VMeta i [] - return (ty, \t ty' -> subsCheckRho scope t ty' ty) - - let go c t = do (t, ty) <- tcRho scope c t mb_ty - subsume t ty - - ts <- mapCM go c ts - return (ts,ty) - -tcCases scope c [] p_ty res_ty = return [] -tcCases scope c ((p,t):cs) p_ty res_ty = do - let (c1,c2,c3,c4) = split4 c - scope' <- tcPatt scope c1 p p_ty - (t,_) <- tcRho scope' c2 t (Just res_ty) - cs <- tcCases scope c3 cs p_ty res_ty - return ((p,t):cs) - -tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP -tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) -tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) -tcApp scope c t0 t args mb_ty = do - let (c1,c23) = split c - let (c2,c3) = split c23 - (t,ty) <- tcRho scope c1 t Nothing - (t,ty) <- reapply1 scope c2 t ty args - instSigma scope c3 t ty mb_ty - -reapply1 :: Scope -> Choice -> Term -> Value -> [Term] -> EvalM (Term,Rho) -reapply1 scope c fun fun_ty [] = return (fun,fun_ty) -reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case - let (c1,c2,c3,c4) = split4 c - (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty - unless (bt == Implicit) $ - evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> - "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho scope c1 arg (Just arg_ty) - g <- globals - res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty - reapply1 scope c3 (App fun (ImplArg arg)) res_ty args -reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case - let (c1,c2,c3,c4) = split4 c - (fun,fun_ty) <- instantiate scope fun fun_ty - (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty - (arg,_) <- tcRho scope c1 arg (Just arg_ty) - g <- globals - res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty - reapply1 scope c3 (App fun arg) res_ty args - -resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) -resolveOverloads scope c t0 q args mb_ty = do - g@(Gl gr _) <- globals - case lookupOverloadTypes gr q of - Bad msg -> evalError (pp msg) - Ok [(t,ty)] -> do let (c1,c23) = split c - (c2,c3) = split c23 - (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args - instSigma scope c3 t ty mb_ty - Ok ttys -> do let (c1,c23) = split c - (c2,c3) = split c23 - arg_tys <- mapCM (checkArg g) c1 args - let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys - try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) - (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys))) - v_ttys - where - checkArg g c (ImplArg arg) = do - let (c1,c2) = split c - (arg,arg_ty) <- tcRho scope c1 arg Nothing - let v = eval g (scopeEnv scope) c2 arg [] - return (ImplArg arg,v,arg_ty) - checkArg g c arg = do - let (c1,c2) = split c - (arg,arg_ty) <- tcRho scope c1 arg Nothing - let v = eval g (scopeEnv scope) c2 arg [] - return (arg,v,arg_ty) - - mkFV [t] = t - mkFV ts = FV ts - - minimum g [] = (maxBound,err) - where - err = evalError (pp "Overload resolution failed") - minimum g (tty@((t,ty),state):ttys) = - let ty' = zonk ty - a = arity ty' - (a',res) = minimum g ttys - in case compare a a' of - GT -> (a',res) - EQ -> (a',join t ty' state res) - LT -> (a ,one t ty' state) - where - arity :: Value -> Int - arity (VProd _ _ _ ty) = 1 + arity ty - arity _ = 0 - - zonk :: Value -> Value - zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2) - zonk (VMeta i vs) = - case Map.lookup i (metaVars state) of - Just (Bound _ v) -> zonk (apply g v vs) - Just (Residuation _ (Just v)) -> zonk (apply g v vs) - _ -> VMeta i (map zonk vs) - zonk (VSusp i k vs) = - case Map.lookup i (metaVars state) of - Just (Bound _ v) -> zonk (apply g (k v) vs) - Just (Residuation _ (Just v)) -> zonk (apply g (k v) vs) - _ -> VSusp i k (map zonk vs) - zonk v = v - - one t ty state = do - t <- withState state (zonkTerm [] t) - return ([t],ty) - - join t ty state res = do - t <- withState state (zonkTerm [] t) - (ts,ty') <- res - ty <- supertype scope (Just ty) ty' - return (t:ts,ty) - -reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) -reapply2 scope c fun fun_ty [] mb_ty = instSigma scope c fun fun_ty mb_ty -reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case - (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty - unless (bt == Implicit) $ - evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> - "is an implicit argument application, but no implicit argument is expected") - arg <- subsCheckRho scope arg arg_ty' arg_ty - res_ty <- evalCodomain x arg_v res_ty - reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty -reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case - (fun,fun_ty) <- instantiate scope fun fun_ty - (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty - arg <- subsCheckRho scope arg arg_ty arg_ty' - res_ty <- evalCodomain x arg_v res_ty - reapply2 scope c (App fun arg) res_ty args mb_ty - -tcPatt scope c PW ty0 = - return scope -tcPatt scope c (PV x) ty0 = - return ((x,ty0):scope) -tcPatt scope c (PP q ps) ty0 = do - g@(Gl gr _) <- globals - ty <- case lookupResType gr q of - Ok ty -> return ty - Bad msg -> evalError (pp msg) - let go scope c ty [] = return (scope,ty) - go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty - let (c1,c2) = split c - scope <- tcPatt scope c1 p arg_ty - go scope c2 res_ty ps - let (c1,c2) = split c - (scope,ty) <- go scope c1 (eval g [] c2 ty []) ps - unify scope ty0 ty - return scope -tcPatt scope c (PInt i) ty0 = do - subsCheckRho scope (EInt i) (vtypeInts i) ty0 - return scope -tcPatt scope c (PString s) ty0 = do - unify scope ty0 vtypeStr - return scope -tcPatt scope c PChar ty0 = do - unify scope ty0 vtypeStr - return scope -tcPatt scope c (PChars cs) ty0 = do - unify scope ty0 vtypeStr - return scope -tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do - unify scope ty0 vtypeStr - let (c1,c2) = split c - scope <- tcPatt scope c1 p1 vtypeStr - scope <- tcPatt scope c2 p2 vtypeStr - return scope -tcPatt scope c (PRep _ _ p) ty0 = do - unify scope ty0 vtypeStr - tcPatt scope c p vtypeStr -tcPatt scope c (PAs x p) ty0 = do - tcPatt ((x,ty0):scope) c p ty0 -tcPatt scope c (PR rs) ty0 = do - let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- newResiduation scope - ltys <- mk_ltys rs - return ((l,p,VMeta i []) : ltys) - go scope c [] = return scope - go scope c ((l,p,ty):rs) = do let (c1,c2) = split c - scope <- tcPatt scope c1 p ty - go scope c2 rs - ltys <- mk_ltys rs - subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,True,ty) | (l,p,ty) <- ltys]) ty0 - go scope c ltys -tcPatt scope c (PAlt p1 p2) ty0 = do - let (c1,c2) = split c - tcPatt scope c1 p1 ty0 - tcPatt scope c2 p2 ty0 - return scope -tcPatt scope c (PM q) ty0 = do - g@(Gl gr _) <- globals - ty <- case lookupResType gr q of - Ok ty -> return ty - Bad msg -> evalError (pp msg) - case ty of - EPattType ty - -> do unify scope ty0 (eval g [] c ty []) - return scope - ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") -tcPatt scope c p ty = unimplemented ("tcPatt "++show p) - -inferRecFields scope c rs = - mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs - -checkRecFields scope c [] ltys - | null ltys = return [] - | otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys]) -checkRecFields scope c ((l,t):lts) ltys = - case takeIt l ltys of - (Just ty,ltys) -> do let (c1,c2) = split c - ltty <- tcRecField scope c1 l t (Just ty) - lttys <- checkRecFields scope c2 lts ltys - return (ltty : lttys) - (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) - lttys <- checkRecFields scope c lts ltys - return lttys -- ignore the field - where - takeIt l1 [] = (Nothing, []) - takeIt l1 (lty@(l2,_,ty):ltys) - | l1 == l2 = (Just ty,ltys) - | otherwise = let (mb_ty,ltys') = takeIt l1 ltys - in (mb_ty,lty:ltys') - -tcRecField scope c l (mb_ann_ty,t) mb_ty = do - (t,ty) <- case mb_ann_ty of - Just ann_ty -> do let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (t,_) <- tcRho scope c3 t (Just v_ann_ty) - instSigma scope c4 t v_ann_ty mb_ty - Nothing -> tcRho scope c t mb_ty - return (l,t,ty) - -tcRecTypeFields scope c [] mb_ty = return ([],mb_ty) -tcRecTypeFields scope c ((l,ty):rs) mb_ty = do - let (c1,c2) = split c - (ty,sort) <- tcRho scope c1 ty mb_ty - mb_ty <- case sort of - VSort s - | s == cType -> return (Just sort) - | s == cPType -> return mb_ty - VMeta _ _ -> return mb_ty - _ -> do sort <- value2termM False (scopeVars scope) sort - evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ - "cannot be of type" <+> ppTerm Unqualified 0 sort) - (rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty - return ((l,ty):rs,mb_ty) - --- | Invariant: if the third argument is (Just rho), --- then rho is in weak-prenex form -instSigma :: Scope -> Choice -> Term -> Sigma -> Maybe Rho -> EvalM (Term, Rho) -instSigma scope s t ty1 Nothing = return (t,ty1) -- INST1 -instSigma scope s t ty1 (Just ty2) = do -- INST2 - t <- subsCheckRho scope t ty1 ty2 - return (t,ty2) - --- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM Term -subsCheckRho scope t (VMeta i vs1) (VMeta j vs2) - | i == j = do sequence_ (zipWith (unify scope) vs1 vs2) - return t - | otherwise = do - mv <- getMeta i - case mv of - Bound _ v1 -> do - g <- globals - subsCheckRho scope t (apply g v1 vs1) (VMeta j vs2) - Residuation scope1 (Just ctr1) -> do - g <- globals - subsCheckRho scope t (apply g ctr1 vs1) (VMeta j vs2) - Residuation scope1 Nothing -> do - mv <- getMeta j - case mv of - Bound _ v2 -> do - g <- globals - subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2) - Residuation scope2 ctr2 - | m > n -> do setMeta i (Bound scope1 (VMeta j vs2)) - return t - | otherwise -> case ctr2 of - Nothing -> do setMeta j (Bound scope2 (VMeta i vs2)) - return t - Just ctr2 -> do g <- globals - subsCheckRho scope t (VMeta i vs1) (apply g ctr2 vs2) - where - m = length scope1 - n = length scope2 -subsCheckRho scope t ty1@(VMeta i vs) ty2 = do - mv <- getMeta i - case mv of - Bound _ ty1 -> do - g <- globals - subsCheckRho scope t (apply g ty1 vs) ty2 - Residuation scope' ctr -> do - occursCheck scope' i scope ty2 - ctr <- subtype scope ctr ty2 - setMeta i (Residuation scope' (Just ctr)) - return t -subsCheckRho scope t ty1 ty2@(VMeta i vs) = do - mv <- getMeta i - case mv of - Bound _ ty2 -> do - g <- globals - subsCheckRho scope t ty1 (apply g ty2 vs) - Residuation scope' ctr -> do - occursCheck scope' i scope ty1 - ctr <- supertype scope ctr ty1 - setMeta i (Residuation scope' (Just ctr)) - return t -subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC - i <- newResiduation scope - g <- globals - let ty2' = case ty2 of - VClosure env c ty2 -> eval g ((x,VMeta i []):env) c ty2 [] - ty2 -> ty2 - subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2 -subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL - let v = newVar scope - ty2 <- evalCodomain x (VGen (length scope) []) ty2 - t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 - return (Abs Implicit v t) -subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN - (_,_,a1,r1) <- unifyFun scope rho1 - subsCheckFun scope t a1 r1 a2 r2 -subsCheckRho scope t (VProd Explicit _ a1 r1) rho2 = do -- Rule FUN - (_,_,a2,r2) <- unifyFun scope rho2 - subsCheckFun scope t a1 r1 a2 r2 -subsCheckRho scope t rho1 (VTable p2 r2) = do -- Rule TABLE - (p1,r1) <- unifyTbl scope rho1 - subsCheckTbl scope t p1 r1 p2 r2 -subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE - (p2,r2) <- unifyTbl scope rho2 - subsCheckTbl scope t p1 r1 p2 r2 -subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE - | s1 == cPType && s2 == cType = return t -subsCheckRho scope t (VApp _ p1 []) rho2 -- for backwards compatibility - | p1 == (cPredef,cErrorType) = return t -subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- This is not correct but there is in the RGL nextPrec relies on it. - | p1 == (cPredef,cInt) && p2 == (cPredef,cInts) = return t -- Should be only a temporary hack. -subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t -subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do - if i <= j - then return t - else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) -subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC - let mkAccess scope t = - case t of - ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 - (scope,mkProj2,mkWrap2) <- mkAccess scope t2 - return (scope - ,\l -> mkProj2 l `mplus` mkProj1 l - ,mkWrap1 . mkWrap2 - ) - R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] - return (scope - ,\l -> lookup l rs - ,id - ) - Vr x -> do return (scope - ,\l -> do VRecType rs <- lookup x scope - ty <- lookup3 l rs - return (Nothing,P t l) - ,id - ) - t -> let x = newVar scope - in return (((x,ty1):scope) - ,\l -> return (Nothing,P (Vr x) l) - ,Let (x, (Nothing, t)) - ) - - mkField scope l (mb_ty,t) ty1 ty2 = do - t <- subsCheckRho scope t ty1 ty2 - return (l, (mb_ty,t)) - - lookup3 l [] = Nothing - lookup3 l ((l',_,v):rs) - | l == l' = Just v - | otherwise = lookup3 l rs - - (scope,mkProj,mkWrap) <- mkAccess scope t - - let fields = [(l,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2] - case [l | (l,_,Nothing) <- fields, not (isLockLabel l)] of - [] -> return () - missing -> evalError ("In the term" <+> pp t $$ - "there are no values for fields:" <+> hsep missing) - rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] - return (mkWrap (R (rs++[(l, (Just (RecType []),R [])) | (l,_,Nothing) <- fields, isLockLabel l]))) -subsCheckRho scope t tau1 (VFV c (VarFree vs)) = do - tau2 <- variants c vs - subsCheckRho scope t tau1 tau2 -subsCheckRho scope t (VFV c (VarFree vs)) tau2 = do - tau1 <- variants c vs - subsCheckRho scope t tau1 tau2 -subsCheckRho scope t tau1 tau2 = do -- Rule EQ - unify scope tau1 tau2 -- Revert to ordinary unification - return t - -subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM Term -subsCheckFun scope t a1 r1 a2 r2 = do - let v = newVar scope - vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 - g <- globals - let r1' = case r1 of - VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 [] - r1 -> r1 - r2' = case r2 of - VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 [] - r2 -> r2 - t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2' - return (Abs Explicit v t) - -subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term -subsCheckTbl scope t p1 r1 p2 r2 = do - let x = newVar scope - xt <- subsCheckRho ((x,p2):scope) (Vr x) p2 p1 - t <- subsCheckRho ((x,p2):scope) (S t xt) r1 r2 - p2 <- value2termM True (scopeVars scope) p2 - return (T (TTyped p2) [(PV x,t)]) - -subtype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VInts Nothing (Just i)) -subtype scope (Just (VInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VInts j (Just (maybe k (min k) i))) -subtype scope Nothing (VRecType ltys) = do - lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys - return (VRecType lctrs) -subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do - lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2 - return (VRecType lctrs) - where - union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1 - return [(l,True,ctr)] - union l o1 ctr1 ((l',o2,ctr2):lctrs) - | l == l' = do ctr <- subtype scope (Just ctr1) ctr2 - return ((l,o1||o2,ctr):lctrs) - | otherwise = do lctrs <- union l o1 ctr1 lctrs - return ((l',o2,ctr2):lctrs) -subtype scope (Just (VTable a1 r1)) (VTable a2 r2) = do - a <- supertype scope (Just a1) a2 - r <- subtype scope (Just r1) r2 - return (VTable a r) -subtype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) - | x == identW && y == identW = do - a <- supertype scope (Just a1) a2 - r <- subtype scope (Just r1) r2 - return (VProd Explicit identW a r) -subtype scope Nothing ty = return ty -subtype scope (Just ctr) ty = do - unify scope ctr ty - return ty - -supertype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VInts (Just i) Nothing) -supertype scope (Just (VInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VInts (Just (maybe k (max k) i)) j) -supertype scope Nothing (VRecType ltys) = do - lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys - return (VRecType lctrs) -supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do - lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1 - return (VRecType lctrs) - where - intersect l o1 ctr1 lctrs [] = return lctrs - intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2) - | l == l' = do ctr <- supertype scope (Just ctr1) ctr2 - return ((l,o1 && o2,ctr):lctrs) - | otherwise = do intersect l o1 ctr1 lctrs lctrs2 -supertype scope (Just (VTable a1 r1)) (VTable a2 r2) = do - a <- subtype scope (Just a1) a2 - r <- supertype scope (Just r1) r2 - return (VTable a r) -supertype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) - | x == identW && y == identW = do - a <- subtype scope (Just a1) a2 - r <- supertype scope (Just r1) r2 - return (VProd Explicit identW a r) -supertype scope Nothing ty = return ty -supertype scope (Just ctr) ty = do - unify scope ctr ty - return ty - ------------------------------------------------------------------------ --- Unification ------------------------------------------------------------------------ - -unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho) -unifyFun scope (VProd bt x arg res) = - return (bt,x,arg,res) -unifyFun scope (VFV c (VarFree vs)) = do - res <- mapM (unifyFun scope) vs - return - ( Explicit - , identW - , VFV c (VarFree [sigma | (_,_,sigma,rho) <- res]) - , VFV c (VarFree [rho | (_,_,sigma,rho) <- res]) - ) -unifyFun scope tau = do - let mk_val i = VMeta i [] - arg <- fmap mk_val $ newResiduation scope - res <- fmap mk_val $ newResiduation scope - let bt = Explicit - unify scope tau (VProd bt identW arg res) - return (bt,identW,arg,res) - -unifyTbl :: Scope -> Rho -> EvalM (Sigma, Rho) -unifyTbl scope (VTable arg res) = - return (arg,res) -unifyTbl scope tau = do - let mk_val i = VMeta i [] - arg <- fmap mk_val $ newResiduation scope - res <- fmap mk_val $ newResiduation scope - unify scope tau (VTable arg res) - return (arg,res) - -unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) -unify scope (VMeta i vs1) (VMeta j vs2) - | i == j = sequence_ (zipWith (unify scope) vs1 vs2) - | otherwise = do - mv <- getMeta i - case mv of - Bound _ v1 -> do - g <- globals - unify scope (apply g v1 vs1) (VMeta j vs2) - Residuation scope1 _ -> do - mv <- getMeta j - case mv of - Bound _ v2 -> do - g <- globals - unify scope (VMeta i vs1) (apply g v2 vs2) - Residuation scope2 _ - | m > n -> setMeta i (Bound scope1 (VMeta j vs2)) - | otherwise -> setMeta j (Bound scope2 (VMeta i vs2)) - where - m = length scope1 - n = length scope2 -unify scope (VMeta i vs) v = unifyVar scope i vs v -unify scope v (VMeta i vs) = unifyVar scope i vs v -unify scope (VGen i vs1) (VGen j vs2) - | i == j = sequence_ (zipWith (unify scope) vs1 vs2) -unify scope (VProd b x d cod) (VProd b' x' d' cod') - | b == b' = do - unify scope d d' - cod <- evalCodomain x (VGen (length scope) []) cod - cod' <- evalCodomain x' (VGen (length scope) []) cod' - unify scope cod cod' -unify scope (VTable p1 res1) (VTable p2 res2) = do - unify scope p2 p1 - unify scope res1 res2 -unify scope (VSort s1) (VSort s2) - | s1 == s2 = return () -unify scope (VInt i) (VInt j) - | i == j = return () -unify scope (VFlt x) (VFlt y) - | x == y = return () -unify scope (VStr s1) (VStr s2) - | s1 == s2 = return () -unify scope VEmpty VEmpty = return () -unify scope v1 v2 = do - t1 <- value2termM False (scopeVars scope) v1 - t2 <- value2termM False (scopeVars scope) v2 - evalError ("Cannot unify:" <+> ppTerm Terse 0 t1 $$ - " with:" <+> ppTerm Terse 0 t2) - - --- | Invariant: tv1 is a flexible type variable -unifyVar :: Scope -> MetaId -> [Value] -> Tau -> EvalM () -unifyVar scope metaid vs ty2 = do -- Check whether i is bound - mv <- getMeta metaid - case mv of - Bound _ ty1 -> do g <- globals - unify scope (apply g ty1 vs) ty2 - Residuation scope' _ -> do occursCheck scope' metaid scope ty2 - setMeta metaid (Bound scope' ty2) - -occursCheck scope' i0 scope v = - let m = length scope' - n = length scope - in check m n v - where - check m n (VApp c f vs) = mapM_ (check m n) vs - check m n (VMeta i vs) - | i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs) - ty2 <- value2termM False (scopeVars scope) v - evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ - nest 2 (ppTerm Unqualified 0 ty2)) - | otherwise = do - s <- getMeta i - case s of - Bound _ v -> do g <- globals - check m n (apply g v vs) - _ -> mapM_ (check m n) vs - check m n (VGen i vs) - | i > m = let (v,_) = reverse scope !! i - in evalError ("Variable" <+> pp v <+> "has escaped") - | otherwise = mapM_ (check m n) vs - check m n (VClosure env c (Abs bt x t)) = do - g <- globals - check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) - check m n (VProd bt x ty1 ty2) = do - check m n ty1 - case ty2 of - VClosure env c t -> do g <- globals - check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) - _ -> check m n ty2 - check m n (VRecType as) = - mapM_ (\(_,_,v) -> check m n v) as - check m n (VR as) = - mapM_ (\(lbl,v) -> check m n v) as - check m n (VP v l vs) = - check m n v >> mapM_ (check m n) vs - check m n (VExtR v1 v2) = - check m n v1 >> check m n v2 - check m n (VTable v1 v2) = - check m n v1 >> check m n v2 - check m n (VT ty env c cs) = - check m n ty -- Traverse cs as well - check m n (VV ty cs) = - check m n ty >> mapM_ (check m n) cs - check m n (VS v1 v2 vs) = - check m n v1 >> check m n v2 >> mapM_ (check m n) vs - check m n (VSort _) = return () - check m n (VInt _) = return () - check m n (VFlt _) = return () - check m n (VStr _) = return () - check m n VEmpty = return () - check m n (VC v1 v2) = - check m n v1 >> check m n v2 - check m n (VGlue v1 v2) = - check m n v1 >> check m n v2 - check m n (VPatt _ _ _) = return () - check m n (VPattType v) = - check m n v - check m n (VFV c vs) = - mapM_ (check m n) (unvariants vs) - check m n (VAlts v vs) = - check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs - check m n (VStrs vs) = - mapM_ (check m n) vs - check m n (VInts _ _) = return () - ------------------------------------------------------------------------ --- Instantiation and quantification ------------------------------------------------------------------------ - --- | Instantiate the topmost implicit arguments with metavariables -instantiate :: Scope -> Term -> Sigma -> EvalM (Term,Rho) -instantiate scope t (VProd Implicit x ty1 ty2) = do - i <- newResiduation scope - ty2 <- case ty2 of - VClosure env c ty2 -> do g <- globals - return (eval g ((x,VMeta i []):env) c ty2 []) - ty2 -> return ty2 - instantiate scope (App t (ImplArg (Meta i))) ty2 -instantiate scope t ty@(VMeta i args) = getMeta i >>= \case - Bound _ v -> instantiate scope t v - Residuation _ (Just v) -> instantiate scope t v - _ -> return (t,ty) -- We don't have enough information to try any instantiation -instantiate scope t ty = do - return (t,ty) - --- | Build fresh lambda abstractions for the topmost implicit arguments -skolemise :: Scope -> Sigma -> EvalM (Scope, Term->Term, Rho) -skolemise scope ty@(VMeta i vs) = do - mv <- getMeta i - case mv of - Residuation _ _ -> return (scope,id,ty) -- guarded constant? - Bound _ ty -> do g <- globals - skolemise scope (apply g ty vs) -skolemise scope (VProd Implicit x ty1 ty2) = do - let v = newVar scope - ty2 <- evalCodomain x (VGen (length scope) []) ty2 - (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 - return (scope,Abs Implicit v . f,ty2) -skolemise scope ty = do - return (scope,id,ty) - --- | Quantify over the specified type variables (all flexible) -quantify :: Scope -> Term -> [MetaId] -> Rho -> EvalM (Term,Sigma) -quantify scope t tvs ty = do - let m = length tvs - n = length scope - (used_bndrs,ty) <- check m n [] ty - let new_bndrs = take m (allBinders \\ used_bndrs) - mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs) - let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs - return (foldr (Abs Implicit) t new_bndrs,ty') - where - bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i [])) - - check m n xs (VApp c f vs) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VApp c f vs) - check m n xs (VMeta i vs) = do - s <- getMeta i - case s of - Bound _ v -> do g <- globals - check m n xs (apply g v vs) - _ -> do (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VMeta i vs) - check m n st (VGen i vs)= do - (st,vs) <- mapAccumM (check m n) st vs - return (st, VGen (m+i) vs) - check m n st (VClosure env c (Abs bt x t)) = do - (st,env) <- mapAccumM (\st (x,v) -> check m n st v >>= \(st,v) -> return (st,(x,v))) st env - return (st,VClosure env c (Abs bt x t)) - check m n xs (VProd bt x v1 v2) = do - (xs,v1) <- check m n xs v1 - case v2 of - VClosure env c t -> do (st,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env - return (x:xs,VProd bt x v1 (VClosure env c t)) - v2 -> do (xs,v2) <- check m (n+1) xs v2 - return (x:xs,VProd bt x v1 v2) - check m n xs (VRecType as) = do - (xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,v))) xs as - return (xs,VRecType as) - check m n xs (VR as) = do - (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as - return (xs,VR as) - check m n xs (VP v l vs) = do - (xs,v) <- check m n xs v - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VP v l vs) - check m n xs (VExtR v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VExtR v1 v2) - check m n xs (VTable v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VTable v1 v2) - check m n xs (VT ty env c cs) = do - (xs,ty) <- check m n xs ty - (xs,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env - return (xs,VT ty env c cs) - check m n xs (VV ty cs) = do - (xs,ty) <- check m n xs ty - (xs,cs) <- mapAccumM (check m n) xs cs - return (xs,VV ty cs) - check m n xs (VS v1 tnk vs) = do - (xs,v1) <- check m n xs v1 - (xs,tnk) <- check m n xs tnk - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VS v1 tnk vs) - check m n xs v@(VSort _) = return (xs,v) - check m n xs v@(VInt _) = return (xs,v) - check m n xs v@(VFlt _) = return (xs,v) - check m n xs v@(VStr _) = return (xs,v) - check m n xs v@VEmpty = return (xs,v) - check m n xs (VC v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VC v1 v2) - check m n xs (VGlue v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VGlue v1 v2) - check m n xs v@(VPatt _ _ _) = return (xs,v) - check m n xs (VPattType v) = do - (xs,v) <- check m n xs v - return (xs,VPattType v) - check m n xs (VFV c (VarFree vs)) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VFV c (VarFree vs)) - check m n xs (VFV c (VarOpts name os)) = do - (xs,os) <- mapAccumM (\acc (l,v) -> second (l,) <$> check m n acc v) xs os - return (xs,VFV c (VarOpts name os)) - check m n xs (VAlts v vs) = do - (xs,v) <- check m n xs v - (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,(v1,v2))) - xs vs - return (xs,VAlts v vs) - check m n xs (VStrs vs) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VStrs vs) - check m n xs v = unimplemented ("check "++show (ppValue Unqualified 5 v)) - - mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c]) - mapAccumM f s [] = return (s,[]) - mapAccumM f s (x:xs) = do - (s,y) <- f s x - (s,ys) <- mapAccumM f s xs - return (s,y:ys) - -allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... -allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ - [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] - ------------------------------------------------------------------------ --- Helpers ------------------------------------------------------------------------ - -type Sigma = Value -type Rho = Value -- No top-level ForAll -type Tau = Value -- No ForAlls anywhere - -unimplemented str = fail ("Unimplemented: "++str) - -newVar :: Scope -> Ident -newVar scope = head [x | i <- [1..], - let x = identS ('v':show i), - isFree scope x] - where - isFree [] x = True - isFree ((y,_):scope) x = x /= y && isFree scope x - -scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] -scopeVars scope = map fst scope -scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) - --- | This function takes account of zonking, and returns a set --- (no duplicates) of unbound meta-type variables -getMetaVars :: [(Scope,Sigma)] -> EvalM [MetaId] -getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys - where - -- Get the MetaIds from a term; no duplicates in result - go acc (VGen i args) = foldM go acc args - go acc (VSort s) = return acc - go acc (VInt _) = return acc - go acc (VRecType vs) = foldM (\acc (lbl,_,v) -> go acc v) acc vs - go acc (VClosure _ _ _) = return acc - go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1 - go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1 - go acc (VMeta m args) - | m `elem` acc = return acc - | otherwise = do res <- getMeta m - case res of - Bound _ v -> go acc v - Residuation _ Nothing -> foldM go (m:acc) args - Residuation _ (Just v) -> go acc v - _ -> return acc - go acc (VApp c f args) = foldM go acc args - go acc (VFV c vs) = foldM go acc (unvariants vs) - go acc (VInts _ _) = return acc - go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) - --- | Eliminate any substitutions in a term -zonkTerm :: [Ident] -> Term -> EvalM Term -zonkTerm xs (Abs b x t) = do - t <- zonkTerm (x:xs) t - return (Abs b x t) -zonkTerm xs (Prod b x t1 t2) = do - t1 <- zonkTerm xs t1 - t2 <- zonkTerm xs' t2 - return (Prod b x t1 t2) - where - xs' | x == identW = xs - | otherwise = x:xs -zonkTerm xs (Meta i) = do - st <- getMeta i - case st of - Bound _ v -> zonkTerm xs =<< value2termM False xs v - Residuation scope v -> case v of - Just v -> zonkTerm xs =<< value2termM False (map fst scope) v - Nothing -> return (Meta i) - Narrowing _ -> return (Meta i) -zonkTerm xs t = composOp (zonkTerm xs) t diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs index 80e60ef8e..895229d94 100644 --- a/src/compiler/api/GF/Interactive.hs +++ b/src/compiler/api/GF/Interactive.hs @@ -14,7 +14,8 @@ import GF.Command.Abstract import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.TypeCheck.Concrete(inferLType) -import GF.Compile.Compute.Concrete(normalForm,stdPredef,Globals(..)) +import qualified GF.Compile.Compute.Concrete as O(normalForm,stdPredef,Globals(..)) +import GF.Compile.Compute.Concrete2(stdPredef,Globals(..)) import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields) import GF.Data.Operations (Err(..)) import GF.Data.Utilities(whenM,repeatM) @@ -317,11 +318,12 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do compileLinTerm sgr mo f mb_t ty = do (t,ty) <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo (Typed t ty) - (t,ty) <- inferLType sgr [] t + let g = Gl sgr (stdPredef g) + (t,ty) <- inferLType g t return (t,ty) Nothing -> case lookupResDef sgr (mo,identS f) of Ok t -> do ty <- renameSourceTerm sgr mo ty - ty <- normalForm (Gl sgr stdPredef) ty + ty <- O.normalForm (O.Gl sgr O.stdPredef) ty return (t,ty) Bad msg -> fail msg let (ctxt,res_ty) = typeFormCnc ty @@ -344,7 +346,8 @@ transactionCommand (CreateLincat opts c mb_t) pgf mb_txnid = do compileLincatTerm sgr mo mb_t = do t <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo t - (t,_) <- inferLType sgr [] t + let g = Gl sgr (stdPredef g) + (t,_) <- inferLType g t return t Nothing -> case lookupResDef sgr (mo,identS c) of Ok t -> return t diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs index 410360ea8..0b2bd2626 100644 --- a/src/compiler/api/GF/Term.hs +++ b/src/compiler/api/GF/Term.hs @@ -9,4 +9,4 @@ module GF.Term (renameSourceTerm, import GF.Compile.Rename import GF.Compile.Compute.Concrete -import GF.Compile.TypeCheck.ConcreteNew +import GF.Compile.TypeCheck.Concrete diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index e0dc76ccb..56875c9bb 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -127,7 +127,6 @@ library GF.Compile.ToAPI GF.Compile.TypeCheck.Abstract GF.Compile.TypeCheck.Concrete - GF.Compile.TypeCheck.ConcreteNew GF.Compile.TypeCheck.TC GF.Compile.Update GF.Data.BacktrackM