diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs
index 47e2f5cde..685855dc9 100644
--- a/src/compiler/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/GF/Compile/Compute/Concrete.hs
@@ -1,9 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+
 -- | Functions for computing the values of terms in the concrete syntax, in
 -- | preparation for PMCFG generation.
 module GF.Compile.Compute.Concrete
            (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
             normalForm,
-            Value(..), Bind(..), Env, value2term, eval, vapply
+            Value(..), Env, value2term, eval
            ) where
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
 
@@ -18,573 +20,140 @@ import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
 import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
 import GF.Data.Utilities(mapFst,mapSnd)
 import GF.Infra.Option
-import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
-import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
---import Data.Char (isUpper,toUpper,toLower)
-import GF.Text.Pretty
+import Data.STRef
+import Control.Monad
+import Control.Monad.ST
+import Control.Applicative
 import qualified Data.Map as Map
-import Debug.Trace(trace)
 
 -- * Main entry points
 
 normalForm :: GlobalEnv -> L Ident -> Term -> Term
-normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
+normalForm ge loc t =
+  case runEvalM (eval [] t [] >>= value2term 0) of
+    [t] -> t
+    ts  -> FV ts
 
-nfx :: GlobalEnv -> Term -> Err Term
-nfx env@(GE _ _ _ loc) t = do
-  v <- eval env [] t
-  return (value2term loc [] v)
-    -- Old value2term error message:
-    -- Left i  -> fail ("variable #"++show i++" is out of scope")
+eval env (Vr x)         vs  = case lookup x env of
+                                Just tnk -> force tnk vs
+                                Nothing  -> error "Unknown variable"
+eval env (Con f)        vs  = return (VApp f vs)
+eval env (K t)          vs  = return (VStr t)
+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 <- newMeta i
+                                 return (VMeta tnk env vs)
+eval env (Typed t ty)   vs  = eval env t vs
+eval env (C t1 t2)      vs  = do tnk1 <- newThunk env t1
+                                 tnk2 <- newThunk env t2
+                                 return (VC tnk1 tnk2)
+eval env (FV ts)        vs  = msum [eval env t vs | t <- ts]
 
-eval :: GlobalEnv -> Env -> Term -> Err Value
-eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
-  where
-    cenv = CE gr rvs opts loc (map fst env)
+apply v                             []  = return v
+apply (VApp f  vs0)                 vs  = return (VApp f (vs0++vs))
+apply (VMeta m env vs0)             vs  = return (VMeta m env (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
 
---apply env = apply' env
 
---------------------------------------------------------------------------------
+value2term i (VApp f tnks) =
+  foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Con f) tnks
+value2term i (VMeta m env tnks) = do
+  res <- zonk m tnks
+  case res of
+    Right i -> foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Meta i) tnks
+    Left  v -> value2term i v
+value2term i (VGen j tnks) =
+  foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Vr (identS ('v':show j))) tnks
+value2term i (VClosure env (Abs b x t)) = do
+  tnk <- newGen i
+  v <- eval ((x,tnk):env) t []
+  t <- value2term (i+1) v
+  return (Abs b (identS ('v':show i)) t)
+value2term i (VStr tok) = return (K tok)
+value2term i (VC tnk1 tnk2) = do
+  t1 <- force tnk1 [] >>= value2term i
+  t2 <- force tnk2 [] >>= value2term i
+  return (C t1 t2)
 
+
+-----------------------------------------------------------------------
 -- * Environments
 
-type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
-
-data GlobalEnv = GE Grammar ResourceValues Options GLocation
-data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
-                       opts::Options,
-                       gloc::GLocation,local::LocalScope}
+data GlobalEnv = GE Grammar Options GLocation
 type GLocation = L Ident
-type LocalScope = [Ident]
-type Stack = [Value]
-type OpenValue = Stack->Value
 
