msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Rename GF.Compile.TypeCheck.RConcrete to GF.Compile.TypeCheck.Concrete

Browse Source
This commit is contained in:
John J. Camilleri
2021-07-01 14:27:11 +02:00
parent 71d99b9ecb
commit 376b1234a2
5 changed files with 224 additions and 946 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
gf.cabal
View File

@@ -207,7 +207,6 @@ library
GF.Compile.TypeCheck.Concrete GF.Compile.TypeCheck.Concrete
GF.Compile.TypeCheck.ConcreteNew GF.Compile.TypeCheck.ConcreteNew
GF.Compile.TypeCheck.Primitives GF.Compile.TypeCheck.Primitives
GF.Compile.TypeCheck.RConcrete
GF.Compile.TypeCheck.TC GF.Compile.TypeCheck.TC
GF.Compile.Update GF.Compile.Update
GF.Data.BacktrackM GF.Data.BacktrackM

2
src/compiler/GF/Command/SourceCommands.hs
View File

@@ -19,7 +19,7 @@ import GF.Grammar.ShowTerm
import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Grammar.Lookup (allOpers,allOpersTo)
import GF.Compile.Rename(renameSourceTerm) import GF.Compile.Rename(renameSourceTerm)
import GF.Compile.Compute.Concrete(normalForm,resourceValues) import GF.Compile.Compute.Concrete(normalForm,resourceValues)
import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType) import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType)
import GF.Infra.Dependencies(depGraph) import GF.Infra.Dependencies(depGraph)
import GF.Infra.CheckM(runCheck) import GF.Infra.CheckM(runCheck)

2
src/compiler/GF/Compile/CheckGrammar.hs
View File

@@ -27,7 +27,7 @@ import GF.Infra.Ident
import GF.Infra.Option import GF.Infra.Option
import GF.Compile.TypeCheck.Abstract import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.RConcrete import GF.Compile.TypeCheck.Concrete
import qualified GF.Compile.TypeCheck.ConcreteNew as CN import qualified GF.Compile.TypeCheck.ConcreteNew as CN
import qualified GF.Compile.Compute.Concrete as CN import qualified GF.Compile.Compute.Concrete as CN

268
src/compiler/GF/Compile/TypeCheck/Concrete.hs
View File

