From 1747b4627499090a0e384761c716ab431665bec8 Mon Sep 17 00:00:00 2001 From: Eve Date: Sun, 26 Jan 2025 00:50:04 +0100 Subject: [PATCH 01/11] Add alex/happy as build tool dependencies, bump up unix version in gf-compiler --- .gitignore | 6 ++++++ src/compiler/api/GF/Interactive.hs | 1 + src/compiler/gf.cabal | 4 +++- 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index aedc1fd42..678397df2 100644 --- a/.gitignore +++ b/.gitignore @@ -56,6 +56,12 @@ DATA_DIR stack*.yaml.lock +# Generated source files +src/compiler/api/GF/Grammar/Lexer.hs +src/compiler/api/GF/Grammar/Parser.hs +src/compiler/api/PackageInfo_gf.hs +src/compiler/api/Paths_gf.hs + # Output files for test suite *.out gf-tests.html diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs index 59d5df5b1..80e60ef8e 100644 --- a/src/compiler/api/GF/Interactive.hs +++ b/src/compiler/api/GF/Interactive.hs @@ -39,6 +39,7 @@ import qualified Data.Sequence as Seq import qualified Text.ParserCombinators.ReadP as RP import System.Directory(getAppUserDataDirectory) import Control.Exception(SomeException,fromException,evaluate,try) +import Control.Monad ((<=<),when,mplus,join) import Control.Monad.State hiding (void) import qualified GF.System.Signal as IO(runInterruptibly) import GF.Command.Messages(welcome) diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index 6135755ab..d33406631 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -70,6 +70,8 @@ library ghc-prim, filepath, directory>=1.2, time, process, haskeline, parallel>=3, json + build-tool-depends: alex:alex >= 3.2.4, + happy:happy >= 1.19.9 exposed-modules: GF.Interactive GF.Compiler @@ -200,7 +202,7 @@ library else build-depends: terminfo >=0.4.0 && < 0.5, - unix >= 2.7.2 && < 2.8 + unix >= 2.7.2 && < 2.9 if flag(server) build-depends: From d9ed763acec45d3c0c064341ffe04101a5461231 Mon Sep 17 00:00:00 2001 From: Eve Date: Sun, 26 Jan 2025 01:13:58 +0100 Subject: [PATCH 02/11] Fix tcApp on pi types, split check/infer into variants inside and outside EvalM --- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 13 +++++++++---- src/compiler/api/GF/Term.hs | 2 +- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index a314aed49..345326d7e 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,5 +1,5 @@ {-# LANGUAGE RankNTypes, CPP #-} -module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where +module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where -- The code here is based on the paper: -- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. @@ -24,14 +24,20 @@ import Data.Maybe(fromMaybe,isNothing) import qualified Control.Monad.Fail as Fail checkLType :: Globals -> Term -> Type -> Check (Term, Type) -checkLType globals t ty = runEvalOneM globals $ do +checkLType globals t ty = runEvalOneM globals (checkLType' t ty) + +checkLType' :: Term -> Type -> EvalM s (Term, Type) +checkLType' t ty = do vty <- eval [] ty [] (t,_) <- tcRho [] t (Just vty) t <- zonkTerm [] t return (t,ty) inferLType :: Globals -> Term -> Check (Term, Type) -inferLType globals t = runEvalOneM globals $ do +inferLType globals t = runEvalOneM globals (inferLType' t) + +inferLType' :: Term -> EvalM s (Term, Type) +inferLType' t = do (t,ty) <- inferSigma [] t t <- zonkTerm [] t ty <- value2term False [] ty @@ -105,7 +111,6 @@ tcRho scope (Abs bt var body) Nothing = do -- ABS1 v2 <- eval ((x,tnk):env) t [] check m (n+1) (b,x:xs) v2 v2 -> check m n st v2 - check m (n+1) (b,x:xs) v2 check m n st (VRecType as) = foldM (\st (l,v) -> check m n st v) st as check m n st (VR as) = foldM (\st (lbl,tnk) -> follow m n st tnk) st as diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs index d9ffc9538..410360ea8 100644 --- a/src/compiler/api/GF/Term.hs +++ b/src/compiler/api/GF/Term.hs @@ -2,7 +2,7 @@ module GF.Term (renameSourceTerm, Globals(..), ConstValue(..), EvalM, stdPredef, Value(..), showValue, Thunk, newThunk, newEvaluatedThunk, evalError, evalWarn, - inferLType, checkLType, + inferLType, inferLType', checkLType, checkLType', normalForm, normalFlatForm, normalStringForm, unsafeIOToEvalM, force ) where From 3b58ccbeef26e4372efbc4133c7e6c76f4cf7576 Mon Sep 17 00:00:00 2001 From: Eve Date: Sun, 26 Jan 2025 01:14:25 +0100 Subject: [PATCH 03/11] Don't evaluate builtins with free variables as arguments --- src/compiler/api/GF/Compile/Compute/Concrete.hs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 7d7d65c7a..3d23d1214 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -207,14 +207,19 @@ eval env (S t1 t2) vs = do v1 <- eval env t1 [] eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1 eval ((x,tnk):env) t2 vs eval env (Q q@(m,id)) vs - | m == cPredef = do vs' <- mapM force vs - res <- evalPredef id vs' - case res of - Const res -> return res - RunTime -> return (VApp q vs) - NonExist -> return (VApp (cPredef,cNonExist) []) + | m == cPredef = do vs' <- mapM force vs -- FIXME this does not allow for partial application! + if any isVar vs' + then return (VApp q vs) + else do res <- evalPredef id vs' + case res of + Const res -> return res + RunTime -> return (VApp q vs) + NonExist -> return (VApp (cPredef,cNonExist) []) | otherwise = do t <- getResDef q eval env t vs + where + isVar (VGen _ _) = True + isVar _ = False eval env (QC q) vs = return (VApp q vs) eval env (C t1 t2) [] = do v1 <- eval env t1 [] v2 <- eval env t2 [] From 8290f79f5235a7c2e15a61ec1f7149f8ca75862b Mon Sep 17 00:00:00 2001 From: Eve Date: Sun, 26 Jan 2025 08:56:37 +0100 Subject: [PATCH 04/11] Rudimentary resource REPL in gf-compiler --- src/compiler/api/GF/Compile/Repl.hs | 132 ++++++++++++++++++++++++++++ src/compiler/gf-repl.hs | 12 +++ src/compiler/gf.cabal | 7 ++ 3 files changed, 151 insertions(+) create mode 100644 src/compiler/api/GF/Compile/Repl.hs create mode 100644 src/compiler/gf-repl.hs diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs new file mode 100644 index 000000000..ec7edf339 --- /dev/null +++ b/src/compiler/api/GF/Compile/Repl.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE LambdaCase #-} + +module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where + +import Control.Monad (unless, forM_) +import Control.Monad.IO.Class (MonadIO) +import Data.Char (isSpace) +import qualified Data.ByteString.Char8 as BS +import qualified Data.Map as Map + +import System.Console.GetOpt (getOpt, ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..)) +import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn) +import System.Directory (getAppUserDataDirectory) + +import GF.Compile (batchCompile) +import GF.Compile.Compute.Concrete (Globals(Gl), normalFlatForm) +import GF.Compile.Rename (renameSourceTerm) +import GF.Compile.TypeCheck.ConcreteNew (inferLType) +import GF.Data.ErrM (Err(..)) +import GF.Grammar.Grammar + ( Grammar + , mGrammar + , Info + , Module + , ModuleName + , ModuleInfo(..) + , ModuleType(MTResource) + , ModuleStatus(MSComplete) + , OpenSpec(OSimple) + , Location (NoLoc) + , Term + , prependModule + ) +import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP) +import GF.Grammar.Parser (pTerm) +import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm) +import GF.Infra.CheckM (Check, runCheck) +import GF.Infra.Ident (moduleNameS) +import GF.Infra.Option (noOptions) +import GF.Text.Pretty (render) + +data ReplOpts = ReplOpts + { noPrelude :: Bool + , inputFiles :: [String] + } + +defaultReplOpts :: ReplOpts +defaultReplOpts = ReplOpts False [] + +replOptDescrs :: [OptDescr (ReplOpts -> ReplOpts)] +replOptDescrs = + [ Option [] ["no-prelude"] (NoArg $ \o -> o { noPrelude = True }) "Don't load the prelude." + ] + +getReplOpts :: [String] -> Either [String] ReplOpts +getReplOpts args = case errs of + [] -> Right $ (foldr ($) defaultReplOpts flags) { inputFiles = inputFiles } + _ -> Left errs + where + (flags, inputFiles, errs) = getOpt RequireOrder [] args + +execCheck :: MonadIO m => Check a -> (a -> InputT m ()) -> InputT m () +execCheck c k = case runCheck c of + Ok (a, warn) -> do + unless (null warn) $ outputStrLn warn + k a + Bad err -> outputStrLn err + +replModNameStr :: String +replModNameStr = "" + +replModName :: ModuleName +replModName = moduleNameS replModNameStr + +parseThen :: MonadIO m => Grammar -> String -> (Term -> InputT m ()) -> InputT m () +parseThen g s k = case runLangP GF pTerm (BS.pack s) of + Left (Pn l c, err) -> outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")" + Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t + +runRepl' :: Globals -> IO () +runRepl' gl@(Gl g _) = do + historyFile <- getAppUserDataDirectory "gfci_history" + runInputT (Settings noCompletion (Just historyFile) True) repl -- TODO tab completion + where + repl = do + getInputLine "gfci> " >>= \case + Nothing -> repl + Just (':' : l) -> let (cmd, arg) = break isSpace l in command cmd (dropWhile isSpace arg) + Just code -> evalPrintLoop code + + command "t" arg = do + parseThen g arg $ \main -> + execCheck (inferLType gl main) $ \(_, ty) -> + outputStrLn $ render (ppTerm Unqualified 0 ty) + outputStrLn "" >> repl + + command "q" _ = outputStrLn "Bye!" + + command cmd _ = do + outputStrLn $ "Unknown REPL command: " ++ cmd + outputStrLn "" >> repl + + evalPrintLoop code = do -- TODO bindings + parseThen g code $ \main -> + execCheck (inferLType gl main >>= \(t, _) -> normalFlatForm gl t) $ \nfs -> + forM_ (zip [1..] nfs) $ \(i, nf) -> + outputStrLn $ show i ++ ". " ++ render (ppTerm Unqualified 0 nf) + outputStrLn "" >> repl + +runRepl :: ReplOpts -> IO () +runRepl (ReplOpts noPrelude inputFiles) = do + -- TODO accept an ngf grammar + -- TODO load prelude + (g0, opens) <- case inputFiles of + [] -> pure (mGrammar [], []) + _ -> do + (_, (pModName, g0)) <- batchCompile noOptions Nothing inputFiles + pure (g0, [OSimple pModName]) + let + modInfo = ModInfo + { mtype = MTResource + , mstatus = MSComplete + , mflags = noOptions + , mextend = [] + , mwith = Nothing + , mopens = opens + , mexdeps = [] + , msrc = replModNameStr + , mseqs = Nothing + , jments = Map.empty + } + runRepl' (Gl (prependModule g0 (replModName, modInfo)) Map.empty) diff --git a/src/compiler/gf-repl.hs b/src/compiler/gf-repl.hs new file mode 100644 index 000000000..7152a212c --- /dev/null +++ b/src/compiler/gf-repl.hs @@ -0,0 +1,12 @@ +import GHC.IO.Encoding (setLocaleEncoding, utf8) + +import System.Environment (getArgs) +import GF.Compile.Repl (getReplOpts, runRepl) + +main :: IO () +main = do + setLocaleEncoding utf8 + args <- getArgs + case getReplOpts args of + Left errs -> mapM_ print errs + Right opts -> runRepl opts diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index d33406631..cdd18f0a8 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -122,6 +122,7 @@ library GF.Grammar.CanonicalJSON GF.Compile.ReadFiles GF.Compile.Rename + GF.Compile.Repl GF.Compile.SubExOpt GF.Compile.Tags GF.Compile.ToAPI @@ -239,6 +240,12 @@ executable gf build-depends: base >= 4.6 && <5, directory>=1.2, gf ghc-options: -threaded +executable gfci + main-is: gf-repl.hs + default-language: Haskell2010 + build-depends: base >= 4.6 && < 5, gf + ghc-options: -threaded + test-suite gf-tests type: exitcode-stdio-1.0 main-is: run.hs From 41cdf5e56aad888e665a65bf0521e3c653bdc6f2 Mon Sep 17 00:00:00 2001 From: Eve Date: Tue, 28 Jan 2025 01:01:13 +0100 Subject: [PATCH 05/11] Load prelude in repl --- src/compiler/api/GF/Compile/Repl.hs | 41 ++++++++++++++++++----------- src/compiler/gf-repl.hs | 2 +- 2 files changed, 26 insertions(+), 17 deletions(-) diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs index ec7edf339..f3b748361 100644 --- a/src/compiler/api/GF/Compile/Repl.hs +++ b/src/compiler/api/GF/Compile/Repl.hs @@ -2,18 +2,20 @@ module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where -import Control.Monad (unless, forM_) +import Control.Monad (unless, forM_, foldM) import Control.Monad.IO.Class (MonadIO) -import Data.Char (isSpace) import qualified Data.ByteString.Char8 as BS +import Data.Char (isSpace) +import Data.Function ((&)) +import Data.Functor ((<&>)) import qualified Data.Map as Map -import System.Console.GetOpt (getOpt, ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..)) +import System.Console.GetOpt (ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..), getOpt, usageInfo) import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn) import System.Directory (getAppUserDataDirectory) import GF.Compile (batchCompile) -import GF.Compile.Compute.Concrete (Globals(Gl), normalFlatForm) +import GF.Compile.Compute.Concrete (Globals(Gl), stdPredef, normalFlatForm) import GF.Compile.Rename (renameSourceTerm) import GF.Compile.TypeCheck.ConcreteNew (inferLType) import GF.Data.ErrM (Err(..)) @@ -37,6 +39,7 @@ import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm) import GF.Infra.CheckM (Check, runCheck) import GF.Infra.Ident (moduleNameS) import GF.Infra.Option (noOptions) +import GF.Infra.UseIO (justModuleName) import GF.Text.Pretty (render) data ReplOpts = ReplOpts @@ -47,17 +50,23 @@ data ReplOpts = ReplOpts defaultReplOpts :: ReplOpts defaultReplOpts = ReplOpts False [] -replOptDescrs :: [OptDescr (ReplOpts -> ReplOpts)] -replOptDescrs = - [ Option [] ["no-prelude"] (NoArg $ \o -> o { noPrelude = True }) "Don't load the prelude." - ] +type Errs a = Either [String] a +type ReplOptsOp = ReplOpts -> Errs ReplOpts -getReplOpts :: [String] -> Either [String] ReplOpts +replOptDescrs :: [OptDescr ReplOptsOp] +replOptDescrs = + [ Option ['h'] ["help"] (NoArg $ \o -> Left [usageInfo "gfci" replOptDescrs]) "Display help." + , Option [] ["no-prelude"] (flag $ \o -> o { noPrelude = True }) "Don't load the prelude." + ] + where + flag f = NoArg $ \o -> pure (f o) + +getReplOpts :: [String] -> Errs ReplOpts getReplOpts args = case errs of - [] -> Right $ (foldr ($) defaultReplOpts flags) { inputFiles = inputFiles } + [] -> foldM (&) defaultReplOpts flags <&> \o -> o { inputFiles = inputFiles } _ -> Left errs where - (flags, inputFiles, errs) = getOpt RequireOrder [] args + (flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args execCheck :: MonadIO m => Check a -> (a -> InputT m ()) -> InputT m () execCheck c k = case runCheck c of @@ -110,12 +119,12 @@ runRepl' gl@(Gl g _) = do runRepl :: ReplOpts -> IO () runRepl (ReplOpts noPrelude inputFiles) = do -- TODO accept an ngf grammar - -- TODO load prelude - (g0, opens) <- case inputFiles of + let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles + (g0, opens) <- case toLoad of [] -> pure (mGrammar [], []) _ -> do - (_, (pModName, g0)) <- batchCompile noOptions Nothing inputFiles - pure (g0, [OSimple pModName]) + (_, (_, g0)) <- batchCompile noOptions Nothing toLoad + pure (g0, OSimple . moduleNameS . justModuleName <$> toLoad) let modInfo = ModInfo { mtype = MTResource @@ -129,4 +138,4 @@ runRepl (ReplOpts noPrelude inputFiles) = do , mseqs = Nothing , jments = Map.empty } - runRepl' (Gl (prependModule g0 (replModName, modInfo)) Map.empty) + runRepl' (Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef)) diff --git a/src/compiler/gf-repl.hs b/src/compiler/gf-repl.hs index 7152a212c..5b890fa9e 100644 --- a/src/compiler/gf-repl.hs +++ b/src/compiler/gf-repl.hs @@ -8,5 +8,5 @@ main = do setLocaleEncoding utf8 args <- getArgs case getReplOpts args of - Left errs -> mapM_ print errs + Left errs -> mapM_ putStrLn errs Right opts -> runRepl opts From 4750ccfb7e8543b4509ead0bdcce2d74ea70261c Mon Sep 17 00:00:00 2001 From: Eve Date: Tue, 4 Feb 2025 13:14:54 +0100 Subject: [PATCH 06/11] Nondeterministic overload resolution in new type checker --- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 107 +++++++++++++----- 1 file changed, 77 insertions(+), 30 deletions(-) diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 345326d7e..1cac75cbf 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, CPP #-} +{-# LANGUAGE RankNTypes, CPP, TupleSections #-} module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where -- The code here is based on the paper: @@ -12,15 +12,16 @@ import GF.Grammar.Predef import GF.Grammar.Lockfield import GF.Compile.Compute.Concrete import GF.Infra.CheckM -import GF.Data.Operations +import GF.Data.ErrM ( Err(Ok, Bad) ) import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM) +import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,when) import Control.Monad.ST import GF.Text.Pretty import Data.STRef import Data.List (nub, (\\), tails) import qualified Data.Map as Map -import Data.Maybe(fromMaybe,isNothing) +import Data.Maybe(fromMaybe,isNothing,mapMaybe) +import Data.Functor((<&>)) import qualified Control.Monad.Fail as Fail checkLType :: Globals -> Term -> Type -> Check (Term, Type) @@ -70,13 +71,13 @@ tcRho scope t@(Vr v) mb_ty = do -- VAR Just v_sigma -> instSigma scope t v_sigma mb_ty Nothing -> evalError ("Unknown variable" <+> v) tcRho scope t@(Q id) mb_ty = do - (t,ty) <- tcApp scope t t + (t,ty) <- tcApp scope t t [] instSigma scope t ty mb_ty tcRho scope t@(QC id) mb_ty = do - (t,ty) <- tcApp scope t t + (t,ty) <- tcApp scope t t [] instSigma scope t ty mb_ty tcRho scope t@(App fun arg) mb_ty = do - (t,ty) <- tcApp scope t t + (t,ty) <- tcApp scope t t [] instSigma scope t ty mb_ty tcRho scope (Abs bt var body) Nothing = do -- ABS1 (i,tnk) <- newResiduation scope @@ -381,21 +382,28 @@ tcCases scope ((p,t):cs) p_ty res_ty = do cs <- tcCases scope cs p_ty res_ty return ((p,t):cs) -tcApp scope t0 t@(App fun (ImplArg arg)) = do -- APP1 - (fun,fun_ty) <- tcApp scope t0 fun +tcApp scope t0 (App fun (ImplArg arg)) args = tcApp scope t0 fun ((arg,False):args) -- APP1 +tcApp scope t0 (App fun arg) args = tcApp scope t0 fun ((arg,True):args) -- APP2 +tcApp scope t0 (Q id) args = resolveOverloads scope t0 id args -- VAR (global) +tcApp scope t0 (QC id) args = resolveOverloads scope t0 id args -- VAR (global) +tcApp scope t0 t args = do + (t,ty) <- tcRho scope t Nothing + reapply scope t ty args + +reapply :: Scope s -> Term -> Constraint s -> [(Term,Bool)] -> EvalM s (Term,Rho s) +reapply scope fun fun_ty [] = return (fun,fun_ty) +reapply scope fun fun_ty ((arg,False):args) = do (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty - if (bt == Implicit) - then return () - else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") + when (bt == Implicit) $ evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") (arg,_) <- tcRho scope arg (Just arg_ty) res_ty <- case res_ty of VClosure res_env res_ty -> do env <- scopeEnv scope tnk <- newThunk env arg eval ((x,tnk):res_env) res_ty [] - res_ty -> return res_ty - return (App fun (ImplArg arg), res_ty) -tcApp scope t0 (App fun arg) = do -- APP2 - (fun,fun_ty) <- tcApp scope t0 fun + res_ty -> return res_ty + reapply scope (App fun (ImplArg arg)) res_ty args +reapply scope fun fun_ty ((arg,True):args) = do (fun,fun_ty) <- instantiate scope fun fun_ty (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty (arg,_) <- tcRho scope arg (Just arg_ty) @@ -404,22 +412,61 @@ tcApp scope t0 (App fun arg) = do -- APP2 tnk <- newThunk env arg eval ((x,tnk):res_env) res_ty [] res_ty -> return res_ty - return (App fun arg, res_ty) -tcApp scope t0 (Q id) = do -- VAR (global) - (t,ty) <- getOverload t0 id - vty <- eval [] ty [] - return (t,vty) -tcApp scope t0 (QC id) = do -- VAR (global) - (t,ty) <- getOverload t0 id - vty <- eval [] ty [] - return (t,vty) -tcApp scope t0 t = tcRho scope t Nothing + reapply scope (App fun arg) res_ty args -tcOverloadFailed t ttys = - evalError ("Overload resolution failed" $$ - "of term " <+> pp t $$ - "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) +resolveOverloads :: Scope s -> Term -> QIdent -> [(Term,Bool)] -> EvalM s (Term,Rho s) +resolveOverloads scope t q args = EvalM $ \gl@(Gl gr _) k mt d r msgs -> + case lookupOverloadTypes gr q of + Bad msg -> return $ Fail (pp msg) msgs + Ok [tty] -> try tty gl k mt d r msgs -- skip overload resolution if there's only one overload + Ok ttys -> do rs <- mapM (\tty -> (tty,) <$> try tty gl k mt d r msgs) ttys + let successes = mapMaybe isSuccess rs + r <- case successes of + [] -> return $ Fail mempty msgs + [(_,r,msgs)] -> return $ Success r msgs + _ -> case unifyOverloads (successes <&> \(tty,_,_) -> tty) of + EvalM f -> f gl k mt d r msgs + return $ case r of + s@(Success _ _) -> s + Fail err msgs -> let h = "Overload resolution failed" $$ + "of term " <+> pp t $$ + "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys] + in Fail (h $+$ err) msgs + where + try (t,ty) = case eval [] ty [] >>= \vty -> reapply scope t vty args of EvalM f -> f + isSuccess (tty, Success r msg) = Just (tty,r,msg) + isSuccess (_, Fail _ _) = Nothing + + unifyOverloads ttys = do + ttys <- forM ttys $ \(t,ty) -> do + vty <- eval [] ty [] + (t,vty) <- papply scope t vty args + return (t,vty) + (_,tnk) <- newResiduation scope + let mv = VMeta tnk [] + mapM_ (\(_,vty) -> unify scope vty mv) ttys + fvty <- force tnk + return (FV (fst <$> ttys), fvty) + + papply scope fun fun_ty [] = return (fun,fun_ty) + papply scope fun (VProd Implicit x arg_ty res_ty) ((arg,False):args) = do + (arg,_) <- tcRho scope arg (Just arg_ty) + res_ty <- case res_ty of + VClosure res_env res_ty -> do env <- scopeEnv scope + tnk <- newThunk env arg + eval ((x,tnk):res_env) res_ty [] + res_ty -> return res_ty + papply scope (App fun (ImplArg arg)) res_ty args + papply scope fun fun_ty ((arg,True):args) = do + (fun,VProd Explicit x arg_ty res_ty) <- instantiate scope fun fun_ty + (arg,_) <- tcRho scope arg (Just arg_ty) + res_ty <- case res_ty of + VClosure res_env res_ty -> do env <- scopeEnv scope + tnk <- newThunk env arg + eval ((x,tnk):res_env) res_ty [] + res_ty -> return res_ty + papply scope (App fun arg) res_ty args tcPatt scope PW ty0 = return scope From 80de452e6db4ab3a890362136b595ebf486fe870 Mon Sep 17 00:00:00 2001 From: Eve Date: Sat, 8 Feb 2025 10:18:28 +0100 Subject: [PATCH 07/11] Fix inverted check in implicit arg app type check, disambiguate implicit args in reapply instead of tcApp --- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 25 +++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 1cac75cbf..8da8d5de7 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete import GF.Infra.CheckM import GF.Data.ErrM ( Err(Ok, Bad) ) import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,when) +import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) import Control.Monad.ST import GF.Text.Pretty import Data.STRef @@ -382,20 +382,19 @@ tcCases scope ((p,t):cs) p_ty res_ty = do cs <- tcCases scope cs p_ty res_ty return ((p,t):cs) -tcApp scope t0 (App fun (ImplArg arg)) args = tcApp scope t0 fun ((arg,False):args) -- APP1 -tcApp scope t0 (App fun arg) args = tcApp scope t0 fun ((arg,True):args) -- APP2 -tcApp scope t0 (Q id) args = resolveOverloads scope t0 id args -- VAR (global) -tcApp scope t0 (QC id) args = resolveOverloads scope t0 id args -- VAR (global) +tcApp scope t0 (App fun arg) args = tcApp scope t0 fun (arg:args) -- APP +tcApp scope t0 (Q id) args = resolveOverloads scope t0 id args -- VAR (global) +tcApp scope t0 (QC id) args = resolveOverloads scope t0 id args -- VAR (global) tcApp scope t0 t args = do (t,ty) <- tcRho scope t Nothing reapply scope t ty args -reapply :: Scope s -> Term -> Constraint s -> [(Term,Bool)] -> EvalM s (Term,Rho s) +reapply :: Scope s -> Term -> Constraint s -> [Term] -> EvalM s (Term,Rho s) reapply scope fun fun_ty [] = return (fun,fun_ty) -reapply scope fun fun_ty ((arg,False):args) = do +reapply scope fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty - when (bt == Implicit) $ evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> - "is an implicit argument application, but no implicit argument is expected") + unless (bt == Implicit) $ evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") (arg,_) <- tcRho scope arg (Just arg_ty) res_ty <- case res_ty of VClosure res_env res_ty -> do env <- scopeEnv scope @@ -403,7 +402,7 @@ reapply scope fun fun_ty ((arg,False):args) = do eval ((x,tnk):res_env) res_ty [] res_ty -> return res_ty reapply scope (App fun (ImplArg arg)) res_ty args -reapply scope fun fun_ty ((arg,True):args) = do +reapply scope fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case (fun,fun_ty) <- instantiate scope fun fun_ty (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty (arg,_) <- tcRho scope arg (Just arg_ty) @@ -414,7 +413,7 @@ reapply scope fun fun_ty ((arg,True):args) = do res_ty -> return res_ty reapply scope (App fun arg) res_ty args -resolveOverloads :: Scope s -> Term -> QIdent -> [(Term,Bool)] -> EvalM s (Term,Rho s) +resolveOverloads :: Scope s -> Term -> QIdent -> [Term] -> EvalM s (Term,Rho s) resolveOverloads scope t q args = EvalM $ \gl@(Gl gr _) k mt d r msgs -> case lookupOverloadTypes gr q of Bad msg -> return $ Fail (pp msg) msgs @@ -450,7 +449,7 @@ resolveOverloads scope t q args = EvalM $ \gl@(Gl gr _) k mt d r msgs -> return (FV (fst <$> ttys), fvty) papply scope fun fun_ty [] = return (fun,fun_ty) - papply scope fun (VProd Implicit x arg_ty res_ty) ((arg,False):args) = do + papply scope fun (VProd Implicit x arg_ty res_ty) ((ImplArg arg):args) = do -- Implicit arg case (arg,_) <- tcRho scope arg (Just arg_ty) res_ty <- case res_ty of VClosure res_env res_ty -> do env <- scopeEnv scope @@ -458,7 +457,7 @@ resolveOverloads scope t q args = EvalM $ \gl@(Gl gr _) k mt d r msgs -> eval ((x,tnk):res_env) res_ty [] res_ty -> return res_ty papply scope (App fun (ImplArg arg)) res_ty args - papply scope fun fun_ty ((arg,True):args) = do + papply scope fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case (fun,VProd Explicit x arg_ty res_ty) <- instantiate scope fun fun_ty (arg,_) <- tcRho scope arg (Just arg_ty) res_ty <- case res_ty of From b4b9974d54198fbabc11f044a3d09d076766b227 Mon Sep 17 00:00:00 2001 From: Eve Date: Sun, 9 Feb 2025 16:53:03 +0100 Subject: [PATCH 08/11] More comprehensive open term check for builtin eval --- .../api/GF/Compile/Compute/Concrete.hs | 49 +++++++++++++++---- src/compiler/api/GF/Data/Utilities.hs | 21 +++++++- 2 files changed, 59 insertions(+), 11 deletions(-) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 3d23d1214..0732da17e 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -26,6 +26,7 @@ import GF.Grammar.Predef import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Printer import GF.Data.Operations(Err(..)) +import GF.Data.Utilities((<||>),anyM) import GF.Infra.CheckM import GF.Infra.Option import Data.STRef @@ -142,6 +143,37 @@ showValue (VAlts _ _) = "VAlts" showValue (VStrs _) = "VStrs" showValue (VSymCat _ _ _) = "VSymCat" +isOpen :: [Ident] -> Term -> EvalM s Bool +isOpen bound (Vr x) = return $ x `notElem` bound +isOpen bound (App f x) = isOpen bound f <||> isOpen bound x +isOpen bound (Abs b x t) = isOpen (x:bound) t +isOpen bound (ImplArg t) = isOpen bound t +isOpen bound (Prod b x d cod) = isOpen bound d <||> isOpen (x:bound) cod +isOpen bound (Typed t ty) = isOpen bound t +isOpen bound (Example t s) = isOpen bound t +isOpen bound (RecType fs) = anyM (isOpen bound . snd) fs +isOpen bound (R fs) = anyM (isOpen bound . snd . snd) fs +isOpen bound (P t f) = isOpen bound t +isOpen bound (ExtR t t') = isOpen bound t <||> isOpen bound t' +isOpen bound (Table d cod) = isOpen bound d <||> isOpen bound cod +isOpen bound (T (TTyped ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs +isOpen bound (T (TWild ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs +isOpen bound (T _ cs) = anyM (isOpen bound . snd) cs +isOpen bound (V ty cs) = isOpen bound ty <||> anyM (isOpen bound) cs +isOpen bound (S t x) = isOpen bound t <||> isOpen bound x +isOpen bound (Let (x,(ty,d)) t) = isOpen bound d <||> isOpen (x:bound) t +isOpen bound (C t t') = isOpen bound t <||> isOpen bound t' +isOpen bound (Glue t t') = isOpen bound t <||> isOpen bound t' +isOpen bound (EPattType ty) = isOpen bound ty +isOpen bound (ELincat c ty) = isOpen bound ty +isOpen bound (ELin c t) = isOpen bound t +isOpen bound (FV ts) = anyM (isOpen bound) ts +isOpen bound (Markup tag as ts) = anyM (isOpen bound) ts <||> anyM (isOpen bound . snd) as +isOpen bound (Reset c t) = isOpen bound t +isOpen bound (Alts d as) = isOpen bound d <||> anyM (\(x,y) -> isOpen bound x <||> isOpen bound y) as +isOpen bound (Strs ts) = anyM (isOpen bound) ts +isOpen _ _ = return False + eval env (Vr x) vs = do (tnk,depth) <- lookup x env withVar depth $ do v <- force tnk @@ -208,18 +240,15 @@ eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1 eval ((x,tnk):env) t2 vs eval env (Q q@(m,id)) vs | m == cPredef = do vs' <- mapM force vs -- FIXME this does not allow for partial application! - if any isVar vs' - then return (VApp q vs) - else do res <- evalPredef id vs' - case res of - Const res -> return res - RunTime -> return (VApp q vs) - NonExist -> return (VApp (cPredef,cNonExist) []) + open <- anyM (value2term True [] >=> isOpen []) vs' + if open then return (VApp q vs) else do + res <- evalPredef id vs' + case res of + Const res -> return res + RunTime -> return (VApp q vs) + NonExist -> return (VApp (cPredef,cNonExist) []) | otherwise = do t <- getResDef q eval env t vs - where - isVar (VGen _ _) = True - isVar _ = False eval env (QC q) vs = return (VApp q vs) eval env (C t1 t2) [] = do v1 <- eval env t1 [] v2 <- eval env t2 [] diff --git a/src/compiler/api/GF/Data/Utilities.hs b/src/compiler/api/GF/Data/Utilities.hs index 913953b6e..1faa0b4ac 100644 --- a/src/compiler/api/GF/Data/Utilities.hs +++ b/src/compiler/api/GF/Data/Utilities.hs @@ -16,7 +16,7 @@ module GF.Data.Utilities(module GF.Data.Utilities) where import Data.Maybe import Data.List -import Control.Monad (MonadPlus(..),liftM,when) +import Control.Monad (MonadPlus(..),foldM,liftM,when) import qualified Data.Set as Set -- * functions on lists @@ -140,6 +140,25 @@ whenM bm m = flip when m =<< bm repeatM m = whenM m (repeatM m) +infixr 3 <&&> +infixr 2 <||> + +-- | Boolean conjunction lifted to applicative functors. +(<&&>) :: Applicative f => f Bool -> f Bool -> f Bool +(<&&>) = liftA2 (&&) + +-- | Boolean disjunction lifted to applicative functors. +(<||>) :: Applicative f => f Bool -> f Bool -> f Bool +(<||>) = liftA2 (||) + +-- | Check whether a monadic predicate holds for every element of a collection. +allM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool +allM p = foldM (\b x -> if b then p x else return False) True + +-- | Check whether a monadic predicate holds for any element of a collection. +anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool +anyM p = foldM (\b x -> if b then return True else p x) False + -- * functions on Maybes -- | Returns true if the argument is Nothing or Just [] From 265db698ac1d65de6b456de3f5cde20eba3fd5b0 Mon Sep 17 00:00:00 2001 From: Eve Date: Sat, 15 Feb 2025 22:27:06 +0100 Subject: [PATCH 09/11] Dereference metavariables in types before structural inspections --- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 8da8d5de7..450aa3a26 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, CPP, TupleSections #-} +{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where -- The code here is based on the paper: @@ -943,6 +943,10 @@ instantiate scope t (VProd Implicit x ty1 ty2) = do VClosure env ty2 -> eval ((x,tnk):env) ty2 [] ty2 -> return ty2 instantiate scope (App t (ImplArg (Meta i))) ty2 +instantiate scope t ty@(VMeta thk args) = getRef thk >>= \case + Evaluated _ v -> instantiate scope t v + Residuation _ _ (Just v) -> instantiate scope t v + _ -> return (t,ty) -- We don't have enough information to try any instantiation instantiate scope t ty = do return (t,ty) @@ -1121,9 +1125,10 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys | m `elem` acc = return acc | otherwise = do res <- getRef m case res of - Evaluated _ v -> go v acc - Residuation _ _ Nothing -> foldM follow (m:acc) args - _ -> return acc + Evaluated _ v -> go v acc + Residuation _ _ Nothing -> foldM follow (m:acc) args + Residuation _ _ (Just v) -> go v acc + _ -> return acc go (VApp f args) acc = foldM follow acc args go v acc = unimplemented ("go "++showValue v) From 815dfcc2fc9c8ece204b1fe76e9ec6ab48f4adb8 Mon Sep 17 00:00:00 2001 From: Eve Date: Sat, 15 Feb 2025 23:07:11 +0100 Subject: [PATCH 10/11] Unification for function types --- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 450aa3a26..f4ceef45d 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -154,19 +154,13 @@ tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 if bt == Implicit then return () else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") - body_ty <- case body_ty of - VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) []) - eval ((x,tnk):env) body_ty [] - body_ty -> return body_ty + body_ty <- evalCodomain scope x body_ty (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (Abs Implicit var body,ty) tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 (scope,f,ty') <- skolemise scope ty (_,x,var_ty,body_ty) <- unifyFun scope ty' - body_ty <- case body_ty of - VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) []) - eval ((x,tnk):env) body_ty [] - body_ty -> return body_ty + body_ty <- evalCodomain scope x body_ty (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) tcRho scope (Meta _) mb_ty = do @@ -375,6 +369,12 @@ tcRho scope (Reset c t) mb_ty = do instSigma scope (Reset c t) vtypeMarkup mb_ty tcRho scope t _ = unimplemented ("tcRho "++show t) +evalCodomain :: Scope s -> Ident -> Value s -> EvalM s (Constraint s) +evalCodomain scope x (VClosure env t) = do + tnk <- newEvaluatedThunk (VGen (length scope) []) + eval ((x,tnk):env) t [] +evalCodomain scope x t = return t + tcCases scope [] p_ty res_ty = return [] tcCases scope ((p,t):cs) p_ty res_ty = do scope' <- tcPatt scope p p_ty @@ -632,10 +632,7 @@ subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC subsCheckRho scope (App t (ImplArg (Meta i))) ty2 rho2 subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL let v = newVar scope - ty2 <- case ty2 of - VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) []) - eval ((x,tnk):env) ty2 [] - ty2 -> return ty2 + ty2 <- evalCodomain scope x ty2 t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 return (Abs Implicit v t) subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN @@ -830,6 +827,12 @@ unify scope (VMeta i vs) v = unifyVar scope i vs v unify scope v (VMeta i vs) = unifyVar scope i vs v unify scope (VGen i vs1) (VGen j vs2) | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) +unify scope (VProd b x d cod) (VProd b' x' d' cod') + | b == b' = do + unify scope d d' + cod <- evalCodomain scope x cod + cod' <- evalCodomain scope x' cod' + unify scope cod cod' unify scope (VTable p1 res1) (VTable p2 res2) = do unify scope p2 p1 unify scope res1 res2 @@ -960,10 +963,7 @@ skolemise scope ty@(VMeta i vs) = do skolemise scope ty skolemise scope (VProd Implicit x ty1 ty2) = do let v = newVar scope - ty2 <- case ty2 of - VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) []) - eval ((x,tnk) : env) ty2 [] - ty2 -> return ty2 + ty2 <- evalCodomain scope x ty2 (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 return (scope,Abs Implicit v . f,ty2) skolemise scope ty = do From 19c5b410f258d60b0ec247ec1e6afc96281e5305 Mon Sep 17 00:00:00 2001 From: Eve Date: Fri, 21 Feb 2025 11:05:23 +0100 Subject: [PATCH 11/11] Predef combinators --- .../api/GF/Compile/Compute/Concrete.hs | 128 +++++++++++++----- src/compiler/api/GF/Data/Utilities.hs | 9 ++ 2 files changed, 103 insertions(+), 34 deletions(-) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 0732da17e..24b92244b 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -1,11 +1,13 @@ -{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-} +{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification, LambdaCase #-} -- | Functions for computing the values of terms in the concrete syntax, in -- | preparation for PMCFG generation. module GF.Compile.Compute.Concrete ( normalForm, normalFlatForm, normalStringForm , Value(..), Thunk, ThunkState(..), Env, Scope, showValue - , MetaThunks, Constraint, Globals(..), ConstValue(..) + , PredefImpl, Predef(..), PredefCombinator, ($\) + , pdForce, pdClosedArgs, pdArity, pdStandard + , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..) , EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn , eval, apply, force, value2term, patternMatch, stdPredef , unsafeIOToEvalM @@ -26,7 +28,7 @@ import GF.Grammar.Predef import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Printer import GF.Data.Operations(Err(..)) -import GF.Data.Utilities((<||>),anyM) +import GF.Data.Utilities(splitAt',(<||>),anyM) import GF.Infra.CheckM import GF.Infra.Option import Data.STRef @@ -238,15 +240,12 @@ eval env (S t1 t2) vs = do v1 <- eval env t1 [] v1 -> return v0 eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1 eval ((x,tnk):env) t2 vs -eval env (Q q@(m,id)) vs - | m == cPredef = do vs' <- mapM force vs -- FIXME this does not allow for partial application! - open <- anyM (value2term True [] >=> isOpen []) vs' - if open then return (VApp q vs) else do - res <- evalPredef id vs' - case res of - Const res -> return res - RunTime -> return (VApp q vs) - NonExist -> return (VApp (cPredef,cNonExist) []) +eval env t@(Q q@(m,id)) vs + | m == cPredef = do res <- evalPredef env t id vs + case res of + Const res -> return res + RunTime -> return (VApp q vs) + NonExist -> return (VApp (cPredef,cNonExist) []) | otherwise = do t <- getResDef q eval env t vs eval env (QC q) vs = return (VApp q vs) @@ -326,25 +325,25 @@ apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs apply v [] = return v -stdPredef :: Map.Map Ident ([Value s] -> EvalM s (ConstValue (Value s))) +stdPredef :: PredefTable s stdPredef = Map.fromList - [(cLength, \[v] -> case value2string v of - Const s -> return (Const (VInt (genericLength s))) - _ -> return RunTime) - ,(cTake, \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2)))) - ,(cDrop, \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2)))) - ,(cTk, \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2)))) - ,(cDp, \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2)))) - ,(cIsUpper,\[v] -> return (fmap toPBool (liftA (all isUpper) (value2string v)))) - ,(cToUpper,\[v] -> return (fmap string2value (liftA (map toUpper) (value2string v)))) - ,(cToLower,\[v] -> return (fmap string2value (liftA (map toLower) (value2string v)))) - ,(cEqStr, \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2)))) - ,(cOccur, \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2)))) - ,(cOccurs, \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2)))) - ,(cEqInt, \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2)))) - ,(cLessInt,\[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2)))) - ,(cPlus, \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2)))) - ,(cError, \[v] -> case value2string v of + [(cLength, pdStandard 1 $\ \[v] -> case value2string v of + Const s -> return (Const (VInt (genericLength s))) + _ -> return RunTime) + ,(cTake, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2)))) + ,(cDrop, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2)))) + ,(cTk, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2)))) + ,(cDp, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2)))) + ,(cIsUpper,pdStandard 1 $\ \[v] -> return (fmap toPBool (liftA (all isUpper) (value2string v)))) + ,(cToUpper,pdStandard 1 $\ \[v] -> return (fmap string2value (liftA (map toUpper) (value2string v)))) + ,(cToLower,pdStandard 1 $\ \[v] -> return (fmap string2value (liftA (map toLower) (value2string v)))) + ,(cEqStr, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2)))) + ,(cOccur, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2)))) + ,(cOccurs, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2)))) + ,(cEqInt, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2)))) + ,(cLessInt,pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2)))) + ,(cPlus, pdStandard 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2)))) + ,(cError, pdStandard 1 $\ \[v] -> case value2string v of Const msg -> fail msg _ -> fail "Indescribable error appeared") ] @@ -705,6 +704,16 @@ instance Applicative ConstValue where liftA2 f _ RunTime = RunTime #endif +instance Foldable ConstValue where + foldr f a (Const x) = f x a + foldr f a RunTime = a + foldr f a NonExist = a + +instance Traversable ConstValue where + traverse f (Const x) = Const <$> f x + traverse f RunTime = pure RunTime + traverse f NonExist = pure NonExist + value2string v = fmap (\(_,ws,_) -> unwords ws) (value2string' v False [] []) value2string' (VStr w1) True (w2:ws) qs = Const (False,(w1++w2):ws,qs) @@ -762,12 +771,63 @@ string2value' (w:ws) = VC (VStr w) (string2value' ws) value2int (VInt n) = Const n value2int _ = RunTime +----------------------------------------------------------------------- +-- * Global/built-in definitions + +type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s)) +newtype Predef a s = Predef { runPredef :: Term -> Env s -> PredefImpl a s } +type PredefCombinator a b s = Predef a s -> Predef b s + +infix 0 $\\ + +($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s +k $\ f = k (Predef (\_ _ -> f)) + +pdForce :: PredefCombinator (Value s) (Thunk s) s +pdForce def = Predef $ \h env args -> do + argValues <- mapM force args + runPredef def h env argValues + +pdClosedArgs :: PredefCombinator (Value s) (Value s) s +pdClosedArgs def = Predef $ \h env args -> do + open <- anyM (value2term True [] >=> isOpen []) args + if open then return RunTime else runPredef def h env args + +pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s +pdArity n def = Predef $ \h env args -> + case splitAt' n args of + Nothing -> do + t <- papply env h args + let t' = abstract 0 (n - length args) t + Const <$> eval env t' [] + Just (usedArgs, remArgs) -> do + res <- runPredef def h env usedArgs + forM res $ \v -> case remArgs of + [] -> return v + _ -> do + t <- value2term False (fst <$> env) v + eval env t remArgs + where + papply env t [] = return t + papply env t (arg:args) = do + arg <- tnk2term False (fst <$> env) arg + papply env (App t arg) args + + abstract i n t + | n <= 0 = t + | otherwise = let x = identV (rawIdentS "a") i + in Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x))) + +pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s +pdStandard n = pdArity n . pdForce . pdClosedArgs + ----------------------------------------------------------------------- -- * Evaluation monad type MetaThunks s = Map.Map MetaId (Thunk s) type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message]) -data Globals = Gl Grammar (forall s . Map.Map Ident ([Value s] -> EvalM s (ConstValue (Value s)))) +type PredefTable s = Map.Map Ident (Predef (Thunk s) s) +data Globals = Gl Grammar (forall s . PredefTable s) newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> Cont s r) instance Functor (EvalM s) where @@ -826,9 +886,9 @@ evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs)) evalWarn :: Message -> EvalM s () evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs)) -evalPredef :: Ident -> [Value s] -> EvalM s (ConstValue (Value s)) -evalPredef id vs = EvalM (\globals@(Gl _ predef) k mt d r msgs -> - case fmap (\f -> f vs) (Map.lookup id predef) of +evalPredef :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s)) +evalPredef env h id args = EvalM (\globals@(Gl _ predef) k mt d r msgs -> + case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of Just (EvalM f) -> f globals k mt d r msgs Nothing -> k RunTime mt d r msgs) diff --git a/src/compiler/api/GF/Data/Utilities.hs b/src/compiler/api/GF/Data/Utilities.hs index 1faa0b4ac..5b3c99a2d 100644 --- a/src/compiler/api/GF/Data/Utilities.hs +++ b/src/compiler/api/GF/Data/Utilities.hs @@ -14,6 +14,7 @@ module GF.Data.Utilities(module GF.Data.Utilities) where +import Data.Bifunctor (first) import Data.Maybe import Data.List import Control.Monad (MonadPlus(..),foldM,liftM,when) @@ -45,6 +46,14 @@ splitBy p [] = ([], []) splitBy p (a : as) = if p a then (a:xs, ys) else (xs, a:ys) where (xs, ys) = splitBy p as +splitAt' :: Int -> [a] -> Maybe ([a], [a]) +splitAt' n xs + | n <= 0 = Just ([], xs) + | otherwise = helper n xs + where helper 0 xs = Just ([], xs) + helper n [] = Nothing + helper n (x:xs) = first (x:) <$> helper (n - 1) xs + foldMerge :: (a -> a -> a) -> a -> [a] -> a foldMerge merge zero = fm where fm [] = zero