-geLoc     (GE _ _ _ loc) = loc
-geGrammar (GE gr _ _ _)  = gr
-
-ext b env = env{local=b:local env}
-extend bs env = env{local=bs++local env}
-global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
-
-var :: CompleteEnv -> Ident -> Err OpenValue
-var env x = maybe unbound pick' (elemIndex x (local env))
-  where
-    unbound = fail ("Unknown variable: "++showIdent x)
-    pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
-    err i vs = bug $ "Stack problem: "++showIdent x++": "
-                    ++unwords (map showIdent (local env))
-                    ++" => "++show (i,length vs)
-    ok v = --trace ("var "++show x++" = "++show v) $
-           v
-
-pick :: Int -> Stack -> Maybe Value
-pick 0 (v:_) = Just v
-pick i (_:vs) = pick (i-1) vs
-pick i vs = Nothing -- bug $ "pick "++show (i,vs)
-
-resource env (m,c) =
---  err bug id $
-    if isPredefCat c
-    then value0 env =<< lockRecType c defLinType -- hmm
-    else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
-  where e = fail $ "Not found: "++render m++"."++showIdent c
+geLoc     (GE _  _ loc) = loc
+geGrammar (GE gr _ _  ) = gr
 
 -- | Convert operators once, not every time they are looked up
 resourceValues :: Options -> SourceGrammar -> GlobalEnv