@@ -1,6 +1,7 @@
{-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
{- import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Data.Operations import GF.Data.Operations
@@ -22,10 +23,16 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
| isPredefConstant ty -> return ty ---- shouldn't be needed | isPredefConstant ty -> return ty ---- shouldn't be needed
Q (m,ident) -> checkIn (text "module" <+> ppIdent m) $ do Q (m,ident) -> checkIn ("module" <+> m) $ do
ty' <- lookupResDef gr (m,ident) ty' <- lookupResDef gr (m,ident)
if ty' == ty then return ty else comp g ty' --- is this necessary to test? 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! Vr ident -> checkLookup ident g -- never needed to compute!
App f a -> do App f a -> do
@@ -73,26 +80,26 @@ inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident) Nothing -> checkError ("unknown in Predef:" <+> ident)
Q ident -> checks [ Q ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g termWith trm $ lookupResType gr ident >>= computeLType gr g
, ,
lookupResDef gr ident >>= inferLType gr g lookupResDef gr ident >>= inferLType gr g
, ,
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm) checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
] ]
QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident) Nothing -> checkError ("unknown in Predef:" <+> ident)
QC ident -> checks [ QC ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g termWith trm $ lookupResType gr ident >>= computeLType gr g
, ,
lookupResDef gr ident >>= inferLType gr g lookupResDef gr ident >>= inferLType gr g
, ,
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm) checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
] ]
Vr ident -> termWith trm $ checkLookup ident g Vr ident -> termWith trm $ checkLookup ident g
@@ -100,7 +107,12 @@ inferLType gr g trm = case trm of
Typed e t -> do Typed e t -> do
t' <- computeLType gr g t t' <- computeLType gr g t
checkLType gr g e t' checkLType gr g e t'
return (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 App f a -> do
over <- getOverload gr g Nothing trm over <- getOverload gr g Nothing trm
@@ -116,7 +128,11 @@ inferLType gr g trm = case trm of
then return val then return val
else substituteLType [(bt,z,a')] val else substituteLType [(bt,z,a')] val
return (App f' a',ty) return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty) _ ->
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 S f x -> do
(f', fty) <- inferLType gr g f (f', fty) <- inferLType gr g f
@@ -124,7 +140,7 @@ inferLType gr g trm = case trm of
Table arg val -> do Table arg val -> do
x'<- justCheck g x arg x'<- justCheck g x arg
return (S f' x', val) return (S f' x', val)
_ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm)) _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
P t i -> do P t i -> do
(t',ty) <- inferLType gr g t --- ?? (t',ty) <- inferLType gr g t --- ??
@@ -132,16 +148,16 @@ inferLType gr g trm = case trm of
let tr2 = P t' i let tr2 = P t' i
termWith tr2 $ case ty' of termWith tr2 $ case ty' of
RecType ts -> case lookup i ts of RecType ts -> case lookup i ts of
Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty')) Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
Just x -> return x Just x -> return x
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$ _ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty') " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
R r -> do R r -> do
let (ls,fs) = unzip r let (ls,fs) = unzip r
fsts <- mapM inferM fs fsts <- mapM inferM fs
let ts = [ty | (Just ty,_) <- fsts] let ts = [ty | (Just ty,_) <- fsts]
checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length 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)) return $ (R (zip ls fsts), RecType (zip ls ts))
T (TTyped arg) pts -> do T (TTyped arg) pts -> do
@@ -153,7 +169,7 @@ inferLType gr g trm = case trm of
T ti pts -> do -- tries to guess: good in oper type inference T ti pts -> do -- tries to guess: good in oper type inference
let pts' = [pt | pt@(p,_) <- pts, isConstPatt p] let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
case pts' of case pts' of
[] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm) [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] ---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do _ -> do
(arg,val) <- checks $ map (inferCase Nothing) pts' (arg,val) <- checks $ map (inferCase Nothing) pts'
@@ -187,7 +203,7 @@ inferLType gr g trm = case trm of
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
Strs (Cn c : ts) | c == cConflict -> do Strs (Cn c : ts) | c == cConflict -> do
checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts)) checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
inferLType gr g (head ts) inferLType gr g (head ts)
Strs ts -> do Strs ts -> do
@@ -208,19 +224,25 @@ inferLType gr g trm = case trm of
return (RecType (zip ls ts'), typeType) return (RecType (zip ls ts'), typeType)
ExtR r s -> do ExtR r s -> do
(r',rT) <- inferLType gr g r
--- over <- getOverload gr g Nothing r
--- let r1 = maybe r fst over
let r1 = r ---
(r',rT) <- inferLType gr g r1
rT' <- computeLType gr g rT rT' <- computeLType gr g rT
(s',sT) <- inferLType gr g s (s',sT) <- inferLType gr g s
sT' <- computeLType gr g sT sT' <- computeLType gr g sT
let trm' = ExtR r' s' let trm' = ExtR r' s'
---- trm' <- plusRecord r' s'
case (rT', sT') of case (rT', sT') of
(RecType rs, RecType ss) -> do (RecType rs, RecType ss) -> do
rt <- plusRecType rT' sT' 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) checkLType gr g trm' rt ---- return (trm', rt)
_ | rT' == typeType && sT' == typeType -> return (trm', typeType) _ | rT' == typeType && sT' == typeType -> do
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm) return (trm', typeType)
_ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
Sort _ -> Sort _ ->
termWith trm $ return typeType termWith trm $ return typeType
@@ -252,7 +274,7 @@ inferLType gr g trm = case trm of
ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009 ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
return $ (ELin c trm', ty') return $ (ELin c trm', ty')
_ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm) _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
where where
isPredef m = elem m [cPredef,cPredefAbs] isPredef m = elem m [cPredef,cPredefAbs]
@@ -299,7 +321,6 @@ inferLType gr g trm = case trm of
PChars _ -> return $ typeStr PChars _ -> return $ typeStr
_ -> inferLType gr g (patt2term p) >>= return . snd _ -> inferLType gr g (patt2term p) >>= return . snd
-- type inference: Nothing, type checking: Just t -- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type -- the latter permits matching with value type
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type)) getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
@@ -310,8 +331,21 @@ getOverload gr g mt ot = case appForm ot of
v <- matchOverload f typs ttys v <- matchOverload f typs ttys
return $ Just v return $ Just v
_ -> return Nothing _ -> 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 _ -> return Nothing
where 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 matchOverload f typs ttys = do
let (tts,tys) = unzip ttys let (tts,tys) = unzip ttys
let vfs = lookupOverloadInstance tys typs let vfs = lookupOverloadInstance tys typs
@@ -329,25 +363,26 @@ getOverload gr g mt ot = case appForm ot of
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
([(_,val,fun)],_) -> return (mkApp fun tts, val) ([(_,val,fun)],_) -> return (mkApp fun tts, val)
([],[(pre,val,fun)]) -> do ([],[(pre,val,fun)]) -> do
checkWarn $ text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$ checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
text "for" $$ "for" $$
nest 2 (showTypes tys) $$ nest 2 (showTypes tys) $$
text "using" $$ "using" $$
nest 2 (showTypes pre) nest 2 (showTypes pre)
return (mkApp fun tts, val) return (mkApp fun tts, val)
([],[]) -> do ([],[]) -> do
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$ checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
text "for" $$ maybe empty (\x -> "with value type" <+> ppType x) mt $$
"for argument list" $$
nest 2 stysError $$ nest 2 stysError $$
text "among" $$ "among alternatives" $$
nest 2 (vcat stypsError) $$ nest 2 (vcat stypsError)
maybe empty (\x -> text "with value type" <+> ppType x) mt
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
([(val,fun)],_) -> do ([(val,fun)],_) -> do
return (mkApp fun tts, val) return (mkApp fun tts, val)
([],[(val,fun)]) -> do ([],[(val,fun)]) -> do
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
return (mkApp fun tts, val) return (mkApp fun tts, val)
----- unsafely exclude irritating warning AR 24/5/2008 ----- unsafely exclude irritating warning AR 24/5/2008
@@ -355,16 +390,22 @@ getOverload gr g mt ot = case appForm ot of
----- "resolved by excluding partial applications:" ++++ ----- "resolved by excluding partial applications:" ++++
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)] ----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
--- now forgiving ambiguity with a warning AR 1/2/2014
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+> -- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
text "for" <+> hsep (map ppType tys) $$ -- But it also gives a chance to ambiguous overloadings that were banned before.
text "with alternatives" $$ (nps1,nps2) -> do
nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2]) 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)] matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
unlocked v = case v of unlocked v = case v of
RecType fs -> RecType $ filter (not . isLockLabel . fst) fs RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
_ -> v _ -> v
---- TODO: accept subtypes ---- TODO: accept subtypes
---- TODO: use a trie ---- TODO: use a trie
@@ -385,7 +426,6 @@ getOverload gr g mt ot = case appForm ot of
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type) checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType gr g trm typ0 = do checkLType gr g trm typ0 = do
typ <- computeLType gr g typ0 typ <- computeLType gr g typ0
case trm of case trm of
@@ -395,10 +435,12 @@ checkLType gr g trm typ0 = do
Prod bt' z a b -> do Prod bt' z a b -> do
(c',b') <- if isWildIdent z (c',b') <- if isWildIdent z
then checkLType gr ((bt,x,a):g) c b then checkLType gr ((bt,x,a):g) c b
else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
checkLType gr ((bt,x,a):g) c b' checkLType gr ((bt,x,a):g) c b'
return $ (Abs bt x c', Prod bt' x a b') return $ (Abs bt x c', Prod bt' z a b')
_ -> checkError $ text "function type expected instead of" <+> ppType typ _ -> 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 App f a -> do
over <- getOverload gr g (Just typ) trm over <- getOverload gr g (Just typ) trm
@@ -408,6 +450,12 @@ checkLType gr g trm typ0 = do
(trm',ty') <- inferLType gr g trm (trm',ty') <- inferLType gr g trm
termWith trm' $ checkEqLType gr g typ ty' 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 Q _ -> do
over <- getOverload gr g (Just typ) trm over <- getOverload gr g (Just typ) trm
case over of case over of
@@ -417,7 +465,7 @@ checkLType gr g trm typ0 = do
termWith trm' $ checkEqLType gr g typ ty' trm' termWith trm' $ checkEqLType gr g typ ty' trm'
T _ [] -> T _ [] ->
checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ) checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of T _ cs -> case typ of
Table arg val -> do Table arg val -> do
case allParamValues gr arg of case allParamValues gr arg of
@@ -426,12 +474,12 @@ checkLType gr g trm typ0 = do
ps <- testOvershadow ps0 vs ps <- testOvershadow ps0 vs
if null ps if null ps
then return () then return ()
else checkWarn (text "patterns never reached:" $$ else checkWarn ("patterns never reached:" $$
nest 2 (vcat (map (ppPatt Unqualified 0) ps))) nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
_ -> return () -- happens with variable types _ -> return () -- happens with variable types
cs' <- mapM (checkCase arg val) cs cs' <- mapM (checkCase arg val) cs
return (T (TTyped arg) cs', typ) return (T (TTyped arg) cs', typ)
_ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ) _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
V arg0 vs -> V arg0 vs ->
case typ of case typ of
Table arg1 val -> Table arg1 val ->
@@ -439,51 +487,54 @@ checkLType gr g trm typ0 = do
vs1 <- allParamValues gr arg1 vs1 <- allParamValues gr arg1
if length vs1 == length vs if length vs1 == length vs
then return () then return ()
else checkError $ text "wrong number of values in table" <+> ppTerm Unqualified 0 trm else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs] vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
return (V arg' vs',typ) return (V arg' vs',typ)
R r -> case typ of --- why needed? because inference may be too difficult R r -> case typ of --- why needed? because inference may be too difficult
RecType rr -> do RecType rr -> do
let (ls,_) = unzip rr -- labels of expected type --let (ls,_) = unzip rr -- labels of expected type
fsts <- mapM (checkM r) rr -- check that they are found in the record fsts <- mapM (checkM r) rr -- check that they are found in the record
return $ (R fsts, typ) -- normalize record return $ (R fsts, typ) -- normalize record
_ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ)) _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
ExtR r s -> case typ of ExtR r s -> case typ of
_ | typ == typeType -> do _ | typ == typeType -> do
trm' <- computeLType gr g trm trm' <- computeLType gr g trm
case trm' of case trm' of
RecType _ -> termWith trm $ return typeType RecType _ -> termWith trm' $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
-- ext t = t ** ... -- ext t = t ** ...
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm)) _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
RecType rr -> do RecType rr -> do
(r',ty,s') <- checks [
do (r',ty) <- inferLType gr g r
return (r',ty,s)
,
do (s',ty) <- inferLType gr g s
return (s',ty,r)
]
case ty of ll2 <- case s of
RecType rr1 -> do R ss -> return $ map fst ss
let (rr0,rr2) = recParts rr rr1 _ -> do
r2 <- justCheck g r' rr0 (s',typ2) <- inferLType gr g s
s2 <- justCheck g s' rr2 case typ2 of
return $ (ExtR r2 s2, typ) RecType ss -> return $ map fst ss
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$ _ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
text "but found" <+> ppTerm Unqualified 0 ty) let ll1 = [l | (l,_) <- rr, notElem l ll2]
--- over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
--- let r1 = maybe r fst over
let r1 = r ---
(r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
(s',_) <- checkLType gr g s (RecType [field | field@(l,_) <- rr, elem l ll2])
let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
return (rec, typ)
ExtR ty ex -> do ExtR ty ex -> do
r' <- justCheck g r ty r' <- justCheck g r ty
s' <- justCheck g s ex s' <- justCheck g s ex
return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ) _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
FV vs -> do FV vs -> do
ttys <- mapM (flip (checkLType gr g) typ) vs ttys <- mapM (flip (checkLType gr g) typ) vs
@@ -498,7 +549,7 @@ checkLType gr g trm typ0 = do
(arg',val) <- checkLType gr g arg p (arg',val) <- checkLType gr g arg p
checkEqLType gr g typ t trm checkEqLType gr g typ t trm
return (S tab' arg', t) return (S tab' arg', t)
_ -> checkError (text "table type expected for applied table instead of" <+> ppType ty') _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
, do , do
(arg',ty) <- inferLType gr g arg (arg',ty) <- inferLType gr g arg
ty' <- computeLType gr g ty ty' <- computeLType gr g ty
@@ -507,7 +558,8 @@ checkLType gr g trm typ0 = do
] ]
Let (x,(mty,def)) body -> case mty of Let (x,(mty,def)) body -> case mty of
Just ty -> do Just ty -> do
(def',ty') <- checkLType gr g def ty (ty0,_) <- checkLType gr g ty typeType
(def',ty') <- checkLType gr g def ty0
body' <- justCheck ((Explicit,x,ty'):g) body typ body' <- justCheck ((Explicit,x,ty'):g) body typ
return (Let (x,(Just ty',def')) body', typ) return (Let (x,(Just ty',def')) body', typ)
_ -> do _ -> do
@@ -523,10 +575,10 @@ checkLType gr g trm typ0 = do
termWith trm' $ checkEqLType gr g typ ty' trm' termWith trm' $ checkEqLType gr g typ ty' trm'
where where
justCheck g ty te = checkLType gr g ty te >>= return . fst justCheck g ty te = checkLType gr g ty te >>= return . fst
{-
recParts rr t = (RecType rr1,RecType rr2) where recParts rr t = (RecType rr1,RecType rr2) where
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr (rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-}
checkM rms (l,ty) = case lookup l rms of checkM rms (l,ty) = case lookup l rms of
Just (Just ty0,t) -> do Just (Just ty0,t) -> do
checkEqLType gr g ty ty0 t checkEqLType gr g ty ty0 t
@@ -538,9 +590,9 @@ checkLType gr g trm typ0 = do
_ -> checkError $ _ -> checkError $
if isLockLabel l if isLockLabel l
then let cat = drop 5 (showIdent (label2ident l)) then let cat = drop 5 (showIdent (label2ident l))
in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
text "; try wrapping it with lin" <+> text cat "; try wrapping it with lin" <+> cat
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms) else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
checkCase arg val (p,t) = do checkCase arg val (p,t) = do
cont <- pattContext gr g arg p cont <- pattContext gr g arg p
@@ -553,7 +605,7 @@ pattContext env g typ p = case p of
PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- lookupResType env (q,c) t <- lookupResType env (q,c)
let (cont,v) = typeFormCnc t let (cont,v) = typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps) (length cont == length ps)
checkEqLType env g typ v (patt2term p) checkEqLType env g typ v (patt2term p)
mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
@@ -564,7 +616,7 @@ pattContext env g typ p = case p of
let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]] let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
----- checkWarn $ prt p ++++ show pts ----- debug ----- checkWarn $ prt p ++++ show pts ----- debug
mapM (uncurry (pattContext env g)) pts >>= return . concat mapM (uncurry (pattContext env g)) pts >>= return . concat
_ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ') _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
PT t p' -> do PT t p' -> do
checkEqLType env g typ t (patt2term p') checkEqLType env g typ t (patt2term p')
pattContext env g typ p' pattContext env g typ p'
@@ -578,9 +630,9 @@ pattContext env g typ p = case p of
g2 <- pattContext env g typ q g2 <- pattContext env g typ q
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1]) let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond checkCond
(text "incompatible bindings of" <+> ("incompatible bindings of" <+>
fsep (map ppIdent pts) <+> fsep pts <+>
text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
return g1 -- must be g1 == g2 return g1 -- must be g1 == g2
PSeq p q -> do PSeq p q -> do
g1 <- pattContext env g typ p g1 <- pattContext env g typ p
@@ -594,7 +646,7 @@ pattContext env g typ p = case p of
noBind typ p' = do noBind typ p' = do
co <- pattContext env g typ p' co <- pattContext env g typ p'
if not (null co) if not (null co)
then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
>> return [] >> return []
else return [] else return []
@@ -603,9 +655,31 @@ checkEqLType gr g t u trm = do
(b,t',u',s) <- checkIfEqLType gr g t u trm (b,t',u',s) <- checkIfEqLType gr g t u trm
case b of case b of
True -> return t' True -> return t'
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$ False ->
text "expected:" <+> ppType t $$ let inferredType = ppTerm Qualified 0 u
text "inferred:" <+> ppType 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
where
-- count the number of arrows in the prettyprinted term
arrows :: Doc -> Int
arrows = length . filter (=="->") . words . render
-- 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
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String) checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType gr g t u trm = do checkIfEqLType gr g t u trm = do
@@ -617,13 +691,13 @@ checkIfEqLType gr g t u trm = do
--- better: use a flag to forgive? (AR 31/1/2006) --- better: use a flag to forgive? (AR 31/1/2006)
_ -> case missingLock [] t' u' of _ -> case missingLock [] t' u' of
Ok lo -> do Ok lo -> do
checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo) checkWarn $ "missing lock field" <+> fsep lo
return (True,t',u',[]) return (True,t',u',[])
Bad s -> return (False,t',u',s) Bad s -> return (False,t',u',s)
where where
-- t is a subtype of u -- check that u is a subtype of t
--- quick hack version of TC.eqVal --- quick hack version of TC.eqVal
alpha g t u = case (t,u) of alpha g t u = case (t,u) of
@@ -635,12 +709,13 @@ checkIfEqLType gr g t u trm = do
-- record subtyping -- record subtyping
(RecType rs, RecType ts) -> all (\ (l,a) -> (RecType rs, RecType ts) -> all (\ (l,a) ->
any (\ (k,b) -> alpha g a b && l == k) ts) rs 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, ExtR r' s') -> alpha g r r' && alpha g s s'
(ExtR r s, t) -> alpha g r t || alpha g s t (ExtR r s, t) -> alpha g r t || alpha g s t
-- the following say that Ints n is a subset of Int and of Ints m >= n -- the following say that Ints n is a subset of Int and of Ints m >= n
(t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> 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! | Just _ <- isTypeInts t, u == typeInt -> True ---- check size!
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005 | t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
@@ -655,7 +730,8 @@ checkIfEqLType gr g t u trm = do
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) (Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m) || elem n (allExtendsPlus gr m)
(Table a b, Table c d) -> alpha g a c && alpha g b d -- 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 (Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
_ -> t == u _ -> t == u
--- the following should be one-way coercions only. AR 4/1/2001 --- the following should be one-way coercions only. AR 4/1/2001
@@ -670,7 +746,7 @@ checkIfEqLType gr g t u trm = do
not (any (\ (k,b) -> alpha g a b && l == k) ts)] not (any (\ (k,b) -> alpha g a b && l == k) ts)]
(locks,others) = partition isLockLabel ls (locks,others) = partition isLockLabel ls
in case others of in case others of
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others))) _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
_ -> return locks _ -> return locks
-- contravariance -- contravariance
(Prod _ x a b, Prod _ y c d) -> do (Prod _ x a b, Prod _ y c d) -> do
@@ -708,14 +784,18 @@ ppType :: Type -> Doc
ppType ty = ppType ty =
case ty of case ty of
RecType fs -> case filter isLockLabel $ map fst fs of RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock))) [lock] -> pp (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty _ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType a <+> text "->" <+> ppType b Prod _ x a b -> ppType a <+> "->" <+> ppType b
_ -> ppTerm Unqualified 0 ty _ -> ppTerm Unqualified 0 ty
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
(pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
(pt,_) -> pt
-}
checkLookup :: Ident -> Context -> Check Type checkLookup :: Ident -> Context -> Check Type
checkLookup x g = checkLookup x g =
case [ty | (b,y,ty) <- g, x == y] of case [ty | (b,y,ty) <- g, x == y] of
[] -> checkError (text "unknown variable" <+> ppIdent x) [] -> checkError ("unknown variable" <+> x)
(ty:_) -> return ty (ty:_) -> return ty
-}

