From c58649bd2972dc088962e87db8ced25e0773dea7 Mon Sep 17 00:00:00 2001 From: hallgren Date: Fri, 4 Apr 2014 13:51:07 +0000 Subject: [PATCH] Removed imports of TypeCheck.Concrete, fixed problems in TypeCheck.RConcrete + The current type checker for concrete syntax is in GF.Compile.TypeCheck.RConcrete, but GF.Compile.TypeCheck.Concrete was still imported in GFI. + Fixed a bug that allowed Ints n as a subtype of Ints m, regardless of m and n. It now requires n<=m. Note: the type checker still allows Int as a subtype of Ints m, regardless of m. + Fixed a potential efficiency problem with large record types, by reducing the number of recursive calls from |R|*|S| to |R| when checking if R<=S. + Fixed a misleading comment: "alpha g t u" checks that u is a subtype of t, the other way around. Similarly, "checkIfEqLType gr g t u trm" checks that u is a subtype of t, not the other way around, and not that t is equal to u. --- src/compiler/GF/Compile/TypeCheck/Concrete.hs | 5 +++-- src/compiler/GF/Compile/TypeCheck/RConcrete.hs | 7 ++++--- src/compiler/GFI.hs | 4 ++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/compiler/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/GF/Compile/TypeCheck/Concrete.hs index 61600da28..7b24ab65a 100644 --- a/src/compiler/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/GF/Compile/TypeCheck/Concrete.hs @@ -1,6 +1,6 @@ {-# LANGUAGE PatternGuards #-} -module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where - +module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where +{- import GF.Infra.CheckM import GF.Data.Operations @@ -714,3 +714,4 @@ checkLookup x g = case [ty | (b,y,ty) <- g, x == y] of [] -> checkError (text "unknown variable" <+> ppIdent x) (ty:_) -> return ty +-} \ No newline at end of file diff --git a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs b/src/compiler/GF/Compile/TypeCheck/RConcrete.hs index bcdd9fdac..4bbd42271 100644 --- a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs +++ b/src/compiler/GF/Compile/TypeCheck/RConcrete.hs @@ -650,7 +650,7 @@ checkIfEqLType gr g t u trm = do where - -- t is a subtype of u + -- check that u is a subtype of t --- quick hack version of TC.eqVal alpha g t u = case (t,u) of @@ -662,12 +662,13 @@ checkIfEqLType gr g t u trm = do -- record subtyping (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, 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 - (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! | t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005 diff --git a/src/compiler/GFI.hs b/src/compiler/GFI.hs index ead5a3ff7..eb1afd22a 100644 --- a/src/compiler/GFI.hs +++ b/src/compiler/GFI.hs @@ -17,7 +17,7 @@ import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) --import GF.Compile.Compute.Concrete (computeConcrete,checkPredefError) import qualified GF.Compile.Compute.ConcreteNew as CN(normalForm,resourceValues) -import GF.Compile.TypeCheck.Concrete (inferLType,ppType) +import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType) import GF.Infra.Dependencies(depGraph) import GF.Infra.CheckM import GF.Infra.UseIO(ioErrorText) @@ -226,7 +226,7 @@ execute1 opts gfenv0 s0 = let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops] let printer = if isRaw then showTerm sgr TermPrintDefault Qualified - else (render . GF.Compile.TypeCheck.Concrete.ppType) + else (render . TC.ppType) let printed = [unwords [showIdent op, ":", printer ty] | (op,ty) <- sigs] mapM_ putStrLn [l | l <- printed, all (flip isInfixOf l) greps] continue gfenv