From 3b3979bf42d4320e03c294a4b92835a839b8d728 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Thu, 5 Feb 2026 10:25:04 +0100 Subject: [PATCH] use the same type checker and evaluator for abstract and concrete syntax --- src/compiler/api/GF/Command/SourceCommands.hs | 6 +- src/compiler/api/GF/Compile/CheckGrammar.hs | 69 ++-- .../{Compute/Concrete.hs => Compute.hs} | 25 +- .../api/GF/Compile/Compute/Abstract.hs | 138 -------- src/compiler/api/GF/Compile/GenerateBC.hs | 28 +- src/compiler/api/GF/Compile/GeneratePMCFG.hs | 20 +- .../api/GF/Compile/GrammarToCanonical.hs | 4 +- src/compiler/api/GF/Compile/Rename.hs | 4 +- .../{TypeCheck/Concrete.hs => TypeCheck.hs} | 158 ++++++--- .../api/GF/Compile/TypeCheck/Abstract.hs | 82 ----- src/compiler/api/GF/Compile/TypeCheck/TC.hs | 324 ------------------ src/compiler/api/GF/Grammar.hs | 2 - src/compiler/api/GF/Grammar/Lookup.hs | 34 +- src/compiler/api/GF/Grammar/Printer.hs | 19 - src/compiler/api/GF/Grammar/Unify.hs | 115 ------- src/compiler/api/GF/Grammar/Values.hs | 57 --- src/compiler/api/GF/Interactive.hs | 8 +- src/compiler/gf.cabal | 8 +- 18 files changed, 209 insertions(+), 892 deletions(-) rename src/compiler/api/GF/Compile/{Compute/Concrete.hs => Compute.hs} (98%) delete mode 100644 src/compiler/api/GF/Compile/Compute/Abstract.hs rename src/compiler/api/GF/Compile/{TypeCheck/Concrete.hs => TypeCheck.hs} (93%) delete mode 100644 src/compiler/api/GF/Compile/TypeCheck/Abstract.hs delete mode 100644 src/compiler/api/GF/Compile/TypeCheck/TC.hs delete mode 100644 src/compiler/api/GF/Grammar/Unify.hs delete mode 100644 src/compiler/api/GF/Grammar/Values.hs diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index 6e856645b..024f7c889 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -19,8 +19,8 @@ import GF.Grammar.Analyse import GF.Grammar.ShowTerm import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) -import GF.Compile.Compute.Concrete(normalForm,normalFlatForm,Globals(..),stdPredef) -import GF.Compile.TypeCheck.Concrete as TC(inferLType) +import GF.Compile.Compute(normalForm,normalFlatForm,Globals(..),stdPredef) +import GF.Compile.TypeCheck as TC(inferLType) import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts) import GF.Command.CommandInfo @@ -253,7 +253,7 @@ checkComputeTerm os sgr t = -- ** Try to compute pre{...} tokens in token sequences singleton x = [x] - g = Gl sgr (stdPredef g) + g = Gl sgr (stdPredef g) False evalStr t = case t of diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index 34fc9fa44..b427ce019 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -26,9 +26,8 @@ import Prelude hiding ((<>)) import GF.Infra.Ident import GF.Infra.Option -import GF.Compile.TypeCheck.Abstract -import GF.Compile.TypeCheck.Concrete(checkLType,inferLType) -import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) +import GF.Compile.TypeCheck(checkLType,inferLType,checkContext,checkDef) +import GF.Compile.Compute(normalForm,Globals(..),noPredef,stdPredef) import GF.Grammar import GF.Grammar.Lexer @@ -157,42 +156,43 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do checkReservedId c case info of AbsCat (Just (L loc cont)) -> - mkCheck loc "the category" $ - checkContext gr cont + chIn loc "the category" $ do + cont <- checkContext ga cont + update sm c (AbsCat (Just (L loc cont))) AbsFun (Just (L loc typ)) ma md moper -> do - mkCheck loc "the type of function" $ - checkTyp gr typ - typ <- compAbsTyp [] typ -- to calculate let definitions + chIn loc "the type of function" $ + checkLType ga typ typeType + typ <- normalForm ga typ -- to calculate let definitions case md of - Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $ - checkDef gr (fst sm,c) typ eq) eqs + Just eqs -> mapM_ (\(L loc eq) -> chIn loc "the definition of function" $ + checkDef ga (fst sm,c) typ eq) eqs Nothing -> return () update sm c (AbsFun (Just (L loc typ)) ma md moper) CncCat mty mdef mref mpr mpmcfg -> do mty <- case mty of Just (L loc typ) -> chIn loc "linearization type of" $ do - (typ,_) <- checkLType g typ typeType - typ <- normalForm g typ + (typ,_) <- checkLType gc typ typeType + typ <- normalForm gc typ return (Just (L loc typ)) Nothing -> return Nothing mdef <- case (mty,mdef) of (Just (L _ typ),Just (L loc def)) -> chIn loc "default linearization of" $ do - (def,_) <- checkLType g def (mkFunType [typeStr] typ) + (def,_) <- checkLType gc def (mkFunType [typeStr] typ) return (Just (L loc def)) _ -> return Nothing mref <- case (mty,mref) of (Just (L _ typ),Just (L loc ref)) -> chIn loc "reference linearization of" $ do - (ref,_) <- checkLType g ref (mkFunType [typ] typeStr) + (ref,_) <- checkLType gc ref (mkFunType [typ] typeStr) return (Just (L loc ref)) _ -> return Nothing mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType g t typeStr + (t,_) <- checkLType gc t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncCat mty mdef mref mpr mpmcfg) @@ -201,13 +201,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do mt <- case (mty,mt) of (Just (args,cat,cont,val),Just (L loc trm)) -> chIn loc "linearization of" $ do - (trm,_) <- checkLType g trm (mkFunType (zipWith (\cat (_,_,ty) -> lock cat ty) args cont) val) -- erases arg vars + (trm,_) <- checkLType gc trm (mkFunType (zipWith (\cat (_,_,ty) -> lock cat ty) args cont) val) -- erases arg vars return (Just (L loc (etaExpand [] trm cont))) _ -> return mt mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType g t typeStr + (t,_) <- checkLType gc t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncFun mty mt mpr mpmcfg) @@ -216,14 +216,14 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do (pty', pde') <- case (pty,pde) of (Just (L loct ty), Just (L locd de)) -> do ty' <- chIn loct "operation" $ do - (ty,_) <- checkLType g ty typeType - normalForm g ty + (ty,_) <- checkLType gc ty typeType + normalForm gc ty (de',_) <- chIn locd "operation" $ - checkLType g de ty' + checkLType gc de ty' return (Just (L loct ty'), Just (L locd de')) (Nothing , Just (L locd de)) -> do (de',ty') <- chIn locd "operation" $ - inferLType g de + inferLType gc de return (Just (L locd ty'), Just (L locd de')) (Just (L loct ty), Nothing) -> do chIn loct "operation" $ @@ -231,10 +231,10 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do update sm c (ResOper pty' pde') ResOverload os tysts -> chIn NoLoc "overloading" $ do - tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones + tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gc t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too tysts1 <- sequence - [checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0] + [checkLType gc tr (mkFunType args val) | (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 $ @@ -249,12 +249,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do _ -> return sm where gr = prependModule sgr sm - g = Gl gr (stdPredef g) + ga = Gl gr noPredef True + gc = Gl gr (stdPredef gc) False chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c) mkParamValues sm c cnt ts [] = return (sm,cnt,[],[]) mkParamValues sm@(mn,mi) c cnt ts ((p,co):pcs) = do - co <- mapM (\(b,v,ty) -> normalForm g ty >>= \ty -> return (b,v,ty)) co + co <- mapM (\(b,v,ty) -> normalForm gc ty >>= \ty -> return (b,v,ty)) co sm <- case lookupIdent p (jments mi) of Ok (ResValue (L loc _) _) -> update sm p (ResValue (L loc (mkProdSimple co (QC (mn,c)))) cnt) Bad msg -> checkError (pp msg) @@ -269,22 +270,6 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do | otherwise -> checkUniq $ y:xs _ -> return () - mkCheck loc cat ss = case ss of - [] -> return sm - _ -> chIn loc cat $ checkError (vcat ss) - - compAbsTyp g t = case t of - Vr x -> maybe (checkError ("no value given to variable" <+> x)) return $ lookup x g - Let (x,(_,a)) b -> do - a' <- compAbsTyp g a - compAbsTyp ((x, a'):g) b - Prod b x a t -> do - a' <- compAbsTyp g a - t' <- compAbsTyp ((x,Vr x):g) t - return $ Prod b x a' t' - Abs _ _ _ -> return t - _ -> composOp (compAbsTyp g) t - etaExpand xs t [] = t etaExpand xs (Abs bt x t) (_ :cont) = Abs bt x (etaExpand (x:xs) t cont) etaExpand xs t ((bt,_,ty):cont) = Abs bt x (etaExpand (x:xs) (App t (Vr x)) cont) @@ -331,4 +316,4 @@ linTypeOfType cnc m (L loc typ) = do lookupLincat cnc m c >>= normalForm g ,return defLinType ] - g = Gl cnc (stdPredef g) + g = Gl cnc (stdPredef g) False diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute.hs similarity index 98% rename from src/compiler/api/GF/Compile/Compute/Concrete.hs rename to src/compiler/api/GF/Compile/Compute.hs index 55494815f..719bc5ef5 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute.hs @@ -1,10 +1,10 @@ {-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-} -module GF.Compile.Compute.Concrete +module GF.Compile.Compute (Env, Scope, Value(..), Variants(..), OptionInfo(..), ConstValue(..), Globals(..), PredefTable, EvalM, mapVariantsC, unvariants, - runEvalM, runEvalMWithInput, stdPredef, globals, + runEvalM, runEvalMWithInput, stdPredef, noPredef, globals, PredefImpl, Predef(..), ($\), pdCanonicalArgs, pdArity, normalForm, normalFlatForm, @@ -17,7 +17,7 @@ import GF.Infra.Ident import GF.Infra.CheckM import GF.Data.Operations(Err(..)) import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM,secondM,bimapM) -import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo) +import GF.Grammar.Lookup(lookupAbsDef,lookupResDef,lookupOrigInfo) import GF.Grammar.Grammar import GF.Grammar.Macros import GF.Grammar.Predef @@ -58,7 +58,7 @@ pdArity n def = Predef $ \g c args -> type Env = [(Ident,Value)] type Scope = [(Ident,Value)] type PredefTable = Map.Map Ident Predef -data Globals = Gl Grammar PredefTable +data Globals = Gl Grammar PredefTable Bool {- True for abstract, False for concrete -} data Value = VApp Choice QIdent [Value] @@ -245,11 +245,17 @@ eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs eval g env c (Q q@(m,id)) vs | m == cPredef = evalPredef g c id vs + | isAbstract = let v0 = VApp c q vs + in case lookupAbsDef gr q of + Ok (Just arity,Just eqs) + | length vs < arity -> v0 + | otherwise -> patternMatch g c v0 (map (\(ps,t) -> (env,ps,vs,t)) eqs) + Bad msg -> error msg | otherwise = case lookupResDef gr q of Ok t -> eval g env c t vs Bad msg -> error msg where - Gl gr predef = g + Gl gr predef isAbstract = g eval g env s (QC q) vs = VApp s q vs eval g env s (C t1 t2) [] = let (!s1,!s2) = split s @@ -325,7 +331,7 @@ eval g env c t@(Opts n cs) vs = if null cs eval g env c t vs = VError ("Cannot reduce term" <+> pp t) evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value -evalPredef g@(Gl gr pds) c n args = +evalPredef g@(Gl gr pds _) c n args = case Map.lookup n pds of Nothing -> VApp c (cPredef,n) args Just def -> let valueOf (Const res) = res @@ -335,6 +341,9 @@ evalPredef g@(Gl gr pds) c n args = valueOf NonExist = VApp c (cPredef,cNonExist) [] in valueOf (runPredef def g c args) +noPredef :: PredefTable +noPredef = Map.empty + stdPredef :: Globals -> PredefTable stdPredef g = Map.fromList [(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs})) @@ -540,7 +549,7 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 (pp t)) Bad msg -> error msg where - Gl gr _ = g + Gl gr _ _ = g match env (PV v :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args match env (PAs v p :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args) match env (PW :ps) eqs (arg:args) = match env ps eqs args @@ -651,7 +660,7 @@ vtableSelect g v0 ty cs v2 vs = Ok res -> res Bad msg -> error msg - Gl gr _ = g + Gl gr _ _ = g value2index (VInt n) (VApp _ c [VInt max]) | Q c == cnPredef cInts = Const (fromIntegral n,fromIntegral max+1) value2index (VFV c vs) vty = CFV c (fmap (\v -> value2index v vty) vs) diff --git a/src/compiler/api/GF/Compile/Compute/Abstract.hs b/src/compiler/api/GF/Compile/Compute/Abstract.hs deleted file mode 100644 index 5ba2eeb21..000000000 --- a/src/compiler/api/GF/Compile/Compute/Abstract.hs +++ /dev/null @@ -1,138 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : GF.Compile.Abstract.Compute --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/10/02 20:50:19 $ --- > CVS $Author: aarne $ --- > CVS $Revision: 1.8 $ --- --- computation in abstract syntax w.r.t. explicit definitions. --- --- old GF computation; to be updated ------------------------------------------------------------------------------ - -module GF.Compile.Compute.Abstract (LookDef, - compute, - computeAbsTerm, - computeAbsTermIn, - beta - ) where - -import GF.Data.Operations - -import GF.Grammar -import GF.Grammar.Lookup - -import Debug.Trace -import Data.List(intersperse) -import Control.Monad (liftM, liftM2) -import GF.Text.Pretty - --- for debugging -tracd m t = t --- tracd = trace - -compute :: SourceGrammar -> Term -> Err Term -compute = computeAbsTerm - -computeAbsTerm :: SourceGrammar -> Term -> Err Term -computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) [] - --- | a hack to make compute work on source grammar as well -type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation]) - -computeAbsTermIn :: LookDef -> [Ident] -> Term -> Err Term -computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where - compt vv t = case t of --- Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b) --- Abs x b -> liftM (Abs x) (compt (x:vv) b) - _ -> do - let t' = beta vv t - (yy,f,aa) <- termForm t' - let vv' = map snd yy ++ vv - aa' <- mapM (compt vv') aa - case look f of - Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $ - case findMatch eqs aa' of - Ok (d,g) -> do - --- let (xs,ts) = unzip g - --- ts' <- alphaFreshAll vv' ts - let g' = g --- zip xs ts' - d' <- compt vv' $ substTerm vv' g' d - tracd (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d' - _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $ - do - let v = mkApp f aa' - return $ mkAbs yy $ v - _ -> do - let t2 = mkAbs yy $ mkApp f aa' - tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2 - - look t = case t of - (Q (m,f)) -> case lookd m f of - Ok (_,md) -> md - _ -> Nothing - _ -> Nothing - -beta :: [Ident] -> Exp -> Exp -beta vv c = case c of - Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b) - App f a -> - let (a',f') = (beta vv a, beta vv f) in - case f' of - Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) - _ -> (if a'==a && f'==f then id else beta vv) $ App f' a' - Prod b x a t -> Prod b x (beta vv a) (beta (x:vv) t) - Abs b x t -> Abs b x (beta (x:vv) t) - _ -> c - --- special version of pattern matching, to deal with comp under lambda - -findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution) -findMatch cases terms = case cases of - [] -> Bad $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms))) - (patts,_):_ | length patts /= length terms -> - Bad (render (text "wrong number of args for patterns :" <+> - hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms))) - (patts,val):cc -> case mapM tryMatch (zip patts terms) of - Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 val) val, concat substs) - _ -> findMatch cc terms - -tryMatch :: (Patt, Term) -> Err [(Ident, Term)] -tryMatch (p,t) = do - t' <- termForm t - trym p t' - where - - trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ---- - case (p,t') of - (PW, _) | notMeta t -> return [] -- optimization with wildcard - (PV x, _) | notMeta t -> return [(x,t)] - (PString s, ([],K i,[])) | s==i -> return [] - (PInt s, ([],EInt i,[])) | s==i -> return [] - (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding? - (PP (q,p) pp, ([], QC (r,f), tt)) | - p `eqStrIdent` f && length pp == length tt -> do - matches <- mapM tryMatch (zip pp tt) - return (concat matches) - (PP (q,p) pp, ([], Q (r,f), tt)) | - p `eqStrIdent` f && length pp == length tt -> do - matches <- mapM tryMatch (zip pp tt) - return (concat matches) - (PT _ p',_) -> trym p' t' - (PAs x p',_) -> do - subst <- trym p' t' - return $ (x,t) : subst - _ -> Bad (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t)) - - notMeta e = case e of - Meta _ -> False - App f a -> notMeta f && notMeta a - Abs _ _ b -> notMeta b - _ -> True - - prtm p g = - ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g]) diff --git a/src/compiler/api/GF/Compile/GenerateBC.hs b/src/compiler/api/GF/Compile/GenerateBC.hs index 338c2bf7d..e380ac409 100644 --- a/src/compiler/api/GF/Compile/GenerateBC.hs +++ b/src/compiler/api/GF/Compile/GenerateBC.hs @@ -101,11 +101,11 @@ compileFun gr eval st vs (App e1 e2) h0 bs args = let (h1,bs1,arg,is1) = compileArg gr st vs e2 h0 bs (h2,bs2,is2) = compileFun gr eval st vs e1 h1 bs1 (arg:args) in (h2,bs2,is1++is2) -compileFun gr eval st vs (Q (m,id)) h0 bs args = - case lookupAbsDef gr m id of +compileFun gr eval st vs (Q q@(m,id)) h0 bs args = + case lookupAbsDef gr q of Ok (_,Just _) -> (h0,bs,eval st (GLOBAL (showIdent id)) args) - _ -> let Ok ty = lookupFunType gr m id + _ -> let Ok ty = lookupFunType gr q (ctxt,_,_) = typeForm ty c_arity = length ctxt n_args = length args @@ -164,10 +164,10 @@ compileFun gr eval st vs e@(Glue e1 e2) h0 bs args = in (h1,bs1,[PUSH_ACCUM (LFlt 0)]++is++[POP_ACCUM]++eval (st+1) (ARG_VAR st) []) compileFun gr eval st vs e _ _ _ = error (show e) -compileArg gr st vs (Q(m,id)) h0 bs = - case lookupAbsDef gr m id of +compileArg gr st vs (Q q@(m,id)) h0 bs = + case lookupAbsDef gr q of Ok (_,Just _) -> (h0,bs,GLOBAL (showIdent id),[]) - _ -> let Ok ty = lookupFunType gr m id + _ -> let Ok ty = lookupFunType gr q (ctxt,_,_) = typeForm ty c_arity = length ctxt in if c_arity == 0 @@ -201,17 +201,9 @@ compileArg gr st vs (ImplArg e) h0 bs = compileArg gr st vs e h0 bs compileArg gr st vs e h0 bs = let (f,es) = appForm e - isConstr = case f of - Q c@(m,id) -> case lookupAbsDef gr m id of - Ok (_,Just _) -> Nothing - _ -> Just c - QC c@(m,id) -> case lookupAbsDef gr m id of - Ok (_,Just _) -> Nothing - _ -> Just c - _ -> Nothing - in case isConstr of - Just (m,id) -> - let Ok ty = lookupFunType gr m id + in case f of + QC q@(m,id) -> + let Ok ty = lookupFunType gr q (ctxt,_,_) = typeForm ty c_arity = length ctxt ((h1,bs1,is1),args) = mapAccumL (\(h,bs,is) e -> let (h1,bs1,arg,is1) = compileArg gr st vs e h bs @@ -234,7 +226,7 @@ compileArg gr st vs e h0 bs = EVAL (HEAP h0) (TailCall diff) : [] in (h2,b:bs1,HEAP h1,is1 ++ (PUT_CLOSURE (length bs):is2)) - Nothing -> compileLambda gr st vs [] e h0 bs + _ -> compileLambda gr st vs [] e h0 bs compileLambda gr st vs xs (Abs _ x e) h0 bs = compileLambda gr st vs (x:xs) e h0 bs diff --git a/src/compiler/api/GF/Compile/GeneratePMCFG.hs b/src/compiler/api/GF/Compile/GeneratePMCFG.hs index c2d360927..a6b0f481f 100644 --- a/src/compiler/api/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/api/GF/Compile/GeneratePMCFG.hs @@ -13,7 +13,7 @@ import GF.Grammar.Macros import GF.Grammar.Predef import GF.Grammar.Printer hiding (ppValue) import GF.Text.Pretty hiding (empty) -import GF.Compile.Compute.Concrete hiding ( getMeta, setMeta, globals, variants ) +import GF.Compile.Compute hiding ( getMeta, setMeta, globals, variants ) import qualified GF.Text.Pretty as PP import qualified Data.Map as Map import qualified Data.Set as Set @@ -30,7 +30,7 @@ generatePMCFG :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check S generatePMCFG opts cwd gr cmo@(cm,cmi) | mstatus cmi == MSComplete && isModCnc cmi = do let gr' = prependModule gr cmo - g = Gl gr' (stdPredef g) + g = Gl gr' (stdPredef g) False js <- Map.traverseWithKey (addPMCFG cwd g cmi) (jments cmi) return (cm,cmi{jments = js}) | otherwise = return cmo @@ -55,7 +55,7 @@ addPMCFG cwd g cmi id (CncCat mty@(Just (L loc ty)) mdef mref mprn Nothing) = do return (Just (L loc prn)) return (CncCat mty mdef mref mprn (Just (defs,refs))) where - Gl sgr _ = g + Gl sgr _ _ = g addPMCFG cwd g cmi id (CncFun (Just lty@(cats,cat,ctxt,ty)) mlin@(Just (L loc term)) mprn Nothing) = do rules <- checkInModule cwd cmi loc ("Happened in the rule generation for" <+> id) $ pmcfgForm g term ctxt ty @@ -66,7 +66,7 @@ addPMCFG cwd g cmi id (CncFun (Just lty@(cats,cat,ctxt,ty)) mlin@(Just (L loc te return (Just (L loc prn)) return (CncFun (Just lty) mlin mprn (Just rules)) where - Gl sgr _ = g + Gl sgr _ _ = g addPMCFG cwd g cmi id info = return info @@ -83,9 +83,9 @@ pmcfgForm g t ctxt ty = do qs <- quantifiers (Map.toList subst) return (Rule qs res_params arg_params lin_idx seq) where - Gl sgr _ = g + Gl sgr _ _ = g - quantifiers vars = GenM (\(Gl sgr _) k svs ms -> + quantifiers vars = GenM (\(Gl sgr _ _) k svs ms -> k [boundsOf sgr ms variable | (variable,v) <- sortOn snd vars] svs ms) where @@ -216,7 +216,7 @@ breakDown g ms c r rs v (Table p q) fn0 fn = do v2 = VMeta i [] v0 = VS v v2 [] (c1,c2) = split c - Gl gr _ = g + Gl gr _ _ = g cnt <- countParamValues gr p (ms,r',fn0,fn) <- mfix $ \(~(_,r',_,_)) -> breakDown g (Map.insert i (Narrowing c1 p) ms) c2 r ((r'-r,(v2,p)):rs) (select v0 v v2) q fn0 fn @@ -480,12 +480,12 @@ getMeta i = GenM $ \_ k svs ms r -> setMeta i st = GenM $ \_ k svs ms -> k () svs (Map.insert i st ms) -getCnt ty = GenM $ \(Gl gr _) k svs ms r -> +getCnt ty = GenM $ \(Gl gr _ _) k svs ms r -> case countParamValues gr ty of Ok c -> k c svs ms r Bad msg -> checkError (pp msg) -getIdxCnt q = GenM $ \(Gl gr _) k svs ms r -> +getIdxCnt q = GenM $ \(Gl gr _ _) k svs ms r -> case lookupOrigInfo gr q of Ok (_,ResValue (L _ ty) idx) -> let (ctxt,QC p) = typeFormCnc ty @@ -495,7 +495,7 @@ getIdxCnt q = GenM $ \(Gl gr _) k svs ms r -> Bad msg -> checkError (pp msg) chooseMetaValue :: Choice -> Type -> GenM Value -chooseMetaValue s ptyp = GenM $ \g@(Gl gr _) k svs ms r -> +chooseMetaValue s ptyp = GenM $ \g@(Gl gr _ _) k svs ms r -> case ptyp of _ | Just n <- isTypeInts ptyp -> foldM (\r i -> k (VInt i) svs ms r) r [0..n] QC c -> do (mod,info) <- lookupOrigInfo gr c diff --git a/src/compiler/api/GF/Compile/GrammarToCanonical.hs b/src/compiler/api/GF/Compile/GrammarToCanonical.hs index ced7d309a..b00060a9d 100644 --- a/src/compiler/api/GF/Compile/GrammarToCanonical.hs +++ b/src/compiler/api/GF/Compile/GrammarToCanonical.hs @@ -9,7 +9,7 @@ import GF.Grammar import GF.Grammar.Lookup(allOrigInfos,lookupOrigInfo) import GF.Infra.Option(Options,noOptions) import GF.Infra.CheckM -import GF.Compile.Compute.Concrete +import GF.Compile.Compute import qualified Data.Map as Map import qualified Data.Set as Set import Data.Maybe(mapMaybe,fromMaybe) @@ -81,7 +81,7 @@ type QSet = Set.Set (ModuleName,Ident) -- | Generate Canonical GF for the given concrete module. concrete2canonical :: Grammar -> ModuleName -> ModuleName -> ModuleInfo -> Check (QSet,Module) concrete2canonical gr absname cncname modinfo = do - let g = Gl gr (stdPredef g) + let g = Gl gr (stdPredef g) False infos <- mapM (convInfo g) (allOrigInfos gr cncname) let pts = Set.unions (map fst infos) return (pts, diff --git a/src/compiler/api/GF/Compile/Rename.hs b/src/compiler/api/GF/Compile/Rename.hs index b6233b8f7..99e3570ec 100644 --- a/src/compiler/api/GF/Compile/Rename.hs +++ b/src/compiler/api/GF/Compile/Rename.hs @@ -30,7 +30,6 @@ module GF.Compile.Rename ( import GF.Infra.Ident import GF.Infra.CheckM import GF.Grammar.Grammar -import GF.Grammar.Values import GF.Grammar.Predef import GF.Grammar.Lookup import GF.Grammar.Macros @@ -87,7 +86,7 @@ renameIdentTerm' env@(act,imps) t0 = -- this facility is mainly for BWC with GF1: you need not import PredefAbs predefAbs c s - | isPredefCat c = return (Q (cPredefAbs,c)) + | isPredefCat c = return (QC (cPredefAbs,c)) | otherwise = checkError s ident alt c = @@ -106,6 +105,7 @@ renameIdentTerm' env@(act,imps) t0 = info2status :: Maybe ModuleName -> Ident -> Info -> Term info2status mq c i = case i of + AbsCat _ -> maybe Con (curry QC) mq c AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq c ResValue _ _ -> maybe Con (curry QC) mq c ResParam _ _ -> maybe Con (curry QC) mq c diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck.hs similarity index 93% rename from src/compiler/api/GF/Compile/TypeCheck/Concrete.hs rename to src/compiler/api/GF/Compile/TypeCheck.hs index 3594927ae..f325f8c03 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/api/GF/Compile/TypeCheck.hs @@ -1,5 +1,10 @@ {-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} -module GF.Compile.TypeCheck.Concrete ( checkLType, checkLType', inferLType, inferLType' ) where +module GF.Compile.TypeCheck + ( checkLType, checkLType' + , inferLType, inferLType' + , checkContext + , checkDef + ) where -- The code here is based on the paper: -- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. @@ -11,7 +16,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) import GF.Grammar.Lookup import GF.Grammar.Predef import GF.Grammar.Lockfield -import GF.Compile.Compute.Concrete +import GF.Compile.Compute import GF.Infra.CheckM import GF.Data.ErrM ( Err(Ok, Bad) ) import Control.Applicative(Applicative(..),(<|>)) @@ -59,6 +64,42 @@ inferLType' t = do t <- zonkTerm [] t return (t,vty) +checkContext :: Globals -> Context -> Check Context +checkContext g ctxt = do + res <- runEvalM g $ check [] unit ctxt + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") + where + check scope c [] = return [] + check scope c ((bt,x,ty):ctxt) = do + let (c1,c23) = split c + (c2,c3) = split c23 + (ty,_) <- tcRho scope c1 ty (Just vtypeType) + g <- globals + ctxt <- check ((x,eval g (scopeEnv scope) c2 ty []):scope) c3 ctxt + return ((bt,x,ty):ctxt) + +checkDef :: Globals -> QIdent -> Type -> Equation -> Check Equation +checkDef g q ty (ps,t) = do + let (c1,c23) = split unit + (c2,c3) = split c23 + res <- runEvalM g $ do + (scope,ty) <- go [] c1 (eval g [] c2 ty []) ps + (t,_) <- tcRho scope c3 t (Just ty) + return (ps,t) + case res of + [eq] -> return eq + _ -> checkError (pp "Encountered variants while type checking") + where + go scope c ty [] = return (scope,ty) + go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty + let (c1,c2) = split c + (scope,arg_ty) <- tcPatt scope c1 p (Just arg_ty) + go scope c2 res_ty ps + + -- tcPatt scope c PW Nothing = do + inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma) inferSigma scope s t = do -- GEN1 (t,ty) <- tcRho scope s t Nothing @@ -195,15 +236,15 @@ tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] (body,_) <- tcRho scope c3 body (Just v_ann_ty) instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty -tcRho scope c (FV ts) mb_ty = do +tcRho scope c (FV ts) mb_ty = concreteOnly "Variants" $ do (ts,ty) <- tcUnifying scope c ts mb_ty return (FV ts, ty) tcRho scope s t@(Sort _) mb_ty = do instSigma scope s t vtypeType mb_ty -tcRho scope c t@(RecType rs) Nothing = do +tcRho scope c t@(RecType rs) Nothing = concreteOnly "Record types" $ do (rs,mb_ty) <- tcRecTypeFields scope c rs Nothing return (RecType rs,fromMaybe vtypePType mb_ty) -tcRho scope c t@(RecType rs) (Just ty) = do +tcRho scope c t@(RecType rs) (Just ty) = concreteOnly "Record types" $ do (scope,f,ty') <- skolemise scope ty case ty' of VSort s @@ -217,7 +258,7 @@ tcRho scope c t@(RecType rs) (Just ty) = do "cannot be of type" <+> ppTerm Unqualified 0 ty) (rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty') return (f (RecType rs),ty) -tcRho scope s t@(Table p res) mb_ty = do +tcRho scope s t@(Table p res) mb_ty = concreteOnly "Tables" $ do let (s1,s23) = split s (s2,s3) = split s23 (p, p_ty) <- tcRho scope s1 p (Just vtypePType) @@ -240,7 +281,7 @@ tcRho scope c (S t p) mb_ty = do (t,t_ty) <- tcRho scope c1 t (Just t_ty) (p,_) <- tcRho scope c2 p (Just p_ty) return (S t p, res_ty) -tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables +tcRho scope c (T tt ps) Nothing = concreteOnly "Tables" $ do -- ABS1/AABS1 for tables let (c1,c2) = split c mb_p_ty <- case tt of TRaw -> return Nothing @@ -251,7 +292,7 @@ tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for (ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing p_ty_t <- value2termM True [] p_ty return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) -tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables +tcRho scope c (T tt ps) (Just ty) = concreteOnly "Tables" $ do -- ABS2/AABS2 for tables let (c12,c34) = split c (c3,c4) = split c34 (scope,f,ty') <- skolemise scope ty @@ -266,7 +307,7 @@ tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for (ps,p_ty,res_ty) <- tcCases scope c3 ps (Just p_ty) (Just res_ty) p_ty_t <- value2termM True (scopeVars scope) p_ty return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) -tcRho scope c (V p_ty ts) Nothing = do +tcRho scope c (V p_ty ts) Nothing = concreteOnly "Tables" $ do let (c1,c2,c3,c4) = split4 c (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType) i <- newResiduation scope @@ -279,7 +320,7 @@ tcRho scope c (V p_ty ts) Nothing = do ts <- mapCM go c2 ts g <- globals return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty) -tcRho scope c (V p_ty0 ts) (Just ty) = do +tcRho scope c (V p_ty0 ts) (Just ty) = concreteOnly "Tables" $ do let (c1,c2,c3,c4) = split4 c (scope,f,ty') <- skolemise scope ty (p_ty, res_ty) <- unifyTbl scope ty' @@ -289,13 +330,13 @@ tcRho scope c (V p_ty0 ts) (Just ty) = do unify scope p_ty p_vty0 ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts return (V p_ty0 ts, VTable p_ty res_ty) -tcRho scope c (R rs) Nothing = do +tcRho scope c (R rs) Nothing = concreteOnly "Records" $ do lttys <- inferRecFields scope c [] rs rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys return (R rs, VRecType [(l,True,ty) | (l,t,ty) <- lttys] False ) -tcRho scope c (R rs) (Just ty) = do +tcRho scope c (R rs) (Just ty) = concreteOnly "Records" $ do (scope,f,ty') <- skolemise scope ty case ty' of (VRecType ltys _)->do lttys <- checkRecFields scope c rs [] ltys @@ -315,12 +356,12 @@ tcRho scope c (P t l) mb_ty = do return (VMeta i []) (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True)) return (P t l,l_ty) -tcRho scope c (C t1 t2) mb_ty = do +tcRho scope c (C t1 t2) mb_ty = concreteOnly "String operations" $ do let (c1,c2,c3,c4) = split4 c (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) instSigma scope c3 (C t1 t2) vtypeStr mb_ty -tcRho scope c (Glue t1 t2) mb_ty = do +tcRho scope c (Glue t1 t2) mb_ty = concreteOnly "String operations" $ do let (c1,c2,c3,c4) = split4 c (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) @@ -417,7 +458,7 @@ tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in th tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser tcRho scope c (ExtR t (RecType [(lockLabel cat,[],RecType [])])) mb_ty -tcRho scope c (Alts t ss) mb_ty = do +tcRho scope c (Alts t ss) mb_ty = concreteOnly "String operations" $ do let (c1,c2,c3,c4) = split4 c (t,_) <- tcRho scope c1 t (Just vtypeStr) ss <- mapCM (\c (t1,t2) -> do @@ -427,17 +468,17 @@ tcRho scope c (Alts t ss) mb_ty = do return (t1,t2)) c2 ss instSigma scope c3 (Alts t ss) vtypeStr mb_ty -tcRho scope c (Strs ss) mb_ty = do +tcRho scope c (Strs ss) mb_ty = concreteOnly "String operations" $ do let (c1,c2) = split c ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr) return t) c1 ss instSigma scope c2 (Strs ss) vtypeStrs mb_ty -tcRho scope c (EPattType ty) mb_ty = do +tcRho scope c (EPattType ty) mb_ty = concreteOnly "Pattern types" $ do let (c1,c2) = split c (ty, _) <- tcRho scope c1 ty (Just vtypeType) instSigma scope c2 (EPattType ty) vtypeType mb_ty -tcRho scope c t@(EPatt _ _ p) mb_ty = do +tcRho scope c t@(EPatt _ _ p) mb_ty = concreteOnly "Patterns" $ do (scope,f,mb_ty) <- case mb_ty of Nothing -> return (scope,id,Nothing) Just ty -> do (scope,f,ty) <- skolemise scope ty @@ -447,7 +488,7 @@ tcRho scope c t@(EPatt _ _ p) mb_ty = do (_,ty) <- tcPatt scope c p mb_ty (min,max,p) <- measurePatt p return (f (EPatt min max p), VPattType ty) -tcRho scope c (Markup tag attrs children) mb_ty = do +tcRho scope c (Markup tag attrs children) mb_ty = concreteOnly "Markups" $ do let (c1,c2,c3,c4) = split4 c attrs <- mapCM (\c (id,t) -> do (t,_) <- tcRho scope c t Nothing @@ -456,7 +497,7 @@ tcRho scope c (Markup tag attrs children) mb_ty = do res <- mapCM (\c (L loc child) -> fmap (L loc . fst) (tcRho scope c child Nothing)) c2 children instSigma scope c3 (Markup tag attrs res) vtypeMarkup mb_ty tcRho scope c (Reset ctl mb_ct t qid) mb_ty - | ctl == cConcat || ctl == cConcat' = do + | ctl == cConcat || ctl == cConcat' = concreteOnly "Control operators" $ do let (c1,c23) = split c (c2,c3 ) = split c23 (t,_) <- tcRho scope c1 t Nothing @@ -465,7 +506,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty return (Just ct) Nothing -> return Nothing instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty - | ctl == cOne = do + | ctl == cOne = concreteOnly "Control operators" $ do let (c1,c2) = split c (t,ty) <- tcRho scope c1 t mb_ty (mb_ct,ty) <- case mb_ct of @@ -473,7 +514,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty return (Just ct,ty) Nothing -> return (Nothing,ty) return (Reset ctl mb_ct t qid,ty) - | ctl == cSelect = do + | ctl == cSelect = concreteOnly "Control operators" $ do let (c1,c2) = split c ty <- case mb_ty of Just ty -> return ty @@ -488,7 +529,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty Nothing -> evalError (pp "[select: .. | ..] requires an integer argument") (t,_) <- tcRho scope c1 t (Just rec_ty) return (Reset ctl mb_ct t qid,ty) - | ctl == cFilter = do + | ctl == cFilter = concreteOnly "Control operators" $ do ty <- case mb_ty of Just ty -> return ty Nothing -> do i <- newResiduation scope @@ -501,7 +542,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty Nothing -> return () (t,_) <- tcRho scope c t (Just rec_ty) return (Reset ctl mb_ct t qid,ty) - | ctl == cDefault = do + | ctl == cDefault = concreteOnly "Control operators" $ do let (c1,c2) = split c (t,ty) <- tcRho scope c1 t mb_ty (mb_ct,ty) <- case mb_ct of @@ -509,7 +550,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty return (Just ct,ty) Nothing -> evalError (pp "[list: .. | ..] requires an argument") return (Reset ctl mb_ct t qid,ty) - | ctl == cList = do + | ctl == cList = concreteOnly "Control operators" $ do do let (c1,c2) = split c mb_ct <- case mb_ct of Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing @@ -519,7 +560,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty case ty of VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) - | ctl == cLen = do + | ctl == cLen = concreteOnly "Control operators" $ do do let (c1,c2) = split c (t,_) <- tcRho scope c1 t Nothing case mb_ct of @@ -530,7 +571,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty (ct,_) <- tcRho scope c2 ct (Just (VProd Explicit identW vtypeInt res_ty)) return (Reset ctl (Just ct) t Nothing, res_ty) Nothing -> instSigma scope c2 (Reset ctl Nothing t Nothing) vtypeInt mb_ty - | ctl == cConst = do + | ctl == cConst = concreteOnly "Control operators" $ do let (c1,c2) = split c (t,_) <- tcRho scope c1 t Nothing (mb_ct,ty) <- case mb_ct of @@ -538,8 +579,8 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty return (Just ct,ty) Nothing -> evalError (pp "[list: .. | ..] requires an argument") return (Reset ctl mb_ct t qid,ty) - | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") -tcRho scope s (Opts n cs) mb_ty = do + | otherwise = concreteOnly "Control operators" $ evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") +tcRho scope s (Opts n cs) mb_ty = concreteOnly "Options" $ do let (s1,s2,s3) = split3 s (n,_) <- tcRho scope s1 n Nothing (ls,_) <- tcUnifyingMaybe scope s2 (fst <$> cs) Nothing @@ -547,6 +588,12 @@ tcRho scope s (Opts n cs) mb_ty = do return (Opts n (zip ls ts), ty) tcRho scope s t _ = unimplemented ("tcRho "++show t) +concreteOnly msg f = do + (Gl _ _ isAbstract) <- globals + if isAbstract + then evalError (pp (msg ++ " are not supported in the abstract syntax")) + else f + evalCodomain :: Ident -> Value -> Value -> EvalM Value evalCodomain x v (VClosure env c ty) = do g <- globals @@ -594,8 +641,8 @@ tcCases scope c ((p,t):cs) mb_p_ty mb_res_ty = do return ((p,t):cs,p_ty,res_ty) tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP -tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) -tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) +tcApp scope c t0 t@(Q q) args mb_ty = resolveOverloads scope c t0 q args mb_ty -- VAR (global) +tcApp scope c t0 t@(QC q) args mb_ty = resolveOverloads scope c t0 q args mb_ty -- VAR (global) tcApp scope c t0 t args mb_ty = do let (c1,c23) = split c let (c2,c3) = split c23 @@ -626,22 +673,29 @@ reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) resolveOverloads scope c t0 q args mb_ty = do - g@(Gl gr _) <- globals - case lookupOverloadTypes gr q of - Bad msg -> evalError (pp msg) - Ok [(t,ty)] -> do let (c1,c23) = split c - (c2,c3) = split c23 - (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args - instSigma scope c3 t ty mb_ty - Ok ttys0 -> do let (c1,c23) = split c - (c2,c3) = split c23 - sz <- checkpoint - arg_tys <- mapCM (checkArg g) c1 args - let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys0 - try sz - (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) - (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys0 arg_tys ttys))) - v_ttys + g@(Gl gr _ isAbstract) <- globals + if isAbstract + then case lookupAbsType gr q of + Bad msg -> evalError (pp msg) + Ok ty -> do let (c1,c23) = split c + (c2,c3) = split c23 + (t,ty) <- reapply1 scope c1 t0 (eval g [] c2 ty []) args + instSigma scope c3 t ty mb_ty + else case lookupOverloadTypes gr q of + Bad msg -> evalError (pp msg) + Ok [(t,ty)] -> do let (c1,c23) = split c + (c2,c3) = split c23 + (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args + instSigma scope c3 t ty mb_ty + Ok ttys0 -> do let (c1,c23) = split c + (c2,c3) = split c23 + sz <- checkpoint + arg_tys <- mapCM (checkArg g) c1 args + let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys0 + try sz + (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) + (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys0 arg_tys ttys))) + v_ttys where checkArg g c (ImplArg arg) = do let (c1,c2) = split c @@ -722,8 +776,8 @@ tcPatt scope c (PV x) Nothing = do tcPatt scope c (PV x) (Just ty) = return ((x,ty):scope,ty) tcPatt scope c (PP q ps) mb_ty = do - g@(Gl gr _) <- globals - ty <- case lookupResType gr q of + g@(Gl gr _ isAbstract) <- globals + ty <- case (if isAbstract then lookupFunType else lookupResType) gr q of Ok ty -> return ty Bad msg -> evalError (pp msg) let go scope c ty [] = return (scope,ty) @@ -839,7 +893,7 @@ tcPatt scope c (PAlt p1 p2) mb_ty = do (_,ty) <- tcPatt scope c2 p2 (Just ty) return (scope,ty) tcPatt scope c (PM q) mb_ty = do - g@(Gl gr _) <- globals + g@(Gl gr _ _) <- globals ty <- case lookupResType gr q of Ok ty -> return ty Bad msg -> evalError (pp msg) @@ -1344,8 +1398,8 @@ unify scope (VStr s1) (VStr s2) | s1 == s2 = return () unify scope VEmpty VEmpty = return () unify scope v1 v2 = - evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$ - " with:" <+> ppValue Qualified 0 v2) + evalError ("Cannot unify:" <+> ppValue Unqualified 0 v1 $$ + " with:" <+> ppValue Unqualified 0 v2) -- | Invariant: tv1 is a flexible type variable diff --git a/src/compiler/api/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/api/GF/Compile/TypeCheck/Abstract.hs deleted file mode 100644 index c76660259..000000000 --- a/src/compiler/api/GF/Compile/TypeCheck/Abstract.hs +++ /dev/null @@ -1,82 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : TypeCheck --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/09/15 16:22:02 $ --- > CVS $Author: aarne $ --- > CVS $Revision: 1.16 $ --- --- (Description of the module) ------------------------------------------------------------------------------ - -module GF.Compile.TypeCheck.Abstract (-- * top-level type checking functions; TC should not be called directly. - checkContext, - checkTyp, - checkDef, - checkConstrs, - ) where - -import GF.Data.Operations - -import GF.Infra.CheckM -import GF.Grammar -import GF.Grammar.Lookup -import GF.Grammar.Unify ---import GF.Compile.Refresh ---import GF.Compile.Compute.Abstract -import GF.Compile.TypeCheck.TC - -import GF.Text.Pretty ---import Control.Monad (foldM, liftM, liftM2) - --- | invariant way of creating TCEnv from context -initTCEnv gamma = - (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) - --- interface to TC type checker - -type2val :: Type -> Val -type2val = VClos [] - -cont2exp :: Context -> Term -cont2exp c = mkProd c eType [] -- to check a context - -cont2val :: Context -> Val -cont2val = type2val . cont2exp - --- some top-level batch-mode checkers for the compiler - -justTypeCheck :: SourceGrammar -> Term -> Val -> Err Constraints -justTypeCheck gr e v = do - (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v - (constrs1,_) <- unifyVal constrs0 - return $ filter notJustMeta constrs1 - -notJustMeta (c,k) = case (c,k) of - (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False - _ -> True - -grammar2theory :: SourceGrammar -> Theory -grammar2theory gr (m,f) = case lookupFunType gr m f of - Ok t -> return $ type2val t - Bad s -> case lookupCatContext gr m f of - Ok cont -> return $ cont2val cont - _ -> Bad s - -checkContext :: SourceGrammar -> Context -> [Message] -checkContext st = checkTyp st . cont2exp - -checkTyp :: SourceGrammar -> Type -> [Message] -checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType - -checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message] -checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do - (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ) - (constrs,_) <- unifyVal cs - return $ filter notJustMeta constrs - -checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String] -checkConstrs gr cat _ = [] ---- check constructors! diff --git a/src/compiler/api/GF/Compile/TypeCheck/TC.hs b/src/compiler/api/GF/Compile/TypeCheck/TC.hs deleted file mode 100644 index fb9049aaa..000000000 --- a/src/compiler/api/GF/Compile/TypeCheck/TC.hs +++ /dev/null @@ -1,324 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : TC --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/10/02 20:50:19 $ --- > CVS $Author: aarne $ --- > CVS $Revision: 1.11 $ --- --- Thierry Coquand's type checking algorithm that creates a trace ------------------------------------------------------------------------------ - -module GF.Compile.TypeCheck.TC ( - AExp(..), - Theory, - checkExp, - inferExp, - checkBranch, - eqVal, - whnf - ) where - -import GF.Data.Operations -import GF.Grammar -import GF.Grammar.Predef - -import Control.Monad ---import Data.List (sortBy) -import Data.Maybe -import GF.Text.Pretty - -data AExp = - AVr Ident Val - | ACn QIdent Val - | AType - | AInt Integer - | AFloat Double - | AStr String - | AMeta MetaId Val - | ALet (Ident,(Val,AExp)) AExp - | AApp AExp AExp Val - | AAbs Ident Val AExp - | AProd Ident AExp AExp --- -- | AEqs [([Exp],AExp)] --- not used - | ARecType [ALabelling] - | AR [AAssign] - | AP AExp Label Val - | AGlue AExp AExp - | AData Val - deriving (Eq,Show) - -type ALabelling = (Label, AExp) -type AAssign = (Label, (Val, AExp)) - -type Theory = QIdent -> Err Val - -lookupConst :: Theory -> QIdent -> Err Val -lookupConst th f = th f - -lookupVar :: Env -> Ident -> Err Val -lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g) --- wild card IW: no error produced, ?0 instead. - -type TCEnv = (Int,Env,Env) - ---emptyTCEnv :: TCEnv ---emptyTCEnv = (0,[],[]) - -whnf :: Val -> Err Val -whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug - case v of - VApp u w -> do - u' <- whnf u - w' <- whnf w - app u' w' - VClos env e -> eval env e - _ -> return v - -app :: Val -> Val -> Err Val -app u v = case u of - VClos env (Abs _ x e) -> eval ((x,v):env) e - _ -> return $ VApp u v - -eval :: Env -> Term -> Err Val -eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ - case e of - Vr x -> lookupVar env x - Q c -> return $ VCn c - QC c -> return $ VCn c ---- == Q ? - Sort c -> return $ VType --- the only sort is Type - App f a -> join $ liftM2 app (eval env f) (eval env a) - RecType xs -> do xs <- mapM (\(l,_,e) -> eval env e >>= \e -> return (l,e)) xs - return (VRecType xs) - _ -> return $ VClos env e - -eqVal :: Int -> Val -> Val -> Err [(Val,Val)] -eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ - do - w1 <- whnf u1 - w2 <- whnf u2 - let v = VGen k - case (w1,w2) of - (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2) - (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) -> - eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2) - (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) -> - liftM2 (++) - (eqVal k (VClos env1 a1) (VClos env2 a2)) - (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)) - (VGen i _, VGen j _) -> return [(w1,w2) | i /= j] - (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j] - --- thus ignore qualifications; valid because inheritance cannot - --- be qualified. Simplifies annotation. AR 17/3/2005 - _ -> return [(w1,w2) | w1 /= w2] --- invariant: constraints are in whnf - -checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)]) -checkType th tenv e = checkExp th tenv e vType - -checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) -checkExp th tenv@(k,rho,gamma) e ty = do - typ <- whnf ty - let v = VGen k - case e of - Meta m -> return $ (AMeta m typ,[]) - - Abs _ x t -> case typ of - VClos env (Prod _ y a b) -> do - a' <- whnf $ VClos env a --- - (t',cs) <- checkExp th - (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b) - return (AAbs x a' t', cs) - _ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ)) - - Let (x, (mb_typ, e1)) e2 -> do - (val,e1,cs1) <- case mb_typ of - Just typ -> do (_,cs1) <- checkType th tenv typ - val <- eval rho typ - (e1,cs2) <- checkExp th tenv e1 val - return (val,e1,cs1++cs2) - Nothing -> do (e1,val,cs) <- inferExp th tenv e1 - return (val,e1,cs) - (e2,cs2) <- checkExp th (k,rho,(x,val):gamma) e2 typ - return (ALet (x,(val,e1)) e2, cs1++cs2) - - Prod _ x a b -> do - testErr (typ == vType) "expected Type" - (a',csa) <- checkType th tenv a - (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b - return (AProd x a' b', csa ++ csb) - - R xs -> - case typ of - VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of - [] -> return () - ls -> fail (render ("no value given for label:" <+> fsep (punctuate ',' ls))) - r <- mapM (checkAssign th tenv ys) xs - let (xs,css) = unzip r - return (AR xs, concat css) - _ -> Bad (render ("record type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ)) - - P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)]) - return (AP r' l typ,cs) - - Glue x y -> do cs1 <- eqVal k valAbsFloat typ - (x,cs2) <- checkExp th tenv x typ - (y,cs3) <- checkExp th tenv y typ - return (AGlue x y,cs1++cs2++cs3) - _ -> checkInferExp th tenv e typ - -checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) -checkInferExp th tenv@(k,_,_) e typ = do - (e',w,cs1) <- inferExp th tenv e - cs2 <- eqVal k w typ - return (e',cs1 ++ cs2) - -inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)]) -inferExp th tenv@(k,rho,gamma) e = case e of - Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x - Q (m,c) | m == cPredefAbs && isPredefCat c - -> return (ACn (m,c) vType, vType, []) - | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) - QC c -> mkAnnot (ACn c) $ noConstr $ lookupConst th c ---- - EInt i -> return (AInt i, valAbsInt, []) - EFloat i -> return (AFloat i, valAbsFloat, []) - K i -> return (AStr i, valAbsString, []) - Sort _ -> return (AType, vType, []) - RecType xs -> do r <- mapM (checkLabelling th tenv) xs - let (xs,css) = unzip r - return (ARecType xs, vType, concat css) - Let (x, (mb_typ, e1)) e2 -> do - (val1,e1,cs1) <- case mb_typ of - Just typ -> do (_,cs1) <- checkType th tenv typ - val <- eval rho typ - (e1,cs2) <- checkExp th tenv e1 val - return (val,e1,cs1++cs2) - Nothing -> do (e1,val,cs) <- inferExp th tenv e1 - return (val,e1,cs) - (e2,val2,cs2) <- inferExp th (k,rho,(x,val1):gamma) e2 - return (ALet (x,(val1,e1)) e2, val2, cs1++cs2) - App f t -> do - (f',w,csf) <- inferExp th tenv f - typ <- whnf w - case typ of - VClos env (Prod _ x a b) -> do - (a',csa) <- checkExp th tenv t (VClos env a) - b' <- whnf $ VClos ((x,VClos rho t):env) b - return $ (AApp f' a' b', b', csf ++ csa) - _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ)) - _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e)) - -checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)]) -checkLabelling th tenv (lbl,_,typ) = do - (atyp,cs) <- checkType th tenv typ - return ((lbl,atyp),cs) - -checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)]) -checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do - (atyp,cs1) <- checkType th tenv typ - val <- eval rho typ - cs2 <- case lookup lbl typs of - Nothing -> return [] - Just val0 -> eqVal k val val0 - (aexp,cs3) <- checkExp th tenv exp val - return ((lbl,(val,aexp)),cs1++cs2++cs3) -checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do - case lookup lbl typs of - Nothing -> do (aexp,val,cs) <- inferExp th tenv exp - return ((lbl,(val,aexp)),cs) - Just val -> do (aexp,cs) <- checkExp th tenv exp val - return ((lbl,(val,aexp)),cs) - -checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)]) -checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ - chB tenv' ps' ty - where - - (ps',_,rho2,k') = ps2ts k ps - tenv' = (k, rho2++rho, gamma) ---- k' ? - (k,rho,gamma) = tenv - - chB tenv@(k,rho,gamma) ps ty = case ps of - p:ps2 -> do - typ <- whnf ty - case typ of - VClos env (Prod _ y a b) -> do - a' <- whnf $ VClos env a - (p', sigma, binds, cs1) <- checkP tenv p y a' - let tenv' = (length binds, sigma ++ rho, binds ++ gamma) - ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b) - return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt - _ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ)) - [] -> do - (e,cs) <- checkExp th tenv t ty - return (([],e),cs) - checkP env@(k,rho,gamma) t x a = do - (delta,cs) <- checkPatt th env t a - let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]] - return (VClos sigma t, sigma, delta, cs) - - ps2ts k = foldr p2t ([],0,[],k) - p2t p (ps,i,g,k) = case p of - PW -> (Meta i : ps, i+1,g,k) - PV x -> (Vr x : ps, i, upd x k g,k+1) - PAs x p -> p2t p (ps,i,g,k) - PString s -> (K s : ps, i, g, k) - PInt n -> (EInt n : ps, i, g, k) - PFloat n -> (EFloat n : ps, i, g, k) - PP c xs -> (mkApp (Q c) xss : ps, j, g',k') - where (xss,j,g',k') = foldr p2t ([],i,g,k) xs - PImplArg p -> p2t p (ps,i,g,k) - PTilde t -> (t : ps, i, g, k) - _ -> error $ render ("undefined p2t case" <+> ppPatt Unqualified 0 p <+> "in checkBranch") - - upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables - - -checkPatt :: Theory -> TCEnv -> Term -> Val -> Err (Binds,[(Val,Val)]) -checkPatt th tenv exp val = do - (aexp,_,cs) <- checkExpP tenv exp val - let binds = extrBinds aexp - return (binds,cs) - where - extrBinds aexp = case aexp of - AVr i v -> [(i,v)] - AApp f a _ -> extrBinds f ++ extrBinds a - _ -> [] -- no other cases are possible - ---- ad hoc, to find types of variables - checkExpP tenv@(k,rho,gamma) exp val = case exp of - Meta m -> return $ (AMeta m val, val, []) - Vr x -> return $ (AVr x val, val, []) - EInt i -> return (AInt i, valAbsInt, []) - EFloat i -> return (AFloat i, valAbsFloat, []) - K s -> return (AStr s, valAbsString, []) - - Q c -> do - typ <- lookupConst th c - return $ (ACn c typ, typ, []) - QC c -> do - typ <- lookupConst th c - return $ (ACn c typ, typ, []) ---- - App f t -> do - (f',w,csf) <- checkExpP tenv f val - typ <- whnf w - case typ of - VClos env (Prod _ x a b) -> do - (a',_,csa) <- checkExpP tenv t (VClos env a) - b' <- whnf $ VClos ((x,VClos rho t):env) b - return $ (AApp f' a' b', b', csf ++ csa) - _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ)) - _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp)) - --- auxiliaries - -noConstr :: Err Val -> Err (Val,[(Val,Val)]) -noConstr er = er >>= (\v -> return (v,[])) - -mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)]) -mkAnnot a ti = do - (v,cs) <- ti - return (a v, v, cs) diff --git a/src/compiler/api/GF/Grammar.hs b/src/compiler/api/GF/Grammar.hs index 9c55dfffc..044e00033 100644 --- a/src/compiler/api/GF/Grammar.hs +++ b/src/compiler/api/GF/Grammar.hs @@ -14,7 +14,6 @@ module GF.Grammar ( module GF.Grammar.Grammar, - module GF.Grammar.Values, module GF.Grammar.Macros, module GF.Grammar.Parser, module GF.Grammar.Printer, @@ -23,7 +22,6 @@ module GF.Grammar ) where import GF.Grammar.Grammar -import GF.Grammar.Values import GF.Grammar.Macros import GF.Grammar.Parser import GF.Grammar.Printer diff --git a/src/compiler/api/GF/Grammar/Lookup.hs b/src/compiler/api/GF/Grammar/Lookup.hs index 968127fe5..e67a374a3 100644 --- a/src/compiler/api/GF/Grammar/Lookup.hs +++ b/src/compiler/api/GF/Grammar/Lookup.hs @@ -26,6 +26,7 @@ module GF.Grammar.Lookup ( allParamValues, countParamValues, lookupAbsDef, + lookupAbsType, lookupLincat, lookupFunType, lookupCatContext, @@ -225,12 +226,12 @@ countParamValues gr ptyp = -- to normalize records and record types sortByLbl = sortBy (\(l1,_,_) (l2,_,_) -> compare l1 l2) -lookupAbsDef :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m (Maybe Int,Maybe [Equation]) -lookupAbsDef gr m c = errIn (render ("looking up absdef of" <+> c)) $ do - info <- lookupQIdentInfo gr (m,c) +lookupAbsDef :: ErrorMonad m => Grammar -> QIdent -> m (Maybe Int,Maybe [Equation]) +lookupAbsDef gr q@(m,c) = errIn (render ("looking up absdef of" <+> c)) $ do + info <- lookupQIdentInfo gr q case info of AbsFun _ a d _ -> return (a,fmap (map unLoc) d) - AnyInd _ n -> lookupAbsDef gr n c + AnyInd _ n -> lookupAbsDef gr (n,c) _ -> return (Nothing,Nothing) lookupLincat :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type @@ -243,12 +244,29 @@ lookupLincat gr m c = do _ -> raise (render (c <+> "has no linearization type in" <+> m)) -- | this is needed at compile time -lookupFunType :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type -lookupFunType gr m c = do - info <- lookupQIdentInfo gr (m,c) +lookupAbsType :: ErrorMonad m => Grammar -> QIdent -> m Type +lookupAbsType gr q@(m,c) + | m == cPredefAbs = + if elem c [cInt,cFloat,cString] + then return typeType + else no_type + | otherwise = do + info <- lookupQIdentInfo gr q + case info of + AbsCat (Just (L _ co)) -> return (mkProd co typeType []) + AbsFun (Just (L _ t)) _ _ _ -> return t + AnyInd _ n -> lookupAbsType gr (n,c) + _ -> no_type + where + no_type = raise (render ("cannot find type of" <+> c)) + +-- | this is needed at compile time +lookupFunType :: ErrorMonad m => Grammar -> QIdent -> m Type +lookupFunType gr q@(m,c) = do + info <- lookupQIdentInfo gr q case info of AbsFun (Just (L _ t)) _ _ _ -> return t - AnyInd _ n -> lookupFunType gr n c + AnyInd _ n -> lookupFunType gr (n,c) _ -> raise (render ("cannot find type of" <+> c)) -- | this is needed at compile time diff --git a/src/compiler/api/GF/Grammar/Printer.hs b/src/compiler/api/GF/Grammar/Printer.hs index 0b38ffcda..4f14c6bb4 100644 --- a/src/compiler/api/GF/Grammar/Printer.hs +++ b/src/compiler/api/GF/Grammar/Printer.hs @@ -16,9 +16,7 @@ module GF.Grammar.Printer , ppParams , ppTerm , ppPatt - , ppValue , ppBind - , ppConstrs , ppQIdent , ppMeta , ppLVar @@ -29,7 +27,6 @@ import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import PGF2(Literal(..),pgfFilePath) import GF.Infra.Ident import GF.Infra.Option -import GF.Grammar.Values import GF.Grammar.Predef import GF.Grammar.Grammar @@ -305,22 +302,6 @@ ppPatt q d (PR xs) = braces (hsep (punctuate ';' [l <+> '=' <+> ppPatt q 0 ppPatt q d (PImplArg p) = braces (ppPatt q 0 p) ppPatt q d (PTilde t) = prec d 2 ('~' <> ppTerm q 6 t) -ppValue :: TermPrintQual -> Int -> Val -> Doc -ppValue q d (VGen i x) = x <> "{-" <> i <> "-}" ---- latter part for debugging -ppValue q d (VApp u v) = prec d 4 (ppValue q 4 u <+> ppValue q 5 v) -ppValue q d (VCn (_,c)) = pp c -ppValue q d (VClos env e) = case e of - Meta _ -> ppTerm q d e <> ppEnv env - _ -> ppTerm q d e ---- ++ prEnv env ---- for debugging -ppValue q d (VRecType xs) = braces (hsep (punctuate ',' [l <> '=' <> ppValue q 0 v | (l,v) <- xs])) -ppValue q d VType = pp "Type" - -ppConstrs :: Constraints -> [Doc] -ppConstrs = map (\(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w)) - -ppEnv :: Env -> Doc -ppEnv e = hcat (map (\(x,t) -> braces (x <> ":=" <> ppValue Unqualified 0 t)) e) - str s = doubleQuotes (pp (foldr showLitChar "" s)) where showLitChar c diff --git a/src/compiler/api/GF/Grammar/Unify.hs b/src/compiler/api/GF/Grammar/Unify.hs deleted file mode 100644 index 4446cfb32..000000000 --- a/src/compiler/api/GF/Grammar/Unify.hs +++ /dev/null @@ -1,115 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : Unify --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/04/21 16:22:31 $ --- > CVS $Author: bringert $ --- > CVS $Revision: 1.4 $ --- --- (c) Petri Mäenpää & Aarne Ranta, 1998--2001 --- --- brute-force adaptation of the old-GF program AR 21\/12\/2001 --- --- the only use is in 'TypeCheck.splitConstraints' ------------------------------------------------------------------------------ - -module GF.Grammar.Unify (unifyVal) where - -import GF.Grammar -import GF.Data.Operations - -import GF.Text.Pretty -import Data.List (partition) - -unifyVal :: Constraints -> Err (Constraints,MetaSubst) -unifyVal cs0 = do - let (cs1,cs2) = partition notSolvable cs0 - let (us,vs) = unzip cs2 - let us' = map val2term us - let vs' = map val2term vs - let (ms,cs) = unifyAll (zip us' vs') [] - return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs], - [(m, VClos [] t) | (m,t) <- ms]) - where - notSolvable (v,w) = case (v,w) of -- don't consider nonempty closures - (VClos (_:_) _,_) -> True - (_,VClos (_:_) _) -> True - _ -> False - -type Unifier = [(MetaId, Term)] -type Constrs = [(Term, Term)] - -unifyAll :: Constrs -> Unifier -> (Unifier,Constrs) -unifyAll [] g = (g, []) -unifyAll ((a@(s, t)) : l) g = - let (g1, c) = unifyAll l g - in case unify s t g1 of - Ok g2 -> (g2, c) - _ -> (g1, a : c) - -unify :: Term -> Term -> Unifier -> Err Unifier -unify e1 e2 g = - case (e1, e2) of - (Meta s, t) -> do - tg <- subst_all g t - let sg = maybe e1 id (lookup s g) - if (sg == Meta s) then extend g s tg else unify sg tg g - (t, Meta s) -> unify e2 e1 g - (Q (_,a), Q (_,b)) | (a == b) -> return g ---- qualif? - (QC (_,a), QC (_,b)) | (a == b)-> return g ---- - (Vr x, Vr y) | (x == y) -> return g - (Abs _ x b, Abs _ y c) -> do let c' = substTerm [x] [(y,Vr x)] c - unify b c' g - (App c a, App d b) -> case unify c d g of - Ok g1 -> unify a b g1 - _ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1)) - (RecType xs,RecType ys) | xs == ys -> return g - _ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1)) - -extend :: Unifier -> MetaId -> Term -> Err Unifier -extend g s t | (t == Meta s) = return g - | occCheck s t = Bad (render ("occurs check" <+> ppTerm Unqualified 0 t)) - | True = return ((s, t) : g) - -subst_all :: Unifier -> Term -> Err Term -subst_all s u = - case (s,u) of - ([], t) -> return t - (a : l, t) -> do - t' <- (subst_all l t) --- successive substs - why ? - return $ substMetas [a] t' - -substMetas :: [(MetaId,Term)] -> Term -> Term -substMetas subst trm = case trm of - Meta x -> case lookup x subst of - Just t -> t - _ -> trm - _ -> composSafeOp (substMetas subst) trm - -substTerm :: [Ident] -> Substitution -> Term -> Term -substTerm ss g c = case c of - Vr x -> maybe c id $ lookup x g - App f a -> App (substTerm ss g f) (substTerm ss g a) - Abs b x t -> let y = mkFreshVarX ss x in - Abs b y (substTerm (y:ss) ((x, Vr y):g) t) - Prod b x a t -> let y = mkFreshVarX ss x in - Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t) - _ -> c - -occCheck :: MetaId -> Term -> Bool -occCheck s u = case u of - Meta v -> s == v - App c a -> occCheck s c || occCheck s a - Abs _ x b -> occCheck s b - _ -> False - -val2term :: Val -> Term -val2term v = case v of - VClos g e -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e - VApp f c -> App (val2term f) (val2term c) - VCn c -> Q c - VGen i x -> Vr x - VRecType xs -> RecType (map (\(l,v) -> (l,[],val2term v)) xs) - VType -> typeType diff --git a/src/compiler/api/GF/Grammar/Values.hs b/src/compiler/api/GF/Grammar/Values.hs deleted file mode 100644 index c8fcb3945..000000000 --- a/src/compiler/api/GF/Grammar/Values.hs +++ /dev/null @@ -1,57 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : Values --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/04/21 16:22:32 $ --- > CVS $Author: bringert $ --- > CVS $Revision: 1.7 $ --- --- (Description of the module) ------------------------------------------------------------------------------ - -module GF.Grammar.Values ( - -- ** Values used in TC type checking - Val(..), Env, - -- ** Annotated tree used in editing - Binds, Constraints, MetaSubst, - -- ** For TC - valAbsInt, valAbsFloat, valAbsString, vType, - isPredefCat, - eType, - ) where - -import GF.Infra.Ident -import GF.Grammar.Grammar -import GF.Grammar.Predef - --- values used in TC type checking - -data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term - deriving (Eq,Show) - -type Env = [(Ident,Val)] - -type Binds = [(Ident,Val)] -type Constraints = [(Val,Val)] -type MetaSubst = [(MetaId,Val)] - - --- for TC - -valAbsInt :: Val -valAbsInt = VCn (cPredefAbs, cInt) - -valAbsFloat :: Val -valAbsFloat = VCn (cPredefAbs, cFloat) - -valAbsString :: Val -valAbsString = VCn (cPredefAbs, cString) - -vType :: Val -vType = VType - -eType :: Term -eType = Sort cType diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs index e6f04309d..18071b16a 100644 --- a/src/compiler/api/GF/Interactive.hs +++ b/src/compiler/api/GF/Interactive.hs @@ -13,8 +13,8 @@ import GF.Command.Help(helpCommand) import GF.Command.Abstract import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand) import GF.Compile.Rename(renameSourceTerm) -import GF.Compile.TypeCheck.Concrete(inferLType) -import GF.Compile.Compute.Concrete(stdPredef,normalForm,Globals(..)) +import GF.Compile.TypeCheck(inferLType) +import GF.Compile.Compute(stdPredef,normalForm,Globals(..)) import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields) import GF.Data.Operations (Err(..)) import GF.Data.Utilities(whenM,repeatM) @@ -315,7 +315,7 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do hypos compileLinTerm sgr mo f mb_t ty = do - let g = Gl sgr (stdPredef g) + let g = Gl sgr (stdPredef g) False (t,ty) <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo (Typed t ty) @@ -344,7 +344,7 @@ transactionCommand (CreateLincat opts c mb_t) pgf mb_txnid = do compileLincatTerm sgr mo mb_t = do t <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo t - let g = Gl sgr (stdPredef g) + let g = Gl sgr (stdPredef g) False (t,_) <- inferLType g t return t Nothing -> case lookupResDef sgr (mo,identS c) of diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index 802f58b58..14ba590f3 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -104,7 +104,7 @@ library GF.Command.TreeOperations GF.Compile.CFGtoPGF GF.Compile.CheckGrammar - GF.Compile.Compute.Concrete + GF.Compile.Compute GF.Compile.ExampleBased GF.Compile.Export GF.Compile.GenerateBC @@ -122,9 +122,7 @@ library GF.Compile.SubExOpt GF.Compile.Tags GF.Compile.ToAPI - GF.Compile.TypeCheck.Abstract - GF.Compile.TypeCheck.Concrete - GF.Compile.TypeCheck.TC + GF.Compile.TypeCheck GF.Compile.Update GF.Data.BacktrackM GF.Data.Graph @@ -147,8 +145,6 @@ library GF.Grammar.Predef GF.Grammar.Printer GF.Grammar.ShowTerm - GF.Grammar.Unify - GF.Grammar.Values GF.Grammar.JSON GF.Infra.Concurrency GF.Infra.Dependencies