msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Merge pull request #173 from phantamanta44/majestic

Browse Source 
majestic: Type-checking improvements + unifying overload resolution + simple REPL
This commit is contained in:
Krasimir Angelov
2025-02-25 13:05:00 +01:00
committed by GitHub
parent ac427d63f2 19c5b410f2
commit a501784a32
9 changed files with 430 additions and 83 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
.gitignore vendored
View File

@@ -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

148
src/compiler/api/GF/Compile/Compute/Concrete.hs
View File

@@ -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,6 +28,7 @@ import GF.Grammar.Predef
import GF.Grammar.Lockfield(lockLabel)
import GF.Grammar.Printer
import GF.Data.Operations(Err(..))
import GF.Data.Utilities(splitAt',(<||>),anyM)
import GF.Infra.CheckM
import GF.Infra.Option
import Data.STRef
@@ -142,6 +145,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
@@ -206,9 +240,8 @@ 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
res <- evalPredef id vs'
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)
@@ -292,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")
]
@@ -671,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)
@@ -728,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
@@ -792,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)

141
src/compiler/api/GF/Compile/Repl.hs Normal file
View File

@@ -0,0 +1,141 @@
{-# LANGUAGE LambdaCase #-}
module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where
import Control.Monad (unless, forM_, foldM)
import Control.Monad.IO.Class (MonadIO)
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 (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), stdPredef, 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.Infra.UseIO (justModuleName)
import GF.Text.Pretty (render)
data ReplOpts = ReplOpts
{ noPrelude :: Bool
, inputFiles :: [String]
}
defaultReplOpts :: ReplOpts
defaultReplOpts = ReplOpts False []
type Errs a = Either [String] a
type ReplOptsOp = ReplOpts -> Errs 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
[] -> foldM (&) defaultReplOpts flags <&> \o -> o { inputFiles = inputFiles }
_ -> Left errs
where
(flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs 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 = "<repl>"
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
let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles
(g0, opens) <- case toLoad of
[] -> pure (mGrammar [], [])
_ -> do
(_, (_, g0)) <- batchCompile noOptions Nothing toLoad
pure (g0, OSimple . moduleNameS . justModuleName <$> toLoad)
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)) (if noPrelude then Map.empty else stdPredef))

162
src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -1,5 +1,5 @@
{-# LANGUAGE RankNTypes, CPP #-}
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-}
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.
@@ -12,26 +12,33 @@ 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,unless)
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)
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
@@ -64,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
@@ -105,7 +112,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
@@ -148,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
@@ -369,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
@@ -376,21 +382,27 @@ 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 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] -> EvalM s (Term,Rho s)
reapply scope fun fun_ty [] = return (fun,fun_ty)
reapply scope fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case
(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")
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
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: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)
@@ -399,22 +411,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] -> 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) ((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
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: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
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
@@ -581,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
@@ -779,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
@@ -892,6 +946,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)
@@ -905,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
@@ -1070,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)

30
src/compiler/api/GF/Data/Utilities.hs
View File

@@ -14,9 +14,10 @@
module GF.Data.Utilities(module GF.Data.Utilities) where
import Data.Bifunctor (first)
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
@@ -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
@@ -140,6 +149,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 []

1
src/compiler/api/GF/Interactive.hs
View File

@@ -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)

2
src/compiler/api/GF/Term.hs
View File

@@ -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

12
src/compiler/gf-repl.hs Normal file
View File

@@ -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_ putStrLn errs
Right opts -> runRepl opts

11
src/compiler/gf.cabal
View File

@@ -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
@@ -120,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
@@ -200,7 +203,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:
@@ -237,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