801
src/compiler/GF/Compile/TypeCheck/RConcrete.hs
View File

@@ -1,801 +0,0 @@
{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.RConcrete( checkLType, inferLType, computeLType, ppType ) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Infra.CheckM
import GF.Data.Operations
import GF.Grammar
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.TypeCheck.Primitives
import Data.List
import Control.Monad
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
_ | isPredefConstant ty -> return ty
_ -> composOp (comp g) ty
-- the underlying algorithms
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
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 (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
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 isWildIdent z
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 -> do
if elem ' ' s
then do
let ss = foldr C Empty (map K (words s))
----- removed irritating warning AR 24/5/2008
----- checkWarn ("token \"" ++ s ++
----- "\" converted to token list" ++ prt ss)
return (ss, typeStr)
else 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]
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
--- over <- getOverload gr g Nothing r
--- let r1 = maybe r fst over
let r1 = r ---
(r',rT) <- inferLType gr g r1
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
return (trm, 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
(_,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
-- 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 isWildIdent z
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
ll2 <- case s of
R ss -> return $ map fst ss
_ -> do
(s',typ2) <- inferLType gr g s
case typ2 of
RecType ss -> return $ map fst ss
_ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
let ll1 = [l | (l,_) <- rr, notElem l ll2]
--- over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
--- let r1 = maybe r fst over
let r1 = r ---
(r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
(s',_) <- checkLType gr g s (RecType [field | field@(l,_) <- rr, elem l ll2])
let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
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
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
where
-- count the number of arrows in the prettyprinted term
arrows :: Doc -> Int
arrows = length . filter (=="->") . words . render
-- 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
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)
where
-- check that u is a subtype of t
--- quick hack version of TC.eqVal
alpha g t u = case (t,u) of
-- error (the empty type!) is subtype of any other type
(_,u) | u == typeError -> True
-- contravariance
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-- 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
-- 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
---- 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)
-- 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)
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
_ -> Bad ""
sTypes = [typeStr, typeTok, typeString]
-- auxiliaries
-- | 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
termWith :: Term -> Check Type -> Check (Term, Type)
termWith t ct = do
ty <- ct
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)
-- 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
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
(pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
(pt,_) -> pt
-}
checkLookup :: Ident -> Context -> Check Type
checkLookup x g =
case [ty | (b,y,ty) <- g, x == y] of
[] -> checkError ("unknown variable" <+> x)
(ty:_) -> return ty