1
0
forked from GitHub/gf-core

Port builtin improvements to new evaluator + opt parsing

This commit is contained in:
Eve
2025-03-22 06:45:06 +01:00
parent 3de005f11c
commit 8bd0d13dd6
8 changed files with 233 additions and 131 deletions

View File

@@ -302,7 +302,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
-- | for grammars obtained otherwise than by parsing ---- update!!
checkReservedId :: Ident -> Check ()
checkReservedId x =
when (isReservedWord x) $
when (isReservedWord GF x) $
checkWarn ("reserved word used as identifier:" <+> x)
-- auxiliaries

View File

@@ -1,4 +1,4 @@
{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification, LambdaCase #-}
{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-}
-- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation.
@@ -297,6 +297,10 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) ->
Nothing -> evalError ("Variable" <+> pp pv <+> "is not in scope")
return (VSymCat d r rs)
eval env (TSymVar d r) [] = do return (VSymVar d r)
eval env t@(Opts n cs) vs = EvalM $ \gr k e mt b r msgs ->
case cs of
[] -> return $ Fail ("No options in expression:" $$ ppTerm Unqualified 0 t) msgs
((l,t):_) -> case eval env t vs of EvalM f -> f gr k e mt b r msgs
eval env t vs = evalError ("Cannot reduce term" <+> pp t)
apply v [] = return v

View File

