From 8bd0d13dd612d31b8608d047abb42b0fec26f137 Mon Sep 17 00:00:00 2001 From: Eve Date: Sat, 22 Mar 2025 06:45:06 +0100 Subject: [PATCH] Port builtin improvements to new evaluator + opt parsing --- src/compiler/api/GF/Compile/CheckGrammar.hs | 2 +- .../api/GF/Compile/Compute/Concrete.hs | 6 +- .../api/GF/Compile/Compute/Concrete2.hs | 188 +++++++++++------- src/compiler/api/GF/Compile/Repl.hs | 31 ++- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 91 +++++---- src/compiler/api/GF/Grammar/Grammar.hs | 6 +- src/compiler/api/GF/Grammar/Lexer.x | 29 ++- src/compiler/api/GF/Grammar/Parser.y | 11 + 8 files changed, 233 insertions(+), 131 deletions(-) diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index a1545cbd5..14fa23f47 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -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 diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 122321010..376cc6aec 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -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 diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs index 02664aefb..22ec9813f 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs @@ -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))) diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs index b13dde7be..af9665b35 100644 --- a/src/compiler/api/GF/Compile/Repl.hs +++ b/src/compiler/api/GF/Compile/Repl.hs @@ -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 = "" 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 diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 44fee0401..37a6a6b75 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -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 diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs index a16b59869..d2a7c6487 100644 --- a/src/compiler/api/GF/Grammar/Grammar.hs +++ b/src/compiler/api/GF/Grammar/Grammar.hs @@ -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)) diff --git a/src/compiler/api/GF/Grammar/Lexer.x b/src/compiler/api/GF/Grammar/Lexer.x index d3f649002..1130aa0f1 100644 --- a/src/compiler/api/GF/Grammar/Lexer.x +++ b/src/compiler/api/GF/Grammar/Lexer.x @@ -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 diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y index f9aa59a31..54b1fb755 100644 --- a/src/compiler/api/GF/Grammar/Parser.y +++ b/src/compiler/api/GF/Grammar/Parser.y @@ -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) }