-resourceValues opts gr = env
-  where
-    env = GE gr rvs opts (L NoLoc identW)
-    rvs = Map.mapWithKey moduleResources (moduleMap gr)
-    moduleResources m = Map.mapWithKey (moduleResource m) . jments
-    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
-                                  let loc = L l c
-                                      qloc = L l (Q (m,c))
-                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)
-
-    traceRes = if flag optTrace opts
-               then traceResource
-               else const id
-
--- * Tracing
-
--- | Insert a call to the trace function under the top-level lambdas
-traceResource (L l q) t =
-  case termFormCnc t of
-    (abs,body) -> mkAbs abs (mkApp traceQ [args,body])
-      where
-        args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
-        lstr = render (l<>":"<>ppTerm Qualified 0 q)
-        traceQ = Q (cPredef,cTrace)
-
--- * Computing values
-
--- | Computing the value of a top-level term
-value0 :: CompleteEnv -> Term -> Err Value
-value0 env = eval (global env) []
-
--- | Computing the value of a term
-value :: CompleteEnv -> Term -> Err OpenValue
-value env t0 =
-  -- Each terms is traversed only once by this function, using only statically
-  -- available information. Notably, the values of lambda bound variables
-  -- will be unknown during the term traversal phase.
-  -- The result is an OpenValue, which is a function that may be applied many
-  -- times to different dynamic values, but without the term traversal overhead
-  -- and without recomputing other statically known information.
-  -- For this to work, there should be no recursive calls under lambdas here.
-  -- Whenever we need to construct the OpenValue function with an explicit
-  -- lambda, we have to lift the recursive calls outside the lambda.
-  -- (See e.g. the rules for Let, Prod and Abs)
-{-
-  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
-                                      brackets (fsep (map ppIdent (local env))),
-                                      ppTerm Unqualified 10 t0]) $
---}
-  errIn (render t0) $
-  case t0 of
-    Vr x   -> var env x
-    Q x@(m,f)
-      | m == cPredef -> if f==cErrorType                -- to be removed
-                        then let p = identS "P"
-                             in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
-                        else if f==cPBool
-                               then const # resource env x
-                               else const . flip VApp [] # predef f
-      | otherwise    -> const # resource env x --valueResDef (fst env) x
-    QC x   -> return $ const (VCApp x [])
-    App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
-    Let (x,(oty,t)) body -> do vb <- value (ext x env) body
-                               vt <- value env t
-                               return $ \ vs -> vb (vt vs:vs)
-    Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
-    Prod bt x t1 t2 ->
-       do vt1 <- value env t1
-          vt2 <- value (ext x env) t2
-          return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
-    Abs bt x t -> do vt <- value (ext x env) t
-                     return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
-    EInt n -> return $ const (VInt n)
-    EFloat f -> return $ const (VFloat f)
-    K s -> return $ const (VString s)
-    Empty -> return $ const (VString "")
-    Sort s | s == cTok -> return $ const (VSort cStr)        -- to be removed
-           | otherwise -> return $ const (VSort s)
-    ImplArg t -> (VImplArg.) # value env t
-    Table p res -> liftM2 VTblType # value env p <# value env res
-    RecType rs -> do lovs <- mapPairsM (value env) rs
-                     return $ \vs->VRecType $ mapSnd ($vs) lovs
-    t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
-    FV ts   -> ((vfv .) # sequence) # mapM (value env) ts
-    R as    -> do lovs <- mapPairsM (value env.snd) as
-                  return $ \ vs->VRec $ mapSnd ($vs) lovs
-    T i cs  -> valueTable env i cs
-    V ty ts -> do pvs <- paramValues env ty
-                  ((VV ty pvs .) . sequence) # mapM (value env) ts
-    C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
-    S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
-    P t l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
-               do ov <- value env t
-                  return $ \ vs -> let v = ov vs
-                                   in maybe (VP v l) id (proj l v)
-    Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
-    Strs ts    -> ((VStrs.) # sequence) # mapM (value env) ts
-    Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
-    ELin c r -> (unlockVRec (gloc env) c.) # value env r
-    EPatt p  -> return $ const (VPatt p) -- hmm
-    EPattType ty -> do vt <- value env ty
-                       return (VPattType . vt)
-    Typed t ty -> value env t
-    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
-
-vconcat vv@(v1,v2) =
-    case vv of
-      (VString "",_) -> v2
-      (_,VString "") -> v1
-      (VApp NonExist _,_) -> v1
-      (_,VApp NonExist _) -> v2
-      _ -> VC v1 v2
-
-proj l v | isLockLabel l = return (VRec [])
-                ---- a workaround 18/2/2005: take this away and find the reason
-                ---- why earlier compilation destroys the lock field
-proj l v =
-    case v of
-      VFV vs -> liftM vfv (mapM (proj l) vs)
-      VRec rs -> lookup l rs
---    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
-      VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
-      _ -> return (ok1 VP v l)
-
-ok1 f v1@(VError {}) _ = v1
-ok1 f v1 v2 = f v1 v2
-
-ok2 f v1@(VError {}) _ = v1
-ok2 f _ v2@(VError {}) = v2
-ok2 f v1 v2 = f v1 v2
-
-ok2p f (v1@VError {},_) = v1
-ok2p f (_,v2@VError {}) = v2
-ok2p f vv = f vv
-
-unlockVRec loc c0 v0 = v0
-{-
-unlockVRec loc c0 v0 = unlockVRec' c0 v0
-  where
-    unlockVRec' ::Ident -> Value -> Value
-    unlockVRec' c v =
-        case v of
-    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
-          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
-          VRec rs        -> plusVRec rs lock
-    --    _              -> VExtR v (VRec lock) -- hmm
-          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
-    --    _              -> bugloc loc $ "unlock non-record "++show v0
-      where
-        lock = [(lockLabel c,VRec [])]
--}
-
--- suspicious, but backwards compatible
-plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
-  where ls2 = map fst rs2
-
-extR t vv =
-    case vv of
-      (VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
-      (v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
-      (VRecType rs1, VRecType rs2) ->
-          case intersect (map fst rs1) (map fst rs2) of
-            [] -> VRecType (rs1 ++ rs2)
-            ls -> error $ "clash"<+>show ls
-      (VRec     rs1, VRec     rs2) -> plusVRec rs1 rs2
-      (v1          , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
-      (VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
---    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
-      (v1,v2) -> error $ "not records" $$ show v1 $$ show v2
-  where
-    error explain = ppbug $ "The term" <+> t
-                            <+> "is not reducible" $$ explain
-
-glue env (v1,v2) = glu v1 v2
-  where
-    glu v1 v2 =
-        case (v1,v2) of
-          (VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
-          (v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
-          (VString s1,VString s2) -> VString (s1++s2)
-          (v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
-             where glx v2 = glu v1 v2
-          (v1@(VAlts {}),v2) ->
-           --err (const (ok2 VGlue v1 v2)) id $
-             err bug id $
-             do y' <- strsFromValue v2
-                x' <- strsFromValue v1
-                return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
-          (VC va vb,v2) -> VC va (glu vb v2)
-          (v1,VC va vb) -> VC (glu v1 va) vb
-          (VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
-          (v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
-          (v1@(VApp NonExist _),_) -> v1
-          (_,v2@(VApp NonExist _)) -> v2
---        (v1,v2) -> ok2 VGlue v1 v2
-          (v1,v2) -> if flag optPlusAsBind (opts env)
-                       then VC v1 (VC (VApp BIND []) v2)
-                       else let loc  = gloc env
-                                vt v = value2term loc (local env) v
-                                        -- Old value2term error message:
-                                        --  Left i  -> Error ('#':show i)
-                                originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
-                                                               (Glue (vt v1) (vt v2)))
-                                term = render $ pp  $ Glue (vt v1) (vt v2)
-                            in error $ unlines
-                                [originalMsg
-                                ,""
-                                ,"There was a problem in the expression `"++term++"`, either:"
-                                ,"1) You are trying to use + on runtime arguments, possibly via an oper."
-                                ,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
-                                ,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
-                                ]
+resourceValues opts gr = GE gr opts (L NoLoc identW)
 
 
--- | to get a string from a value that represents a sequence of terminals
-strsFromValue :: Value -> Err [Str]
-strsFromValue t = case t of
-  VString s   -> return [str s]
-  VC s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [plusStr x y | x <- s', y <- t']
-{-
-  VGlue s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [glueStr x y | x <- s', y <- t']
--}
-  VAlts d vs -> do
-    d0 <- strsFromValue d
-    v0 <- mapM (strsFromValue . fst) vs
-    c0 <- mapM (strsFromValue . snd) vs
-  --let vs' = zip v0 c0
-    return [strTok (str2strings def) vars |
-              def  <- d0,
-              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
-                                                          vv <- sequence v0]
-           ]
-  VFV ts -> concat # mapM strsFromValue ts
-  VStrs ts -> concat # mapM strsFromValue ts
+-----------------------------------------------------------------------
+-- * Evaluation monad
 
-  _ -> fail ("cannot get Str from value " ++ show t)
+type MetaThunks s = Map.Map MetaId (Thunk s)
 
-vfv vs = case nub vs of
-           [v] -> v
-           vs -> VFV vs
+newtype EvalM s a = EvalM (forall r . (a -> MetaThunks s -> r -> ST s r) -> MetaThunks s -> r -> ST s r)
 
-select env vv =
-    case vv of
-      (v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
-      (VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
-      (v1@(VV pty vs rs),v2) ->
-         err (const (VS v1 v2)) id $
-         do --ats <- allParamValues (srcgr env) pty
-            --let vs = map (value0 env) ats
-            i <- maybeErr "no match" $ findIndex (==v2) vs
-            return (ix (gloc env) "select" rs i)
-      (VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
-      (v1@(VT _ _ cs),v2) ->
-                 err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
-                 match (gloc env) cs v2
-      (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
-      (v1,v2) -> ok2 VS v1 v2
+instance Functor (EvalM s) where
+  fmap f (EvalM g) = EvalM (\k -> g (k . f))
 
-match loc cs v =
-  err bad return (matchPattern cs (value2term loc [] v))
-    -- Old value2term error message:
-    -- Left i  -> bad ("variable #"++show i++" is out of scope")
-  where
-    bad = fail . ("In pattern matching: "++)
+instance Applicative (EvalM s) where
+  pure x = EvalM (\k -> k x)
+  (EvalM f) <*> (EvalM x) = EvalM (\k -> f (\f -> x (\x -> k (f x))))
 
-valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
-valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
+instance Monad (EvalM s) where
+  (EvalM f) >>= g = EvalM (\k -> f (\x -> case g x of
+                                            EvalM g -> g k))
 
-valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
-valueTable env i cs =
-    case i of
-      TComp ty -> do pvs <- paramValues env ty
-                     ((VV ty pvs .) # sequence) # mapM (value env.snd) cs
-      _ -> do ty <- getTableType i
-              cs' <- mapM valueCase cs
-              err (dynamic cs' ty) return (convert cs' ty)
-  where
-    dynamic cs' ty _ = cases cs' # value env ty
+instance Alternative (EvalM s) where
+  empty = EvalM (\k _ -> return)
+  (EvalM f) <|> (EvalM g) = EvalM (\k mt r -> f k mt r >>= \r -> g k mt r)
 
-    cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
-      where
-        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
-                   VT wild (vty vs) (mapSnd ($vs) cs')
-
-    wild = case i of TWild _ -> True; _ -> False
-
-    convertv cs' vty =
-      convert' cs' =<< paramValues'' env (value2term (gloc env) [] vty)
-        -- Old value2term error message: Left i    -> fail ("variable #"++show i++" is out of scope")
-
-    convert cs' ty = convert' cs' =<< paramValues' env ty
-
-    convert' cs' ((pty,vs),pvs) =
-      do sts  <- mapM (matchPattern cs') vs
-         return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
-                                           (mapFst ($vs) sts)
-
-    valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
-                         pvs <- linPattVars p'
-                         vt <- value (extend pvs env) t
-                         return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
-
-    inlinePattMacro p =
-        case p of
-          PM qc -> do r <- resource env qc
-                      case r of
-                        VPatt p' -> inlinePattMacro p'
-                        _ -> ppbug $ hang "Expected pattern macro:" 4
-                                          (show r)
-          _ -> composPattOp inlinePattMacro p
+instance MonadPlus (EvalM s) where
 
 
-paramValues env ty = snd # paramValues' env ty
+runEvalM :: (forall s . EvalM s a) -> [a]
+runEvalM f = reverse $
+             runST (case f of
+                      EvalM f -> f (\x mt xs -> return (x:xs)) Map.empty [])
 
-paramValues' env ty = paramValues'' env =<< nfx (global env) ty
+newThunk env t = EvalM $ \k mt r -> do
+ tnk <- newSTRef (Unevaluated env t)
+ k tnk mt r
 
-paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
-                           pvs <- mapM (eval (global env) []) ats
-                           return ((pty,ats),pvs)
+newMeta i = EvalM $ \k mt r ->
+  if i == 0
+    then do tnk <- newSTRef (Unbound i)
+            k tnk mt r
+    else case Map.lookup i mt of
+           Just tnk -> k tnk mt r
+           Nothing  -> do tnk <- newSTRef (Unbound i)
+                          k tnk (Map.insert i tnk mt) r
 
-push' p bs xs = if length bs/=length xs
-                then bug $ "push "++show (p,bs,xs)
-                else push bs xs
+newGen i = EvalM $ \k mt r -> do
+ tnk <- newSTRef (Evaluated (VGen i []))
+ k tnk mt r
 
-push :: Env -> LocalScope -> Stack -> Stack
-push bs [] vs = vs
-push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
-  where  err = bug $ "Unbound pattern variable "++showIdent x
+force tnk vs = EvalM $ \k mt r -> do 
+  s <- readSTRef tnk
+  case s of
+    Unevaluated env t -> case eval env t vs of
+                           EvalM f -> f (\v mt r -> do writeSTRef tnk (Evaluated v)
+                                                       r <- k v mt r
+                                                       writeSTRef tnk s
+                                                       return r) mt r
+    Evaluated v       -> case apply v vs of
+                           EvalM f -> f k mt r
 
-apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
-apply' env t [] = value env t
-apply' env t vs =
-  case t of
-    QC x                   -> return $ \ svs -> VCApp x (map ($svs) vs)
-{-
-    Q x@(m,f) | m==cPredef -> return $
-                              let constr = --trace ("predef "++show x) .
-                                           VApp x
-                              in \ svs -> maybe constr id (Map.lookup f predefs)
-                                          $ map ($svs) vs
-              | otherwise  -> do r <- resource env x
-                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
--}
-    App t1 t2              -> apply' env t1 . (:vs) =<< value env t2
-    _                      -> do fv <- value env t
-                                 return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
-
-vapply :: GLocation -> Value -> [Value] -> Value
-vapply loc v [] = v
-vapply loc v vs =
-  case v of
-    VError {} -> v
---  VClosure env (Abs b x t) -> beta gr env b x t vs
-    VAbs bt _ (Bind f) -> vbeta loc bt f vs
-    VApp pre vs1 -> delta' pre (vs1++vs)
-      where
-        delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
-                                  in vtrace loc v1 vr
-        delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
-        --msg = const (VApp pre (vs1++vs))
-        msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
-    VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
-    VFV fs -> vfv [vapply loc f vs|f<-fs]
-    VCApp f vs0 -> VCApp f (vs0++vs)
-    VMeta i env vs0 -> VMeta i env (vs0++vs)
-    VGen i vs0 -> VGen i (vs0++vs)
-    v -> bug $ "vapply "++show v++" "++show vs
-
-vbeta loc bt f (v:vs) =
-  case (bt,v) of
-    (Implicit,VImplArg v) -> ap v
-    (Explicit,         v) -> ap v
-  where
-    ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
-    ap v         = vapply loc (f v) vs
-
-vary (VFV vs) = vs
-vary v = [v]
-varyList = mapM vary
-
-{-
-beta env b x t (v:vs) =
-  case (b,v) of
-    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
-    (Explicit,         v) -> apply' (ext (x,v) env) t vs
--}
-
-vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
-  where
-    pv v = case v of
-             VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
-             _ -> ppV v
-    pf (_,VString n) = pp n
-    pf (_,v) = ppV v
-    pa (_,v) = ppV v
-    ppV v = ppTerm Unqualified 10 (value2term' True loc [] v)
-              -- Old value2term error message:
-              -- Left i  -> "variable #" <> pp i <+> "is out of scope"
-
--- | Convert a value back to a term
-value2term :: GLocation -> [Ident] -> Value -> Term
-value2term = value2term' False
-
-value2term' :: Bool -> p -> [Ident] -> Value -> Term
-value2term' stop loc xs v0 =
-  case v0 of
-    VApp pre vs    -> applyMany (Q (cPredef,predefName pre)) vs
-    VCApp f vs     -> applyMany (QC f)                       vs
-    VGen j vs      -> applyMany (var j)                      vs
-    VMeta j env vs -> applyMany (Meta j)                     vs
-    VProd bt v x f -> Prod bt x (v2t v)  (v2t' x f)
-    VAbs  bt   x f -> Abs  bt x          (v2t' x f)
-    VInt n         -> EInt n
-    VFloat f       -> EFloat f
-    VString s      -> if null s then Empty else K s
-    VSort s        -> Sort s
-    VImplArg v     -> ImplArg (v2t v)
-    VTblType p res -> Table (v2t p) (v2t res)
-    VRecType rs    -> RecType [(l, v2t v) | (l,v) <- rs]
-    VRec as        -> R       [(l, (Nothing, v2t v)) | (l,v) <- as]
-    VV t _ vs      -> V t     (map v2t vs)
-    VT wild v cs   -> T ((if wild then TWild else TTyped) (v2t v)) (map nfcase cs)
-    VFV vs         -> FV (map v2t vs)
-    VC v1 v2       -> C (v2t v1) (v2t v2)
-    VS v1 v2       -> S (v2t v1) (v2t v2)
-    VP v l         -> P (v2t v) l
-    VPatt p        -> EPatt p
-    VPattType v    -> EPattType $ v2t v
-    VAlts v vvs    -> Alts (v2t v) [(v2t x, v2t y) | (x,y) <- vvs]
-    VStrs vs       -> Strs (map v2t vs)
---  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
---  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
-    VError err     -> Error err
-  where
-    applyMany f vs = foldl App f (map v2t vs)
-    v2t = v2txs xs
-    v2txs = value2term' stop loc
-    v2t' x f = v2txs (x:xs) (bind f (gen xs))
-
-    var j
-      | j<length xs = Vr (reverse xs !! j)
-      | otherwise   = error ("variable #"++show j++" is out of scope")
-
-
-    pushs xs e = foldr push e xs
-    push x (env,xs) = ((x,gen xs):env,x:xs)
-    gen xs = VGen (length xs) []
-
-    nfcase (p,f) = (,) p (v2txs xs' (bind f env'))
-      where (env',xs') = pushs (pattVars p) ([],xs)
-
-    bind (Bind f) x = if stop
-                      then VSort (identS "...") -- hmm
-                      else f x
-
-
-linPattVars p =
-    if null dups
-    then return pvs
-    else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
-  where
-    allpvs = allPattVars p
-    pvs = nub allpvs
-    dups = allpvs \\ pvs
-
-pattVars = nub . allPattVars
-allPattVars p =
-    case p of
-      PV i    -> [i]
-      PAs i p -> i:allPattVars p
-      _       -> collectPattOp allPattVars p
-
----
-ix loc fn xs i =
-    if i<n
-    then xs !! i
-    else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
-  where n = length xs
-
-infixl 1 #,<# --,@@
-
-f # x = fmap f x
-mf <# mx  = ap mf mx
---m1 @@ m2 = (m1 =<<) . m2
-
-both f (x,y) = (,) # f x <# f y
-
-bugloc loc s = ppbug $ ppL loc s
-
-bug msg = ppbug msg
-ppbug doc = error $ render $ hang "Internal error in Compute.Concrete:" 4 doc
+zonk tnk vs = EvalM $ \k mt r -> do
+  s <- readSTRef tnk
+  case s of
+    Evaluated v -> case apply v vs of
+                     EvalM f -> f (k . Left) mt r
+    Unbound i   -> k (Right i) mt r
diff --git a/src/compiler/GF/Compile/Compute/Predef.hs b/src/compiler/GF/Compile/Compute/Predef.hs
index fe75be09d..9a17aa186 100644
--- a/src/compiler/GF/Compile/Compute/Predef.hs
+++ b/src/compiler/GF/Compile/Compute/Predef.hs
@@ -2,6 +2,10 @@
 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 module GF.Compile.Compute.Predef(predef,predefName,delta) where
 
+predef = undefined
+predefName = undefined
+delta = undefined
+{-
 import qualified Data.Map as Map
 import Data.Array(array,(!))
 import Data.List (isInfixOf,genericTake,genericDrop,genericLength)
@@ -174,3 +178,4 @@ bug msg = ppbug msg
 ppbug doc = error $ render $
                     hang "Internal error in Compute.Predef:" 4 doc
 -}
+-}
diff --git a/src/compiler/GF/Compile/Compute/Value.hs b/src/compiler/GF/Compile/Compute/Value.hs
index ea3db72a2..0871f3889 100644
--- a/src/compiler/GF/Compile/Compute/Value.hs
+++ b/src/compiler/GF/Compile/Compute/Value.hs
@@ -1,56 +1,27 @@
 module GF.Compile.Compute.Value where
-import GF.Grammar.Grammar(Label,Type,MetaId,Patt,QIdent)
+
+import Data.STRef
+import qualified Data.Map as Map
+import Control.Monad
+import Control.Monad.ST
+import Control.Applicative
+
+import GF.Grammar.Grammar(MetaId,Term)
 import PGF2(BindType)
 import GF.Infra.Ident(Ident)
-import Text.Show.Functions()
-import Data.Ix(Ix)
 
--- | Self-contained (not quite) representation of values
-data Value
-  = VApp Predefined [Value] -- from Q, always Predef.x, has a built-in value
-  | VCApp QIdent [Value] -- from QC, constructors
-  | VGen Int [Value] -- for lambda bound variables, possibly applied
-  | VMeta MetaId Env [Value]
--- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
-  | VAbs BindType Ident Binding -- used in Compute.Concrete
-  | VProd BindType Value Ident Binding -- used in Compute.Concrete
-  | VInt Integer
-  | VFloat Double
-  | VString String
-  | VSort Ident
-  | VImplArg Value
-  | VTblType Value Value
-  | VRecType [(Label,Value)]
-  | VRec [(Label,Value)]
-  | VV Type [Value] [Value] -- preserve type for conversion back to Term
-  | VT Wild Value [(Patt,Bind Env)]
-  | VC Value Value
-  | VS Value Value
-  | VP Value Label
-  | VPatt Patt
-  | VPattType Value
-  | VFV [Value]
-  | VAlts Value [(Value, Value)]
-  | VStrs [Value]
--- -- | VGlue Value Value -- hmm
--- --  | VExtR Value Value -- hmm
-  | VError String
-  deriving (Eq,Show)
+data ThunkState s
+  = Unevaluated (Env s) Term
+  | Evaluated (Value s)
+  | Unbound {-# UNPACK #-} !MetaId
 
-type Wild = Bool
-type Binding = Bind Value
-data Bind a = Bind (a->Value) deriving Show
+type Thunk s = STRef s (ThunkState s)
+type Env s = [(Ident,Thunk s)]
 
-instance Eq (Bind a) where x==y = False
-
-type Env = [(Ident,Value)]
-
--- | Predefined functions
-data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
-                | ToLower | IsUpper | Length | Plus | EqInt | LessInt
-             {- | Show | Read | ToStr | MapStr | EqVal -}
-                | Error | Trace
-                -- Canonical values below:
-                | PBool | PFalse | PTrue | Int | Float | Ints | NonExist
-                | BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
-                deriving (Show,Eq,Ord,Ix,Bounded,Enum)
+data Value s
+  = VApp Ident [Thunk s]
+  | VMeta (Thunk s) (Env s) [Thunk s]
+  | VGen  {-# UNPACK #-} !Int [Thunk s]
+  | VClosure (Env s) Term
+  | VStr String
+  | VC (Thunk s) (Thunk s)
diff --git a/src/compiler/GF/Compile/GrammarToCanonical.hs b/src/compiler/GF/Compile/GrammarToCanonical.hs
index 05b6a858b..2fcf5e5af 100644
--- a/src/compiler/GF/Compile/GrammarToCanonical.hs
+++ b/src/compiler/GF/Compile/GrammarToCanonical.hs
@@ -16,7 +16,7 @@ import GF.Grammar.Macros(typeForm,collectOp,collectPattOp,composSafeOp,mkAbs,mkA
 import GF.Grammar.Lockfield(isLockLabel)
 import GF.Grammar.Predef(cPredef,cInts)
 import GF.Compile.Compute.Predef(predef)
-import GF.Compile.Compute.Value(Predefined(..))
+-- import GF.Compile.Compute.Value(Predefined(..))
 import GF.Infra.Ident(ModuleName(..),Ident,ident2raw,rawIdentS,showIdent,isWildIdent)
 import GF.Infra.Option(Options,optionsPGF)
 import PGF2(Literal(..))
@@ -204,7 +204,7 @@ convert' gr vs = ppT
 
     ppCase (p,t) = TableRow (ppP p) (ppTv (patVars p++vs) t)
 
-    ppPredef n =
+    ppPredef n = error "TODO: ppPredef" {-
       case predef n of
         Ok BIND       -> p "BIND"
         Ok SOFT_BIND  -> p "SOFT_BIND"
@@ -214,7 +214,7 @@ convert' gr vs = ppT
         _ -> VarValue (gQId cPredef n) -- hmm
       where
        p = PredefValue . PredefId . rawIdentS
-
+-}
     ppP p =
       case p of
         PC c ps -> ParamPattern (Param (gId c) (map ppP ps))
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index ed3a20ce0..8eb6e7db6 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -23,19 +23,19 @@ import Data.Maybe(fromMaybe,isNothing)
 import qualified Control.Monad.Fail as Fail
 
 checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
-checkLType ge t ty = runTcM $ do
+checkLType ge t ty = error "TODO: checkLType" {- runTcM $ do
   vty <- liftErr (eval ge [] ty)
   (t,_) <- tcRho ge [] t (Just vty)
   t <- zonkTerm t
-  return (t,ty)
+  return (t,ty) -}
 
 inferLType :: GlobalEnv -> Term -> Check (Term, Type)
-inferLType ge t = runTcM $ do
+inferLType ge t = error "TODO: inferLType" {- runTcM $ do
   (t,ty) <- inferSigma ge [] t
   t  <- zonkTerm t
   ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty
-  return (t,ty)
-
+  return (t,ty) -}
+{-
 inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
 inferSigma ge scope t = do                                      -- GEN1
   (t,ty) <- tcRho ge scope t Nothing
@@ -800,3 +800,4 @@ runTcA g f = TcM (\ms msgs -> case f of
                                                  [(x,ms,msgs)] -> TcOk x ms msgs
                                                  rs            -> unTcM (g xs) ms msgs
                                 TcSingle f                     -> f ms msgs)
+-}