@@ -2,11 +2,13 @@
module GF.Compile.Compute.Concrete2
(Env, Scope, Value(..), Constraint, ConstValue(..), Globals(..), PredefTable, EvalM,
runEvalM, stdPredef, globals, pdArity,
runEvalM, stdPredef, globals,
PredefImpl, Predef(..), ($\),
pdCanonicalArgs, pdArity,
normalForm, normalFlatForm,
eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect,
newResiduation, getMeta, setMeta, MetaState(..), variants, try,
evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
evalError, evalWarn, ppValue, Choice, unit, poison, split, split3, split4, mapC, mapCM) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Infra.Ident
@@ -24,19 +26,37 @@ import Control.Monad
import Control.Applicative hiding (Const)
import qualified Control.Applicative as A
import qualified Data.Map as Map
import Data.Functor ((<&>))
import Data.Maybe (fromMaybe,fromJust)
import Data.List
import Data.Char
type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value
newtype Predef = Predef { runPredef :: PredefImpl }
infix 1 $\
($\) :: (Predef -> Predef) -> PredefImpl -> Predef
k $\ f = k (Predef f)
pdCanonicalArgs :: Bool -> Predef -> Predef
pdCanonicalArgs flat def = Predef $ \g c args ->
if all (isCanonicalForm flat) args then runPredef def g c args else RunTime
pdArity :: Int -> Predef -> Predef
pdArity n def = Predef $ \g c args ->
case splitAt' n args of
Nothing -> RunTime
Just (usedArgs, remArgs) ->
runPredef def g c usedArgs <&> \v -> apply g v remArgs
type Env = [(Ident,Value)]
type Scope = [(Ident,Value)]
type Predef a = Globals -> Choice -> [Value] -> ConstValue a
type PredefCombinator a = Predef a -> Predef a
type PredefTable = Map.Map Ident (Predef Value)
type PredefTable = Map.Map Ident Predef
data Globals = Gl Grammar PredefTable
data Value
= VApp QIdent [Value]
= VApp Choice QIdent [Value]
| VMeta {-# UNPACK #-} !MetaId [Value]
| VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value]
| VGen {-# UNPACK #-} !Int [Value]
@@ -60,6 +80,7 @@ data Value
| VPatt Int (Maybe Int) Patt
| VPattType Value
| VFV Choice [Value]
| VOpts Choice Value [(Value, Value)]
| VAlts Value [(Value, Value)]
| VStrs [Value]
| VMarkup Ident [(Ident,Value)] [Value]
@@ -71,6 +92,29 @@ data Value
| VCRecType [(Label, Bool, Value)]
| VCInts (Maybe Integer) (Maybe Integer)
isCanonicalForm :: Bool -> Value -> Bool
isCanonicalForm flat (VClosure {}) = True
isCanonicalForm flat (VProd b x d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VRecType fs) = all (isCanonicalForm flat . snd) fs
isCanonicalForm flat (VR {}) = True
isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VT {}) = True
isCanonicalForm flat (VV {}) = True
isCanonicalForm flat (VSort {}) = True
isCanonicalForm flat (VInt {}) = True
isCanonicalForm flat (VFlt {}) = True
isCanonicalForm flat (VStr {}) = True
isCanonicalForm flat VEmpty = True
isCanonicalForm True (VFV c vs) = False
isCanonicalForm False (VFV c vs) = all (isCanonicalForm False) vs
isCanonicalForm True (VOpts c n os) = False
isCanonicalForm False (VOpts c n os) = all (isCanonicalForm False . snd) os
isCanonicalForm flat (VAlts d vs) = all (isCanonicalForm flat . snd) vs
isCanonicalForm flat (VStrs vs) = all (isCanonicalForm flat) vs
isCanonicalForm flat (VMarkup tag as vs) = all (isCanonicalForm flat . snd) as && all (isCanonicalForm flat) vs
isCanonicalForm flat (VReset ctl v) = isCanonicalForm flat v
isCanonicalForm flat _ = False
data ConstValue a
= Const a
| CSusp MetaId (Value -> ConstValue a)
@@ -179,20 +223,13 @@ eval g env s (S t1 t2) vs = let (!s1,!s2) = split s
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 = case Map.lookup id predef of
Nothing -> VApp q vs
Just fn -> let valueOf (Const res) = res
valueOf (CFV i vs) = VFV i (map valueOf vs)
valueOf (CSusp i k) = VSusp i (valueOf . k) []
valueOf RunTime = VApp q vs
valueOf NonExist = VApp (cPredef,cNonExist) []
in valueOf (fn g c vs)
| m == cPredef = evalPredef g c id vs
| otherwise = case lookupResDef gr q of
Ok t -> eval g env c t vs
Bad msg -> error msg
where
Gl gr predef = g
eval g env s (QC q) vs = VApp q vs
eval g env s (QC q) vs = VApp s q vs
eval g env s (C t1 t2) [] = let (!s1,!s2) = split s
concat v1 VEmpty = v1
@@ -210,12 +247,12 @@ eval g env s (Glue t1 t2) [] = let (!s1,!s2) = split s
glue VEmpty v = v
glue (VC v1 v2) v = VC v1 (glue v2 v)
glue (VApp q []) v
| q == (cPredef,cNonExist) = VApp q []
glue (VApp c q []) v
| q == (cPredef,cNonExist) = VApp c q []
glue v VEmpty = v
glue v (VC v1 v2) = VC (glue v v1) v2
glue v (VApp q [])
| q == (cPredef,cNonExist) = VApp q []
glue v (VApp c q [])
| q == (cPredef,cNonExist) = VApp c q []
glue (VStr s1) (VStr s2) = VStr (s1++s2)
glue v (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas]
glue (VAlts d vas) (VStr s) = pre d vas s
@@ -256,25 +293,42 @@ eval g env c (Markup tag as ts) [] =
in (VMarkup tag vas vs)
eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [])
eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
eval g env c t@(Opts n cs) vs = if null cs
then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
else let (c1,c2,c3) = split3 c
vn = eval g env c1 n []
vcs = mapC evalOpt c cs
in VOpts c3 vn vcs
where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
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 = case Map.lookup n pds of
Nothing -> VApp c (cPredef,n) args
Just def -> let valueOf (Const res) = res
valueOf (CFV i vs) = VFV i (map valueOf vs)
valueOf (CSusp i k) = VSusp i (valueOf . k) []
valueOf RunTime = VApp c (cPredef,n) args
valueOf NonExist = VApp c (cPredef,cNonExist) []
in valueOf (runPredef def g c args)
stdPredef :: Globals -> PredefTable
stdPredef g = Map.fromList
[(cLength, pdArity 1 $ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
,(cTake, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
,(cDrop, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
,(cTk, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
,(cDp, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
,(cIsUpper,pdArity 1 $ \g c [v] -> fmap toPBool (liftA (all isUpper) (value2string g v)))
,(cToUpper,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toUpper) (value2string g v)))
,(cToLower,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toLower) (value2string g v)))
,(cEqStr, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
,(cOccur, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
,(cOccurs, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
,(cEqInt, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
,(cLessInt,pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
,(cPlus, pdArity 2 $ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
,(cError, pdArity 1 $ \g c [v] -> fmap (VError . pp) (value2string g v))
[(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
,(cTake, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
,(cTk, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
,(cDp, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
,(cIsUpper,pdArity 1 $\ \g c [v] -> fmap toPBool (liftA (all isUpper) (value2string g v)))
,(cToUpper,pdArity 1 $\ \g c [v] -> fmap string2value (liftA (map toUpper) (value2string g v)))
,(cToLower,pdArity 1 $\ \g c [v] -> fmap string2value (liftA (map toLower) (value2string g v)))
,(cEqStr, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
,(cOccur, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
,(cOccurs, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
,(cEqInt, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
,(cLessInt,pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
,(cPlus, pdArity 2 $\ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
,(cError, pdArity 1 $\ \g c [v] -> fmap (VError . pp) (value2string g v))
]
where
genericTk n = reverse . genericDrop n . reverse
@@ -282,7 +336,9 @@ stdPredef g = Map.fromList
apply g (VMeta i vs0) vs = VMeta i (vs0++vs)
apply g (VSusp i k vs0) vs = VSusp i k (vs0++vs)
apply g (VApp f vs0) vs = VApp f (vs0++vs)
apply g (VApp c f@(m,n) vs0) vs
| m == cPredef = evalPredef g c n (vs0++vs)
| otherwise = VApp c f (vs0++vs)
apply g (VGen i vs0) vs = VGen i (vs0++vs)
apply g (VFV i fvs) vs = VFV i [apply g v vs | v <- fvs]
apply g (VS v1 v2 vs') vs = VS v1 v2 (vs'++vs)
@@ -291,7 +347,7 @@ apply g v [] = v
bubble v = snd (bubble v)
where
bubble (VApp f vs) = liftL (VApp f) vs
bubble (VApp c f vs) = liftL (VApp c f) vs
bubble (VMeta metaid vs) = liftL (VMeta metaid) vs
bubble (VSusp metaid k vs) = liftL (VSusp metaid k) vs
bubble (VGen i vs) = liftL (VGen i) vs
@@ -407,8 +463,8 @@ bubble v = snd (bubble v)
mergeChoices1 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,cnt+1)) id unitfy
mergeChoices2 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,2)) unitfy unitfy
toPBool True = VApp (cPredef,cPTrue) []
toPBool False = VApp (cPredef,cPFalse) []
toPBool True = VApp poison (cPredef,cPTrue) []
toPBool False = VApp poison (cPredef,cPFalse) []
occur s1 [] = False
occur s1 s2@(_:tail) = check s1 s2
@@ -452,7 +508,7 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
(p, VGen i vs) -> v0
(p, VSusp i k vs) -> VSusp i (\v -> match' env p ps eqs (apply g (k v) vs) args) []
(p, VFV s vs) -> VFV s [match' env p ps eqs arg args | arg <- vs]
(PP q qs, VApp r vs)
(PP q qs, VApp c r vs)
| q == r -> match env (qs++ps) eqs (vs++args)
(PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args
(PString s1, VStr s2)
@@ -525,9 +581,9 @@ vtableSelect g v0 ty cs v2 vs =
(compute lbls)
Nothing -> error (show ("Missing value for label" <+> pp lbl $$
"among" <+> hsep (punctuate (pp ',') (map fst as))))
value2index (VApp q tnks) ty =
value2index (VApp c q args) ty =
let (r ,ctxt,cnt ) = getIdxCnt q
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt tnks)
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args)
where
getIdxCnt q =
let (_,ResValue (L _ ty) idx) = getInfo q
@@ -566,10 +622,16 @@ data MetaState
= Bound Scope Value
| Narrowing Type
| Residuation Scope (Maybe Constraint)
data OptionInfo
= OptionInfo
{ optLabel :: Value
, optChoices :: [Value]
}
data State
= State
= State
{ choices :: Map.Map Choice Int
, metaVars :: Map.Map MetaId MetaState
, options :: [OptionInfo]
}
type Cont r = State -> r -> [Message] -> CheckResult r [Message]
newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r)
@@ -613,14 +675,12 @@ reset (EvalM f) = EvalM $ \g k state r ws ->
case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
Fail msg ws -> Fail msg ws
Success xs ws -> k (reverse xs) state r ws
where
empty = State Map.empty Map.empty
globals :: EvalM Globals
globals = EvalM (\g k -> k g)
variants :: Choice -> [a] -> EvalM a
variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
variants c xs = EvalM (\g k state@(State choices metas opts) r msgs ->
case Map.lookup c choices of
Just j -> k (xs !! j) state r msgs
Nothing -> backtrack 0 xs k choices metas r msgs)
@@ -632,7 +692,7 @@ variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
Success r msgs -> backtrack (j+1) xs k choices metas r msgs
variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term
variants' c f xs = EvalM (\g k state@(State choices metas) r msgs ->
variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
case Map.lookup c choices of
Just j -> case f (xs !! j) of
EvalM f -> f g k state r msgs
@@ -668,7 +728,7 @@ try f xs msg = EvalM (\g k state r msgs ->
Success r msgs -> continue g k res r msgs
newResiduation :: Scope -> EvalM MetaId
newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
let meta_id = Map.size metas+1
in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas)) r msgs)
@@ -679,12 +739,12 @@ getMeta i = EvalM (\g k state r msgs ->
Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs)
setMeta :: MetaId -> MetaState -> EvalM ()
setMeta i ms = EvalM (\g k (State choices metas) r msgs ->
setMeta i ms = EvalM (\g k (State choices metas opts) r msgs ->
let state' = State choices (Map.insert i ms metas)
in k () state' r msgs)
value2termM :: Bool -> [Ident] -> Value -> EvalM Term
value2termM flat xs (VApp q vs) =
value2termM flat xs (VApp c q vs) =
foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs
value2termM flat xs (VMeta i vs) = do
mv <- getMeta i
@@ -855,7 +915,7 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
pattVars st _ = st
ppValue q d (VApp c vs) = prec d 4 (hsep (ppQIdent q c : map (ppValue q 5) vs))
ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
ppValue q d (VGen _ _) = pp "VGen"
@@ -914,24 +974,24 @@ value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b
concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs
concat v1 (CFV i vs) = CFV i [concat v1 v2 | v2 <- vs]
concat v1 res = res
value2string' g (VApp q []) b ws qs
value2string' g (VApp c q []) b ws qs
| q == (cPredef,cNonExist) = NonExist
value2string' g (VApp q []) b ws qs
value2string' g (VApp c q []) b ws qs
| q == (cPredef,cSOFT_SPACE) = if null ws
then Const (b,ws,q:qs)
else Const (b,ws,qs)
value2string' g (VApp q []) b ws qs
value2string' g (VApp c q []) b ws qs
| q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND)
= if null ws
then Const (True,ws,q:qs)
else Const (True,ws,qs)
value2string' g (VApp q []) b ws qs
value2string' g (VApp c q []) b ws qs
| q == (cPredef,cCAPIT) = capit ws
where
capit [] = Const (b,[],q:qs)
capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs)
capit ws = Const (b,ws,qs)
value2string' g (VApp q []) b ws qs
value2string' g (VApp c q []) b ws qs
| q == (cPredef,cALL_CAPIT) = all_capit ws
where
all_capit [] = Const (b,[],q:qs)
@@ -971,9 +1031,15 @@ newtype Choice = Choice Integer deriving (Eq,Ord,Pretty,Show)
unit :: Choice
unit = Choice 1
poison :: Choice
poison = Choice (-1)
split :: Choice -> (Choice,Choice)
split (Choice c) = (Choice (2*c), Choice (2*c+1))
split3 :: Choice -> (Choice,Choice,Choice)
split3 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (2*c+1))
split4 :: Choice -> (Choice,Choice,Choice,Choice)
split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3))
@@ -993,15 +1059,3 @@ mapCM f c (x:xs) = do
y <- f c1 x
ys <- mapCM f c2 xs
return (y:ys)
pdArity :: Int -> PredefCombinator Value
pdArity n def = \g c args ->
case splitAt' n args of
Nothing -> RunTime
Just (usedArgs, remArgs) ->
fmap (\v -> apply g v remArgs) (def g c usedArgs)
where
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)))

View File

@@ -33,7 +33,7 @@ import GF.Grammar.Grammar
, Term(Typed)
, prependModule
)
import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP)
import GF.Grammar.Lexer (Posn(..), Lang(..), runLangP)
import GF.Grammar.Parser (pTerm)
import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm)
import GF.Infra.CheckM (Check, runCheck)
@@ -41,14 +41,16 @@ import GF.Infra.Ident (moduleNameS)
import GF.Infra.Option (noOptions)
import GF.Infra.UseIO (justModuleName)
import GF.Text.Pretty (render)
import Debug.Trace
data ReplOpts = ReplOpts
{ noPrelude :: Bool
{ lang :: Lang
, noPrelude :: Bool
, inputFiles :: [String]
}
defaultReplOpts :: ReplOpts
defaultReplOpts = ReplOpts False []
defaultReplOpts = ReplOpts GF False []
type Errs a = Either [String] a
type ReplOptsOp = ReplOpts -> Errs ReplOpts
@@ -57,6 +59,13 @@ 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."
, Option [] ["lang"] (ReqArg (\s o -> case s of
"gf" -> Right (o { lang = GF })
"bnfc" -> Right (o { lang = BNFC })
"nlg" -> Right (o { lang = NLG })
_ -> Left ["Unknown language variant: " ++ s])
"{gf,bnfc,nlg}")
"Set the active language variant."
]
where
flag f = NoArg $ \o -> pure (f o)
@@ -81,13 +90,13 @@ 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
parseThen :: MonadIO m => Lang -> Grammar -> String -> (Term -> InputT m ()) -> InputT m ()
parseThen l g s k = case runLangP l 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
runRepl' :: Lang -> Globals -> IO ()
runRepl' l gl@(Gl g _) = do
historyFile <- getAppUserDataDirectory "gfci_history"
runInputT (Settings noCompletion (Just historyFile) True) repl -- TODO tab completion
where
@@ -98,7 +107,7 @@ runRepl' gl@(Gl g _) = do
Just code -> evalPrintLoop code
command "t" arg = do
parseThen g arg $ \main ->
parseThen l g arg $ \main ->
execCheck (inferLType gl main) $ \res ->
forM_ res $ \(t, ty) ->
let t' = case t of
@@ -114,14 +123,14 @@ runRepl' gl@(Gl g _) = do
outputStrLn "" >> repl
evalPrintLoop code = do -- TODO bindings
parseThen g code $ \main ->
parseThen l 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
runRepl (ReplOpts lang noPrelude inputFiles) = do
-- TODO accept an ngf grammar
let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles
(g0, opens) <- case toLoad of
@@ -143,4 +152,4 @@ runRepl (ReplOpts noPrelude inputFiles) = do
, jments = Map.empty
}
g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g)
runRepl' g
runRepl' lang g

View File

@@ -57,14 +57,14 @@ inferSigma scope s t = do -- GEN1
let forall_tvs = res_tvs \\ env_tvs
quantify scope t forall_tvs ty
vtypeInt = VApp (cPredef,cInt) []
vtypeFloat = VApp (cPredef,cFloat) []
vtypeInts i= VApp (cPredef,cInts) [VInt i]
vtypeInt = VApp poison (cPredef,cInt) []
vtypeFloat = VApp poison (cPredef,cFloat) []
vtypeInts i= VApp poison (cPredef,cInts) [VInt i]
vtypeStr = VSort cStr
vtypeStrs = VSort cStrs
vtypeType = VSort cType
vtypePType = VSort cPType
vtypeMarkup= VApp (cPredef,cMarkup) []
vtypeMarkup= VApp poison (cPredef,cMarkup) []
tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT
@@ -90,7 +90,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
in return (Abs bt var body, (VProd bt v arg_ty body_ty))
else return (Abs bt var body, (VProd bt identW arg_ty body_ty))
where
check m n st (VApp f vs) = foldM (check m n) st vs
check m n st (VApp c f vs) = foldM (check m n) st vs
check m n st (VMeta i vs) = do
state <- getMeta i
case state of
@@ -98,8 +98,8 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
check m n st (apply g v vs)
_ -> foldM (check m n) st vs
check m n st@(b,xs) (VGen i vs)
| i == m = return (True, xs)
| otherwise = return st
| i == m = return (True, xs)
| otherwise = return st
check m n st (VClosure env c (Abs bt x t)) = do
g <- globals
check m (n+1) st (eval g ((x,VGen n []):env) c t [])
@@ -118,7 +118,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
check m n st v1 >>= \st -> check m n st v2
check m n st (VTable v1 v2) =
check m n st v1 >>= \st -> check m n st v2
check m n st (VT ty env c cs) =
check m n st (VT ty env c cs) =
check m n st ty -- Traverse cs as well
check m n st (VV ty cs) =
check m n st ty >>= \st -> foldM (check m n) st cs
@@ -186,17 +186,7 @@ tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT
(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
(ty,subsume) <-
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty)
let go c t = do (t, ty) <- tcRho scope c t mb_ty
subsume t ty
ts <- mapCM go c ts
(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
@@ -389,11 +379,17 @@ tcRho scope c (Reset ctl t) mb_ty =
Limit n -> do (t,_) <- tcRho scope c1 t Nothing
instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
Coordination mb_mn@(Just mn) conj _
-> do tcRho scope c1 (QC (mn,conj)) (Just (VApp (mn,identS "Conj") []))
-> do tcRho scope c1 (QC (mn,conj)) (Just (VApp poison (mn,identS "Conj") []))
(t,ty) <- tcRho scope c2 t mb_ty
case ty of
VApp id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
VApp c id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
tcRho scope s (Opts n cs) mb_ty = do
let (s1,s2,s3) = split3 s
(n,_) <- tcRho scope s1 n Nothing
(ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
(ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
return (Opts n (zip ls ts), ty)
tcRho scope s t _ = unimplemented ("tcRho "++show t)
evalCodomain :: Scope -> Ident -> Value -> EvalM Value
@@ -402,6 +398,21 @@ evalCodomain scope x (VClosure env c t) = do
return (eval g ((x,VGen (length scope) []):env) c t [])
evalCodomain scope x t = return t
tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint)
tcUnifying scope c ts mb_ty = do
(ty,subsume) <-
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty)
let go c t = do (t, ty) <- tcRho scope c t mb_ty
subsume t ty
ts <- mapCM go c ts
return (ts,ty)
tcCases scope c [] p_ty res_ty = return []
tcCases scope c ((p,t):cs) p_ty res_ty = do
let (c1,c2,c3,c4) = split4 c
@@ -690,9 +701,9 @@ subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE
subsCheckTbl scope t p1 r1 p2 r2
subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE
| s1 == cPType && s2 == cType = return t
subsCheckRho scope t (VApp p1 _) (VApp p2 _) -- Rule INT1
subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1
| p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t
subsCheckRho scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2
subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2
| p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do
if i <= j
then return t
@@ -751,13 +762,13 @@ subsCheckFun scope t a1 r1 a2 r2 = do
let v = newVar scope
vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1
g <- globals
let r1 = case r1 of
VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
r1 -> r1
let r2 = case r2 of
VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
r2 -> r2
t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1 r2
let r1' = case r1 of
VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
r1 -> r1
r2' = case r2 of
VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
r2 -> r2
t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2'
return (Abs Explicit v t)
subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term
@@ -768,10 +779,10 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
p2 <- value2termM True (scopeVars scope) p2
return (T (TTyped p2) [(PV x,t)])
subtype scope Nothing (VApp p [VInt i])
subtype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do
return (VCInts Nothing (Just i))
subtype scope (Just (VCInts i j)) (VApp p [VInt k])
subtype scope (Just (VCInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do
return (VCInts j (Just (maybe k (min k) i)))
subtype scope Nothing (VRecType ltys) = do
@@ -793,10 +804,10 @@ subtype scope (Just ctr) ty = do
unify scope ctr ty
return ty
supertype scope Nothing (VApp p [VInt i])
supertype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do
return (VCInts (Just i) Nothing)
supertype scope (Just (VCInts i j)) (VApp p [VInt k])
supertype scope (Just (VCInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do
return (VCInts (Just (maybe k (max k) i)) j)
supertype scope Nothing (VRecType ltys) = do
@@ -844,7 +855,7 @@ unifyTbl scope tau = do
unify scope tau (VTable arg res)
return (arg,res)
unify scope (VApp f1 vs1) (VApp f2 vs2)
unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2)
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2)
unify scope (VMeta i vs1) (VMeta j vs2)
| i == j = sequence_ (zipWith (unify scope) vs1 vs2)
@@ -910,7 +921,7 @@ occursCheck scope' i0 scope v =
n = length scope
in check m n v
where
check m n (VApp f vs) = mapM_ (check m n) vs
check m n (VApp c f vs) = mapM_ (check m n) vs
check m n (VMeta i vs)
| i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs)
ty2 <- value2termM False (scopeVars scope) v
@@ -1019,9 +1030,9 @@ quantify scope t tvs ty = do
where
bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i []))
check m n xs (VApp f vs) = do
check m n xs (VApp c f vs) = do
(xs,vs) <- mapAccumM (check m n) xs vs
return (xs,VApp f vs)
return (xs,VApp c f vs)
check m n xs (VMeta i vs) = do
s <- getMeta i
case s of
@@ -1159,7 +1170,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
Residuation _ Nothing -> foldM go (m:acc) args
Residuation _ (Just v) -> go acc v
_ -> return acc
go acc (VApp f args) = foldM go acc args
go acc (VApp c f args) = foldM go acc args
go acc (VFV c vs) = foldM go acc vs
go acc (VCRecType vs) = foldM (\acc (lbl,b,v) -> go acc v) acc vs
go acc (VCInts _ _) = return acc

View File

@@ -54,6 +54,7 @@ module GF.Grammar.Grammar (
Equation,
Labelling,
Assign,
Option,
Case,
LocalDef,
Param,
@@ -372,7 +373,9 @@ data Term =
| R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Opts Term [Option] -- ^ options: @options s in { e => x ; ... }@
| Table Term Term -- ^ table type: @P => A@
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@
| V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
@@ -471,6 +474,7 @@ type Equation = ([Patt],Term)
type Labelling = (Label, Type)
type Assign = (Label, (Maybe Type, Term))
type Option = (Term, Term)
type Case = (Patt, Term)
--type Cases = ([Patt], Term)
type LocalDef = (Ident, (Maybe Type, Term))

View File

@@ -41,7 +41,7 @@ $u = [.\n] -- universal: any character
"{-" ([$u # \-] | \- [$u # \}])* ("-")+ "}" ;
$white+ ;
@rsyms { tok ident }
@rsyms { \lang -> tok (ident lang) lang }
\< $white* @ident $white* (\/ | \>)
{ \lang inp@(AI pos s) inp' _ ->
let inp0 = AI (alexMove pos '<') (BS.tail s)
@@ -74,7 +74,7 @@ $white+ ;
in POk (inp,inp0) T_less
} }
\' ([. # [\' \\ \n]] | (\\ (\' | \\)))+ \' { tok (T_Ident . identS . unescapeInitTail . unpack) }
@ident { tok ident }
@ident { \lang -> tok (ident lang) lang }
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | $d+)))* \" { tok (T_String . unescapeInitTail . unpack) }
@@ -85,7 +85,7 @@ $white+ ;
{
unpack = UTF8.toString
ident = res T_Ident . identC . rawIdentC
ident lang = res lang T_Ident . identC . rawIdentC
tok f _ inp@(AI _ s) inp' len = POk (inp,inp') (f (UTF8.take len s))
@@ -149,6 +149,7 @@ data Token
| T_of
| T_open
| T_oper
| T_option
| T_param
| T_pattern
| T_pre
@@ -174,16 +175,20 @@ data Token
deriving Show -- debug
res = eitherResIdent
eitherResIdent :: (Ident -> Token) -> Ident -> Token
eitherResIdent tv s =
case Map.lookup s resWords of
eitherResIdent :: Lang -> (Ident -> Token) -> Ident -> Token
eitherResIdent lang tv s =
case Map.lookup s (resWords lang) of
Just t -> t
Nothing -> tv s
isReservedWord :: Ident -> Bool
isReservedWord ident = Map.member ident resWords
isReservedWord :: Lang -> Ident -> Bool
isReservedWord lang ident = Map.member ident (resWords lang)
resWords = Map.fromList
resWords :: Lang -> Map.Map Ident Token
resWords NLG = nlgResWords
resWords _ = coreResWords
coreResWords = Map.fromList
[ b "!" T_exclmark
, b "#" T_patt
, b "$" T_int_label
@@ -255,13 +260,17 @@ resWords = Map.fromList
, b "variants" T_variants
, b "where" T_where
, b "with" T_with
, b "coercions" T_coercions
, b "coercions" T_coercions -- FIXME ..
, b "terminator" T_terminator
, b "separator" T_separator
, b "nonempty" T_nonempty
]
where b s t = (identS s, t)
-- bnfcResWords = _
nlgResWords = Map.insert (identS "option") T_option coreResWords
unescapeInitTail :: String -> String
unescapeInitTail = unesc . tail where
unesc s = case s of

View File

@@ -101,6 +101,7 @@ import qualified Data.Map as Map
'of' { T_of }
'open' { T_open }
'oper' { T_oper }
'option' { T_option }
'param' { T_param }
'pattern' { T_pattern }
'pre' { T_pre }
@@ -452,6 +453,7 @@ Exp4 :: { Term }
Exp4
: Exp4 Exp5 { App $1 $2 }
| Exp4 '{' Exp '}' { App $1 (ImplArg $3) }
| 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
| 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
Typed _ t -> TTyped t
_ -> TRaw
@@ -608,6 +610,15 @@ ListPattTupleComp
| Patt { [$1] }
| Patt ',' ListPattTupleComp { $1 : $3 }
Opt :: { Option }
Opt
: '(' Exp ')' '=>' Exp { ($2,$5) }
ListOpt :: { [Option] }
ListOpt
: Opt { [$1] }
| Opt ';' ListOpt { $1 : $3 }
Case :: { Case }
Case
: Patt '=>' Exp { ($1,$3) }