diff options
| -rw-r--r-- | gf.cabal | 3 | ||||
| -rw-r--r-- | src/compiler/GF/Command/SourceCommands.hs | 6 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/CheckGrammar.hs | 50 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Compute/Concrete.hs | 591 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Compute/ConcreteNew.hs | 588 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Compute/Value.hs | 8 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/GeneratePMCFG.hs | 12 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/GrammarToCanonical.hs | 2 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Optimize.hs | 16 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/TypeCheck/Concrete.hs | 366 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs | 38 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/TypeCheck/RConcrete.hs | 801 |
12 files changed, 878 insertions, 1603 deletions
@@ -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 diff --git a/src/compiler/GF/Command/SourceCommands.hs b/src/compiler/GF/Command/SourceCommands.hs index 0ba60d245..91ada899d 100644 --- a/src/compiler/GF/Command/SourceCommands.hs +++ b/src/compiler/GF/Command/SourceCommands.hs @@ -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 diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs index 24582bba2..71bce96c4 100644 --- a/src/compiler/GF/Compile/CheckGrammar.hs +++ b/src/compiler/GF/Compile/CheckGrammar.hs @@ -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!! diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index f411f2ca0..4b54c8c84 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -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 diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs deleted file mode 100644 index 6f00c45e1..000000000 --- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs +++ /dev/null @@ -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 diff --git a/src/compiler/GF/Compile/Compute/Value.hs b/src/compiler/GF/Compile/Compute/Value.hs index 7eb0c3bfb..c3fb83b4b 100644 --- a/src/compiler/GF/Compile/Compute/Value.hs +++ b/src/compiler/GF/Compile/Compute/Value.hs @@ -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) diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index ab6476b31..8383f0624 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -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 diff --git a/src/compiler/GF/Compile/GrammarToCanonical.hs b/src/compiler/GF/Compile/GrammarToCanonical.hs index a600573ac..b0e356bc5 100644 --- a/src/compiler/GF/Compile/GrammarToCanonical.hs +++ b/src/compiler/GF/Compile/GrammarToCanonical.hs @@ -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 diff --git a/src/compiler/GF/Compile/Optimize.hs b/src/compiler/GF/Compile/Optimize.hs index 393deb020..ac3fa357c 100644 --- a/src/compiler/GF/Compile/Optimize.hs +++ b/src/compiler/GF/Compile/Optimize.hs @@ -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 diff --git a/src/compiler/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/GF/Compile/TypeCheck/Concrete.hs index 2afff7c6a..380970405 100644 --- a/src/compiler/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/GF/Compile/TypeCheck/Concrete.hs @@ -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 --} diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index b35aaf9ed..c32afa7a5 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -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])]) diff --git a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs b/src/compiler/GF/Compile/TypeCheck/RConcrete.hs deleted file mode 100644 index aa13d5406..000000000 --- a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs +++ /dev/null @@ -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 |