GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #119 from GrammaticalFramework/concrete-new

Browse Source 
Clean up Compute.ConcreteNew and TypeCheck.RConcrete
This commit is contained in:
Inari Listenmaa
2021-07-06 14:05:00 +02:00
committed by GitHub
parent 1b66bf2773 d2fb755fab
commit 5e052ff499
12 changed files with 877 additions and 1602 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
gf.cabal
View File

@@ -178,7 +178,7 @@ library
GF.Command.TreeOperations
GF.Compile.CFGtoPGF
GF.Compile.CheckGrammar
GF.Compile.Compute.ConcreteNew
GF.Compile.Compute.Concrete
GF.Compile.Compute.Predef
GF.Compile.Compute.Value
GF.Compile.ExampleBased
@@ -207,7 +207,6 @@ library
GF.Compile.TypeCheck.Concrete
GF.Compile.TypeCheck.ConcreteNew
GF.Compile.TypeCheck.Primitives
GF.Compile.TypeCheck.RConcrete
GF.Compile.TypeCheck.TC
GF.Compile.Update
GF.Data.BacktrackM

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

@@ -18,8 +18,8 @@ import GF.Grammar.Parser (runP, pExp)
import GF.Grammar.ShowTerm
import GF.Grammar.Lookup (allOpers,allOpersTo)
import GF.Compile.Rename(renameSourceTerm)
import qualified GF.Compile.Compute.ConcreteNew as CN(normalForm,resourceValues)
import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType)
import GF.Compile.Compute.Concrete(normalForm,resourceValues)
import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType)
import GF.Infra.Dependencies(depGraph)
import GF.Infra.CheckM(runCheck)
@@ -259,7 +259,7 @@ checkComputeTerm os sgr t =
((t,_),_) <- runCheck $ do t <- renameSourceTerm sgr mo t
inferLType sgr [] t
let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
t1 = CN.normalForm (CN.resourceValues opts sgr) (L NoLoc identW) t
t1 = normalForm (resourceValues opts sgr) (L NoLoc identW) t
t2 = evalStr t1
checkPredefError t2
where

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

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.31 $
--
@@ -27,9 +27,9 @@ import GF.Infra.Ident
import GF.Infra.Option
import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.RConcrete
import qualified GF.Compile.TypeCheck.ConcreteNew as CN
import qualified GF.Compile.Compute.ConcreteNew as CN
import GF.Compile.TypeCheck.Concrete(computeLType,checkLType,inferLType,ppType)
import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)
import GF.Grammar
import GF.Grammar.Lexer
@@ -74,9 +74,9 @@ checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty
let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
let incld c = Set.member c (Set.fromList incl)
let illegal c = Set.member c (Set.fromList excl)
let illegals = [(f,is) |
let illegals = [(f,is) |
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
case illegals of
case illegals of
[] -> return ()
cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
@@ -92,12 +92,12 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
-- check that all abstract constants are in concrete; build default lin and lincats
jsc <- foldM checkAbs jsc (Map.toList jsa)
return (cm,cnc{jments=jsc})
where
checkAbs js i@(c,info) =
case info of
AbsFun (Just (L loc ty)) _ _ _
AbsFun (Just (L loc ty)) _ _ _
-> do let mb_def = do
let (cxt,(_,i),_) = typeForm ty
info <- lookupIdent i js
@@ -136,11 +136,11 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
_ -> return js
checkCnc js (c,info) =
case info of
CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
do (cont,val) <- linTypeOfType gr cm ty
let linty = (snd (valCat ty),cont,val)
return $ Map.insert c (CncFun (Just linty) d mn mf) js
@@ -159,14 +159,14 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
_ -> return $ Map.insert c info js
-- | General Principle: only Just-values are checked.
-- | General Principle: only Just-values are checked.
-- A May-value has always been checked in its origin module.
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
checkReservedId c
case info of
AbsCat (Just (L loc cont)) ->
mkCheck loc "the category" $
AbsCat (Just (L loc cont)) ->
mkCheck loc "the category" $
checkContext gr cont
AbsFun (Just (L loc typ0)) ma md moper -> do
@@ -181,7 +181,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
CncCat mty mdef mref mpr mpmcfg -> do
mty <- case mty of
Just (L loc typ) -> chIn loc "linearization type of" $
Just (L loc typ) -> chIn loc "linearization type of" $
(if False --flag optNewComp opts
then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
typ <- computeLType gr [] typ
@@ -191,19 +191,19 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
return (Just (L loc typ)))
Nothing -> return Nothing
mdef <- case (mty,mdef) of
(Just (L _ typ),Just (L loc def)) ->
(Just (L _ typ),Just (L loc def)) ->
chIn loc "default linearization of" $ do
(def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
return (Just (L loc def))
_ -> return Nothing
mref <- case (mty,mref) of
(Just (L _ typ),Just (L loc ref)) ->
(Just (L _ typ),Just (L loc ref)) ->
chIn loc "reference linearization of" $ do
(ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
return (Just (L loc ref))
_ -> return Nothing
mpr <- case mpr of
(Just (L loc t)) ->
(Just (L loc t)) ->
chIn loc "print name of" $ do
(t,_) <- checkLType gr [] t typeStr
return (Just (L loc t))
@@ -212,13 +212,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
CncFun mty mt mpr mpmcfg -> do
mt <- case (mty,mt) of
(Just (cat,cont,val),Just (L loc trm)) ->
(Just (cat,cont,val),Just (L loc trm)) ->
chIn loc "linearization of" $ do
(trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
return (Just (L loc trm))
_ -> return mt
mpr <- case mpr of
(Just (L loc t)) ->
(Just (L loc t)) ->
chIn loc "print name of" $ do
(t,_) <- checkLType gr [] t typeStr
return (Just (L loc t))
@@ -251,16 +251,16 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
ResOverload os tysts -> chIn NoLoc "overloading" $ do
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
tysts0 <- lookupOverload gr (m,c) -- check against inherited ones too
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
--- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given
checkUniq $
checkUniq $
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (L loc pcs)) _ -> do
ts <- chIn loc "parameter type" $
ts <- chIn loc "parameter type" $
liftM concat $ mapM mkPar pcs
return (ResParam (Just (L loc pcs)) (Just ts))
@@ -274,9 +274,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
return $ map (mkApp (QC (m,f))) vs
checkUniq xss = case xss of
x:y:xs
x:y:xs
| x == y -> checkError $ "ambiguous for type" <+>
ppType (mkFunType (tail x) (head x))
ppType (mkFunType (tail x) (head x))
| otherwise -> checkUniq $ y:xs
_ -> return ()
@@ -294,7 +294,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
t' <- compAbsTyp ((x,Vr x):g) t
return $ Prod b x a' t'
Abs _ _ _ -> return t
_ -> composOp (compAbsTyp g) t
_ -> composOp (compAbsTyp g) t
-- | for grammars obtained otherwise than by parsing ---- update!!

591
src/compiler/GF/Compile/Compute/Concrete.hs
View File

@@ -1,3 +1,588 @@
module GF.Compile.Compute.Concrete{-(module M)-} where
--import GF.Compile.Compute.ConcreteLazy as M -- New
--import GF.Compile.Compute.ConcreteStrict as M -- Old, inefficient
-- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation.
module GF.Compile.Compute.Concrete
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
normalForm,
Value(..), Bind(..), Env, value2term, eval, vapply
) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
import GF.Compile.Compute.Value hiding (Error)
import GF.Compile.Compute.Predef(predef,predefName,delta)
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
import GF.Data.Utilities(mapFst,mapSnd)
import GF.Infra.Option
import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
--import Data.Char (isUpper,toUpper,toLower)
import GF.Text.Pretty
import qualified Data.Map as Map
import Debug.Trace(trace)
-- * Main entry points
normalForm :: GlobalEnv -> L Ident -> Term -> Term
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
nfx env@(GE _ _ _ loc) t = do
v <- eval env [] t
case value2term loc [] v of
Left i -> fail ("variable #"++show i++" is out of scope")
Right t -> return t
eval :: GlobalEnv -> Env -> Term -> Err Value
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
where
cenv = CE gr rvs opts loc (map fst env)
--apply env = apply' env
--------------------------------------------------------------------------------
-- * Environments
type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
data GlobalEnv = GE Grammar ResourceValues Options GLocation
data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
opts::Options,
gloc::GLocation,local::LocalScope}
type GLocation = L Ident
type LocalScope = [Ident]
type Stack = [Value]
type OpenValue = Stack->Value
geLoc (GE _ _ _ loc) = loc
geGrammar (GE gr _ _ _) = gr
ext b env = env{local=b:local env}
extend bs env = env{local=bs++local env}
global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
var :: CompleteEnv -> Ident -> Err OpenValue
var env x = maybe unbound pick' (elemIndex x (local env))
where
unbound = fail ("Unknown variable: "++showIdent x)
pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
err i vs = bug $ "Stack problem: "++showIdent x++": "
++unwords (map showIdent (local env))
++" => "++show (i,length vs)
ok v = --trace ("var "++show x++" = "++show v) $
v
pick :: Int -> Stack -> Maybe Value
pick 0 (v:_) = Just v
pick i (_:vs) = pick (i-1) vs
pick i vs = Nothing -- bug $ "pick "++show (i,vs)
resource env (m,c) =
-- err bug id $
if isPredefCat c
then value0 env =<< lockRecType c defLinType -- hmm
else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
where e = fail $ "Not found: "++render m++"."++showIdent c
-- | Convert operators once, not every time they are looked up
resourceValues :: Options -> SourceGrammar -> GlobalEnv
resourceValues opts gr = env
where
env = GE gr rvs opts (L NoLoc identW)
rvs = Map.mapWithKey moduleResources (moduleMap gr)
moduleResources m = Map.mapWithKey (moduleResource m) . jments
moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
let loc = L l c
qloc = L l (Q (m,c))
eval (GE gr rvs opts loc) [] (traceRes qloc t)
traceRes = if flag optTrace opts
then traceResource
else const id
-- * Tracing
-- | Insert a call to the trace function under the top-level lambdas
traceResource (L l q) t =
case termFormCnc t of
(abs,body) -> mkAbs abs (mkApp traceQ [args,body])
where
args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
lstr = render (l<>":"<>ppTerm Qualified 0 q)
traceQ = Q (cPredef,cTrace)
-- * Computing values
-- | Computing the value of a top-level term
value0 :: CompleteEnv -> Term -> Err Value
value0 env = eval (global env) []
-- | Computing the value of a term
value :: CompleteEnv -> Term -> Err OpenValue
value env t0 =
-- Each terms is traversed only once by this function, using only statically
-- available information. Notably, the values of lambda bound variables
-- will be unknown during the term traversal phase.
-- The result is an OpenValue, which is a function that may be applied many
-- times to different dynamic values, but without the term traversal overhead
-- and without recomputing other statically known information.
-- For this to work, there should be no recursive calls under lambdas here.
-- Whenever we need to construct the OpenValue function with an explicit
-- lambda, we have to lift the recursive calls outside the lambda.
-- (See e.g. the rules for Let, Prod and Abs)
{-
trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
brackets (fsep (map ppIdent (local env))),
ppTerm Unqualified 10 t0]) $
--}
errIn (render t0) $
case t0 of
Vr x -> var env x
Q x@(m,f)
| m == cPredef -> if f==cErrorType -- to be removed
then let p = identS "P"
in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
else if f==cPBool
then const # resource env x
else const . flip VApp [] # predef f
| otherwise -> const # resource env x --valueResDef (fst env) x
QC x -> return $ const (VCApp x [])
App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
Let (x,(oty,t)) body -> do vb <- value (ext x env) body
vt <- value env t
return $ \ vs -> vb (vt vs:vs)
Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
Prod bt x t1 t2 ->
do vt1 <- value env t1
vt2 <- value (ext x env) t2
return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
Abs bt x t -> do vt <- value (ext x env) t
return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
EInt n -> return $ const (VInt n)
EFloat f -> return $ const (VFloat f)
K s -> return $ const (VString s)
Empty -> return $ const (VString "")
Sort s | s == cTok -> return $ const (VSort cStr) -- to be removed
| otherwise -> return $ const (VSort s)
ImplArg t -> (VImplArg.) # value env t
Table p res -> liftM2 VTblType # value env p <# value env res
RecType rs -> do lovs <- mapPairsM (value env) rs
return $ \vs->VRecType $ mapSnd ($vs) lovs
t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
FV ts -> ((vfv .) # sequence) # mapM (value env) ts
R as -> do lovs <- mapPairsM (value env.snd) as
return $ \ vs->VRec $ mapSnd ($vs) lovs
T i cs -> valueTable env i cs
V ty ts -> do pvs <- paramValues env ty
((VV ty pvs .) . sequence) # mapM (value env) ts
C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
P t l -> --maybe (bug $ "project "++show l++" from "++show v) id $
do ov <- value env t
return $ \ vs -> let v = ov vs
in maybe (VP v l) id (proj l v)
Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
Strs ts -> ((VStrs.) # sequence) # mapM (value env) ts
Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
ELin c r -> (unlockVRec (gloc env) c.) # value env r
EPatt p -> return $ const (VPatt p) -- hmm
EPattType ty -> do vt <- value env ty
return (VPattType . vt)
Typed t ty -> value env t
t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
vconcat vv@(v1,v2) =
case vv of
(VString "",_) -> v2
(_,VString "") -> v1
(VApp NonExist _,_) -> v1
(_,VApp NonExist _) -> v2
_ -> VC v1 v2
proj l v | isLockLabel l = return (VRec [])
---- a workaround 18/2/2005: take this away and find the reason
---- why earlier compilation destroys the lock field
proj l v =
case v of
VFV vs -> liftM vfv (mapM (proj l) vs)
VRec rs -> lookup l rs
-- VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
_ -> return (ok1 VP v l)
ok1 f v1@(VError {}) _ = v1
ok1 f v1 v2 = f v1 v2
ok2 f v1@(VError {}) _ = v1
ok2 f _ v2@(VError {}) = v2
ok2 f v1 v2 = f v1 v2
ok2p f (v1@VError {},_) = v1
ok2p f (_,v2@VError {}) = v2
ok2p f vv = f vv
unlockVRec loc c0 v0 = v0
{-
unlockVRec loc c0 v0 = unlockVRec' c0 v0
where
unlockVRec' ::Ident -> Value -> Value
unlockVRec' c v =
case v of
-- VClosure env t -> err bug (VClosure env) (unlockRecord c t)
VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
VRec rs -> plusVRec rs lock
-- _ -> VExtR v (VRec lock) -- hmm
_ -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
-- _ -> bugloc loc $ "unlock non-record "++show v0
where
lock = [(lockLabel c,VRec [])]
-}
-- suspicious, but backwards compatible
plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
where ls2 = map fst rs2
extR t vv =
case vv of
(VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
(v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
(VRecType rs1, VRecType rs2) ->
case intersect (map fst rs1) (map fst rs2) of
[] -> VRecType (rs1 ++ rs2)
ls -> error $ "clash"<+>show ls
(VRec rs1, VRec rs2) -> plusVRec rs1 rs2
(v1 , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
(VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
-- (v1,v2) -> ok2 VExtR v1 v2 -- hmm
(v1,v2) -> error $ "not records" $$ show v1 $$ show v2
where
error explain = ppbug $ "The term" <+> t
<+> "is not reducible" $$ explain
glue env (v1,v2) = glu v1 v2
where
glu v1 v2 =
case (v1,v2) of
(VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
(v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
(VString s1,VString s2) -> VString (s1++s2)
(v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
where glx v2 = glu v1 v2
(v1@(VAlts {}),v2) ->
--err (const (ok2 VGlue v1 v2)) id $
err bug id $
do y' <- strsFromValue v2
x' <- strsFromValue v1
return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
(VC va vb,v2) -> VC va (glu vb v2)
(v1,VC va vb) -> VC (glu v1 va) vb
(VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
(v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
(v1@(VApp NonExist _),_) -> v1
(_,v2@(VApp NonExist _)) -> v2
-- (v1,v2) -> ok2 VGlue v1 v2
(v1,v2) -> if flag optPlusAsBind (opts env)
then VC v1 (VC (VApp BIND []) v2)
else let loc = gloc env
vt v = case value2term loc (local env) v of
Left i -> Error ('#':show i)
Right t -> t
originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
(Glue (vt v1) (vt v2)))
term = render $ pp $ Glue (vt v1) (vt v2)
in error $ unlines
[originalMsg
,""
,"There was a problem in the expression `"++term++"`, either:"
,"1) You are trying to use + on runtime arguments, possibly via an oper."
,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
]
-- | to get a string from a value that represents a sequence of terminals
strsFromValue :: Value -> Err [Str]
strsFromValue t = case t of
VString s -> return [str s]
VC s t -> do
s' <- strsFromValue s
t' <- strsFromValue t
return [plusStr x y | x <- s', y <- t']
{-
VGlue s t -> do
s' <- strsFromValue s
t' <- strsFromValue t
return [glueStr x y | x <- s', y <- t']
-}
VAlts d vs -> do
d0 <- strsFromValue d
v0 <- mapM (strsFromValue . fst) vs
c0 <- mapM (strsFromValue . snd) vs
--let vs' = zip v0 c0
return [strTok (str2strings def) vars |
def <- d0,
vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
vv <- sequence v0]
]
VFV ts -> concat # mapM strsFromValue ts
VStrs ts -> concat # mapM strsFromValue ts
_ -> fail ("cannot get Str from value " ++ show t)
vfv vs = case nub vs of
[v] -> v
vs -> VFV vs
select env vv =
case vv of
(v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
(VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
(v1@(VV pty vs rs),v2) ->
err (const (VS v1 v2)) id $
do --ats <- allParamValues (srcgr env) pty
--let vs = map (value0 env) ats
i <- maybeErr "no match" $ findIndex (==v2) vs
return (ix (gloc env) "select" rs i)
(VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
(v1@(VT _ _ cs),v2) ->
err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
match (gloc env) cs v2
(VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
(v1,v2) -> ok2 VS v1 v2
match loc cs v =
case value2term loc [] v of
Left i -> bad ("variable #"++show i++" is out of scope")
Right t -> err bad return (matchPattern cs t)
where
bad = fail . ("In pattern matching: "++)
valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
valueTable env i cs =
case i of
TComp ty -> do pvs <- paramValues env ty
((VV ty pvs .) # sequence) # mapM (value env.snd) cs
_ -> do ty <- getTableType i
cs' <- mapM valueCase cs
err (dynamic cs' ty) return (convert cs' ty)
where
dynamic cs' ty _ = cases cs' # value env ty
cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
where
keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
VT wild (vty vs) (mapSnd ($vs) cs')
wild = case i of TWild _ -> True; _ -> False
convertv cs' vty =
case value2term (gloc env) [] vty of
Left i -> fail ("variable #"++show i++" is out of scope")
Right pty -> convert' cs' =<< paramValues'' env pty
convert cs' ty = convert' cs' =<< paramValues' env ty
convert' cs' ((pty,vs),pvs) =
do sts <- mapM (matchPattern cs') vs
return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
(mapFst ($vs) sts)
valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
pvs <- linPattVars p'
vt <- value (extend pvs env) t
return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
inlinePattMacro p =
case p of
PM qc -> do r <- resource env qc
case r of
VPatt p' -> inlinePattMacro p'
_ -> ppbug $ hang "Expected pattern macro:" 4
(show r)
_ -> composPattOp inlinePattMacro p
paramValues env ty = snd # paramValues' env ty
paramValues' env ty = paramValues'' env =<< nfx (global env) ty
paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
pvs <- mapM (eval (global env) []) ats
return ((pty,ats),pvs)
push' p bs xs = if length bs/=length xs
then bug $ "push "++show (p,bs,xs)
else push bs xs
push :: Env -> LocalScope -> Stack -> Stack
push bs [] vs = vs
push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
where err = bug $ "Unbound pattern variable "++showIdent x
apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
apply' env t [] = value env t
apply' env t vs =
case t of
QC x -> return $ \ svs -> VCApp x (map ($svs) vs)
{-
Q x@(m,f) | m==cPredef -> return $
let constr = --trace ("predef "++show x) .
VApp x
in \ svs -> maybe constr id (Map.lookup f predefs)
$ map ($svs) vs
| otherwise -> do r <- resource env x
return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
-}
App t1 t2 -> apply' env t1 . (:vs) =<< value env t2
_ -> do fv <- value env t
return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
vapply :: GLocation -> Value -> [Value] -> Value
vapply loc v [] = v
vapply loc v vs =
case v of
VError {} -> v
-- VClosure env (Abs b x t) -> beta gr env b x t vs
VAbs bt _ (Bind f) -> vbeta loc bt f vs
VApp pre vs1 -> delta' pre (vs1++vs)
where
delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
in vtrace loc v1 vr
delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
--msg = const (VApp pre (vs1++vs))
msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
VFV fs -> vfv [vapply loc f vs|f<-fs]
VCApp f vs0 -> VCApp f (vs0++vs)
VMeta i env vs0 -> VMeta i env (vs0++vs)
VGen i vs0 -> VGen i (vs0++vs)
v -> bug $ "vapply "++show v++" "++show vs
vbeta loc bt f (v:vs) =
case (bt,v) of
(Implicit,VImplArg v) -> ap v
(Explicit, v) -> ap v
where
ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
ap v = vapply loc (f v) vs
vary (VFV vs) = vs
vary v = [v]
varyList = mapM vary
{-
beta env b x t (v:vs) =
case (b,v) of
(Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
(Explicit, v) -> apply' (ext (x,v) env) t vs
-}
vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
where
pv v = case v of
VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
_ -> ppV v
pf (_,VString n) = pp n
pf (_,v) = ppV v
pa (_,v) = ppV v
ppV v = case value2term' True loc [] v of
Left i -> "variable #" <> pp i <+> "is out of scope"
Right t -> ppTerm Unqualified 10 t
-- | Convert a value back to a term
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
value2term = value2term' False
value2term' stop loc xs v0 =
case v0 of
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
VInt n -> return (EInt n)
VFloat f -> return (EFloat f)
VString s -> return (if null s then Empty else K s)
VSort s -> return (Sort s)
VImplArg v -> liftM ImplArg (v2t v)
VTblType p res -> liftM2 Table (v2t p) (v2t res)
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
VV t _ vs -> liftM (V t) (mapM v2t vs)
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
VFV vs -> liftM FV (mapM v2t vs)
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
VP v l -> v2t v >>= \t -> return (P t l)
VPatt p -> return (EPatt p)
VPattType v -> v2t v >>= return . EPattType
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
VStrs vs -> liftM Strs (mapM v2t vs)
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
VError err -> return (Error err)
where
v2t = v2txs xs
v2txs = value2term' stop loc
v2t' x f = v2txs (x:xs) (bind f (gen xs))
var j
| j<length xs = Right (Vr (reverse xs !! j))
| otherwise = Left j
pushs xs e = foldr push e xs
push x (env,xs) = ((x,gen xs):env,x:xs)
gen xs = VGen (length xs) []
nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
where (env',xs') = pushs (pattVars p) ([],xs)
bind (Bind f) x = if stop
then VSort (identS "...") -- hmm
else f x
linPattVars p =
if null dups
then return pvs
else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
where
allpvs = allPattVars p
pvs = nub allpvs
dups = allpvs \\ pvs
pattVars = nub . allPattVars
allPattVars p =
case p of
PV i -> [i]
PAs i p -> i:allPattVars p
_ -> collectPattOp allPattVars p
---
ix loc fn xs i =
if i<n
then xs !! i
else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
where n = length xs
infixl 1 #,<# --,@@
f # x = fmap f x
mf <# mx = ap mf mx
--m1 @@ m2 = (m1 =<<) . m2
both f (x,y) = (,) # f x <# f y
bugloc loc s = ppbug $ ppL loc s
bug msg = ppbug msg
ppbug doc = error $ render $ hang "Internal error in Compute.Concrete:" 4 doc

588
src/compiler/GF/Compile/Compute/ConcreteNew.hs
View File

@@ -1,588 +0,0 @@
-- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation.
module GF.Compile.Compute.ConcreteNew
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
normalForm,
Value(..), Bind(..), Env, value2term, eval, vapply
) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
import GF.Compile.Compute.Value hiding (Error)
import GF.Compile.Compute.Predef(predef,predefName,delta)
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
import GF.Data.Utilities(mapFst,mapSnd)
import GF.Infra.Option
import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
--import Data.Char (isUpper,toUpper,toLower)
import GF.Text.Pretty
import qualified Data.Map as Map
import Debug.Trace(trace)
-- * Main entry points
normalForm :: GlobalEnv -> L Ident -> Term -> Term
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
nfx env@(GE _ _ _ loc) t = do
v <- eval env [] t
case value2term loc [] v of
Left i -> fail ("variable #"++show i++" is out of scope")
Right t -> return t
eval :: GlobalEnv -> Env -> Term -> Err Value
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
where
cenv = CE gr rvs opts loc (map fst env)
--apply env = apply' env
--------------------------------------------------------------------------------
-- * Environments
type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
data GlobalEnv = GE Grammar ResourceValues Options GLocation
data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
opts::Options,
gloc::GLocation,local::LocalScope}
type GLocation = L Ident
type LocalScope = [Ident]
type Stack = [Value]
type OpenValue = Stack->Value
geLoc (GE _ _ _ loc) = loc
geGrammar (GE gr _ _ _) = gr
ext b env = env{local=b:local env}
extend bs env = env{local=bs++local env}
global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
var :: CompleteEnv -> Ident -> Err OpenValue
var env x = maybe unbound pick' (elemIndex x (local env))
where
unbound = fail ("Unknown variable: "++showIdent x)
pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
err i vs = bug $ "Stack problem: "++showIdent x++": "
++unwords (map showIdent (local env))
++" => "++show (i,length vs)
ok v = --trace ("var "++show x++" = "++show v) $
v
pick :: Int -> Stack -> Maybe Value
pick 0 (v:_) = Just v
pick i (_:vs) = pick (i-1) vs
pick i vs = Nothing -- bug $ "pick "++show (i,vs)
resource env (m,c) =
-- err bug id $
if isPredefCat c
then value0 env =<< lockRecType c defLinType -- hmm
else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
where e = fail $ "Not found: "++render m++"."++showIdent c
-- | Convert operators once, not every time they are looked up
resourceValues :: Options -> SourceGrammar -> GlobalEnv
resourceValues opts gr = env
where
env = GE gr rvs opts (L NoLoc identW)
rvs = Map.mapWithKey moduleResources (moduleMap gr)
moduleResources m = Map.mapWithKey (moduleResource m) . jments
moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
let loc = L l c
qloc = L l (Q (m,c))
eval (GE gr rvs opts loc) [] (traceRes qloc t)
traceRes = if flag optTrace opts
then traceResource
else const id
-- * Tracing
-- | Insert a call to the trace function under the top-level lambdas
traceResource (L l q) t =
case termFormCnc t of
(abs,body) -> mkAbs abs (mkApp traceQ [args,body])
where
args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
lstr = render (l<>":"<>ppTerm Qualified 0 q)
traceQ = Q (cPredef,cTrace)
-- * Computing values
-- | Computing the value of a top-level term
value0 :: CompleteEnv -> Term -> Err Value
value0 env = eval (global env) []
-- | Computing the value of a term
value :: CompleteEnv -> Term -> Err OpenValue
value env t0 =
-- Each terms is traversed only once by this function, using only statically
-- available information. Notably, the values of lambda bound variables
-- will be unknown during the term traversal phase.
-- The result is an OpenValue, which is a function that may be applied many
-- times to different dynamic values, but without the term traversal overhead
-- and without recomputing other statically known information.
-- For this to work, there should be no recursive calls under lambdas here.
-- Whenever we need to construct the OpenValue function with an explicit
-- lambda, we have to lift the recursive calls outside the lambda.
-- (See e.g. the rules for Let, Prod and Abs)
{-
trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
brackets (fsep (map ppIdent (local env))),
ppTerm Unqualified 10 t0]) $
--}
errIn (render t0) $
case t0 of
Vr x -> var env x
Q x@(m,f)
| m == cPredef -> if f==cErrorType -- to be removed
then let p = identS "P"
in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
else if f==cPBool
then const # resource env x
else const . flip VApp [] # predef f
| otherwise -> const # resource env x --valueResDef (fst env) x
QC x -> return $ const (VCApp x [])
App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
Let (x,(oty,t)) body -> do vb <- value (ext x env) body
vt <- value env t
return $ \ vs -> vb (vt vs:vs)
Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
Prod bt x t1 t2 ->
do vt1 <- value env t1
vt2 <- value (ext x env) t2
return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
Abs bt x t -> do vt <- value (ext x env) t
return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
EInt n -> return $ const (VInt n)
EFloat f -> return $ const (VFloat f)
K s -> return $ const (VString s)
Empty -> return $ const (VString "")
Sort s | s == cTok -> return $ const (VSort cStr) -- to be removed
| otherwise -> return $ const (VSort s)
ImplArg t -> (VImplArg.) # value env t
Table p res -> liftM2 VTblType # value env p <# value env res
RecType rs -> do lovs <- mapPairsM (value env) rs
return $ \vs->VRecType $ mapSnd ($vs) lovs
t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
FV ts -> ((vfv .) # sequence) # mapM (value env) ts
R as -> do lovs <- mapPairsM (value env.snd) as
return $ \ vs->VRec $ mapSnd ($vs) lovs
T i cs -> valueTable env i cs
V ty ts -> do pvs <- paramValues env ty
((VV ty pvs .) . sequence) # mapM (value env) ts
C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
P t l -> --maybe (bug $ "project "++show l++" from "++show v) id $
do ov <- value env t
return $ \ vs -> let v = ov vs
in maybe (VP v l) id (proj l v)
Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
Strs ts -> ((VStrs.) # sequence) # mapM (value env) ts
Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
ELin c r -> (unlockVRec (gloc env) c.) # value env r
EPatt p -> return $ const (VPatt p) -- hmm
EPattType ty -> do vt <- value env ty
return (VPattType . vt)
Typed t ty -> value env t
t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
vconcat vv@(v1,v2) =
case vv of
(VString "",_) -> v2
(_,VString "") -> v1
(VApp NonExist _,_) -> v1
(_,VApp NonExist _) -> v2
_ -> VC v1 v2
proj l v | isLockLabel l = return (VRec [])
---- a workaround 18/2/2005: take this away and find the reason
---- why earlier compilation destroys the lock field
proj l v =
case v of
VFV vs -> liftM vfv (mapM (proj l) vs)
VRec rs -> lookup l rs
-- VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
_ -> return (ok1 VP v l)
ok1 f v1@(VError {}) _ = v1
ok1 f v1 v2 = f v1 v2
ok2 f v1@(VError {}) _ = v1
ok2 f _ v2@(VError {}) = v2
ok2 f v1 v2 = f v1 v2
ok2p f (v1@VError {},_) = v1
ok2p f (_,v2@VError {}) = v2
ok2p f vv = f vv
unlockVRec loc c0 v0 = v0
{-
unlockVRec loc c0 v0 = unlockVRec' c0 v0
where
unlockVRec' ::Ident -> Value -> Value
unlockVRec' c v =
case v of
-- VClosure env t -> err bug (VClosure env) (unlockRecord c t)
VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
VRec rs -> plusVRec rs lock
-- _ -> VExtR v (VRec lock) -- hmm
_ -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
-- _ -> bugloc loc $ "unlock non-record "++show v0
where
lock = [(lockLabel c,VRec [])]
-}
-- suspicious, but backwards compatible
plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
where ls2 = map fst rs2
extR t vv =
case vv of
(VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
(v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
(VRecType rs1, VRecType rs2) ->
case intersect (map fst rs1) (map fst rs2) of
[] -> VRecType (rs1 ++ rs2)
ls -> error $ "clash"<+>show ls
(VRec rs1, VRec rs2) -> plusVRec rs1 rs2
(v1 , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
(VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
-- (v1,v2) -> ok2 VExtR v1 v2 -- hmm
(v1,v2) -> error $ "not records" $$ show v1 $$ show v2
where
error explain = ppbug $ "The term" <+> t
<+> "is not reducible" $$ explain
glue env (v1,v2) = glu v1 v2
where
glu v1 v2 =
case (v1,v2) of
(VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
(v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
(VString s1,VString s2) -> VString (s1++s2)
(v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
where glx v2 = glu v1 v2
(v1@(VAlts {}),v2) ->
--err (const (ok2 VGlue v1 v2)) id $
err bug id $
do y' <- strsFromValue v2
x' <- strsFromValue v1
return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
(VC va vb,v2) -> VC va (glu vb v2)
(v1,VC va vb) -> VC (glu v1 va) vb
(VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
(v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
(v1@(VApp NonExist _),_) -> v1
(_,v2@(VApp NonExist _)) -> v2
-- (v1,v2) -> ok2 VGlue v1 v2
(v1,v2) -> if flag optPlusAsBind (opts env)
then VC v1 (VC (VApp BIND []) v2)
else let loc = gloc env
vt v = case value2term loc (local env) v of
Left i -> Error ('#':show i)
Right t -> t
originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
(Glue (vt v1) (vt v2)))
term = render $ pp $ Glue (vt v1) (vt v2)
in error $ unlines
[originalMsg
,""
,"There was a problem in the expression `"++term++"`, either:"
,"1) You are trying to use + on runtime arguments, possibly via an oper."
,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
]
-- | to get a string from a value that represents a sequence of terminals
strsFromValue :: Value -> Err [Str]
strsFromValue t = case t of
VString s -> return [str s]
VC s t -> do
s' <- strsFromValue s
t' <- strsFromValue t
return [plusStr x y | x <- s', y <- t']
{-
VGlue s t -> do
s' <- strsFromValue s
t' <- strsFromValue t
return [glueStr x y | x <- s', y <- t']
-}
VAlts d vs -> do
d0 <- strsFromValue d
v0 <- mapM (strsFromValue . fst) vs
c0 <- mapM (strsFromValue . snd) vs
--let vs' = zip v0 c0
return [strTok (str2strings def) vars |
def <- d0,
vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
vv <- sequence v0]
]
VFV ts -> concat # mapM strsFromValue ts
VStrs ts -> concat # mapM strsFromValue ts
_ -> fail ("cannot get Str from value " ++ show t)
vfv vs = case nub vs of
[v] -> v
vs -> VFV vs
select env vv =
case vv of
(v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
(VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
(v1@(VV pty vs rs),v2) ->
err (const (VS v1 v2)) id $
do --ats <- allParamValues (srcgr env) pty
--let vs = map (value0 env) ats
i <- maybeErr "no match" $ findIndex (==v2) vs
return (ix (gloc env) "select" rs i)
(VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
(v1@(VT _ _ cs),v2) ->
err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
match (gloc env) cs v2
(VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
(v1,v2) -> ok2 VS v1 v2
match loc cs v =
case value2term loc [] v of
Left i -> bad ("variable #"++show i++" is out of scope")
Right t -> err bad return (matchPattern cs t)
where
bad = fail . ("In pattern matching: "++)
valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
valueTable env i cs =
case i of
TComp ty -> do pvs <- paramValues env ty
((VV ty pvs .) # sequence) # mapM (value env.snd) cs
_ -> do ty <- getTableType i
cs' <- mapM valueCase cs
err (dynamic cs' ty) return (convert cs' ty)
where
dynamic cs' ty _ = cases cs' # value env ty
cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
where
keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
VT wild (vty vs) (mapSnd ($vs) cs')
wild = case i of TWild _ -> True; _ -> False
convertv cs' vty =
case value2term (gloc env) [] vty of
Left i -> fail ("variable #"++show i++" is out of scope")
Right pty -> convert' cs' =<< paramValues'' env pty
convert cs' ty = convert' cs' =<< paramValues' env ty
convert' cs' ((pty,vs),pvs) =
do sts <- mapM (matchPattern cs') vs
return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
(mapFst ($vs) sts)
valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
pvs <- linPattVars p'
vt <- value (extend pvs env) t
return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
inlinePattMacro p =
case p of
PM qc -> do r <- resource env qc
case r of
VPatt p' -> inlinePattMacro p'
_ -> ppbug $ hang "Expected pattern macro:" 4
(show r)
_ -> composPattOp inlinePattMacro p
paramValues env ty = snd # paramValues' env ty
paramValues' env ty = paramValues'' env =<< nfx (global env) ty
paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
pvs <- mapM (eval (global env) []) ats
return ((pty,ats),pvs)
push' p bs xs = if length bs/=length xs
then bug $ "push "++show (p,bs,xs)
else push bs xs
push :: Env -> LocalScope -> Stack -> Stack
push bs [] vs = vs
push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
where err = bug $ "Unbound pattern variable "++showIdent x
apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
apply' env t [] = value env t
apply' env t vs =
case t of
QC x -> return $ \ svs -> VCApp x (map ($svs) vs)
{-
Q x@(m,f) | m==cPredef -> return $
let constr = --trace ("predef "++show x) .
VApp x
in \ svs -> maybe constr id (Map.lookup f predefs)
$ map ($svs) vs
| otherwise -> do r <- resource env x
return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
-}
App t1 t2 -> apply' env t1 . (:vs) =<< value env t2
_ -> do fv <- value env t
return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
vapply :: GLocation -> Value -> [Value] -> Value
vapply loc v [] = v
vapply loc v vs =
case v of
VError {} -> v
-- VClosure env (Abs b x t) -> beta gr env b x t vs
VAbs bt _ (Bind f) -> vbeta loc bt f vs
VApp pre vs1 -> delta' pre (vs1++vs)
where
delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
in vtrace loc v1 vr
delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
--msg = const (VApp pre (vs1++vs))
msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
VFV fs -> vfv [vapply loc f vs|f<-fs]
VCApp f vs0 -> VCApp f (vs0++vs)
VMeta i env vs0 -> VMeta i env (vs0++vs)
VGen i vs0 -> VGen i (vs0++vs)
v -> bug $ "vapply "++show v++" "++show vs
vbeta loc bt f (v:vs) =
case (bt,v) of
(Implicit,VImplArg v) -> ap v
(Explicit, v) -> ap v
where
ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
ap v = vapply loc (f v) vs
vary (VFV vs) = vs
vary v = [v]
varyList = mapM vary
{-
beta env b x t (v:vs) =
case (b,v) of
(Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
(Explicit, v) -> apply' (ext (x,v) env) t vs
-}
vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
where
pv v = case v of
VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
_ -> ppV v
pf (_,VString n) = pp n
pf (_,v) = ppV v
pa (_,v) = ppV v
ppV v = case value2term' True loc [] v of
Left i -> "variable #" <> pp i <+> "is out of scope"
Right t -> ppTerm Unqualified 10 t
-- | Convert a value back to a term
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
value2term = value2term' False
value2term' stop loc xs v0 =
case v0 of
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
VInt n -> return (EInt n)
VFloat f -> return (EFloat f)
VString s -> return (if null s then Empty else K s)
VSort s -> return (Sort s)
VImplArg v -> liftM ImplArg (v2t v)
VTblType p res -> liftM2 Table (v2t p) (v2t res)
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
VV t _ vs -> liftM (V t) (mapM v2t vs)
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
VFV vs -> liftM FV (mapM v2t vs)
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
VP v l -> v2t v >>= \t -> return (P t l)
VPatt p -> return (EPatt p)
VPattType v -> v2t v >>= return . EPattType
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
VStrs vs -> liftM Strs (mapM v2t vs)
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
VError err -> return (Error err)
where
v2t = v2txs xs
v2txs = value2term' stop loc
v2t' x f = v2txs (x:xs) (bind f (gen xs))
var j
| j<length xs = Right (Vr (reverse xs !! j))
| otherwise = Left j
pushs xs e = foldr push e xs
push x (env,xs) = ((x,gen xs):env,x:xs)
gen xs = VGen (length xs) []
nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
where (env',xs') = pushs (pattVars p) ([],xs)
bind (Bind f) x = if stop
then VSort (identS "...") -- hmm
else f x
linPattVars p =
if null dups
then return pvs
else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
where
allpvs = allPattVars p
pvs = nub allpvs
dups = allpvs \\ pvs
pattVars = nub . allPattVars
allPattVars p =
case p of
PV i -> [i]
PAs i p -> i:allPattVars p
_ -> collectPattOp allPattVars p
---
ix loc fn xs i =
if i<n
then xs !! i
else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
where n = length xs
infixl 1 #,<# --,@@
f # x = fmap f x
mf <# mx = ap mf mx
--m1 @@ m2 = (m1 =<<) . m2
both f (x,y) = (,) # f x <# f y
bugloc loc s = ppbug $ ppL loc s
bug msg = ppbug msg
ppbug doc = error $ render $ hang "Internal error in Compute.ConcreteNew:" 4 doc

8
src/compiler/GF/Compile/Compute/Value.hs
View File

@@ -12,8 +12,8 @@ data Value
| VGen Int [Value] -- for lambda bound variables, possibly applied
| VMeta MetaId Env [Value]
-- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
| VAbs BindType Ident Binding -- used in Compute.ConcreteNew
| VProd BindType Value Ident Binding -- used in Compute.ConcreteNew
| VAbs BindType Ident Binding -- used in Compute.Concrete
| VProd BindType Value Ident Binding -- used in Compute.Concrete
| VInt Int
| VFloat Double
| VString String
@@ -47,10 +47,10 @@ type Env = [(Ident,Value)]
-- | Predefined functions
data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
| ToLower | IsUpper | Length | Plus | EqInt | LessInt
| ToLower | IsUpper | Length | Plus | EqInt | LessInt
{- | Show | Read | ToStr | MapStr | EqVal -}
| Error | Trace
-- Canonical values below:
| PBool | PFalse | PTrue | Int | Float | Ints | NonExist
| PBool | PFalse | PTrue | Int | Float | Ints | NonExist
| BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
deriving (Show,Eq,Ord,Ix,Bounded,Enum)

12
src/compiler/GF/Compile/GeneratePMCFG.hs
View File

@@ -25,7 +25,7 @@ import GF.Data.BacktrackM
import GF.Data.Operations
import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
import GF.Data.Utilities (updateNthM) --updateNth
import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
import GF.Compile.Compute.Concrete(normalForm,resourceValues)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
@@ -82,7 +82,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
(goB b1 CNil [])
(pres,pargs)
pmcfg = getPMCFG pmcfgEnv1
stats = let PMCFG prods funs = pmcfg
(s,e) = bounds funs
!prods_cnt = length prods
@@ -103,7 +103,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
newArgs = map getFIds newArgs'
in addFunction env0 newCat fun newArgs
addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
mdef@(Just (L loc1 def))
mref@(Just (L loc2 ref))
mprn
@@ -162,7 +162,7 @@ pgfCncCat :: SourceGrammar -> Type -> Int -> CncCat
pgfCncCat gr lincat index =
let ((_,size),schema) = computeCatRange gr lincat
in PGF.CncCat index (index+size-1)
(mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
(mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
(getStrPaths schema)))
where
getStrPaths :: Schema Identity s c -> [Path]
@@ -243,7 +243,7 @@ choices nr path = do (args,_) <- get
| (value,index) <- values])
descend schema path rpath = bug $ "descend "++show (schema,path,rpath)
updateEnv path value gr c (args,seq) =
updateEnv path value gr c (args,seq) =
case updateNthM (restrictProtoFCat path value) nr args of
Just args -> c value (args,seq)
Nothing -> bug "conflict in updateEnv"
@@ -606,7 +606,7 @@ restrictProtoFCat path v (PFCat cat f schema) = do
Just index -> return (CPar (m,[(v,index)]))
Nothing -> mzero
addConstraint CNil v (CStr _) = bug "restrictProtoFCat: string path"
update k0 f [] = return []
update k0 f (x@(k,Identity v):xs)
| k0 == k = do v <- f v

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

@@ -20,7 +20,7 @@ import GF.Compile.Compute.Value(Predefined(..))
import GF.Infra.Ident(ModuleName(..),Ident,ident2raw,rawIdentS,showIdent,isWildIdent)
import GF.Infra.Option(Options,optionsPGF)
import PGF.Internal(Literal(..))
import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
import GF.Grammar.Canonical as C
import System.FilePath ((</>), (<.>))
import qualified Debug.Trace as T

16
src/compiler/GF/Compile/Optimize.hs
View File

@@ -6,7 +6,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/16 13:56:13 $
-- > CVS $Date: 2005/09/16 13:56:13 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.18 $
--
@@ -21,7 +21,7 @@ import GF.Grammar.Printer
import GF.Grammar.Macros
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
import GF.Data.Operations
import GF.Infra.Option
@@ -90,7 +90,7 @@ evalInfo opts resenv sgr m c info = do
let ppr' = fmap (evalPrintname resenv c) ppr
return $ CncFun mt pde' ppr' mpmcfg -- only cat in type actually needed
{-
ResOper pty pde
ResOper pty pde
| not new && OptExpand `Set.member` optim -> do
pde' <- case pde of
Just (L loc de) -> do de <- computeConcrete gr de
@@ -171,13 +171,13 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
_ -> Bad (render ("linearization type field cannot be" <+> typ))
mkLinReference :: SourceGrammar -> Type -> Err Term
mkLinReference gr typ =
liftM (Abs Explicit varStr) $
mkLinReference gr typ =
liftM (Abs Explicit varStr) $
case mkDefField typ (Vr varStr) of
Bad "no string" -> return Empty
x -> x
where
mkDefField ty trm =
mkDefField ty trm =
case ty of
Table pty ty -> do ps <- allParamValues gr pty
case ps of
@@ -203,7 +203,7 @@ factor param c i t =
T (TComp ty) cs -> factors ty [(p, factor param c (i+1) v) | (p, v) <- cs]
_ -> composSafeOp (factor param c i) t
where
factors ty pvs0
factors ty pvs0
| not param = V ty (map snd pvs0)
factors ty [] = V ty []
factors ty pvs0@[(p,v)] = V ty [v]
@@ -224,7 +224,7 @@ factor param c i t =
replace :: Term -> Term -> Term -> Term
replace old new trm =
case trm of
-- these are the important cases, since they can correspond to patterns
-- these are the important cases, since they can correspond to patterns
QC _ | trm == old -> new
App _ _ | trm == old -> new
R _ | trm == old -> new

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

@@ -1,6 +1,7 @@
{-# 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.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
| 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)
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
@@ -73,26 +80,26 @@ inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
Nothing -> checkError ("unknown in Predef:" <+> ident)
Q ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType 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
Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
Nothing -> checkError ("unknown in Predef:" <+> ident)
QC ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType 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
@@ -100,7 +107,12 @@ inferLType gr g trm = case trm of
Typed e t -> do
t' <- computeLType gr g 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
over <- getOverload gr g Nothing trm
@@ -110,13 +122,17 @@ inferLType gr g trm = case trm of
(f',fty) <- inferLType gr g f
fty' <- computeLType gr g fty
case fty' of
Prod bt z arg val -> do
Prod bt z arg val -> do
a' <- justCheck g a arg
ty <- if isWildIdent z
ty <- if isWildIdent z
then return val
else substituteLType [(bt,z,a')] val
return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
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
@@ -124,7 +140,7 @@ inferLType gr g trm = case trm of
Table arg val -> do
x'<- justCheck g x arg
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
(t',ty) <- inferLType gr g t --- ??
@@ -132,16 +148,16 @@ inferLType gr g trm = case trm of
let tr2 = P t' i
termWith tr2 $ case ty' 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
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
_ -> 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 (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))
T (TTyped arg) pts -> do
@@ -152,10 +168,10 @@ inferLType gr g trm = case trm of
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 (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do
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
@@ -166,9 +182,9 @@ inferLType gr g trm = case trm of
K s -> do
if elem ' ' s
then do
let ss = foldr C Empty (map K (words s))
let ss = foldr C Empty (map K (words s))
----- removed irritating warning AR 24/5/2008
----- checkWarn ("token \"" ++ s ++
----- checkWarn ("token \"" ++ s ++
----- "\" converted to token list" ++ prt ss)
return (ss, typeStr)
else return (trm, typeStr)
@@ -179,50 +195,56 @@ inferLType gr g trm = case trm of
Empty -> return (trm, typeStr)
C s1 s2 ->
C s1 s2 ->
check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
Glue s1 s2 ->
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 (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)
Strs ts -> do
ts' <- mapM (\t -> justCheck g t typeStr) ts
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
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
ts' <- mapM (flip (justCheck g) typeType) ts
return (RecType (zip ls ts'), typeType)
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
(s',sT) <- inferLType gr g s
sT' <- computeLType gr g sT
let trm' = ExtR r' s'
---- trm' <- plusRecord r' s'
case (rT', sT') of
(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)
_ | rT' == typeType && sT' == typeType -> return (trm', typeType)
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
_ | rT' == typeType && sT' == typeType -> do
return (trm', typeType)
_ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
Sort _ ->
Sort _ ->
termWith trm $ return typeType
Prod bt x a b -> do
@@ -231,7 +253,7 @@ inferLType gr g trm = case trm of
return (Prod bt x a' b', typeType)
Table p t -> do
p' <- justCheck g p typeType --- check p partype!
p' <- justCheck g p typeType --- check p partype!
t' <- justCheck g t typeType
return $ (Table p' t', typeType)
@@ -250,9 +272,9 @@ inferLType gr g trm = case trm of
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')
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
isPredef m = elem m [cPredef,cPredefAbs]
@@ -299,7 +321,6 @@ inferLType gr g trm = case trm of
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))
@@ -310,15 +331,28 @@ getOverload gr g mt ot = case appForm ot of
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
@@ -329,50 +363,57 @@ getOverload gr g mt ot = case appForm ot of
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
([(_,val,fun)],_) -> return (mkApp fun tts, val)
([],[(pre,val,fun)]) -> do
checkWarn $ text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
text "for" $$
checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
"for" $$
nest 2 (showTypes tys) $$
text "using" $$
"using" $$
nest 2 (showTypes pre)
return (mkApp fun tts, val)
([],[]) -> do
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
text "for" $$
checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
maybe empty (\x -> "with value type" <+> ppType x) mt $$
"for argument list" $$
nest 2 stysError $$
text "among" $$
nest 2 (vcat stypsError) $$
maybe empty (\x -> text "with value type" <+> ppType x) mt
"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 (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)
----- unsafely exclude irritating warning AR 24/5/2008
----- checkWarn $ "overloading of" +++ prt f +++
----- checkWarn $ "overloading of" +++ prt f +++
----- "resolved by excluding partial applications:" ++++
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
text "for" <+> hsep (map ppType tys) $$
text "with alternatives" $$
nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2])
--- 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) fs
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) |
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 (pre,rest) = splitAt lt ty,
let isExact = pre == tys,
isExact || map unlocked pre == map unlocked tys
]
@@ -385,20 +426,21 @@ getOverload gr g mt ot = case appForm ot of
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
Prod bt' z a b -> do
(c',b') <- if isWildIdent z
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'
return $ (Abs bt x c', Prod bt' x a b')
_ -> checkError $ text "function type expected instead of" <+> ppType typ
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
@@ -408,6 +450,12 @@ checkLType gr g trm typ0 = 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
@@ -417,21 +465,21 @@ checkLType gr g trm typ0 = do
termWith trm' $ checkEqLType gr g typ ty' trm'
T _ [] ->
checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of
Table arg val -> do
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 (text "patterns never reached:" $$
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 $ 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 ->
case typ of
Table arg1 val ->
@@ -439,51 +487,54 @@ checkLType gr g trm typ0 = do
vs1 <- allParamValues gr arg1
if length vs1 == length vs
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]
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
--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 (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
_ | typ == typeType -> do
trm' <- computeLType gr g trm
case trm' of
RecType _ -> termWith trm $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
RecType _ -> termWith trm' $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
-- 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
(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
RecType rr1 -> do
let (rr0,rr2) = recParts rr rr1
r2 <- justCheck g r' rr0
s2 <- justCheck g s' rr2
return $ (ExtR r2 s2, typ)
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
text "but found" <+> ppTerm Unqualified 0 ty)
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 (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
_ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
FV vs -> do
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
checkEqLType gr g typ t trm
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
(arg',ty) <- inferLType gr g arg
ty' <- computeLType gr g ty
@@ -507,7 +558,8 @@ checkLType gr g trm typ0 = do
]
Let (x,(mty,def)) body -> case mty of
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
return (Let (x,(Just ty',def')) body', typ)
_ -> do
@@ -523,10 +575,10 @@ checkLType gr g trm typ0 = do
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
{-
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
@@ -535,12 +587,12 @@ checkLType gr g trm typ0 = do
Just (_,t) -> do
(t',ty') <- checkLType gr g t ty
return (l,(Just ty',t'))
_ -> checkError $
if isLockLabel l
_ -> checkError $
if isLockLabel l
then let cat = drop 5 (showIdent (label2ident l))
in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <>
text "; try wrapping it with lin" <+> text cat
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
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
@@ -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
t <- lookupResType env (q,c)
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)
checkEqLType env g typ v (patt2term p)
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]]
----- checkWarn $ prt p ++++ show pts ----- debug
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
checkEqLType env g typ t (patt2term p')
pattContext env g typ p'
@@ -577,10 +629,10 @@ pattContext env g typ p = case p of
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
(text "incompatible bindings of" <+>
fsep (map ppIdent pts) <+>
text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
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
@@ -590,11 +642,11 @@ pattContext env g typ p = case p of
PNeg p' -> noBind typ p'
_ -> return [] ---- check types!
where
where
noBind typ p' = do
co <- pattContext env g typ p'
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 []
else return []
@@ -603,9 +655,31 @@ checkEqLType gr g t u trm = do
(b,t',u',s) <- checkIfEqLType gr g t u trm
case b of
True -> return t'
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
text "expected:" <+> ppType t $$
text "inferred:" <+> ppType u
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
@@ -617,60 +691,62 @@ checkIfEqLType gr g t u trm = do
--- better: use a flag to forgive? (AR 31/1/2006)
_ -> case missingLock [] t' u' of
Ok lo -> do
checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
checkWarn $ "missing lock field" <+> fsep lo
return (True,t',u',[])
Bad s -> return (False,t',u',s)
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
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
(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) -> alpha g a b && l == k) ts) rs
(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
(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
---- this should be made in Rename
(Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
(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)
(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)
(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)
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| 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
_ -> t == u
_ -> 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)
|| (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,
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 (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
_:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
_ -> return locks
-- contravariance
(Prod _ x a b, Prod _ y c d) -> do
@@ -696,7 +772,7 @@ termWith t ct = do
return (t,ty)
-- | compositional check\/infer of binary operations
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
Term -> Term -> Type -> Check (Term,Type)
check2 chk con a b t = do
a' <- chk a
@@ -708,14 +784,18 @@ ppType :: Type -> Doc
ppType ty =
case ty 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
Prod _ x a b -> ppType a <+> text "->" <+> ppType b
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 (text "unknown variable" <+> ppIdent x)
[] -> checkError ("unknown variable" <+> x)
(ty:_) -> return ty
-}

38
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -10,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield
import GF.Compile.Compute.ConcreteNew
import GF.Compile.Compute.Concrete
import GF.Compile.Compute.Predef(predef,predefName)
import GF.Infra.CheckM
import GF.Data.Operations
@@ -133,7 +133,7 @@ tcRho ge scope t@(RecType rs) (Just ty) = do
[] -> unifyVar ge scope i env vs vtypePType
_ -> return ()
ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
"cannot be of type" <+> ppTerm Unqualified 0 ty)
(rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
return (f (RecType rs),ty)
@@ -187,7 +187,7 @@ tcRho ge scope (R rs) (Just ty) = do
case ty' of
(VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return ((f . R) rs,
return ((f . R) rs,
VRecType [(l, ty) | (l,t,ty) <- lttys]
)
ty -> do lttys <- inferRecFields ge scope rs
@@ -277,11 +277,11 @@ tcApp ge scope (App fun arg) = -- APP2
varg <- liftErr (eval ge (scopeEnv scope) arg)
return (App fun arg, res_ty varg)
tcApp ge scope (Q id) = -- VAR (global)
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
do ty <- liftErr (eval ge [] ty)
return (t,ty)
tcApp ge scope (QC id) = -- VAR (global)
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
do ty <- liftErr (eval ge [] ty)
return (t,ty)
tcApp ge scope t =
@@ -350,7 +350,7 @@ tcPatt ge scope (PM q) ty0 = do
Bad err -> tcError (pp err)
tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
inferRecFields ge scope rs =
inferRecFields ge scope rs =
mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
checkRecFields ge scope [] ltys
@@ -368,7 +368,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
where
takeIt l1 [] = (Nothing, [])
takeIt l1 (lty@(l2,ty):ltys)
| l1 == l2 = (Just ty,ltys)
| l1 == l2 = (Just ty,ltys)
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
in (mb_ty,lty:ltys')
@@ -390,7 +390,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
| s == cPType -> return mb_ty
VMeta _ _ _ -> return mb_ty
_ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
return ((l,ty):rs,mb_ty)
@@ -444,11 +444,11 @@ subsCheckRho ge scope t (VApp p1 _) (VApp p2 _) -- Rule
| predefName p1 == cInts && predefName p2 == cInt = return t
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2
| predefName p1 == cInts && predefName p2 == cInts =
if i <= j
if i <= j
then return t
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
let mkAccess scope t =
let mkAccess scope t =
case t of
ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
(scope,mkProj2,mkWrap2) <- mkAccess scope t2
@@ -557,7 +557,7 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
unify ge scope v1 v2 = do
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
ppTerm Unqualified 0 t2))
-- | Invariant: tv1 is a flexible type variable
@@ -609,7 +609,7 @@ quantify ge scope t tvs ty0 = do
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
ty <- zonkTerm ty -- of doing the substitution
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
return (foldr (Abs Implicit) t new_bndrs,vty)
@@ -619,7 +619,7 @@ quantify ge scope t tvs ty0 = do
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
bndrs _ = []
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
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']]
@@ -688,12 +688,12 @@ runTcM f = case unTcM f IntMap.empty [] of
TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
newMeta :: Scope -> Sigma -> TcM MetaId
newMeta scope ty = TcM (\ms msgs ->
newMeta scope ty = TcM (\ms msgs ->
let i = IntMap.size ms
in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\ms msgs ->
getMeta i = TcM (\ms msgs ->
case IntMap.lookup i ms of
Just mv -> TcOk mv ms msgs
Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
@@ -702,7 +702,7 @@ setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
newVar :: Scope -> Ident
newVar scope = head [x | i <- [1..],
newVar scope = head [x | i <- [1..],
let x = identS ('v':show i),
isFree scope x]
where
@@ -721,7 +721,7 @@ getMetaVars loc sc_tys = do
return (foldr go [] tys)
where
-- Get the MetaIds from a term; no duplicates in result
go (Vr tv) acc = acc
go (Vr tv) acc = acc
go (App x y) acc = go x (go y acc)
go (Meta i) acc
| i `elem` acc = acc
@@ -741,7 +741,7 @@ getFreeVars loc sc_tys = do
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
return (foldr (go []) [] tys)
where
go bound (Vr tv) acc
go bound (Vr tv) acc
| tv `elem` bound = acc
| tv `elem` acc = acc
| otherwise = tv : acc
@@ -771,7 +771,7 @@ tc_value2term loc xs v =
data TcA x a
data TcA x a
= TcSingle (MetaStore -> [Message] -> TcResult a)
| TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])

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