From a0c810530e9d77de13befea5151a05c323c3a59d Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Thu, 13 Nov 2025 18:54:40 +0100 Subject: [PATCH] remove the old evaluator --- src/compiler/api/GF/Command/SourceCommands.hs | 2 +- src/compiler/api/GF/Compile/CheckGrammar.hs | 2 +- .../api/GF/Compile/Compute/Concrete.hs | 1924 +++++++++-------- .../api/GF/Compile/Compute/Concrete2.hs | 1229 ----------- src/compiler/api/GF/Compile/GeneratePMCFG.hs | 2 +- .../api/GF/Compile/GrammarToCanonical.hs | 2 +- .../api/GF/Compile/TypeCheck/Concrete.hs | 2 +- src/compiler/api/GF/Interactive.hs | 9 +- src/compiler/api/GF/Term.hs | 12 - src/compiler/gf.cabal | 2 - 10 files changed, 1074 insertions(+), 2112 deletions(-) delete mode 100644 src/compiler/api/GF/Compile/Compute/Concrete2.hs delete mode 100644 src/compiler/api/GF/Term.hs diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index 33badb3ea..6e856645b 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -19,7 +19,7 @@ import GF.Grammar.Analyse import GF.Grammar.ShowTerm import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) -import GF.Compile.Compute.Concrete2(normalForm,normalFlatForm,Globals(..),stdPredef) +import GF.Compile.Compute.Concrete(normalForm,normalFlatForm,Globals(..),stdPredef) import GF.Compile.TypeCheck.Concrete as TC(inferLType) import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts) diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index 5f0deb696..c734d8cb7 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -28,7 +28,7 @@ import GF.Infra.Option import GF.Compile.TypeCheck.Abstract import GF.Compile.TypeCheck.Concrete(checkLType,inferLType) -import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef) +import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) import GF.Grammar import GF.Grammar.Lexer diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 35e98b612..f35dd3f54 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -1,343 +1,508 @@ -{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-} +{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-} --- | 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, isCanonicalForm - , PredefImpl, Predef(..), PredefCombinator, ($\) - , pdForce, pdCanonicalArgs, pdArity, pdStandard - , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..) - , EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn - , eval, apply, force, value2term, patternMatch, stdPredef - , unsafeIOToEvalM - , newThunk, newEvaluatedThunk - , newResiduation, newNarrowing, getVariables - , getRef, setRef - , getResDef, getInfo, getResType, getOverload - , getAllParamValues - ) where + (Env, Scope, Value(..), Variants(..), OptionInfo(..), + ConstValue(..), Globals(..), PredefTable, EvalM, + mapVariantsC, unvariants, + runEvalM, runEvalMWithInput, stdPredef, globals, + PredefImpl, Predef(..), ($\), + pdCanonicalArgs, pdArity, + normalForm, normalFlatForm, + eval, apply, value2term, value2termM, value2string, value2int, value2float, value2expr, string2value, bubble, patternMatch, vtableSelect, State(..), + newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try, + 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.Grammar hiding (Env, VGen, VApp, VRecType) -import GF.Grammar.Lookup(lookupResDef,lookupResType, - lookupOrigInfo,lookupOverloadTypes, - allParamValues) -import GF.Grammar.Predef -import GF.Grammar.Lockfield(lockLabel) -import GF.Grammar.Printer -import GF.Data.Operations(Err(..)) -import GF.Data.Utilities(splitAt') +import GF.Infra.Ident import GF.Infra.CheckM -import GF.Infra.Option -import Data.STRef -import Data.Maybe(fromMaybe) +import GF.Data.Operations(Err(..)) +import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM,secondM,bimapM) +import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo) +import GF.Grammar.Grammar +import GF.Grammar.Macros +import GF.Grammar.Predef +import GF.Grammar.Printer hiding (ppValue) +import GF.Grammar.Lockfield(lockLabel) +import GF.Text.Pretty hiding (empty) +import qualified GF.Text.Pretty as PP +import Control.Monad +import Control.Applicative hiding (Const) +import qualified Control.Applicative as A +import qualified Data.Map as Map +import Data.Bifunctor (second) +import Data.Functor ((<&>)) +import Data.Maybe (fromMaybe,fromJust) import Data.List import Data.Char -import Control.Monad -import Control.Monad.ST -import Control.Monad.ST.Unsafe -import Control.Applicative hiding (Const) -import qualified Control.Monad.Fail as Fail -import Data.Functor ((<&>)) -import qualified Data.Map as Map -import GF.Text.Pretty -import PGF2.Transactions(LIndex) +import PGF2(Expr(..),Literal(..)) --- * Main entry points +type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value +newtype Predef = Predef { runPredef :: PredefImpl } --- | The term is fully evaluated. Variants are only expanded if necessary for the evaluation. -normalForm :: Globals -> Term -> Check Term -normalForm globals t = - fmap mkFV (runEvalM globals (eval [] t [] >>= value2term False [])) - where - mkFV [t] = t - mkFV ts = FV ts +infix 1 $\ --- | The result is a list of terms and contains all variants. Each term by itself does not contain any variants. -normalFlatForm :: Globals -> Term -> Check [Term] -normalFlatForm globals t = - runEvalM globals (eval [] t [] >>= value2term True []) +($\) :: (Predef -> Predef) -> PredefImpl -> Predef +k $\ f = k (Predef f) -normalStringForm :: Globals -> Term -> Check [String] -normalStringForm globals t = - fmap toStrs (runEvalM globals (fmap value2string (eval [] t []))) - where - toStrs [] = [] - toStrs (Const s:cfs) = s : toStrs cfs - toStrs (_ :cfs) = toStrs cfs +pdCanonicalArgs :: Bool -> Predef -> Predef +pdCanonicalArgs flat def = Predef $ \g c args -> + if all (isCanonicalForm flat) args then runPredef def g c args else RunTime -type Sigma s = Value s -type Constraint s = Value s +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 -data ThunkState s - = Unevaluated (Env s) Term - | Evaluated {-# UNPACK #-} !Int (Value s) - | Hole {-# UNPACK #-} !MetaId - | Narrowing {-# UNPACK #-} !MetaId Type - | Residuation {-# UNPACK #-} !MetaId (Scope s) (Maybe (Constraint s)) +type Env = [(Ident,Value)] +type Scope = [(Ident,Value)] +type PredefTable = Map.Map Ident Predef +data Globals = Gl Grammar PredefTable -type Thunk s = STRef s (ThunkState s) -type Env s = [(Ident,Thunk s)] -type Scope s = [(Ident,Value s)] - -data Value s - = VApp QIdent [Thunk s] - | VMeta (Thunk s) [Thunk s] - | VSusp (Thunk s) (Value s -> EvalM s (Value s)) [Thunk s] - | VGen {-# UNPACK #-} !Int [Thunk s] - | VClosure (Env s) Term - | VProd BindType Ident (Value s) (Value s) - | VRecType [(Label, Value s)] - | VR [(Label, Thunk s)] - | VP (Value s) Label [Thunk s] - | VExtR (Value s) (Value s) - | VTable (Value s) (Value s) - | VT (Value s) (Env s) [Case] - | VV (Value s) [Thunk s] - | VS (Value s) (Thunk s) [Thunk s] +data Value + = VApp Choice QIdent [Value] + | VMeta {-# UNPACK #-} !MetaId [Value] + | VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value] + | VGen {-# UNPACK #-} !Int [Value] + | VClosure Env Choice Term + | VProd BindType Ident Value Value + | VRecType [(Label, Bool, Value)] Bool + | VR [(Label, Value)] + | VP Value Label [Value] + | VExtR Value Value + | VTable Value Value + | VT Value Env Choice [Case] + | VV Value [Value] + | VS Value Value [Value] | VSort Ident | VInt Integer | VFlt Double | VStr String | VEmpty - | VC (Value s) (Value s) - | VGlue (Value s) (Value s) + | VC Value Value + | VGlue Value Value | VPatt Int (Maybe Int) Patt - | VPattType (Value s) - | VAlts (Value s) [(Value s, Value s)] - | VStrs [Value s] - | VMarkup Ident [(Ident,Value s)] [Value s] - -- These two constructors are only used internally - -- in the PMCFG generator. - | VSymCat Int LIndex [(LIndex, (Thunk s, Type))] - | VSymVar Int Int - -- These two constructors are only used internally - -- in the type checker. - | VCRecType [(Label, Bool, Constraint s)] - | VCInts (Maybe Integer) (Maybe Integer) + | VPattType Value + | VFV Choice (Variants Value) + | VAlts Value [(Value, Value)] + | VStrs [Value] + | VMarkup Ident [(Ident,Value)] [L Value] + | VReset Ident (Maybe Value) Value (Maybe QIdent) + | VSymCat Int LIndex [(LIndex, (Value, Type))] + | VError Doc + | VInts Integer Bool -showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")" -showValue (VMeta _ _) = "VMeta" -showValue (VSusp _ _ _) = "VSusp" -showValue (VGen i _) = "(VGen "++show i++")" -showValue (VClosure _ _) = "VClosure" -showValue (VProd _ x v1 v2) = "VProd ("++show x++") ("++showValue v1++") ("++showValue v2++")" -showValue (VRecType _) = "VRecType" -showValue (VR lbls) = "(VR {"++unwords (map (\(lbl,_) -> show lbl) lbls)++"})" -showValue (VP v l _) = "(VP "++showValue v++" "++show l++")" -showValue (VExtR _ _) = "VExtR" -showValue (VTable v1 v2) = "VTable ("++showValue v1++") ("++showValue v2++")" -showValue (VT _ _ cs) = "(VT "++show cs++")" -showValue (VV _ _) = "VV" -showValue (VS v _ _) = "(VS "++showValue v++")" -showValue (VSort s) = "(VSort "++show s++")" -showValue (VInt _) = "VInt" -showValue (VFlt _) = "VFlt" -showValue (VStr s) = "(VStr "++show s++")" -showValue VEmpty = "VEmpty" -showValue (VC v1 v2) = "(VC "++showValue v1++" "++showValue v2++")" -showValue (VGlue _ _) = "VGlue" -showValue (VPatt _ _ _) = "VPatt" -showValue (VPattType _) = "VPattType" -showValue (VAlts _ _) = "VAlts" -showValue (VStrs _) = "VStrs" -showValue (VSymCat _ _ _) = "VSymCat" +data Variants a + = VarFree [a] + | VarOpts Value [(Value, a)] -isCanonicalForm :: Value s -> Bool -isCanonicalForm (VClosure {}) = True -isCanonicalForm (VProd b x d cod) = isCanonicalForm d && isCanonicalForm cod -isCanonicalForm (VRecType fs) = all (isCanonicalForm . snd) fs -isCanonicalForm (VR {}) = True -isCanonicalForm (VTable d cod) = isCanonicalForm d && isCanonicalForm cod -isCanonicalForm (VT {}) = True -isCanonicalForm (VV {}) = True -isCanonicalForm (VSort {}) = True -isCanonicalForm (VInt {}) = True -isCanonicalForm (VFlt {}) = True -isCanonicalForm (VStr {}) = True -isCanonicalForm VEmpty = True -isCanonicalForm (VAlts d vs) = all (isCanonicalForm . snd) vs -isCanonicalForm (VStrs vs) = all isCanonicalForm vs -isCanonicalForm (VMarkup tag as vs) = all (isCanonicalForm . snd) as && all isCanonicalForm vs -isCanonicalForm _ = False +instance Functor Variants where + fmap f (VarFree vs) = VarFree (f <$> vs) + fmap f (VarOpts n cs) = VarOpts n (second f <$> cs) -eval env (Vr x) vs = do (tnk,depth) <- lookup x env - withVar depth $ do - v <- force tnk - apply v vs - where - lookup x [] = evalError ("Variable" <+> pp x <+> "is not in scope") - lookup x ((y,tnk):env) - | x == y = return (tnk,length env) - | otherwise = lookup x env -eval env (Sort s) [] - | s == cTok = return (VSort cStr) - | otherwise = return (VSort s) -eval env (EInt n) [] = return (VInt n) -eval env (EFloat d) [] = return (VFlt d) -eval env (K t) [] = return (VStr t) -eval env Empty [] = return VEmpty -eval env (App t1 t2) vs = do tnk <- newThunk env t2 - eval env t1 (tnk : vs) -eval env (Abs b x t) [] = return (VClosure env (Abs b x t)) -eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs -eval env (Meta i) vs = do tnk <- newHole i - return (VMeta tnk vs) -eval env (ImplArg t) [] = eval env t [] -eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 [] - return (VProd b x v1 (VClosure env t2)) -eval env (Typed t ty) vs = eval env t vs -eval env (RecType lbls) [] = do lbls <- mapM (\(lbl,ty) -> fmap ((,) lbl) (eval env ty [])) lbls - return (VRecType (sortRec lbls)) -eval env (R as) [] = do as <- mapM (\(lbl,(_,t)) -> fmap ((,) lbl) (newThunk env t)) as - return (VR as) -eval env (P t lbl) vs = do v <- eval env t [] - case v of - VR as -> case lookup lbl as of - Nothing -> evalError ("Missing value for label" <+> pp lbl $$ - "in" <+> pp (P t lbl)) - Just tnk -> do v <- force tnk - apply v vs - v -> return (VP v lbl vs) -eval env (ExtR t1 t2) [] = do v1 <- eval env t1 [] - v2 <- eval env t2 [] - case (v1,v2) of - (VR as1,VR as2) -> return (VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2)) - (VRecType as1,VRecType as2) -> return (VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2)) - _ -> return (VExtR v1 v2) -eval env (Table t1 t2) [] = do v1 <- eval env t1 [] - v2 <- eval env t2 [] - return (VTable v1 v2) -eval env (T (TTyped ty) cs)[]=do vty <- eval env ty [] - return (VT vty env cs) -eval env (T (TWild ty) cs) []=do vty <- eval env ty [] - return (VT vty env cs) -eval env (V ty ts) [] = do vty <- eval env ty [] - tnks <- mapM (newThunk env) ts - return (VV vty tnks) -eval env (S t1 t2) vs = do v1 <- eval env t1 [] - tnk2 <- newThunk env t2 - let v0 = VS v1 tnk2 vs - case v1 of - VT _ env cs -> patternMatch v0 (map (\(p,t) -> (env,[p],tnk2:vs,t)) cs) - VV vty tnks -> do ty <- value2term True (map fst env) vty - vtableSelect v0 ty tnks tnk2 vs - 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 = evalPredef id vs - | otherwise = do t <- getResDef q - eval env t vs -eval env (QC q) vs = return (VApp q vs) -eval env (C t1 t2) [] = do v1 <- eval env t1 [] - v2 <- eval env t2 [] - case (v1,v2) of - (v1, VEmpty) -> return v1 - (VEmpty,v2 ) -> return v2 - _ -> return (VC v1 v2) -eval env t@(Glue t1 t2) [] = do v1 <- eval env t1 [] - v2 <- eval env t2 [] - let glue VEmpty v = v - glue (VC v1 v2) v = VC v1 (glue v2 v) - glue (VApp q []) v - | q == (cPredef,cNonExist) = VApp 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 (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 - glue (VAlts d vas) v = glue d v - glue v1 v2 = VGlue v1 v2 +mapVariantsC :: (Choice -> a -> b) -> Choice -> Variants a -> Variants b +mapVariantsC f c (VarFree vs) = VarFree (mapC f c vs) +mapVariantsC f c (VarOpts n cs) = VarOpts n (mapC (\c (x,y) -> (x,f c y)) c cs) - pre vd [] s = glue vd (VStr s) - pre vd ((v,VStrs ss):vas) s - | or [startsWith s' s | VStr s' <- ss] = glue v (VStr s) - | otherwise = pre vd vas s +unvariants :: Variants a -> [a] +unvariants (VarFree vs) = vs +unvariants (VarOpts n cs) = snd <$> cs - return (glue v1 v2) -eval env (EPatt min max p) [] = return (VPatt min max p) -eval env (EPattType t) [] = do v <- eval env t [] - return (VPattType v) -eval env (ELincat c ty) [] = do v <- eval env ty [] - let lbl = lockLabel c - lv = VRecType [] - case v of - (VRecType as) -> return (VRecType (update lbl lv as)) - _ -> return (VExtR v (VRecType [(lbl,lv)])) -eval env (ELin c t) [] = do v <- eval env t [] - let lbl = lockLabel c - tnk <- newEvaluatedThunk (VR []) - case v of - (VR as) -> return (VR (update lbl tnk as)) - _ -> return (VExtR v (VR [(lbl,tnk)])) -eval env (FV ts) vs = msum [eval env t vs | t <- ts] -eval env (Alts d as) [] = do vd <- eval env d [] - vas <- forM as $ \(t,s) -> do - vt <- eval env t [] - vs <- eval env s [] - return (vt,vs) - return (VAlts vd vas) -eval env (Strs ts) [] = do vs <- mapM (\t -> eval env t []) ts - return (VStrs vs) -eval env (Markup tag as ts) [] = - do as <- mapM (\(id,t) -> eval env t [] >>= \v -> return (id,v)) as - vs <- mapM (\t -> eval env (unLoc t) []) ts - return (VMarkup tag as vs) -eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) -> - case lookup pv env of - Just tnk -> return (i,(tnk,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) +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 (\(l,_,ty) -> isCanonicalForm flat ty) 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 {}) = False +isCanonicalForm False (VFV c vs) = all (isCanonicalForm False) (unvariants vs) +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 . unLoc) vs +isCanonicalForm flat (VReset ctl cv v _) = maybe True (isCanonicalForm flat) cv && isCanonicalForm flat v +isCanonicalForm flat _ = False -apply v [] = return v -apply (VMeta m vs0) vs = return (VMeta m (vs0++vs)) -apply (VSusp m k vs0) vs = return (VSusp m k (vs0++vs)) -apply (VApp f@(m,p) vs0) vs - | m == cPredef = evalPredef p (vs0++vs) - | otherwise = return (VApp f (vs0++vs)) -apply (VGen i vs0) vs = return (VGen i (vs0++vs)) -apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs +data ConstValue a + = Const a + | CSusp MetaId (Value -> ConstValue a) + | CFV Choice (Variants (ConstValue a)) + | RunTime + | NonExist +instance Functor ConstValue where + fmap f (Const c) = Const (f c) + fmap f (CFV i vs) = CFV i (fmap (fmap f) vs) + fmap f (CSusp i k) = CSusp i (fmap f . k) + fmap f RunTime = RunTime + fmap f NonExist = NonExist -stdPredef :: PredefTable s -stdPredef = Map.fromList - [(cLength, pd 1 $\ \[v] -> case value2string v of - Const s -> return (Const (VInt (genericLength s))) - _ -> return RunTime) - ,(cTake, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2)))) - ,(cDrop, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2)))) - ,(cTk, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2)))) - ,(cDp, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2)))) - ,(cIsUpper,pd 1 $\ \[v] -> return (fmap toPBool (liftA (all isUpper) (value2string v)))) - ,(cToUpper,pd 1 $\ \[v] -> return (fmap string2value (liftA (map toUpper) (value2string v)))) - ,(cToLower,pd 1 $\ \[v] -> return (fmap string2value (liftA (map toLower) (value2string v)))) - ,(cEqStr, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2)))) - ,(cOccur, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2)))) - ,(cOccurs, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2)))) - ,(cEqInt, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2)))) - ,(cLessInt,pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2)))) - ,(cPlus, pd 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2)))) - ,(cError, pd 1 $\ \[v] -> case value2string v of - Const msg -> fail msg - _ -> fail "Indescribable error appeared") +instance Applicative ConstValue where + pure = Const + + (Const f) <*> (Const x) = Const (f x) + (CFV s vs) <*> v2 = CFV s (fmap (<*> v2) vs) + v1 <*> (CFV s vs) = CFV s (fmap (v1 <*>) vs) + (CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2) + v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v) + NonExist <*> _ = NonExist + _ <*> NonExist = NonExist + RunTime <*> _ = RunTime + _ <*> RunTime = RunTime + +normalForm :: Globals -> Term -> Check Term +normalForm g t = value2term g [] (bubble (eval g [] unit t [])) + +normalFlatForm :: Globals -> Term -> Check [Term] +normalFlatForm g t = runEvalM g (value2termM True [] (eval g [] unit t [])) + +eval :: Globals -> Env -> Choice -> Term -> [Value] -> Value +eval g env s (Vr x) vs = case lookup x env of + Nothing -> VError ("Variable" <+> pp x <+> "is not in scope") + Just v -> apply g v vs +eval g env s (Sort sort) [] + | sort == cTok = VSort cStr + | otherwise = VSort sort +eval g env s (EInt n) [] = VInt n +eval g env s (EFloat d) [] = VFlt d +eval g env s (K t) [] = VStr t +eval g env s Empty [] = VEmpty +eval g env s (App t1 t2) vs = let (s1,s2) = split s + in eval g env s1 t1 (eval g env s2 t2 [] : vs) +eval g env s (Abs b x t) [] = VClosure env s (Abs b x t) +eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs +eval g env s (Meta i) vs = VMeta i vs +eval g env s (ImplArg t) [] = eval g env s t [] +eval g env s (Prod b x t1 t2)[] + | x == identW = let (s1,s2) = split s + in VProd b x (eval g env s1 t1 []) (eval g env s2 t2 []) + | otherwise = let (s1,s2) = split s + in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2) +eval g env s (Typed t ty) vs = eval g env s t vs +eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls) False +eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as) +eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of + Nothing -> VError ("Missing value for label" <+> pp lbl $$ + "in" <+> pp (P t lbl)) + Just v -> apply g v vs + project (VFV s fvs) = VFV s (fmap project fvs) + project (VMeta i vs) = VSusp i (\v -> project (apply g v vs)) [] + project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) [] + project v = VP v lbl vs + in project (eval g env s t []) +eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s + + extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2) + extend (VRecType as1 e1) (VRecType as2 e2)=VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2) (e1 || e2) + extend (VFV i fvs) v2 = VFV i (fmap (`extend` v2) fvs) + extend v1 (VFV i fvs) = VFV i (fmap (v1 `extend`) fvs) + extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) [] + extend v1 (VMeta i vs) = VSusp i (\v -> extend v1 (apply g v vs)) [] + extend (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) [] + extend v1 (VSusp i k vs) = VSusp i (\v -> extend v1 (apply g (k v) vs)) [] + extend v1 v2 = VExtR v1 v2 + + in extend (eval g env s1 t1 []) (eval g env s2 t2 []) +eval g env s (Table t1 t2) [] = let (!s1,!s2) = split s + in VTable (eval g env s1 t1 []) (eval g env s2 t2 []) +eval g env s (T (TTyped ty) cs)[]=let (!s1,!s2) = split s + in VT (eval g env s1 ty []) env s2 cs +eval g env s (T (TWild ty) cs) []=let (!s1,!s2) = split s + in VT (eval g env s1 ty []) env s2 cs +eval g env s (V ty ts) [] = let (!s1,!s2) = split s + in VV (eval g env s1 ty []) (mapC (\s t -> eval g env s t []) s2 ts) +eval g env s (S t1 t2) vs = let (!s1,!s2) = split s + v1 = eval g env s1 t1 [] + v2 = eval g env s2 t2 [] + v0 = VS v1 v2 vs + + select (VT _ env s cs) = patternMatch g s v0 (map (\(p,t) -> (env,[p],v2:vs,t)) cs) + select (VV vty tvs) = case value2termM False (map fst env) vty of + EvalM f -> case f g (\x state xs ws -> Success (x:xs) ws) empty [] [] of + Fail msg ws -> VError msg + Success tys ws -> case tys of + [ty] -> vtableSelect g v0 ty tvs v2 vs + tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs + select (VFV i fvs) = VFV i (fmap select fvs) + select (VMeta i vs) = VSusp i (\v -> select (apply g v vs)) [] + select (VSusp i k vs) = VSusp i (\v -> select (apply g (k v) vs)) [] + select v1 = v0 + + -- FIXME: options=[] is definitely not correct and this shouldn't be using value2termM at all + empty = State [] Map.empty Map.empty [] + + in select v1 +eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s + in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs +eval g env c (Q q@(m,id)) vs + | m == cPredef = evalPredef g c id vs + | 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 s q vs +eval g env s (C t1 t2) [] = let (!s1,!s2) = split s + + concat v1 VEmpty = v1 + concat VEmpty v2 = v2 + concat (VFV i fvs) v2 = VFV i (fmap (`concat` v2) fvs) + concat v1 (VFV i fvs) = VFV i (fmap (v1 `concat`) fvs) + concat (VMeta i vs) v2 = VSusp i (\v -> concat (apply g v vs) v2) [] + concat v1 (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) [] + concat (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) [] + concat v1 (VSusp i k vs) = VSusp i (\v -> concat v1 (apply g (k v) vs)) [] + concat v1 v2 = VC v1 v2 + + in concat (eval g env s1 t1 []) (eval g env s2 t2 []) +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 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 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 + glue (VAlts d vas) v = glue d v + glue (VFV i fvs) v2 = VFV i (fmap (`glue` v2) fvs) + glue v1 (VFV i fvs) = VFV i (fmap (v1 `glue`) fvs) + glue (VMeta i vs) v2 = VSusp i (\v -> glue (apply g v vs) v2) [] + glue v1 (VMeta i vs) = VSusp i (\v -> glue v1 (apply g v vs)) [] + glue (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) [] + glue v1 (VSusp i k vs)= VSusp i (\v -> glue v1 (apply g (k v) vs)) [] + glue v1 v2 = VGlue v1 v2 + + pre vd [] s = glue vd (VStr s) + pre vd ((v,VStrs ss):vas) s + | or [startsWith s' s | VStr s' <- ss] = glue v (VStr s) + | otherwise = pre vd vas s + + in glue (eval g env s1 t1 []) (eval g env s2 t2 []) +eval g env s (EPatt min max p) [] = VPatt min max p +eval g env s (EPattType t) [] = VPattType (eval g env s t []) +eval g env s (ELincat c ty) [] = let lbl = lockLabel c + lty = RecType [] + in eval g env s (ExtR ty (RecType [(lbl,lty)])) [] +eval g env s (ELin c t) [] = let lbl = lockLabel c + lt = R [] + in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) [] +eval g env s (FV ts) vs = VFV s (VarFree (mapC (\s t -> eval g env s t vs) s ts)) +eval g env s (Alts d as) [] = let (!s1,!s2) = split s + vd = eval g env s1 d [] + vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s + in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as + in VAlts vd vas +eval g env c (Strs ts) [] = VStrs (mapC (\c t -> eval g env c t []) c ts) +eval g env c (Markup tag as ts) [] = + let (c1,c2) = split c + vas = mapC (\c (id,t) -> (id,eval g env c t [])) c1 as + vs = mapC (\c (L loc t) -> L loc (eval g env c t [])) c2 ts + in (VMarkup tag vas vs) +eval g env c (Reset ctl mb_ct t qid) [] = VReset ctl (fmap (\t -> eval g env c t []) mb_ct) (eval g env c t []) qid +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 VFV c3 (VarOpts vn vcs) + where evalOpt c' (Just l, t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs) + evalOpt c' (Nothing,t) = let v = eval g env c' t vs in (v, v) +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 (fmap 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 + [(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs})) + ,(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 - pd n = pdArity n . pdForce genericTk n = reverse . genericDrop n . reverse genericDp n = reverse . genericTake n . reverse -toPBool True = VApp (cPredef,cPTrue) [] -toPBool False = VApp (cPredef,cPFalse) [] +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 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 (fmap (\v -> apply g v vs) fvs) +apply g (VS v1 v2 vs') vs = VS v1 v2 (vs'++vs) +apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs +apply g v [] = v + +data BubbleVariants + = BubbleFree Int + | BubbleOpts Value [Value] + +bubble v = snd (bubble v) + where + 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 + bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env + bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2 + bubble v@(VRecType lbls ext) = + let (union,lbls') = mapAccumL descendR Map.empty lbls + in (union, addVariants (VRecType lbls' ext) union) + bubble (VR as) = liftL' VR as + bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs + bubble (VExtR v1 v2) = lift2 VExtR v1 v2 + bubble (VTable v1 v2) = lift2 VTable v1 v2 + bubble (VT v env c cs) = lift1L' (\v env -> VT v env c cs) v env + bubble (VV v vs) = lift1L VV v vs + bubble (VS v1 v2 vs) = lift2L VS v1 v2 vs + bubble v@(VSort _) = lift0 v + bubble v@(VInt _) = lift0 v + bubble v@(VFlt _) = lift0 v + bubble v@(VStr _) = lift0 v + bubble v@VEmpty = lift0 v + bubble (VC v1 v2) = lift2 VC v1 v2 + bubble (VGlue v1 v2) = lift2 VGlue v1 v2 + bubble v@(VPatt _ _ _) = lift0 v + bubble (VPattType v) = lift1 VPattType v + bubble v@(VFV c (VarFree vs)) + | null vs = (Map.empty, v) + | otherwise = let (union,vs') = mapAccumL descend Map.empty vs + in (Map.insert c (BubbleFree (length vs),1) union, VFV c (VarFree vs')) + bubble v@(VFV c (VarOpts n os)) + | null os = (Map.empty, v) + | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os + in (Map.insert c (BubbleOpts n (map fst os),1) union, VFV c (VarOpts n os')) + bubble (VAlts v vs) = lift1L2 VAlts v vs + bubble (VStrs vs) = liftL VStrs vs + bubble (VMarkup tag attrs vs) = + let (union1,attrs') = mapAccumL descend' Map.empty attrs + (union2,vs') = mapAccumL descendL union1 vs + in (union2, VMarkup tag attrs' vs') + bubble (VReset ctl mb_cv v id) = + let (union,v') = bubble v + in (Map.empty,VReset ctl mb_cv v' id) + bubble (VSymCat d i0 vs) = + let (union,vs') = mapAccumL descendC Map.empty vs + in (union, addVariants (VSymCat d i0 vs') union) + bubble v@(VError _) = lift0 v + bubble v@(VInts _ _) = lift0 v + + lift0 v = (Map.empty, v) + + lift1 f v = + let (union,v') = bubble v + in (union,f v') + + liftL f vs = + let (union,vs') = mapAccumL descend Map.empty vs + in (union, addVariants (f vs') union) + + liftL' f vs = + let (union,vs') = mapAccumL descend' Map.empty vs + in (union, addVariants (f vs') union) + + lift1L f v vs = + let (choices,v') = bubble v + (union, vs') = mapAccumL descend (unitfy choices) vs + in (union, addVariants (f v' vs') union) + + lift1L' f v vs = + let (choices,v') = bubble v + (union, vs') = mapAccumL descend' (unitfy choices) vs + in (union, addVariants (f v' vs') union) + + lift1L2 f v vs = + let (choices,v') = bubble v + (union, vs') = mapAccumL descend2 (unitfy choices) vs + in (union, addVariants (f v' vs') union) + + lift2L f v1 v2 vs = + let (choices1,v1') = bubble v1 + (choices2,v2') = bubble v2 + union = mergeChoices2 choices1 choices2 + (union', vs') = mapAccumL descend union vs + in (union', addVariants (f v1' v2' vs') union') + + lift2 f v1 v2 = + let (choices1,v1') = bubble v1 + (choices2,v2') = bubble v2 + union = mergeChoices2 choices1 choices2 + in (union, addVariants (f v1' v2') union) + + descend union v = + let (choices,v') = bubble v + in (mergeChoices1 union choices,v') + + descend' :: Map.Map Choice (BubbleVariants,Int) -> (a,Value) -> (Map.Map Choice (BubbleVariants,Int),(a,Value)) + descend' union (x,v) = + let (choices,v') = bubble v + in (mergeChoices1 union choices,(x,v')) + + descend2 union (v1,v2) = + let (choices1,v1') = bubble v1 + (choices2,v2') = bubble v2 + in (mergeChoices1 (mergeChoices1 union choices1) choices2,(v1',v2')) + + descendC union (i,(v,ty)) = + let (choices,v') = bubble v + in (mergeChoices1 union choices,(i,(v',ty))) + + descendL union (L loc v) = + let (choices,v') = bubble v + in (mergeChoices1 union choices,L loc v') + + descendR union (l,b,v) = + let (choices,v') = bubble v + in (mergeChoices1 union choices,(l,b,v')) + + addVariants v = Map.foldrWithKey addVariant v + where + addVariant c (bvs,cnt) v + | cnt > 1 = VFV c $ case bvs of + BubbleFree k -> VarFree (replicate k v) + BubbleOpts n os -> VarOpts n (map (\l -> (l,v)) os) + | otherwise = v + + unitfy = fmap (\(n,_) -> (n,1)) + 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 poison (cPredef,cPTrue) [] +toPBool False = VApp poison (cPredef,cPFalse) [] occur s1 [] = False occur s1 s2@(_:tail) = check s1 s2 @@ -355,669 +520,710 @@ update lbl v (a@(lbl',_):as) | lbl==lbl' = (lbl,v) : as | otherwise = a : update lbl v as +update3 lbl o v [] = [(lbl,o,v)] +update3 lbl o v (a@(lbl',o',_):as) + | lbl==lbl' = (lbl,o||o',v) : as + | otherwise = a : update3 lbl o v as -patternMatch v0 [] = return v0 -patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 +patternMatch g s v0 [] = v0 +patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 where - match env [] eqs args = eval env t args + match env [] eqs args = eval g env s t args match env (PT ty p :ps) eqs args = match env (p:ps) eqs args match env (PAlt p1 p2:ps) eqs args = match env (p1:ps) ((env,p2:ps,args,t):eqs) args - match env (PM q :ps) eqs args = do t <- getResDef q - v <- eval [] t [] - case v of - VPatt _ _ p -> match env (p:ps) eqs args - _ -> evalError $ hang "Expected pattern macro:" 4 - (pp t) + match env (PM q :ps) eqs args = case lookupResDef gr q of + Ok t -> case eval g [] unit t [] of + VPatt _ _ p -> match env (p:ps) eqs args + _ -> error $ render (hang "Expected pattern macro:" 4 + (pp t)) + Bad msg -> error msg + where + Gl gr _ = g match env (PV v :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args match env (PAs v p :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args) match env (PW :ps) eqs (arg:args) = match env ps eqs args match env (PTilde _ :ps) eqs (arg:args) = match env ps eqs args - match env (p :ps) eqs (arg:args) = do - v <- force arg - match' env p ps eqs arg v args + match env (p :ps) eqs (arg:args) = match' env p ps eqs arg args - match' env p ps eqs arg v args = do - case (p,v) of - (p, VMeta i vs) -> susp i (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args) - (p, VGen i vs) -> return v0 - (p, VSusp i k vs) -> susp i (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args) - (PP q qs, VApp r tnks) - | q == r -> match env (qs++ps) eqs (tnks++args) - (PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args + match' env p ps eqs arg args = + case (p,arg) of + (p, VMeta i vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) [] + (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 (fmap (\arg -> match' env p ps eqs arg args) 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) - | s1 == s2 -> match env ps eqs args + | s1 == s2 -> match env ps eqs args (PString s1, VEmpty) - | null s1 -> match env ps eqs args + | null s1 -> match env ps eqs args (PSeq min1 max1 p1 min2 max2 p2,v) - -> case value2string v of - Const s -> let n = length s - lo = min1 `max` (n-fromMaybe n max2) - hi = (n-min2) `min` fromMaybe n max1 - (ds,cs) = splitAt lo s - in if lo <= hi - then do eqs <- matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args - patternMatch v0 eqs - else patternMatch v0 eqs - RunTime -> return v0 - NonExist-> patternMatch v0 eqs + -> case value2string g v of + Const str -> let n = length str + lo = min1 `max` (n-fromMaybe n max2) + hi = (n-min2) `min` fromMaybe n max1 + (ds,cs) = splitAt lo str + + eqs' = matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args + + in patternMatch g s v0 eqs' + RunTime -> v0 + NonExist -> patternMatch g s v0 eqs (PRep minp maxp p, v) - -> case value2string v of - Const s -> do let n = length s `div` (max minp 1) - eqs <- matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args) - patternMatch v0 eqs - RunTime -> return v0 - NonExist-> patternMatch v0 eqs - (PChar, VStr [c]) -> match env ps eqs args + -> case value2string g v of + Const str -> let n = length (str::String) `div` (max minp 1) + eqs' = matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args) + in patternMatch g s v0 eqs' + RunTime -> v0 + NonExist -> patternMatch g s v0 eqs + (PChar, VStr [_]) -> match env ps eqs args (PChars cs, VStr [c]) | elem c cs -> match env ps eqs args (PInt n, VInt m) | n == m -> match env ps eqs args (PFloat n, VFlt m) | n == m -> match env ps eqs args - _ -> patternMatch v0 eqs + _ -> patternMatch g s v0 eqs matchRec env [] as ps eqs args = match env ps eqs args matchRec env ((lbl,p):pas) as ps eqs args = case lookup lbl as of Just tnk -> matchRec env pas as (p:ps) eqs (tnk:args) - Nothing -> evalError ("Missing value for label" <+> pp lbl) + Nothing -> VError ("Missing value for label" <+> pp lbl) - matchStr env ps eqs i ds [] args = do - arg1 <- newEvaluatedThunk (string2value (reverse ds)) - arg2 <- newEvaluatedThunk (string2value []) - return ((env,ps,arg1:arg2:args,t) : eqs) - matchStr env ps eqs 0 ds cs args = do - arg1 <- newEvaluatedThunk (string2value (reverse ds)) - arg2 <- newEvaluatedThunk (string2value cs) - return ((env,ps,arg1:arg2:args,t) : eqs) - matchStr env ps eqs i ds (c:cs) args = do - arg1 <- newEvaluatedThunk (string2value (reverse ds)) - arg2 <- newEvaluatedThunk (string2value (c:cs)) - eqs <- matchStr env ps eqs (i-1 :: Int) (c:ds) cs args - return ((env,ps,arg1:arg2:args,t) : eqs) + matchStr env ps eqs i ds [] args = + (env,ps,(string2value (reverse ds)):(string2value []):args,t) : eqs + matchStr env ps eqs 0 ds cs args = + (env,ps,(string2value (reverse ds)):(string2value cs):args,t) : eqs + matchStr env ps eqs i ds (c:cs) args = + (env,ps,(string2value (reverse ds)):(string2value (c:cs)):args,t) : + matchStr env ps eqs (i-1 :: Int) (c:ds) cs args - matchRep env 0 minp maxp p minq maxq q ps eqs args = do - return eqs - matchRep env n minp maxp p minq maxq q ps eqs args = do + matchRep env 0 minp maxp p minq maxq q ps eqs args = eqs + matchRep env n minp maxp p minq maxq q ps eqs args = matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args - -vtableSelect v0 ty tnks tnk2 vs = do - v2 <- force tnk2 - (i,_) <- value2index v2 ty - v <- force (tnks !! i) - apply v vs +vtableSelect g v0 ty cs v2 vs = + apply g (select (value2index v2 ty)) vs where + select (Const (i,_)) = cs !! i + select (CSusp i k) = VSusp i (\v -> select (k v)) [] + select (CFV c vs) = VFV c (fmap select vs) + select _ = v0 + + value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty) + value2index (VSusp i k vs) ty = CSusp i (\v -> value2index (apply g (k v) vs) ty) value2index (VR as) (RecType lbls) = compute lbls where - compute [] = return (0,1) - compute ((lbl,ty):lbls) = do + compute [] = pure (0,1) + compute ((lbl,ty):lbls) = case lookup lbl as of - Just tnk -> do v <- force tnk - (r, cnt ) <- value2index v ty - (r',cnt') <- compute lbls - return (r*cnt'+r',cnt*cnt') - Nothing -> evalError ("Missing value for label" <+> pp lbl $$ - "among" <+> hsep (punctuate (pp ',') (map fst as))) - value2index (VApp q tnks) ty = do - (r ,ctxt,cnt ) <- getIdxCnt q - (r', cnt') <- compute ctxt tnks - return (r+r',cnt) + Just v -> liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt')) + (value2index v ty) + (compute lbls) + Nothing -> error (show ("Missing value for label" <+> pp lbl $$ + "among" <+> hsep (punctuate (pp ',') (map fst as)))) + value2index (VApp c q args) ty = + let (r ,ctxt,cnt ) = getIdxCnt q + in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args) where - getIdxCnt q = do - (_,ResValue (L _ ty) idx) <- getInfo q - let (ctxt,QC p) = typeFormCnc ty - (_,ResParam _ (Just (_,cnt))) <- getInfo p - return (idx,ctxt,cnt) + getIdxCnt q = + let (_,ResValue (L _ ty) idx) = getInfo q + (ctxt,QC p) = typeFormCnc ty + (_,ResParam _ (Just (_,cnt))) = getInfo p + in (idx,ctxt,cnt) - compute [] [] = return (0,1) - compute ((_,_,ty):ctxt) (tnk:tnks) = do - v <- force tnk - (r, cnt ) <- value2index v ty - (r',cnt') <- compute ctxt tnks - return (r*cnt'+r',cnt*cnt') + compute [] [] = pure (0,1) + compute ((_,_,ty):ctxt) (v:vs) = + liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt')) + (value2index v ty) + (compute ctxt vs) + + getInfo :: QIdent -> (ModuleName,Info) + getInfo q = + case lookupOrigInfo gr q of + Ok res -> res + Bad msg -> error msg + + Gl gr _ = g value2index (VInt n) ty - | Just max <- isTypeInts ty = return (fromIntegral n,fromIntegral max+1) - value2index (VMeta i vs) ty = do - v <- susp i (\v -> apply v vs) - value2index v ty - value2index (VSusp i k vs) ty = do - v <- susp i (\v -> k v >>= \v -> apply v vs) - value2index v ty - value2index v ty = do t <- value2term True [] v - evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$ - "cannot be evaluated at compile time.") + | Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1) + value2index (VFV c vs) ty = CFV c (fmap (\v -> value2index v ty) vs) + value2index v ty = RunTime -susp i ki = EvalM $ \globals@(Gl gr _) k e mt d r msgs -> do - s <- readSTRef i - case s of - Narrowing id (QC q) -> case lookupOrigInfo gr q of - Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k e mt d r msgs s m ps - Bad msg -> return (Fail (pp msg) msgs) - Narrowing id ty - | Just max <- isTypeInts ty - -> bindInt globals k e mt d r msgs s 0 max - Evaluated _ v -> case ki v of - EvalM f -> f globals k e mt d r msgs - _ -> k (VSusp i ki []) mt d r msgs +value2term :: Globals -> [Ident] -> Value -> Check Term +value2term g xs v = do + res <- runEvalM g (value2termM False xs v) + case res of + [t] -> return t + ts -> return (FV ts) + +data MetaState + = Bound Scope Value + | Narrowing Choice Type + | Residuation Scope +data OptionInfo + = OptionInfo + { optChoice :: Choice + , optValue :: Int + , optLabel :: Value + , optChoices :: [Value] + } +data State + = State + { input :: [(Choice, Int)] + , 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) + +instance Functor EvalM where + fmap f (EvalM m) = EvalM (\g k -> m g (k . f)) + +instance Applicative EvalM where + pure x = EvalM (\g k -> k x) + (EvalM f) <*> (EvalM h) = EvalM (\g k -> f g (\fn -> h g (\x -> k (fn x)))) + +instance Alternative EvalM where + empty = EvalM (\g k _ r msgs -> Success r msgs) + (EvalM f) <|> (EvalM g) = EvalM $ \gl k state r msgs -> + case f gl k state r msgs of + Fail msg msgs -> Fail msg msgs + Success r msgs -> g gl k state r msgs + +instance Monad EvalM where + (EvalM f) >>= h = EvalM (\g k -> f g (\x -> case h x of {EvalM h -> h g k})) + +instance MonadFail EvalM where + fail msg = EvalM (\g k _ _ msgs -> Fail (pp msg) msgs) + +instance MonadPlus EvalM where + +evalError msg = EvalM (\g k _ _ msgs -> Fail msg msgs) + +evalWarn msg = EvalM (\g k state r msgs -> k () state r (msg:msgs)) + +runEvalM :: Globals -> EvalM a -> Check [a] +runEvalM g (EvalM f) = Check $ \(es,ws) -> + case f g (\x state xs ws -> Success (x:xs) ws) empty [] ws of + Fail msg ws -> Fail msg (es,ws) + Success xs ws -> Success (reverse xs) (es,ws) where - bindParam gr k e mt d r msgs s m [] = return (Success r msgs) - bindParam gr k e mt d r msgs s m ((p, ctxt):ps) = do - (mt',tnks) <- mkArgs mt ctxt - let v = VApp (m,p) tnks - writeSTRef i (Evaluated 0 v) - res <- case ki v of - EvalM f -> f gr k e mt' d r msgs - writeSTRef i s - case res of - Fail msg msgs -> return (Fail msg msgs) - Success r msgs -> bindParam gr k e mt d r msgs s m ps + empty = State [] Map.empty Map.empty [] - mkArgs mt [] = return (mt,[]) - mkArgs mt ((_,_,ty):ctxt) = do - let i = case Map.maxViewWithKey mt of - Just ((i,_),_) -> i+1 - _ -> 0 - tnk <- newSTRef (Narrowing i ty) - (mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt - return (mt,tnk:tnks) +runEvalMWithInput :: Globals -> [(Choice,Int)] -> EvalM a -> Check [(a, [OptionInfo])] +runEvalMWithInput g input (EvalM f) = Check $ \(es,ws) -> + case f g (\x (State _ cs mvs os) xs ws -> Success ((x,reverse os):xs) ws) init [] ws of + Fail msg ws -> Fail msg (es,ws) + Success xs ws -> Success (reverse xs) (es,ws) + where + init = State input Map.empty Map.empty [] - bindInt gr k e mt d r msgs s iv max - | iv <= max = do - let v = VInt iv - writeSTRef i (Evaluated 0 v) - res <- case ki v of - EvalM f -> f gr k e mt d r msgs - writeSTRef i s - case res of - Fail msg msgs -> return (Fail msg msgs) - Success r msgs -> bindInt gr k e mt d r msgs s (iv+1) max - | otherwise = return (Success r msgs) +reset :: EvalM a -> EvalM [a] +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 +reset1 :: EvalM a -> EvalM (Maybe a) +reset1 (EvalM f) = EvalM $ \g k state r ws -> + case f g (\x' state x ws -> Success (x <|> Just x') ws) state Nothing ws of + Fail msg ws -> Fail msg ws + Success x ws -> k x state r ws -value2term flat xs (VApp q tnks) = - foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (if fst q == cPredef then Q q else QC q) tnks -value2term flat xs (VMeta m vs) = do - s <- getRef m - case s of - Evaluated _ v -> do v <- apply v vs - value2term flat xs v - Unevaluated env t -> do v <- eval env t vs - value2term flat xs v - Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs - Residuation i _ ctr -> case ctr of - Just ctr -> value2term flat xs ctr - Nothing -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs - Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs -value2term flat xs (VSusp j k vs) = do - v <- k (VGen maxBound vs) - value2term flat xs v -value2term flat xs (VGen j tnks) = - foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Vr (reverse xs !! j)) tnks -value2term flat xs (VClosure env (Abs b x t)) = do - tnk <- newEvaluatedThunk (VGen (length xs) []) - v <- eval ((x,tnk):env) t [] - let x' = mkFreshVar xs x - t <- value2term flat (x':xs) v +globals :: EvalM Globals +globals = EvalM (\g k -> k g) + +variants :: Choice -> [a] -> EvalM a +variants c xs = EvalM (\g k state@(State input choices metas opts) r msgs -> + case Map.lookup c choices of + Just j -> k (xs !! j) state r msgs + Nothing -> backtrack 0 xs k input choices metas opts r msgs) + where + backtrack j [] k input choices metas opts r msgs = Success r msgs + backtrack j (x:xs) k input choices metas opts r msgs = + case k x (State input (Map.insert c j choices) metas opts) r msgs of + Fail msg msgs -> Fail msg msgs + Success r msgs -> backtrack (j+1) xs k input choices metas opts r msgs + +variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term +variants' c f xs = EvalM (\g k state@(State input 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 + Nothing -> case backtrack g 0 xs input choices metas opts [] msgs of + Fail msg msgs -> Fail msg msgs + Success ts msgs -> k (FV (reverse ts)) state r msgs) + where + backtrack g j [] input choices metas opts ts msgs = Success ts msgs + backtrack g j (x:xs) input choices metas opts ts msgs = + case f x of + EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State input (Map.insert c j choices) metas opts) ts msgs of + Fail msg msgs -> Fail msg msgs + Success ts msgs -> backtrack g (j+1) xs input choices metas opts ts msgs + +try :: Int -> (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b +try sz f select xs = EvalM (\g k state r msgs -> + let (state',res,msgs') = backtrack sz g xs state [] msgs + in case select res of + EvalM f' -> f' g k state' r msgs') + where + backtrack sz g [] state res msgs = (state,res,msgs) + backtrack sz g (x:xs) state res msgs = + case f x of + EvalM f -> case f g (\y state' (_,ys) msgs -> Success (cut sz state state',y:ys) msgs) state (state,res) msgs of + Fail msg _ -> backtrack sz g xs state res msgs + Success (state,res) msgs -> backtrack sz g xs state res msgs + + cut sz state state' = state'{metaVars=Map.mapWithKey select (metaVars state')} + where + select k ms + | k <= sz = ms + | otherwise = case Map.lookup k (metaVars state) of + Just ms -> ms + Nothing -> ms + +newResiduation :: Scope -> EvalM MetaId +newResiduation scope = EvalM (\g k (State input choices metas opts) r msgs -> + let meta_id = Map.size metas+1 + in k meta_id (State input choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs) + +checkpoint :: EvalM Int +checkpoint = EvalM (\g k state r msgs -> + k (Map.size (metaVars state)) state r msgs) + +getMeta :: MetaId -> EvalM MetaState +getMeta i = EvalM (\g k state r msgs -> + case Map.lookup i (metaVars state) of + Just ms -> k ms state r msgs + Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) + +setMeta :: MetaId -> MetaState -> EvalM () +setMeta i ms = EvalM (\g k (State input choices metas opts) r msgs -> + let state' = State input choices (Map.insert i ms metas) opts + in k () state' r msgs) + +value2termM :: Bool -> [Ident] -> Value -> EvalM Term +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 + case mv of + Bound scope v -> do g <- globals + value2termM flat (map fst scope) (apply g v vs) + Residuation _ -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs +value2termM flat xs (VSusp j k vs) = + let v = k (VGen maxBound vs) + in value2termM flat xs v +value2termM flat xs (VGen j tnks) = + foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (Vr (reverse xs !! j)) tnks +value2termM flat xs (VClosure env s (Abs b x t)) = do + g <- globals + let v = eval g ((x,VGen (length xs) []):env) s t [] + x' = mkFreshVar xs x + t <- value2termM flat (x':xs) v return (Abs b x' t) -value2term flat xs (VProd b x v1 v2) - | x == identW = do t1 <- value2term flat xs v1 - v2 <- case v2 of - VClosure env t2 -> eval env t2 [] - v2 -> return v2 - t2 <- value2term flat xs v2 - return (Prod b x t1 t2) - | otherwise = do t1 <- value2term flat xs v1 - tnk <- newEvaluatedThunk (VGen (length xs) []) - v2 <- case v2 of - VClosure env t2 -> eval ((x,tnk):env) t2 [] - v2 -> return v2 - t2 <- value2term flat (x:xs) v2 - return (Prod b (mkFreshVar xs x) t1 t2) -value2term flat xs (VRecType lbls) = do - lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term flat xs v)) lbls +value2termM flat xs (VClosure env s t) = do + return t +value2termM flat xs (VProd b x v1 (VClosure env c2 t2)) = do + g <- globals + t1 <- value2termM flat xs v1 + t2 <- value2termM flat (x:xs) (eval g ((x,VGen (length xs) []):env) c2 t2 []) + return (Prod b (mkFreshVar xs x) t1 t2) +value2termM flat xs (VProd b x v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 + return (Prod b x t1 t2) +value2termM flat xs (VRecType lbls _) = do + lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls return (RecType lbls) -value2term flat xs (VR as) = do - as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (tnk2term flat xs tnk)) as +value2termM flat xs (VR as) = do + as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as return (R as) -value2term flat xs (VP v lbl tnks) = do - t <- value2term flat xs v - foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (P t lbl) tnks -value2term flat xs (VExtR v1 v2) = do - t1 <- value2term flat xs v1 - t2 <- value2term flat xs v2 +value2termM flat xs (VP v lbl vs) = do + t <- value2termM flat xs v + foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (P t lbl) vs +value2termM flat xs (VExtR v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 return (ExtR t1 t2) -value2term flat xs (VTable v1 v2) = do - t1 <- value2term flat xs v1 - t2 <- value2term flat xs v2 +value2termM flat xs (VTable v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 return (Table t1 t2) -value2term flat xs (VT vty env cs)= do - ty <- value2term flat xs vty +value2termM flat xs (VT vty env s cs)= do + ty <- value2termM flat xs vty cs <- forM cs $ \(p,t) -> do - (_,xs',env') <- pattVars (length xs,xs,env) p - v <- eval env' t [] - t <- value2term flat xs' v + let (_,xs',env') = pattVars (length xs,xs,env) p + g <- globals + t <- value2termM flat xs' (eval g env' s t []) return (p,t) return (T (TTyped ty) cs) -value2term flat xs (VV vty tnks)= do - ty <- value2term flat xs vty - ts <- mapM (tnk2term flat xs) tnks +value2termM flat xs (VV vty vs)= do + ty <- value2termM flat xs vty + ts <- mapM (value2termM flat xs) vs return (V ty ts) -value2term flat xs (VS v1 tnk2 tnks) = do - t1 <- value2term flat xs v1 - t2 <- tnk2term flat xs tnk2 - foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (S t1 t2) tnks -value2term flat xs (VSort s) = return (Sort s) -value2term flat xs (VStr tok) = return (K tok) -value2term flat xs (VInt n) = return (EInt n) -value2term flat xs (VFlt n) = return (EFloat n) -value2term flat xs VEmpty = return Empty -value2term flat xs (VC v1 v2) = do - t1 <- value2term flat xs v1 - t2 <- value2term flat xs v2 +value2termM flat xs (VS v1 v2 vs) = + case v1 of + VT vty env s cs -> do + ty <- value2termM flat xs vty + g <- globals + cs <- forM cs $ \(p,t) -> do + let (_,xs',env') = pattVars (length xs,xs,env) p + t <- value2termM flat xs' (eval g env' s t vs) + return (p,t) + t2 <- value2termM flat xs v2 + return (S (T (TTyped ty) cs) t2) + + VV vty vs' -> do + ty <- value2termM flat xs vty + g <- globals + ts <- forM vs' $ \v -> + value2termM flat xs (apply g v vs) + t2 <- value2termM flat xs v2 + return (S (V ty ts) t2) + + v1 -> do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 + foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (S t1 t2) vs +value2termM flat xs (VSort s) = return (Sort s) +value2termM flat xs (VStr tok) = return (K tok) +value2termM flat xs (VInt n) = return (EInt n) +value2termM flat xs (VFlt n) = return (EFloat n) +value2termM flat xs VEmpty = return Empty +value2termM flat xs (VC v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 return (C t1 t2) -value2term flat xs (VGlue v1 v2) = do - t1 <- value2term flat xs v1 - t2 <- value2term flat xs v2 +value2termM flat xs (VGlue v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 return (Glue t1 t2) -value2term flat xs (VPatt min max p) = return (EPatt min max p) -value2term flat xs (VPattType v) = do - t <- value2term flat xs v - return (EPattType t) -value2term flat xs (VAlts vd vas) = do - d <- value2term flat xs vd +value2termM True xs (VFV i (VarFree vs)) = do + v <- variants i vs + value2termM True xs v +value2termM False xs (VFV c (VarFree vs)) = variants' c (value2termM False xs) vs +value2termM flat xs (VFV c (VarOpts n os)) = + EvalM $ \g k (State input choices metas opts) r msgs -> + let (j,input',choices',opts') = + case Map.lookup c choices of + Just j -> (j,input,choices,opts) + Nothing -> case input of + (c',j):input | c == c' -> let oi = OptionInfo c j n (map fst os) + in (j,input,Map.insert c j choices,oi:opts) + _ -> let oi = OptionInfo c 0 n (map fst os) + in (0,[],Map.insert c 0 choices,oi:opts) + in case os `maybeAt` j of + Just (l,t) -> case value2termM flat xs t of + EvalM f -> f g k (State input' choices' metas opts') r msgs + Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs +value2termM flat xs (VPatt min max p) = return (EPatt min max p) +value2termM flat xs (VPattType v) = do t <- value2termM flat xs v + return (EPattType t) +value2termM flat xs (VAlts vd vas) = do + d <- value2termM flat xs vd as <- forM vas $ \(vt,vs) -> do - t <- value2term flat xs vt - s <- value2term flat xs vs + t <- value2termM flat xs vt + s <- value2termM flat xs vs return (t,s) return (Alts d as) -value2term flat xs (VStrs vs) = do - ts <- mapM (value2term flat xs) vs +value2termM flat xs (VStrs vs) = do + ts <- mapM (value2termM flat xs) vs return (Strs ts) -value2term flat xs (VMarkup tag as vs) = do - as <- mapM (\(id,v) -> value2term flat xs v >>= \t -> return (id,t)) as - ts <- mapM (value2term flat xs) vs - return (Markup tag as (map noLoc ts)) -value2term flat xs (VCInts (Just i) Nothing) = return (App (Q (cPredef,cInts)) (EInt i)) -value2term flat xs (VCInts Nothing (Just j)) = return (App (Q (cPredef,cInts)) (EInt j)) -value2term flat xs (VCRecType lctrs) = do - ltys <- mapM (\(l,o,ctr) -> value2term flat xs ctr >>= \ty -> return (l,ty)) lctrs - return (RecType ltys) -value2term flat xs (VSymCat d r rs) = return (TSymCat d r [(i,(identW,ty)) | (i,(_,ty)) <- rs]) -value2term flat xs v = error (showValue v) +value2termM flat xs (VMarkup tag as vs) = do + as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as + ts <- mapM (mapM (value2termM flat xs)) vs + return (Markup tag as ts) +value2termM flat xs (VReset ctl mb_cv v mb_qid) = do + ts <- reset (value2termM True xs v) + reduce ctl mb_cv ts + where + reduce ctl mb_cv ts + | ctl == cConcat = do + ts <- case mb_cv of + Just (VInt n) -> return (genericTake n ts) + Nothing -> return ts + _ -> evalError (pp "[concat: .. | ..] requires an integer constant") + case ts of + [t] -> return t + ts -> return (Markup identW [] (map noLoc ts)) + | ctl == cConcat' = do + ts <- case mb_cv of + Just (VInt n) -> return (genericTake n ts) + Nothing -> return ts + _ -> evalError (pp "[concat: .. | ..] requires an integer constant") + case ts of + [] -> mzero + [t] -> return t + ts -> return (Markup identW [] (map noLoc ts)) + | ctl == cOne = + case (ts,mb_cv) of + ([] ,Nothing) -> mzero + ([] ,Just v) -> value2termM flat xs v + (t:ts,_) -> return t + | ctl == cSelect = + case mb_cv of + Just (VInt n) | n >= 0 -> select n ts' + | otherwise -> select (-n-1) (reverse ts') + where + ts' = sortBy compareKey ts -pattVars st (PP _ ps) = foldM pattVars st ps + select _ [] = mzero + select 0 (t:ts) = + case t of + R rs -> case lookup (ident2label cp1) rs of + Just (_,t) -> return t + Nothing -> evalError (pp "Missing label p1") + _ -> evalError (pp "The term must be a record") + select n (t:ts) = select (n-1) ts + _ -> evalError (pp "[select: .. | ..] requires an integer constant") + | ctl == cFilter = + let filter [] = mzero + filter (t:ts) = + case t of + R rs -> case (lookup (ident2label cp1) rs, lookup (ident2label cp2) rs) of + (Just (_,t), Just (_,Q q)) + | q == (cPredef,cTrue) -> pure t `mplus` filter ts + _ -> filter ts + _ -> evalError (pp "The term must be a record") + in filter ts + | ctl == cDefault = + case (ts,mb_cv) of + ([] ,Nothing) -> mzero + ([] ,Just v) -> value2termM flat xs v + (ts,_) -> msum (map pure ts) + | ctl == cList = + case (ts,mb_cv) of + ([], _) -> mzero + ([t], _) -> return t + (ts,Just cv) -> + do let Just (mn,id) = mb_qid + cat = showIdent id + ct <- value2termM flat xs cv + t <- listify mn cat ts + return (App (App (QC (mn,identS ("Conj"++cat))) ct) t) + _ -> evalError (pp "[list: .. | ..] requires an argument") + | ctl == cLen = + case mb_cv of + Just cv -> do g <- globals + value2termM True xs (apply g cv [VInt (genericLength ts)]) + Nothing -> return (EInt (genericLength ts)) + | ctl == cConst = + case mb_cv of + Just cv -> do ct <- value2termM flat xs cv + msum (map (pure . const ct) ts) + _ -> evalError (pp "[const: .. | ..] requires an argument") + | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") + + listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2) + listify mn cat (t1:ts) = do t2 <- listify mn cat ts + return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2) + + compareKey (R rs1) (R rs2) = + case (lookup (ident2label cp2) rs1, lookup (ident2label cp2) rs2) of + (Just (_,K s1), Just (_,K s2)) -> compare s1 s2 + +value2termM flat xs (VError msg) = evalError msg +value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n)) +value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v) + + +pattVars st (PP _ ps) = foldl pattVars st ps pattVars st (PV x) = case st of - (i,xs,env) -> do tnk <- newEvaluatedThunk (VGen i []) - return (i+1,x:xs,(x,tnk):env) -pattVars st (PR as) = foldM (\st (_,p) -> pattVars st p) st as + (i,xs,env) -> (i+1,x:xs,(x,VGen i []):env) +pattVars st (PR as) = foldl (\st (_,p) -> pattVars st p) st as pattVars st (PT ty p) = pattVars st p -pattVars st (PAs x p) = do st <- case st of - (i,xs,env) -> do tnk <- newEvaluatedThunk (VGen i []) - return (i+1,x:xs,(x,tnk):env) - pattVars st p +pattVars st (PAs x p) = case st of + (i,xs,env) -> pattVars (i+1,x:xs,(x,VGen i []):env) p pattVars st (PImplArg p) = pattVars st p -pattVars st (PSeq _ _ p1 _ _ p2) = do st <- pattVars st p1 - pattVars st p2 -pattVars st _ = return st +pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2 +pattVars st _ = st -data ConstValue a - = Const a - | RunTime - | NonExist -instance Functor ConstValue where - fmap f (Const c) = Const (f c) - fmap f RunTime = RunTime - fmap f NonExist = NonExist -instance Applicative ConstValue where - pure = Const +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" +ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]" +ppValue q d (VProd bt x a b) = + if x == identW && bt == Explicit + then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b) + else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b) +ppValue q d (VRecType xs ext) + | q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of + [cat] -> pp cat + _ -> doc + | otherwise = doc + where + doc = braces (fsep (punctuate ';' ([l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs] ++ [pp ".." | ext]))) +ppValue q d (VR _) = pp "VR" +ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs)) +ppValue q d (VExtR _ _) = pp "VExtR" +ppValue q d (VTable kt vt) = prec d 0 (ppValue q 3 kt <+> "=>" <+> ppValue q 0 vt) +ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$ + nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$ + '}' + where + ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e +ppValue q d (VV _ _) = pp "VV" +ppValue q d (VS v1 v2 vs) = prec d 3 (hsep (hang (ppValue q 3 v1) 2 ("!" <+> ppValue q 4 v2) : map (ppValue q 5) vs)) +ppValue q d (VSort s) = pp s +ppValue q d (VInt n) = pp n +ppValue q d (VFlt f) = pp f +ppValue q d (VStr s) = ppTerm q d (K s) +ppValue q d VEmpty = pp "[]" +ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 v2)) +ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2) +ppValue q d (VPatt _ _ p) = prec d 4 ('#' <+> ppPatt q 2 p) +ppValue q d (VPattType v) = prec d 4 ("pattern" <+> ppValue q 0 v) +ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants vs))))) +ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs)))) +ppValue q d (VStrs _) = pp "VStrs" +ppValue q d (VMarkup _ _ _) = pp "VMarkup" +ppValue q d (VReset ctl ct t _) = pp "[" <> pp ctl <> + maybe PP.empty (\v -> pp ':' <+> ppValue q 6 v) ct <> + pp "|" <> ppValue q 0 t <> + pp "]" +ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>' +ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg))) +ppValue q d (VInts n ext) + | ext = prec d 4 (pp "Ints" <+> brackets (pp n <> "..")) + | otherwise = prec d 4 (pp "Ints" <+> pp n) - (Const f) <*> (Const x) = Const (f x) - NonExist <*> _ = NonExist - _ <*> NonExist = NonExist - RunTime <*> _ = RunTime - _ <*> RunTime = RunTime +ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y -#if MIN_VERSION_base(4,10,0) - liftA2 f (Const a) (Const b) = Const (f a b) - liftA2 f NonExist _ = NonExist - liftA2 f _ NonExist = NonExist - liftA2 f RunTime _ = RunTime - liftA2 f _ RunTime = RunTime -#endif +prec d1 d2 doc + | d1 > d2 = parens doc + | otherwise = doc -instance Foldable ConstValue where - foldr f a (Const x) = f x a - foldr f a RunTime = a - foldr f a NonExist = a +value2string g v = fmap (\(_,ws,_) -> unwords ws) (value2string' g v False [] []) -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) -value2string' (VStr w) _ ws qs = Const (False,w :ws,qs) -value2string' VEmpty b ws qs = Const (b,ws,qs) -value2string' (VC v1 v2) b ws qs = - case value2string' v2 b ws qs of - Const (b,ws,qs) -> value2string' v1 b ws qs - res -> res -value2string' (VApp q []) b ws qs +value2string' g (VMeta i vs) b ws qs = CSusp i (\v -> value2string' g (apply g v vs) b ws qs) +value2string' g (VSusp i k vs) b ws qs = CSusp i (\v -> value2string' g (apply g (k v) vs) b ws qs) +value2string' g (VStr w1) True (w2:ws) qs = Const (False,(w1++w2):ws,qs) +value2string' g (VStr w) _ ws qs = Const (False,w :ws,qs) +value2string' g VEmpty b ws qs = Const (b,ws,qs) +value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b ws qs) + where + concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs + concat v1 (CFV c vs) = CFV c (fmap (concat v1) vs) + concat v1 res = res +value2string' g (VApp c q []) b ws qs | q == (cPredef,cNonExist) = NonExist -value2string' (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' (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' (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' (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) all_capit (w : ws) = Const (b,map toUpper w : ws,qs) -value2string' (VAlts vd vas) b ws qs = +value2string' g (VAlts vd vas) b ws qs = case ws of - [] -> value2string' vd b ws qs + [] -> value2string' g vd b ws qs (w:_) -> pre vd vas w b ws qs where - pre vd [] w = value2string' vd + pre vd [] w = value2string' g vd pre vd ((v,VStrs ss):vas) w - | or [startsWith s w | VStr s <- ss] = value2string' v + | or [startsWith s w | VStr s <- ss] = value2string' g v | otherwise = pre vd vas w -value2string' _ _ _ _ = RunTime +value2string' g (VFV s vs) b ws qs = + CFV s (fmap (\v -> value2string' g v b ws qs) vs) +value2string' _ _ _ _ _ = RunTime startsWith [] _ = True startsWith (x:xs) (y:ys) | x == y = startsWith xs ys startsWith _ _ = False - string2value s = string2value' (words s) string2value' [] = VEmpty string2value' [w] = VStr w string2value' (w:ws) = VC (VStr w) (string2value' ws) -value2int (VInt n) = Const n -value2int _ = RunTime +value2int g (VMeta i vs) = CSusp i (\v -> value2int g (apply g v vs)) +value2int g (VSusp i k vs) = CSusp i (\v -> value2int g (apply g (k v) vs)) +value2int g (VInt n) = Const n +value2int g (VFV s vs) = CFV s (fmap (value2int g) vs) +value2int g _ = RunTime ------------------------------------------------------------------------ --- * Global/built-in definitions +value2float g (VMeta i vs) = CSusp i (\v -> value2float g (apply g v vs)) +value2float g (VSusp i k vs) = CSusp i (\v -> value2float g (apply g (k v) vs)) +value2float g (VFlt f) = Const f +value2float g (VFV s vs) = CFV s (fmap (value2float g) vs) +value2float g _ = RunTime -type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s)) -newtype Predef a s = Predef { runPredef :: PredefImpl a s } -type PredefCombinator a b s = Predef a s -> Predef b s +value2expr g xs (VApp _ (m,f) vs) + | m /= cPredef = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EFun (showIdent f))) vs +value2expr g xs (VMeta i vs) = CSusp i (\v -> value2expr g xs (apply g v vs)) +value2expr g xs (VSusp i k vs) = CSusp i (\v -> value2expr g xs (apply g (k v) vs)) +value2expr g xs (VGen j vs) = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EVar (length xs - j - 1))) vs +value2expr g xs (VClosure env s (Abs b x t)) = + let v = eval g ((x,VGen (length xs) []):env) s t [] + x' = mkFreshVar xs x + in fmap (EAbs b (showIdent x')) (value2expr g (x':xs) v) +value2expr g xs (VInt n) = pure (ELit (LInt n)) +value2expr g xs (VFlt f) = pure (ELit (LFlt f)) +value2expr g xs (VFV s vs) = CFV s (fmap (value2expr g xs) vs) +value2expr g xs v = fmap (ELit . LStr) (value2string g v) -infix 1 $\\ +newtype Choice = Choice { unchoice :: Integer } + deriving (Eq,Ord,Pretty,Show) -($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s -k $\ f = k (Predef f) +unit :: Choice +unit = Choice 1 -pdForce :: PredefCombinator (Value s) (Thunk s) s -pdForce def = Predef $ \args -> do - argValues <- mapM force args - runPredef def argValues +poison :: Choice +poison = Choice (-1) -pdCanonicalArgs :: PredefCombinator (Value s) (Value s) s -pdCanonicalArgs def = Predef $ \args -> - if all isCanonicalForm args then runPredef def args else return RunTime +split :: Choice -> (Choice,Choice) +split (Choice c) = (Choice (2*c), Choice (2*c+1)) -pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s -pdArity n def = Predef $ \args -> - case splitAt' n args of - Nothing -> return RunTime - Just (usedArgs, remArgs) -> do - res <- runPredef def usedArgs - forM res $ \v -> apply v remArgs +split3 :: Choice -> (Choice,Choice,Choice) +split3 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (2*c+1)) -pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s -pdStandard n = pdArity n . pdForce . pdCanonicalArgs +split4 :: Choice -> (Choice,Choice,Choice,Choice) +split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3)) ------------------------------------------------------------------------ --- * Evaluation monad +mapC :: (Choice -> a -> b) -> Choice -> [a] -> [b] +mapC f c [] = [] +mapC f c [x] = [f c x] +mapC f c (x:xs) = + let (!c1,!c2) = split c + in f c1 x : mapC f c2 xs -type MetaThunks s = Map.Map MetaId (Thunk s) -type Do s r = [Message] -> ST s (CheckResult r [Message]) -type Cont s r = MetaThunks s -> Int -> r -> Do s r -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) -> (Message -> Do s r) -> Cont s r) +forC :: Choice -> [a] -> (Choice -> a -> b) -> [b] +forC c xs f = mapC f c xs -instance Functor (EvalM s) where - fmap f (EvalM g) = EvalM (\gr k e -> g gr (k . f) e) - -instance Applicative (EvalM s) where - pure x = EvalM (\gr k e -> k x) - (EvalM f) <*> (EvalM x) = EvalM (\gr k e -> f gr (\f -> x gr (\x -> k (f x)) e) e) - -instance Monad (EvalM s) where - (EvalM f) >>= g = EvalM (\gr k e -> f gr (\x -> case g x of - EvalM g -> g gr k e) e) - -instance Fail.MonadFail (EvalM s) where - fail msg = EvalM (\gr k e _ _ r -> e (pp msg)) - -instance Alternative (EvalM s) where - empty = EvalM (\gr k e _ _ r msgs -> return (Success r msgs)) - (EvalM f) <|> (EvalM g) = EvalM $ \gr k e mt b r msgs -> do - res <- f gr k e mt b r msgs - case res of - Fail msg msgs -> return (Fail msg msgs) - Success r msgs -> g gr k e mt b r msgs - -instance MonadPlus (EvalM s) where - -runEvalM :: Globals -> (forall s . EvalM s a) -> Check [a] -runEvalM gr f = Check $ \(es,ws) -> - case runST (case f of - EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of - Fail msg ws -> Fail msg (es,ws) - Success xs ws -> Success (reverse xs) (es,ws) - -runEvalOneM :: Globals -> (forall s . EvalM s (Term,Type)) -> Check (Term,Type) -runEvalOneM gr f = Check $ \(es,ws) -> - case runST (case f of - EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of - Fail msg ws -> Fail msg (es,ws) - Success [] ws -> Fail (pp "The evaluation produced no results") (es,ws) - Success xs ws -> Success (FV (map fst xs),snd (head xs)) (es,ws) - -reset :: EvalM s a -> EvalM s [a] -reset (EvalM f) = EvalM $ \gl k e mt d r ws -> do - res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) mt d [] ws - case res of - Fail msg ws -> e msg ws - Success xs ws -> k (reverse xs) mt d r ws - -try :: EvalM s a -> EvalM s a -> EvalM s a -try (EvalM f) (EvalM g) = EvalM (\gl k e mt d r ws -> f gl k (\msg _ -> g gl k e mt d r ws) mt d r ws) - -evalError :: Message -> EvalM s a -evalError msg = EvalM (\gr k e _ _ r ws -> e msg ws) - -evalWarn :: Message -> EvalM s () -evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs)) - -evalPredef :: Ident -> [Thunk s] -> EvalM s (Value s) -evalPredef id args = do - res <- EvalM $ \globals@(Gl _ predef) k e mt d r msgs -> - case Map.lookup id predef <&> \def -> runPredef def args of - Just (EvalM f) -> f globals k e mt d r msgs - Nothing -> k RunTime mt d r msgs - case res of - Const res -> return res - RunTime -> return $ VApp (cPredef,id) args - NonExist -> return $ VApp (cPredef,cNonExist) [] - -getResDef :: QIdent -> EvalM s Term -getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do - case lookupResDef gr q of - Ok t -> k t mt d r msgs - Bad msg -> e (pp msg) msgs - -getInfo :: QIdent -> EvalM s (ModuleName,Info) -getInfo q = EvalM $ \(Gl gr _) k e mt d r msgs -> do - case lookupOrigInfo gr q of - Ok res -> k res mt d r msgs - Bad msg -> e (pp msg) msgs - -getResType :: QIdent -> EvalM s Type -getResType q = EvalM $ \(Gl gr _) k e mt d r msgs -> do - case lookupResType gr q of - Ok t -> k t mt d r msgs - Bad msg -> e (pp msg) msgs - -getOverload :: Term -> QIdent -> EvalM s (Term,Type) -getOverload t q = EvalM $ \(Gl gr _) k e mt d r msgs -> do - case lookupOverloadTypes gr q of - Ok ttys -> let err = "Overload resolution failed" $$ - "of term " <+> pp t $$ - "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys] - - go r [] = return (Success r msgs) - go r (tty:ttys) = do res <- k tty mt d r msgs - case res of - Fail _ _ -> go r ttys - Success r msgs -> go r ttys - - in go r ttys - Bad msg -> e (pp msg) msgs - -getAllParamValues :: Type -> EvalM s [Term] -getAllParamValues ty = EvalM $ \(Gl gr _) k e mt d r msgs -> - case allParamValues gr ty of - Ok ts -> k ts mt d r msgs - Bad msg -> e (pp msg) msgs - -newThunk env t = EvalM $ \gr k e mt d r msgs -> do - tnk <- newSTRef (Unevaluated env t) - k tnk mt d r msgs - -newEvaluatedThunk v = EvalM $ \gr k e mt d r msgs -> do - tnk <- newSTRef (Evaluated maxBound v) - k tnk mt d r msgs - -newHole i = EvalM $ \gr k e mt d r msgs -> - if i == 0 - then do tnk <- newSTRef (Hole i) - k tnk mt d r msgs - else case Map.lookup i mt of - Just tnk -> k tnk mt d r msgs - Nothing -> do tnk <- newSTRef (Hole i) - k tnk (Map.insert i tnk mt) d r msgs - -newResiduation scope = EvalM $ \gr k e mt d r msgs -> do - let i = Map.size mt + 1 - tnk <- newSTRef (Residuation i scope Nothing) - k (i,tnk) (Map.insert i tnk mt) d r msgs - -newNarrowing ty = EvalM $ \gr k e mt d r msgs -> do - let i = Map.size mt + 1 - tnk <- newSTRef (Narrowing i ty) - k (i,tnk) (Map.insert i tnk mt) d r msgs - -withVar d0 (EvalM f) = EvalM $ \gr k e mt d1 r msgs -> - let !d = min d0 d1 - in f gr k e mt d r msgs - -getVariables :: EvalM s [(LVar,LIndex)] -getVariables = EvalM $ \(Gl gr _) k e mt d ws r -> do - ps <- metas2params gr (Map.elems mt) - k ps mt d ws r - where - metas2params gr [] = return [] - metas2params gr (tnk:tnks) = do - st <- readSTRef tnk - case st of - Narrowing i ty -> do let cnt = case allParamValues gr ty of - Ok ts -> length ts - Bad msg -> error msg - params <- metas2params gr tnks - if cnt > 1 - then return ((i-1,cnt):params) - else return params - _ -> metas2params gr tnks - -getRef tnk = EvalM $ \gr k e mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs -setRef tnk st = EvalM $ \gr k e mt d r msgs -> do - old <- readSTRef tnk - writeSTRef tnk st - res <- k () mt d r msgs - writeSTRef tnk old - return res - -force tnk = EvalM $ \gr k e mt d r msgs -> do - s <- readSTRef tnk - case s of - Unevaluated env t -> case eval env t [] of - EvalM f -> f gr (\v mt b r msgs -> do let d = length env - writeSTRef tnk (Evaluated d v) - r <- k v mt d r msgs - writeSTRef tnk s - return r) e mt d r msgs - Evaluated d v -> k v mt d r msgs - Hole _ -> k (VMeta tnk []) mt d r msgs - Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs - Narrowing _ _ -> k (VMeta tnk []) mt d r msgs - -tnk2term True xs tnk = force tnk >>= value2term True xs -tnk2term False xs tnk = EvalM $ \gr k e mt d r msgs -> - let join f g = do res <- f - case res of - Fail msg msgs -> return (Fail msg msgs) - Success r msgs -> g r msgs - - flush [] k1 mt r msgs = k1 mt r msgs - flush [x] k1 mt r msgs = join (k x mt d r msgs) (k1 mt) - flush xs k1 mt r msgs = join (k (FV (reverse xs)) mt d r msgs) (k1 mt) - - acc d0 x mt d (r,!c,xs) msgs - | d < d0 = flush xs (\mt r msgs -> join (k x mt d r msgs) (\r msgs -> return (Success (r,c+1,[]) msgs))) mt r msgs - | otherwise = return (Success (r,c+1,x:xs) msgs) - - err msg msgs = return (Fail msg msgs) - - in do s <- readSTRef tnk - case s of - Unevaluated env t -> do let d0 = length env - res <- case eval env t [] of - EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v) - r <- case value2term False xs v of - EvalM f -> f gr (acc d0) err mt d msgs r - writeSTRef tnk s - return r) err mt maxBound (r,0,[]) msgs - case res of - Fail msg msgs -> return (Fail msg msgs) - Success (r,0,xs) msgs -> k (FV []) mt d r msgs - Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs - Evaluated d0 v -> do res <- case value2term False xs v of - EvalM f -> f gr (acc d0) err mt maxBound (r,0,[]) msgs - case res of - Fail msg msgs -> return (Fail msg msgs) - Success (r,0,xs) msgs -> k (FV []) mt d r msgs - Success (r,c,xs) msgs -> flush xs (\mt r msgs -> return (Success r msgs)) mt r msgs - Hole i -> k (Meta i) mt d r msgs - Residuation i _ _ -> k (Meta i) mt d r msgs - Narrowing i _ -> k (Meta i) mt d r msgs - -scopeEnv scope = zipWithM (\x i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] - - -unsafeIOToEvalM :: IO a -> EvalM s a -unsafeIOToEvalM f = EvalM (\gr k e mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs) +mapCM :: Monad m => (Choice -> a -> m b) -> Choice -> [a] -> m [b] +mapCM f c [] = return [] +mapCM f c [x] = do y <- f c x + return [y] +mapCM f c (x:xs) = do + let (!c1,!c2) = split c + y <- f c1 x + ys <- mapCM f c2 xs + return (y:ys) +forCM :: Monad m => Choice -> [a] -> (Choice -> a -> m b) -> m [b] +forCM c xs f = mapCM f c xs diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs deleted file mode 100644 index f0e0d5943..000000000 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ /dev/null @@ -1,1229 +0,0 @@ -{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-} - -module GF.Compile.Compute.Concrete2 - (Env, Scope, Value(..), Variants(..), OptionInfo(..), - ConstValue(..), Globals(..), PredefTable, EvalM, - mapVariantsC, unvariants, - runEvalM, runEvalMWithInput, stdPredef, globals, - PredefImpl, Predef(..), ($\), - pdCanonicalArgs, pdArity, - normalForm, normalFlatForm, - eval, apply, value2term, value2termM, value2string, value2int, value2float, value2expr, string2value, bubble, patternMatch, vtableSelect, State(..), - newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try, - 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 -import GF.Infra.CheckM -import GF.Data.Operations(Err(..)) -import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM,secondM,bimapM) -import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo) -import GF.Grammar.Grammar -import GF.Grammar.Macros -import GF.Grammar.Predef -import GF.Grammar.Printer hiding (ppValue) -import GF.Grammar.Lockfield(lockLabel) -import GF.Text.Pretty hiding (empty) -import qualified GF.Text.Pretty as PP -import Control.Monad -import Control.Applicative hiding (Const) -import qualified Control.Applicative as A -import qualified Data.Map as Map -import Data.Bifunctor (second) -import Data.Functor ((<&>)) -import Data.Maybe (fromMaybe,fromJust) -import Data.List -import Data.Char -import PGF2(Expr(..),Literal(..)) - -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 PredefTable = Map.Map Ident Predef -data Globals = Gl Grammar PredefTable - -data Value - = VApp Choice QIdent [Value] - | VMeta {-# UNPACK #-} !MetaId [Value] - | VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value] - | VGen {-# UNPACK #-} !Int [Value] - | VClosure Env Choice Term - | VProd BindType Ident Value Value - | VRecType [(Label, Bool, Value)] Bool - | VR [(Label, Value)] - | VP Value Label [Value] - | VExtR Value Value - | VTable Value Value - | VT Value Env Choice [Case] - | VV Value [Value] - | VS Value Value [Value] - | VSort Ident - | VInt Integer - | VFlt Double - | VStr String - | VEmpty - | VC Value Value - | VGlue Value Value - | VPatt Int (Maybe Int) Patt - | VPattType Value - | VFV Choice (Variants Value) - | VAlts Value [(Value, Value)] - | VStrs [Value] - | VMarkup Ident [(Ident,Value)] [L Value] - | VReset Ident (Maybe Value) Value (Maybe QIdent) - | VSymCat Int LIndex [(LIndex, (Value, Type))] - | VError Doc - | VInts Integer Bool - -data Variants a - = VarFree [a] - | VarOpts Value [(Value, a)] - -instance Functor Variants where - fmap f (VarFree vs) = VarFree (f <$> vs) - fmap f (VarOpts n cs) = VarOpts n (second f <$> cs) - -mapVariantsC :: (Choice -> a -> b) -> Choice -> Variants a -> Variants b -mapVariantsC f c (VarFree vs) = VarFree (mapC f c vs) -mapVariantsC f c (VarOpts n cs) = VarOpts n (mapC (\c (x,y) -> (x,f c y)) c cs) - -unvariants :: Variants a -> [a] -unvariants (VarFree vs) = vs -unvariants (VarOpts n cs) = snd <$> cs - -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 (\(l,_,ty) -> isCanonicalForm flat ty) 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 {}) = False -isCanonicalForm False (VFV c vs) = all (isCanonicalForm False) (unvariants vs) -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 . unLoc) vs -isCanonicalForm flat (VReset ctl cv v _) = maybe True (isCanonicalForm flat) cv && isCanonicalForm flat v -isCanonicalForm flat _ = False - -data ConstValue a - = Const a - | CSusp MetaId (Value -> ConstValue a) - | CFV Choice (Variants (ConstValue a)) - | RunTime - | NonExist - -instance Functor ConstValue where - fmap f (Const c) = Const (f c) - fmap f (CFV i vs) = CFV i (fmap (fmap f) vs) - fmap f (CSusp i k) = CSusp i (fmap f . k) - fmap f RunTime = RunTime - fmap f NonExist = NonExist - -instance Applicative ConstValue where - pure = Const - - (Const f) <*> (Const x) = Const (f x) - (CFV s vs) <*> v2 = CFV s (fmap (<*> v2) vs) - v1 <*> (CFV s vs) = CFV s (fmap (v1 <*>) vs) - (CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2) - v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v) - NonExist <*> _ = NonExist - _ <*> NonExist = NonExist - RunTime <*> _ = RunTime - _ <*> RunTime = RunTime - -normalForm :: Globals -> Term -> Check Term -normalForm g t = value2term g [] (bubble (eval g [] unit t [])) - -normalFlatForm :: Globals -> Term -> Check [Term] -normalFlatForm g t = runEvalM g (value2termM True [] (eval g [] unit t [])) - -eval :: Globals -> Env -> Choice -> Term -> [Value] -> Value -eval g env s (Vr x) vs = case lookup x env of - Nothing -> VError ("Variable" <+> pp x <+> "is not in scope") - Just v -> apply g v vs -eval g env s (Sort sort) [] - | sort == cTok = VSort cStr - | otherwise = VSort sort -eval g env s (EInt n) [] = VInt n -eval g env s (EFloat d) [] = VFlt d -eval g env s (K t) [] = VStr t -eval g env s Empty [] = VEmpty -eval g env s (App t1 t2) vs = let (s1,s2) = split s - in eval g env s1 t1 (eval g env s2 t2 [] : vs) -eval g env s (Abs b x t) [] = VClosure env s (Abs b x t) -eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs -eval g env s (Meta i) vs = VMeta i vs -eval g env s (ImplArg t) [] = eval g env s t [] -eval g env s (Prod b x t1 t2)[] - | x == identW = let (s1,s2) = split s - in VProd b x (eval g env s1 t1 []) (eval g env s2 t2 []) - | otherwise = let (s1,s2) = split s - in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2) -eval g env s (Typed t ty) vs = eval g env s t vs -eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls) False -eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as) -eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of - Nothing -> VError ("Missing value for label" <+> pp lbl $$ - "in" <+> pp (P t lbl)) - Just v -> apply g v vs - project (VFV s fvs) = VFV s (fmap project fvs) - project (VMeta i vs) = VSusp i (\v -> project (apply g v vs)) [] - project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) [] - project v = VP v lbl vs - in project (eval g env s t []) -eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s - - extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2) - extend (VRecType as1 e1) (VRecType as2 e2)=VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2) (e1 || e2) - extend (VFV i fvs) v2 = VFV i (fmap (`extend` v2) fvs) - extend v1 (VFV i fvs) = VFV i (fmap (v1 `extend`) fvs) - extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) [] - extend v1 (VMeta i vs) = VSusp i (\v -> extend v1 (apply g v vs)) [] - extend (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) [] - extend v1 (VSusp i k vs) = VSusp i (\v -> extend v1 (apply g (k v) vs)) [] - extend v1 v2 = VExtR v1 v2 - - in extend (eval g env s1 t1 []) (eval g env s2 t2 []) -eval g env s (Table t1 t2) [] = let (!s1,!s2) = split s - in VTable (eval g env s1 t1 []) (eval g env s2 t2 []) -eval g env s (T (TTyped ty) cs)[]=let (!s1,!s2) = split s - in VT (eval g env s1 ty []) env s2 cs -eval g env s (T (TWild ty) cs) []=let (!s1,!s2) = split s - in VT (eval g env s1 ty []) env s2 cs -eval g env s (V ty ts) [] = let (!s1,!s2) = split s - in VV (eval g env s1 ty []) (mapC (\s t -> eval g env s t []) s2 ts) -eval g env s (S t1 t2) vs = let (!s1,!s2) = split s - v1 = eval g env s1 t1 [] - v2 = eval g env s2 t2 [] - v0 = VS v1 v2 vs - - select (VT _ env s cs) = patternMatch g s v0 (map (\(p,t) -> (env,[p],v2:vs,t)) cs) - select (VV vty tvs) = case value2termM False (map fst env) vty of - EvalM f -> case f g (\x state xs ws -> Success (x:xs) ws) empty [] [] of - Fail msg ws -> VError msg - Success tys ws -> case tys of - [ty] -> vtableSelect g v0 ty tvs v2 vs - tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs - select (VFV i fvs) = VFV i (fmap select fvs) - select (VMeta i vs) = VSusp i (\v -> select (apply g v vs)) [] - select (VSusp i k vs) = VSusp i (\v -> select (apply g (k v) vs)) [] - select v1 = v0 - - -- FIXME: options=[] is definitely not correct and this shouldn't be using value2termM at all - empty = State [] Map.empty Map.empty [] - - in select v1 -eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s - in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs -eval g env c (Q q@(m,id)) vs - | m == cPredef = evalPredef g c id vs - | 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 s q vs -eval g env s (C t1 t2) [] = let (!s1,!s2) = split s - - concat v1 VEmpty = v1 - concat VEmpty v2 = v2 - concat (VFV i fvs) v2 = VFV i (fmap (`concat` v2) fvs) - concat v1 (VFV i fvs) = VFV i (fmap (v1 `concat`) fvs) - concat (VMeta i vs) v2 = VSusp i (\v -> concat (apply g v vs) v2) [] - concat v1 (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) [] - concat (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) [] - concat v1 (VSusp i k vs) = VSusp i (\v -> concat v1 (apply g (k v) vs)) [] - concat v1 v2 = VC v1 v2 - - in concat (eval g env s1 t1 []) (eval g env s2 t2 []) -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 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 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 - glue (VAlts d vas) v = glue d v - glue (VFV i fvs) v2 = VFV i (fmap (`glue` v2) fvs) - glue v1 (VFV i fvs) = VFV i (fmap (v1 `glue`) fvs) - glue (VMeta i vs) v2 = VSusp i (\v -> glue (apply g v vs) v2) [] - glue v1 (VMeta i vs) = VSusp i (\v -> glue v1 (apply g v vs)) [] - glue (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) [] - glue v1 (VSusp i k vs)= VSusp i (\v -> glue v1 (apply g (k v) vs)) [] - glue v1 v2 = VGlue v1 v2 - - pre vd [] s = glue vd (VStr s) - pre vd ((v,VStrs ss):vas) s - | or [startsWith s' s | VStr s' <- ss] = glue v (VStr s) - | otherwise = pre vd vas s - - in glue (eval g env s1 t1 []) (eval g env s2 t2 []) -eval g env s (EPatt min max p) [] = VPatt min max p -eval g env s (EPattType t) [] = VPattType (eval g env s t []) -eval g env s (ELincat c ty) [] = let lbl = lockLabel c - lty = RecType [] - in eval g env s (ExtR ty (RecType [(lbl,lty)])) [] -eval g env s (ELin c t) [] = let lbl = lockLabel c - lt = R [] - in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) [] -eval g env s (FV ts) vs = VFV s (VarFree (mapC (\s t -> eval g env s t vs) s ts)) -eval g env s (Alts d as) [] = let (!s1,!s2) = split s - vd = eval g env s1 d [] - vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s - in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as - in VAlts vd vas -eval g env c (Strs ts) [] = VStrs (mapC (\c t -> eval g env c t []) c ts) -eval g env c (Markup tag as ts) [] = - let (c1,c2) = split c - vas = mapC (\c (id,t) -> (id,eval g env c t [])) c1 as - vs = mapC (\c (L loc t) -> L loc (eval g env c t [])) c2 ts - in (VMarkup tag vas vs) -eval g env c (Reset ctl mb_ct t qid) [] = VReset ctl (fmap (\t -> eval g env c t []) mb_ct) (eval g env c t []) qid -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 VFV c3 (VarOpts vn vcs) - where evalOpt c' (Just l, t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs) - evalOpt c' (Nothing,t) = let v = eval g env c' t vs in (v, v) -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 (fmap 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 - [(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs})) - ,(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 - genericDp n = reverse . genericTake n . reverse - -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 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 (fmap (\v -> apply g v vs) fvs) -apply g (VS v1 v2 vs') vs = VS v1 v2 (vs'++vs) -apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs -apply g v [] = v - -data BubbleVariants - = BubbleFree Int - | BubbleOpts Value [Value] - -bubble v = snd (bubble v) - where - 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 - bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env - bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2 - bubble v@(VRecType lbls ext) = - let (union,lbls') = mapAccumL descendR Map.empty lbls - in (union, addVariants (VRecType lbls' ext) union) - bubble (VR as) = liftL' VR as - bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs - bubble (VExtR v1 v2) = lift2 VExtR v1 v2 - bubble (VTable v1 v2) = lift2 VTable v1 v2 - bubble (VT v env c cs) = lift1L' (\v env -> VT v env c cs) v env - bubble (VV v vs) = lift1L VV v vs - bubble (VS v1 v2 vs) = lift2L VS v1 v2 vs - bubble v@(VSort _) = lift0 v - bubble v@(VInt _) = lift0 v - bubble v@(VFlt _) = lift0 v - bubble v@(VStr _) = lift0 v - bubble v@VEmpty = lift0 v - bubble (VC v1 v2) = lift2 VC v1 v2 - bubble (VGlue v1 v2) = lift2 VGlue v1 v2 - bubble v@(VPatt _ _ _) = lift0 v - bubble (VPattType v) = lift1 VPattType v - bubble v@(VFV c (VarFree vs)) - | null vs = (Map.empty, v) - | otherwise = let (union,vs') = mapAccumL descend Map.empty vs - in (Map.insert c (BubbleFree (length vs),1) union, VFV c (VarFree vs')) - bubble v@(VFV c (VarOpts n os)) - | null os = (Map.empty, v) - | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os - in (Map.insert c (BubbleOpts n (map fst os),1) union, VFV c (VarOpts n os')) - bubble (VAlts v vs) = lift1L2 VAlts v vs - bubble (VStrs vs) = liftL VStrs vs - bubble (VMarkup tag attrs vs) = - let (union1,attrs') = mapAccumL descend' Map.empty attrs - (union2,vs') = mapAccumL descendL union1 vs - in (union2, VMarkup tag attrs' vs') - bubble (VReset ctl mb_cv v id) = - let (union,v') = bubble v - in (Map.empty,VReset ctl mb_cv v' id) - bubble (VSymCat d i0 vs) = - let (union,vs') = mapAccumL descendC Map.empty vs - in (union, addVariants (VSymCat d i0 vs') union) - bubble v@(VError _) = lift0 v - bubble v@(VInts _ _) = lift0 v - - lift0 v = (Map.empty, v) - - lift1 f v = - let (union,v') = bubble v - in (union,f v') - - liftL f vs = - let (union,vs') = mapAccumL descend Map.empty vs - in (union, addVariants (f vs') union) - - liftL' f vs = - let (union,vs') = mapAccumL descend' Map.empty vs - in (union, addVariants (f vs') union) - - lift1L f v vs = - let (choices,v') = bubble v - (union, vs') = mapAccumL descend (unitfy choices) vs - in (union, addVariants (f v' vs') union) - - lift1L' f v vs = - let (choices,v') = bubble v - (union, vs') = mapAccumL descend' (unitfy choices) vs - in (union, addVariants (f v' vs') union) - - lift1L2 f v vs = - let (choices,v') = bubble v - (union, vs') = mapAccumL descend2 (unitfy choices) vs - in (union, addVariants (f v' vs') union) - - lift2L f v1 v2 vs = - let (choices1,v1') = bubble v1 - (choices2,v2') = bubble v2 - union = mergeChoices2 choices1 choices2 - (union', vs') = mapAccumL descend union vs - in (union', addVariants (f v1' v2' vs') union') - - lift2 f v1 v2 = - let (choices1,v1') = bubble v1 - (choices2,v2') = bubble v2 - union = mergeChoices2 choices1 choices2 - in (union, addVariants (f v1' v2') union) - - descend union v = - let (choices,v') = bubble v - in (mergeChoices1 union choices,v') - - descend' :: Map.Map Choice (BubbleVariants,Int) -> (a,Value) -> (Map.Map Choice (BubbleVariants,Int),(a,Value)) - descend' union (x,v) = - let (choices,v') = bubble v - in (mergeChoices1 union choices,(x,v')) - - descend2 union (v1,v2) = - let (choices1,v1') = bubble v1 - (choices2,v2') = bubble v2 - in (mergeChoices1 (mergeChoices1 union choices1) choices2,(v1',v2')) - - descendC union (i,(v,ty)) = - let (choices,v') = bubble v - in (mergeChoices1 union choices,(i,(v',ty))) - - descendL union (L loc v) = - let (choices,v') = bubble v - in (mergeChoices1 union choices,L loc v') - - descendR union (l,b,v) = - let (choices,v') = bubble v - in (mergeChoices1 union choices,(l,b,v')) - - addVariants v = Map.foldrWithKey addVariant v - where - addVariant c (bvs,cnt) v - | cnt > 1 = VFV c $ case bvs of - BubbleFree k -> VarFree (replicate k v) - BubbleOpts n os -> VarOpts n (map (\l -> (l,v)) os) - | otherwise = v - - unitfy = fmap (\(n,_) -> (n,1)) - 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 poison (cPredef,cPTrue) [] -toPBool False = VApp poison (cPredef,cPFalse) [] - -occur s1 [] = False -occur s1 s2@(_:tail) = check s1 s2 - where - check xs [] = False - check [] ys = True - check (x:xs) (y:ys) - | x == y = check xs ys - check _ _ = occur s1 tail - -occurs cs s2 = any (\c -> elem c s2) cs - -update lbl v [] = [(lbl,v)] -update lbl v (a@(lbl',_):as) - | lbl==lbl' = (lbl,v) : as - | otherwise = a : update lbl v as - -update3 lbl o v [] = [(lbl,o,v)] -update3 lbl o v (a@(lbl',o',_):as) - | lbl==lbl' = (lbl,o||o',v) : as - | otherwise = a : update3 lbl o v as - -patternMatch g s v0 [] = v0 -patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 - where - match env [] eqs args = eval g env s t args - match env (PT ty p :ps) eqs args = match env (p:ps) eqs args - match env (PAlt p1 p2:ps) eqs args = match env (p1:ps) ((env,p2:ps,args,t):eqs) args - match env (PM q :ps) eqs args = case lookupResDef gr q of - Ok t -> case eval g [] unit t [] of - VPatt _ _ p -> match env (p:ps) eqs args - _ -> error $ render (hang "Expected pattern macro:" 4 - (pp t)) - Bad msg -> error msg - where - Gl gr _ = g - match env (PV v :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args - match env (PAs v p :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args) - match env (PW :ps) eqs (arg:args) = match env ps eqs args - match env (PTilde _ :ps) eqs (arg:args) = match env ps eqs args - match env (p :ps) eqs (arg:args) = match' env p ps eqs arg args - - match' env p ps eqs arg args = - case (p,arg) of - (p, VMeta i vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) [] - (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 (fmap (\arg -> match' env p ps eqs arg args) 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) - | s1 == s2 -> match env ps eqs args - (PString s1, VEmpty) - | null s1 -> match env ps eqs args - (PSeq min1 max1 p1 min2 max2 p2,v) - -> case value2string g v of - Const str -> let n = length str - lo = min1 `max` (n-fromMaybe n max2) - hi = (n-min2) `min` fromMaybe n max1 - (ds,cs) = splitAt lo str - - eqs' = matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args - - in patternMatch g s v0 eqs' - RunTime -> v0 - NonExist -> patternMatch g s v0 eqs - (PRep minp maxp p, v) - -> case value2string g v of - Const str -> let n = length (str::String) `div` (max minp 1) - eqs' = matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args) - in patternMatch g s v0 eqs' - RunTime -> v0 - NonExist -> patternMatch g s v0 eqs - (PChar, VStr [_]) -> match env ps eqs args - (PChars cs, VStr [c]) - | elem c cs -> match env ps eqs args - (PInt n, VInt m) - | n == m -> match env ps eqs args - (PFloat n, VFlt m) - | n == m -> match env ps eqs args - _ -> patternMatch g s v0 eqs - - matchRec env [] as ps eqs args = match env ps eqs args - matchRec env ((lbl,p):pas) as ps eqs args = - case lookup lbl as of - Just tnk -> matchRec env pas as (p:ps) eqs (tnk:args) - Nothing -> VError ("Missing value for label" <+> pp lbl) - - matchStr env ps eqs i ds [] args = - (env,ps,(string2value (reverse ds)):(string2value []):args,t) : eqs - matchStr env ps eqs 0 ds cs args = - (env,ps,(string2value (reverse ds)):(string2value cs):args,t) : eqs - matchStr env ps eqs i ds (c:cs) args = - (env,ps,(string2value (reverse ds)):(string2value (c:cs)):args,t) : - matchStr env ps eqs (i-1 :: Int) (c:ds) cs args - - matchRep env 0 minp maxp p minq maxq q ps eqs args = eqs - matchRep env n minp maxp p minq maxq q ps eqs args = - matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args - -vtableSelect g v0 ty cs v2 vs = - apply g (select (value2index v2 ty)) vs - where - select (Const (i,_)) = cs !! i - select (CSusp i k) = VSusp i (\v -> select (k v)) [] - select (CFV c vs) = VFV c (fmap select vs) - select _ = v0 - - value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty) - value2index (VSusp i k vs) ty = CSusp i (\v -> value2index (apply g (k v) vs) ty) - value2index (VR as) (RecType lbls) = compute lbls - where - compute [] = pure (0,1) - compute ((lbl,ty):lbls) = - case lookup lbl as of - Just v -> liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt')) - (value2index v ty) - (compute lbls) - Nothing -> error (show ("Missing value for label" <+> pp lbl $$ - "among" <+> hsep (punctuate (pp ',') (map fst as)))) - value2index (VApp c q args) ty = - let (r ,ctxt,cnt ) = getIdxCnt q - in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args) - where - getIdxCnt q = - let (_,ResValue (L _ ty) idx) = getInfo q - (ctxt,QC p) = typeFormCnc ty - (_,ResParam _ (Just (_,cnt))) = getInfo p - in (idx,ctxt,cnt) - - compute [] [] = pure (0,1) - compute ((_,_,ty):ctxt) (v:vs) = - liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt')) - (value2index v ty) - (compute ctxt vs) - - getInfo :: QIdent -> (ModuleName,Info) - getInfo q = - case lookupOrigInfo gr q of - Ok res -> res - Bad msg -> error msg - - Gl gr _ = g - value2index (VInt n) ty - | Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1) - value2index (VFV c vs) ty = CFV c (fmap (\v -> value2index v ty) vs) - value2index v ty = RunTime - - -value2term :: Globals -> [Ident] -> Value -> Check Term -value2term g xs v = do - res <- runEvalM g (value2termM False xs v) - case res of - [t] -> return t - ts -> return (FV ts) - -data MetaState - = Bound Scope Value - | Narrowing Choice Type - | Residuation Scope -data OptionInfo - = OptionInfo - { optChoice :: Choice - , optValue :: Int - , optLabel :: Value - , optChoices :: [Value] - } -data State - = State - { input :: [(Choice, Int)] - , 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) - -instance Functor EvalM where - fmap f (EvalM m) = EvalM (\g k -> m g (k . f)) - -instance Applicative EvalM where - pure x = EvalM (\g k -> k x) - (EvalM f) <*> (EvalM h) = EvalM (\g k -> f g (\fn -> h g (\x -> k (fn x)))) - -instance Alternative EvalM where - empty = EvalM (\g k _ r msgs -> Success r msgs) - (EvalM f) <|> (EvalM g) = EvalM $ \gl k state r msgs -> - case f gl k state r msgs of - Fail msg msgs -> Fail msg msgs - Success r msgs -> g gl k state r msgs - -instance Monad EvalM where - (EvalM f) >>= h = EvalM (\g k -> f g (\x -> case h x of {EvalM h -> h g k})) - -instance MonadFail EvalM where - fail msg = EvalM (\g k _ _ msgs -> Fail (pp msg) msgs) - -instance MonadPlus EvalM where - -evalError msg = EvalM (\g k _ _ msgs -> Fail msg msgs) - -evalWarn msg = EvalM (\g k state r msgs -> k () state r (msg:msgs)) - -runEvalM :: Globals -> EvalM a -> Check [a] -runEvalM g (EvalM f) = Check $ \(es,ws) -> - case f g (\x state xs ws -> Success (x:xs) ws) empty [] ws of - Fail msg ws -> Fail msg (es,ws) - Success xs ws -> Success (reverse xs) (es,ws) - where - empty = State [] Map.empty Map.empty [] - -runEvalMWithInput :: Globals -> [(Choice,Int)] -> EvalM a -> Check [(a, [OptionInfo])] -runEvalMWithInput g input (EvalM f) = Check $ \(es,ws) -> - case f g (\x (State _ cs mvs os) xs ws -> Success ((x,reverse os):xs) ws) init [] ws of - Fail msg ws -> Fail msg (es,ws) - Success xs ws -> Success (reverse xs) (es,ws) - where - init = State input Map.empty Map.empty [] - -reset :: EvalM a -> EvalM [a] -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 - -reset1 :: EvalM a -> EvalM (Maybe a) -reset1 (EvalM f) = EvalM $ \g k state r ws -> - case f g (\x' state x ws -> Success (x <|> Just x') ws) state Nothing ws of - Fail msg ws -> Fail msg ws - Success x ws -> k x state r ws - -globals :: EvalM Globals -globals = EvalM (\g k -> k g) - -variants :: Choice -> [a] -> EvalM a -variants c xs = EvalM (\g k state@(State input choices metas opts) r msgs -> - case Map.lookup c choices of - Just j -> k (xs !! j) state r msgs - Nothing -> backtrack 0 xs k input choices metas opts r msgs) - where - backtrack j [] k input choices metas opts r msgs = Success r msgs - backtrack j (x:xs) k input choices metas opts r msgs = - case k x (State input (Map.insert c j choices) metas opts) r msgs of - Fail msg msgs -> Fail msg msgs - Success r msgs -> backtrack (j+1) xs k input choices metas opts r msgs - -variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term -variants' c f xs = EvalM (\g k state@(State input 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 - Nothing -> case backtrack g 0 xs input choices metas opts [] msgs of - Fail msg msgs -> Fail msg msgs - Success ts msgs -> k (FV (reverse ts)) state r msgs) - where - backtrack g j [] input choices metas opts ts msgs = Success ts msgs - backtrack g j (x:xs) input choices metas opts ts msgs = - case f x of - EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State input (Map.insert c j choices) metas opts) ts msgs of - Fail msg msgs -> Fail msg msgs - Success ts msgs -> backtrack g (j+1) xs input choices metas opts ts msgs - -try :: Int -> (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b -try sz f select xs = EvalM (\g k state r msgs -> - let (state',res,msgs') = backtrack sz g xs state [] msgs - in case select res of - EvalM f' -> f' g k state' r msgs') - where - backtrack sz g [] state res msgs = (state,res,msgs) - backtrack sz g (x:xs) state res msgs = - case f x of - EvalM f -> case f g (\y state' (_,ys) msgs -> Success (cut sz state state',y:ys) msgs) state (state,res) msgs of - Fail msg _ -> backtrack sz g xs state res msgs - Success (state,res) msgs -> backtrack sz g xs state res msgs - - cut sz state state' = state'{metaVars=Map.mapWithKey select (metaVars state')} - where - select k ms - | k <= sz = ms - | otherwise = case Map.lookup k (metaVars state) of - Just ms -> ms - Nothing -> ms - -newResiduation :: Scope -> EvalM MetaId -newResiduation scope = EvalM (\g k (State input choices metas opts) r msgs -> - let meta_id = Map.size metas+1 - in k meta_id (State input choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs) - -checkpoint :: EvalM Int -checkpoint = EvalM (\g k state r msgs -> - k (Map.size (metaVars state)) state r msgs) - -getMeta :: MetaId -> EvalM MetaState -getMeta i = EvalM (\g k state r msgs -> - case Map.lookup i (metaVars state) of - Just ms -> k ms state r msgs - Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) - -setMeta :: MetaId -> MetaState -> EvalM () -setMeta i ms = EvalM (\g k (State input choices metas opts) r msgs -> - let state' = State input choices (Map.insert i ms metas) opts - in k () state' r msgs) - -value2termM :: Bool -> [Ident] -> Value -> EvalM Term -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 - case mv of - Bound scope v -> do g <- globals - value2termM flat (map fst scope) (apply g v vs) - Residuation _ -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs -value2termM flat xs (VSusp j k vs) = - let v = k (VGen maxBound vs) - in value2termM flat xs v -value2termM flat xs (VGen j tnks) = - foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (Vr (reverse xs !! j)) tnks -value2termM flat xs (VClosure env s (Abs b x t)) = do - g <- globals - let v = eval g ((x,VGen (length xs) []):env) s t [] - x' = mkFreshVar xs x - t <- value2termM flat (x':xs) v - return (Abs b x' t) -value2termM flat xs (VClosure env s t) = do - return t -value2termM flat xs (VProd b x v1 (VClosure env c2 t2)) = do - g <- globals - t1 <- value2termM flat xs v1 - t2 <- value2termM flat (x:xs) (eval g ((x,VGen (length xs) []):env) c2 t2 []) - return (Prod b (mkFreshVar xs x) t1 t2) -value2termM flat xs (VProd b x v1 v2) = do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - return (Prod b x t1 t2) -value2termM flat xs (VRecType lbls _) = do - lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls - return (RecType lbls) -value2termM flat xs (VR as) = do - as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as - return (R as) -value2termM flat xs (VP v lbl vs) = do - t <- value2termM flat xs v - foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (P t lbl) vs -value2termM flat xs (VExtR v1 v2) = do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - return (ExtR t1 t2) -value2termM flat xs (VTable v1 v2) = do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - return (Table t1 t2) -value2termM flat xs (VT vty env s cs)= do - ty <- value2termM flat xs vty - cs <- forM cs $ \(p,t) -> do - let (_,xs',env') = pattVars (length xs,xs,env) p - g <- globals - t <- value2termM flat xs' (eval g env' s t []) - return (p,t) - return (T (TTyped ty) cs) -value2termM flat xs (VV vty vs)= do - ty <- value2termM flat xs vty - ts <- mapM (value2termM flat xs) vs - return (V ty ts) -value2termM flat xs (VS v1 v2 vs) = - case v1 of - VT vty env s cs -> do - ty <- value2termM flat xs vty - g <- globals - cs <- forM cs $ \(p,t) -> do - let (_,xs',env') = pattVars (length xs,xs,env) p - t <- value2termM flat xs' (eval g env' s t vs) - return (p,t) - t2 <- value2termM flat xs v2 - return (S (T (TTyped ty) cs) t2) - - VV vty vs' -> do - ty <- value2termM flat xs vty - g <- globals - ts <- forM vs' $ \v -> - value2termM flat xs (apply g v vs) - t2 <- value2termM flat xs v2 - return (S (V ty ts) t2) - - v1 -> do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (S t1 t2) vs -value2termM flat xs (VSort s) = return (Sort s) -value2termM flat xs (VStr tok) = return (K tok) -value2termM flat xs (VInt n) = return (EInt n) -value2termM flat xs (VFlt n) = return (EFloat n) -value2termM flat xs VEmpty = return Empty -value2termM flat xs (VC v1 v2) = do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - return (C t1 t2) -value2termM flat xs (VGlue v1 v2) = do - t1 <- value2termM flat xs v1 - t2 <- value2termM flat xs v2 - return (Glue t1 t2) -value2termM True xs (VFV i (VarFree vs)) = do - v <- variants i vs - value2termM True xs v -value2termM False xs (VFV c (VarFree vs)) = variants' c (value2termM False xs) vs -value2termM flat xs (VFV c (VarOpts n os)) = - EvalM $ \g k (State input choices metas opts) r msgs -> - let (j,input',choices',opts') = - case Map.lookup c choices of - Just j -> (j,input,choices,opts) - Nothing -> case input of - (c',j):input | c == c' -> let oi = OptionInfo c j n (map fst os) - in (j,input,Map.insert c j choices,oi:opts) - _ -> let oi = OptionInfo c 0 n (map fst os) - in (0,[],Map.insert c 0 choices,oi:opts) - in case os `maybeAt` j of - Just (l,t) -> case value2termM flat xs t of - EvalM f -> f g k (State input' choices' metas opts') r msgs - Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs -value2termM flat xs (VPatt min max p) = return (EPatt min max p) -value2termM flat xs (VPattType v) = do t <- value2termM flat xs v - return (EPattType t) -value2termM flat xs (VAlts vd vas) = do - d <- value2termM flat xs vd - as <- forM vas $ \(vt,vs) -> do - t <- value2termM flat xs vt - s <- value2termM flat xs vs - return (t,s) - return (Alts d as) -value2termM flat xs (VStrs vs) = do - ts <- mapM (value2termM flat xs) vs - return (Strs ts) -value2termM flat xs (VMarkup tag as vs) = do - as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as - ts <- mapM (mapM (value2termM flat xs)) vs - return (Markup tag as ts) -value2termM flat xs (VReset ctl mb_cv v mb_qid) = do - ts <- reset (value2termM True xs v) - reduce ctl mb_cv ts - where - reduce ctl mb_cv ts - | ctl == cConcat = do - ts <- case mb_cv of - Just (VInt n) -> return (genericTake n ts) - Nothing -> return ts - _ -> evalError (pp "[concat: .. | ..] requires an integer constant") - case ts of - [t] -> return t - ts -> return (Markup identW [] (map noLoc ts)) - | ctl == cConcat' = do - ts <- case mb_cv of - Just (VInt n) -> return (genericTake n ts) - Nothing -> return ts - _ -> evalError (pp "[concat: .. | ..] requires an integer constant") - case ts of - [] -> mzero - [t] -> return t - ts -> return (Markup identW [] (map noLoc ts)) - | ctl == cOne = - case (ts,mb_cv) of - ([] ,Nothing) -> mzero - ([] ,Just v) -> value2termM flat xs v - (t:ts,_) -> return t - | ctl == cSelect = - case mb_cv of - Just (VInt n) | n >= 0 -> select n ts' - | otherwise -> select (-n-1) (reverse ts') - where - ts' = sortBy compareKey ts - - select _ [] = mzero - select 0 (t:ts) = - case t of - R rs -> case lookup (ident2label cp1) rs of - Just (_,t) -> return t - Nothing -> evalError (pp "Missing label p1") - _ -> evalError (pp "The term must be a record") - select n (t:ts) = select (n-1) ts - _ -> evalError (pp "[select: .. | ..] requires an integer constant") - | ctl == cFilter = - let filter [] = mzero - filter (t:ts) = - case t of - R rs -> case (lookup (ident2label cp1) rs, lookup (ident2label cp2) rs) of - (Just (_,t), Just (_,Q q)) - | q == (cPredef,cTrue) -> pure t `mplus` filter ts - _ -> filter ts - _ -> evalError (pp "The term must be a record") - in filter ts - | ctl == cDefault = - case (ts,mb_cv) of - ([] ,Nothing) -> mzero - ([] ,Just v) -> value2termM flat xs v - (ts,_) -> msum (map pure ts) - | ctl == cList = - case (ts,mb_cv) of - ([], _) -> mzero - ([t], _) -> return t - (ts,Just cv) -> - do let Just (mn,id) = mb_qid - cat = showIdent id - ct <- value2termM flat xs cv - t <- listify mn cat ts - return (App (App (QC (mn,identS ("Conj"++cat))) ct) t) - _ -> evalError (pp "[list: .. | ..] requires an argument") - | ctl == cLen = - case mb_cv of - Just cv -> do g <- globals - value2termM True xs (apply g cv [VInt (genericLength ts)]) - Nothing -> return (EInt (genericLength ts)) - | ctl == cConst = - case mb_cv of - Just cv -> do ct <- value2termM flat xs cv - msum (map (pure . const ct) ts) - _ -> evalError (pp "[const: .. | ..] requires an argument") - | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") - - listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2) - listify mn cat (t1:ts) = do t2 <- listify mn cat ts - return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2) - - compareKey (R rs1) (R rs2) = - case (lookup (ident2label cp2) rs1, lookup (ident2label cp2) rs2) of - (Just (_,K s1), Just (_,K s2)) -> compare s1 s2 - -value2termM flat xs (VError msg) = evalError msg -value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n)) -value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v) - - -pattVars st (PP _ ps) = foldl pattVars st ps -pattVars st (PV x) = case st of - (i,xs,env) -> (i+1,x:xs,(x,VGen i []):env) -pattVars st (PR as) = foldl (\st (_,p) -> pattVars st p) st as -pattVars st (PT ty p) = pattVars st p -pattVars st (PAs x p) = case st of - (i,xs,env) -> pattVars (i+1,x:xs,(x,VGen i []):env) p -pattVars st (PImplArg p) = pattVars st p -pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2 -pattVars st _ = st - - - -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" -ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]" -ppValue q d (VProd bt x a b) = - if x == identW && bt == Explicit - then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b) - else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b) -ppValue q d (VRecType xs ext) - | q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of - [cat] -> pp cat - _ -> doc - | otherwise = doc - where - doc = braces (fsep (punctuate ';' ([l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs] ++ [pp ".." | ext]))) -ppValue q d (VR _) = pp "VR" -ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs)) -ppValue q d (VExtR _ _) = pp "VExtR" -ppValue q d (VTable kt vt) = prec d 0 (ppValue q 3 kt <+> "=>" <+> ppValue q 0 vt) -ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$ - nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$ - '}' - where - ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e -ppValue q d (VV _ _) = pp "VV" -ppValue q d (VS v1 v2 vs) = prec d 3 (hsep (hang (ppValue q 3 v1) 2 ("!" <+> ppValue q 4 v2) : map (ppValue q 5) vs)) -ppValue q d (VSort s) = pp s -ppValue q d (VInt n) = pp n -ppValue q d (VFlt f) = pp f -ppValue q d (VStr s) = ppTerm q d (K s) -ppValue q d VEmpty = pp "[]" -ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 v2)) -ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2) -ppValue q d (VPatt _ _ p) = prec d 4 ('#' <+> ppPatt q 2 p) -ppValue q d (VPattType v) = prec d 4 ("pattern" <+> ppValue q 0 v) -ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants vs))))) -ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs)))) -ppValue q d (VStrs _) = pp "VStrs" -ppValue q d (VMarkup _ _ _) = pp "VMarkup" -ppValue q d (VReset ctl ct t _) = pp "[" <> pp ctl <> - maybe PP.empty (\v -> pp ':' <+> ppValue q 6 v) ct <> - pp "|" <> ppValue q 0 t <> - pp "]" -ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>' -ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg))) -ppValue q d (VInts n ext) - | ext = prec d 4 (pp "Ints" <+> brackets (pp n <> "..")) - | otherwise = prec d 4 (pp "Ints" <+> pp n) - -ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y - -prec d1 d2 doc - | d1 > d2 = parens doc - | otherwise = doc - -value2string g v = fmap (\(_,ws,_) -> unwords ws) (value2string' g v False [] []) - -value2string' g (VMeta i vs) b ws qs = CSusp i (\v -> value2string' g (apply g v vs) b ws qs) -value2string' g (VSusp i k vs) b ws qs = CSusp i (\v -> value2string' g (apply g (k v) vs) b ws qs) -value2string' g (VStr w1) True (w2:ws) qs = Const (False,(w1++w2):ws,qs) -value2string' g (VStr w) _ ws qs = Const (False,w :ws,qs) -value2string' g VEmpty b ws qs = Const (b,ws,qs) -value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b ws qs) - where - concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs - concat v1 (CFV c vs) = CFV c (fmap (concat v1) vs) - concat v1 res = res -value2string' g (VApp c q []) b ws qs - | q == (cPredef,cNonExist) = NonExist -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 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 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 c q []) b ws qs - | q == (cPredef,cALL_CAPIT) = all_capit ws - where - all_capit [] = Const (b,[],q:qs) - all_capit (w : ws) = Const (b,map toUpper w : ws,qs) -value2string' g (VAlts vd vas) b ws qs = - case ws of - [] -> value2string' g vd b ws qs - (w:_) -> pre vd vas w b ws qs - where - pre vd [] w = value2string' g vd - pre vd ((v,VStrs ss):vas) w - | or [startsWith s w | VStr s <- ss] = value2string' g v - | otherwise = pre vd vas w -value2string' g (VFV s vs) b ws qs = - CFV s (fmap (\v -> value2string' g v b ws qs) vs) -value2string' _ _ _ _ _ = RunTime - -startsWith [] _ = True -startsWith (x:xs) (y:ys) - | x == y = startsWith xs ys -startsWith _ _ = False - -string2value s = string2value' (words s) - -string2value' [] = VEmpty -string2value' [w] = VStr w -string2value' (w:ws) = VC (VStr w) (string2value' ws) - -value2int g (VMeta i vs) = CSusp i (\v -> value2int g (apply g v vs)) -value2int g (VSusp i k vs) = CSusp i (\v -> value2int g (apply g (k v) vs)) -value2int g (VInt n) = Const n -value2int g (VFV s vs) = CFV s (fmap (value2int g) vs) -value2int g _ = RunTime - -value2float g (VMeta i vs) = CSusp i (\v -> value2float g (apply g v vs)) -value2float g (VSusp i k vs) = CSusp i (\v -> value2float g (apply g (k v) vs)) -value2float g (VFlt f) = Const f -value2float g (VFV s vs) = CFV s (fmap (value2float g) vs) -value2float g _ = RunTime - -value2expr g xs (VApp _ (m,f) vs) - | m /= cPredef = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EFun (showIdent f))) vs -value2expr g xs (VMeta i vs) = CSusp i (\v -> value2expr g xs (apply g v vs)) -value2expr g xs (VSusp i k vs) = CSusp i (\v -> value2expr g xs (apply g (k v) vs)) -value2expr g xs (VGen j vs) = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EVar (length xs - j - 1))) vs -value2expr g xs (VClosure env s (Abs b x t)) = - let v = eval g ((x,VGen (length xs) []):env) s t [] - x' = mkFreshVar xs x - in fmap (EAbs b (showIdent x')) (value2expr g (x':xs) v) -value2expr g xs (VInt n) = pure (ELit (LInt n)) -value2expr g xs (VFlt f) = pure (ELit (LFlt f)) -value2expr g xs (VFV s vs) = CFV s (fmap (value2expr g xs) vs) -value2expr g xs v = fmap (ELit . LStr) (value2string g v) - -newtype Choice = Choice { unchoice :: 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)) - -mapC :: (Choice -> a -> b) -> Choice -> [a] -> [b] -mapC f c [] = [] -mapC f c [x] = [f c x] -mapC f c (x:xs) = - let (!c1,!c2) = split c - in f c1 x : mapC f c2 xs - -forC :: Choice -> [a] -> (Choice -> a -> b) -> [b] -forC c xs f = mapC f c xs - -mapCM :: Monad m => (Choice -> a -> m b) -> Choice -> [a] -> m [b] -mapCM f c [] = return [] -mapCM f c [x] = do y <- f c x - return [y] -mapCM f c (x:xs) = do - let (!c1,!c2) = split c - y <- f c1 x - ys <- mapCM f c2 xs - return (y:ys) - -forCM :: Monad m => Choice -> [a] -> (Choice -> a -> m b) -> m [b] -forCM c xs f = mapCM f c xs diff --git a/src/compiler/api/GF/Compile/GeneratePMCFG.hs b/src/compiler/api/GF/Compile/GeneratePMCFG.hs index 6bfcbeabf..c1a1f5aee 100644 --- a/src/compiler/api/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/api/GF/Compile/GeneratePMCFG.hs @@ -13,7 +13,7 @@ import GF.Grammar.Macros import GF.Grammar.Predef import GF.Grammar.Printer hiding (ppValue) import GF.Text.Pretty hiding (empty) -import GF.Compile.Compute.Concrete2 hiding ( getMeta, setMeta, globals, variants ) +import GF.Compile.Compute.Concrete hiding ( getMeta, setMeta, globals, variants ) import qualified GF.Text.Pretty as PP import qualified Data.Map as Map import qualified Data.Set as Set diff --git a/src/compiler/api/GF/Compile/GrammarToCanonical.hs b/src/compiler/api/GF/Compile/GrammarToCanonical.hs index c251c933e..7b859b1d1 100644 --- a/src/compiler/api/GF/Compile/GrammarToCanonical.hs +++ b/src/compiler/api/GF/Compile/GrammarToCanonical.hs @@ -9,7 +9,7 @@ import GF.Grammar import GF.Grammar.Lookup(allOrigInfos,lookupOrigInfo) import GF.Infra.Option(Options,noOptions) import GF.Infra.CheckM -import GF.Compile.Compute.Concrete2 +import GF.Compile.Compute.Concrete import qualified Data.Map as Map import qualified Data.Set as Set import Data.Maybe(mapMaybe,fromMaybe) diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs index a4ffa1ab1..d0caa76ff 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs @@ -10,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) import GF.Grammar.Lookup import GF.Grammar.Predef import GF.Grammar.Lockfield -import GF.Compile.Compute.Concrete2 +import GF.Compile.Compute.Concrete import GF.Infra.CheckM import GF.Data.ErrM ( Err(Ok, Bad) ) import Control.Applicative(Applicative(..),(<|>)) diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs index 802c914e5..e6f04309d 100644 --- a/src/compiler/api/GF/Interactive.hs +++ b/src/compiler/api/GF/Interactive.hs @@ -14,8 +14,7 @@ import GF.Command.Abstract import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.TypeCheck.Concrete(inferLType) -import qualified GF.Compile.Compute.Concrete as O(normalForm,stdPredef,Globals(..)) -import GF.Compile.Compute.Concrete2(stdPredef,Globals(..)) +import GF.Compile.Compute.Concrete(stdPredef,normalForm,Globals(..)) import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields) import GF.Data.Operations (Err(..)) import GF.Data.Utilities(whenM,repeatM) @@ -316,18 +315,18 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do hypos compileLinTerm sgr mo f mb_t ty = do + let g = Gl sgr (stdPredef g) (t,ty) <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo (Typed t ty) - let g = Gl sgr (stdPredef g) + (t,ty) <- inferLType g t return (t,ty) Nothing -> case lookupResDef sgr (mo,identS f) of Ok t -> do ty <- renameSourceTerm sgr mo ty - ty <- O.normalForm (O.Gl sgr O.stdPredef) ty + ty <- normalForm g ty return (t,ty) Bad msg -> fail msg let (ctxt,res_ty) = typeFormCnc ty - let g = Gl sgr (stdPredef g) rules <- pmcfgForm g t ctxt res_ty return (rules,type2fields sgr res_ty) diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs deleted file mode 100644 index 0b2bd2626..000000000 --- a/src/compiler/api/GF/Term.hs +++ /dev/null @@ -1,12 +0,0 @@ -module GF.Term (renameSourceTerm, - Globals(..), ConstValue(..), EvalM, stdPredef, - Value(..), showValue, Thunk, newThunk, newEvaluatedThunk, - evalError, evalWarn, - inferLType, inferLType', checkLType, checkLType', - normalForm, normalFlatForm, normalStringForm, - unsafeIOToEvalM, force - ) where - -import GF.Compile.Rename -import GF.Compile.Compute.Concrete -import GF.Compile.TypeCheck.Concrete diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index e79a7fdad..802f58b58 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -76,7 +76,6 @@ library GF.Interactive GF.Compiler GF.Grammar - GF.Term GF.Compile GF.CompileInParallel GF.Data.ErrM @@ -106,7 +105,6 @@ library GF.Compile.CFGtoPGF GF.Compile.CheckGrammar GF.Compile.Compute.Concrete - GF.Compile.Compute.Concrete2 GF.Compile.ExampleBased GF.Compile.Export GF.Compile.GenerateBC