diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs
index a1545cbd5..14fa23f47 100644
--- a/src/compiler/api/GF/Compile/CheckGrammar.hs
+++ b/src/compiler/api/GF/Compile/CheckGrammar.hs
@@ -302,7 +302,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
 -- | for grammars obtained otherwise than by parsing ---- update!!
 checkReservedId :: Ident -> Check ()
 checkReservedId x =
-  when (isReservedWord x) $
+  when (isReservedWord GF x) $
        checkWarn ("reserved word used as identifier:" <+> x)
 
 -- auxiliaries
diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs
index edb3d6721..376cc6aec 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification, LambdaCase #-}
+{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-}
 
 -- | Functions for computing the values of terms in the concrete syntax, in
 -- | preparation for PMCFG generation.
 module GF.Compile.Compute.Concrete
            ( normalForm, normalFlatForm, normalStringForm
-           , Value(..), Thunk, ThunkState(..), Env, Scope, showValue
+           , Value(..), Thunk, ThunkState(..), Env, Scope, showValue, isCanonicalForm
            , PredefImpl, Predef(..), PredefCombinator, ($\)
-           , pdForce, pdClosedArgs, pdArity, pdStandard
+           , pdForce, pdCanonicalArgs, pdArity, pdStandard
            , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
            , EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn
            , eval, apply, force, value2term, patternMatch, stdPredef
@@ -27,7 +27,7 @@ import GF.Grammar.Predef
 import GF.Grammar.Lockfield(lockLabel)
 import GF.Grammar.Printer
 import GF.Data.Operations(Err(..))
-import GF.Data.Utilities(splitAt',(<||>),anyM)
+import GF.Data.Utilities(splitAt')
 import GF.Infra.CheckM
 import GF.Infra.Option
 import Data.STRef
@@ -39,6 +39,7 @@ 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)
@@ -143,36 +144,23 @@ showValue (VAlts _ _) = "VAlts"
 showValue (VStrs _) = "VStrs"
 showValue (VSymCat _ _ _) = "VSymCat"
 
-isOpen :: [Ident] -> Term -> EvalM s Bool
-isOpen bound (Vr x) = return $ x `notElem` bound
-isOpen bound (App f x) = isOpen bound f <||> isOpen bound x
-isOpen bound (Abs b x t) = isOpen (x:bound) t
-isOpen bound (ImplArg t) = isOpen bound t
-isOpen bound (Prod b x d cod) = isOpen bound d <||> isOpen (x:bound) cod
-isOpen bound (Typed t ty) = isOpen bound t
-isOpen bound (Example t s) = isOpen bound t
-isOpen bound (RecType fs) = anyM (isOpen bound . snd) fs
-isOpen bound (R fs) = anyM (isOpen bound . snd . snd) fs
-isOpen bound (P t f) = isOpen bound t
-isOpen bound (ExtR t t') = isOpen bound t <||> isOpen bound t'
-isOpen bound (Table d cod) = isOpen bound d <||> isOpen bound cod
-isOpen bound (T (TTyped ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs
-isOpen bound (T (TWild ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs
-isOpen bound (T _ cs) = anyM (isOpen bound . snd) cs
-isOpen bound (V ty cs) = isOpen bound ty <||> anyM (isOpen bound) cs
-isOpen bound (S t x) = isOpen bound t <||> isOpen bound x
-isOpen bound (Let (x,(ty,d)) t) = isOpen bound d <||> isOpen (x:bound) t
-isOpen bound (C t t') = isOpen bound t <||> isOpen bound t'
-isOpen bound (Glue t t') = isOpen bound t <||> isOpen bound t'
-isOpen bound (EPattType ty) = isOpen bound ty
-isOpen bound (ELincat c ty) = isOpen bound ty
-isOpen bound (ELin c t) = isOpen bound t
-isOpen bound (FV ts) = anyM (isOpen bound) ts
-isOpen bound (Markup tag as ts) = anyM (isOpen bound) ts <||> anyM (isOpen bound . snd) as
-isOpen bound (Reset c t) = isOpen bound t
-isOpen bound (Alts d as) = isOpen bound d <||> anyM (\(x,y) -> isOpen bound x <||> isOpen bound y) as
-isOpen bound (Strs ts) = anyM (isOpen bound) ts
-isOpen _ _ = return False
+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
 
 eval env (Vr x)         vs  = do (tnk,depth) <- lookup x env
                                  withVar depth $ do
@@ -238,12 +226,8 @@ eval env (S t1 t2)      vs  = do v1   <- eval env t1 []
                                    v1           -> return v0
 eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
                                      eval ((x,tnk):env) t2 vs
-eval env t@(Q q@(m,id)) vs
-  | m == cPredef            = do res <- evalPredef env t id vs
-                                 case res of
-                                   Const res -> return res
-                                   RunTime   -> return (VApp q vs)
-                                   NonExist  -> return (VApp (cPredef,cNonExist) [])
+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)
@@ -313,39 +297,46 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) ->
                                            Nothing  -> evalError ("Variable" <+> pp pv <+> "is not in scope")
                                  return (VSymCat d r rs)
 eval env (TSymVar d r)  []  = do return (VSymVar d r)
+eval env t@(Opts n cs)  vs  = EvalM $ \gr k e mt b r msgs ->
+  case cs of
+    []        -> return $ Fail ("No options in expression:" $$ ppTerm Unqualified 0 t) msgs
+    ((l,t):_) -> case eval env t vs of EvalM f -> f gr k e mt b r msgs
 eval env t              vs  = evalError ("Cannot reduce term" <+> pp t)
 
+apply v                             []  = return v
 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  vs0)                 vs  = return (VApp f (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
-apply v                             []  = return v
 
 
 stdPredef :: PredefTable s
 stdPredef = Map.fromList
-  [(cLength, pdStandard 1 $\ \[v] -> case value2string v of
-                                       Const s -> return (Const (VInt (genericLength s)))
-                                       _       -> return RunTime)
-  ,(cTake,   pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2))))
-  ,(cDrop,   pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2))))
-  ,(cTk,     pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2))))
-  ,(cDp,     pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2))))
-  ,(cIsUpper,pdStandard 1 $\ \[v]     -> return (fmap toPBool (liftA (all isUpper) (value2string v))))
-  ,(cToUpper,pdStandard 1 $\ \[v]     -> return (fmap string2value (liftA (map toUpper) (value2string v))))
-  ,(cToLower,pdStandard 1 $\ \[v]     -> return (fmap string2value (liftA (map toLower) (value2string v))))
-  ,(cEqStr,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2))))
-  ,(cOccur,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2))))
-  ,(cOccurs, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2))))
-  ,(cEqInt,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2))))
-  ,(cLessInt,pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2))))
-  ,(cPlus,   pdStandard 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2))))
-  ,(cError,  pdStandard 1 $\ \[v]     -> case value2string v of
-                           Const msg -> fail msg
-                           _         -> fail "Indescribable error appeared")
+  [(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")
   ]
   where
+    pd n = pdArity n . pdForce
     genericTk n = reverse . genericDrop n . reverse
     genericDp n = reverse . genericTake n . reverse
 
@@ -773,51 +764,33 @@ value2int _        = RunTime
 -- * Global/built-in definitions
 
 type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s))
-newtype Predef a s = Predef { runPredef :: Term -> Env s -> PredefImpl a s }
+newtype Predef a s = Predef { runPredef :: PredefImpl a s }
 type PredefCombinator a b s = Predef a s -> Predef b s
 
-infix 0 $\\
+infix 1 $\\
 
 ($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s
-k $\ f = k (Predef (\_ _ -> f))
+k $\ f = k (Predef f)
 
 pdForce :: PredefCombinator (Value s) (Thunk s) s
-pdForce def = Predef $ \h env args -> do
+pdForce def = Predef $ \args -> do
   argValues <- mapM force args
-  runPredef def h env argValues
+  runPredef def argValues
 
-pdClosedArgs :: PredefCombinator (Value s) (Value s) s
-pdClosedArgs def = Predef $ \h env args -> do
-  open <- anyM (value2term True [] >=> isOpen []) args
-  if open then return RunTime else runPredef def h env args
+pdCanonicalArgs :: PredefCombinator (Value s) (Value s) s
+pdCanonicalArgs def = Predef $ \args ->
+  if all isCanonicalForm args then runPredef def args else return RunTime
 
 pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s
-pdArity n def = Predef $ \h env args ->
+pdArity n def = Predef $ \args ->
   case splitAt' n args of
-    Nothing -> do
-      t <- papply env h args
-      let t' = abstract 0 (n - length args) t
-      Const <$> eval env t' []
+    Nothing                  -> return RunTime
     Just (usedArgs, remArgs) -> do
-      res <- runPredef def h env usedArgs
-      forM res $ \v -> case remArgs of
-        [] -> return v
-        _  -> do
-          t <- value2term False (fst <$> env) v
-          eval env t remArgs
-  where
-    papply env t []         = return t
-    papply env t (arg:args) = do
-      arg <- tnk2term False (fst <$> env) arg
-      papply env (App t arg) args
-    
-    abstract i n t
-      | n <= 0    = t
-      | otherwise = let x = identV (rawIdentS "a") i
-                    in  Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))
+      res <- runPredef def usedArgs
+      forM res $ \v -> apply v remArgs
 
 pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s
-pdStandard n = pdArity n . pdForce . pdClosedArgs
+pdStandard n = pdArity n . pdForce . pdCanonicalArgs
 
 -----------------------------------------------------------------------
 -- * Evaluation monad
@@ -884,11 +857,16 @@ 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 :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s))
-evalPredef env h id args = EvalM (\globals@(Gl _ predef) k e mt d r msgs ->
-  case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of
-    Just (EvalM f) -> f globals k e mt d r msgs
-    Nothing        -> k RunTime mt d r 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
diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
index 02664aefb..8afe8b92e 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
@@ -1,18 +1,22 @@
-{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-}
 
 module GF.Compile.Compute.Concrete2
-           (Env, Scope, Value(..), Constraint, ConstValue(..), Globals(..), PredefTable, EvalM,
-            runEvalM, stdPredef, globals, pdArity,
+           (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
+            ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
+            mapVariants, unvariants, variants2consts, consts2variants,
+            runEvalM, runEvalMWithOpts, stdPredef, globals,
+            PredefImpl, Predef(..), ($\),
+            pdCanonicalArgs, pdArity,
             normalForm, normalFlatForm,
             eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect,
             newResiduation, getMeta, setMeta, MetaState(..), variants, try,
-            evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
+            evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
 import GF.Infra.Ident
 import GF.Infra.CheckM
 import GF.Data.Operations(Err(..))
-import GF.Data.Utilities(splitAt',(<||>),anyM)
+import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM)
 import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
 import GF.Grammar.Grammar
 import GF.Grammar.Macros
@@ -24,19 +28,38 @@ 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
 
+type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value
+newtype Predef = Predef { runPredef :: PredefImpl }
+
+infix 1 $\
+
+($\) :: (Predef -> Predef) -> PredefImpl -> Predef
+k $\ f = k (Predef f)
+
+pdCanonicalArgs :: Bool -> Predef -> Predef
+pdCanonicalArgs flat def = Predef $ \g c args ->
+  if all (isCanonicalForm flat) args then runPredef def g c args else RunTime
+
+pdArity :: Int -> Predef -> Predef
+pdArity n def = Predef $ \g c args ->
+  case splitAt' n args of
+    Nothing -> RunTime
+    Just (usedArgs, remArgs) ->
+      runPredef def g c usedArgs <&> \v -> apply g v remArgs
+
 type Env  = [(Ident,Value)]
 type Scope = [(Ident,Value)]
-type Predef a = Globals -> Choice -> [Value] -> ConstValue a
-type PredefCombinator a = Predef a -> Predef a
-type PredefTable = Map.Map Ident (Predef Value)
+type PredefTable = Map.Map Ident Predef
 data Globals = Gl Grammar PredefTable
 
 data Value
-  = VApp QIdent [Value]
+  = VApp Choice QIdent [Value]
   | VMeta {-# UNPACK #-} !MetaId [Value]
   | VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value]
   | VGen  {-# UNPACK #-} !Int [Value]
@@ -59,7 +82,7 @@ data Value
   | VGlue Value Value
   | VPatt Int (Maybe Int) Patt
   | VPattType Value
-  | VFV Choice [Value]
+  | VFV Choice Variants
   | VAlts Value [(Value, Value)]
   | VStrs [Value]
   | VMarkup Ident [(Ident,Value)] [Value]
@@ -71,16 +94,61 @@ data Value
   | VCRecType [(Label, Bool, Value)]
   | VCInts (Maybe Integer) (Maybe Integer)
 
+data Variants
+  = VarFree [Value]
+  | VarOpts Value [(Value, Value)]
+
+mapVariants :: (Value -> Value) -> Variants -> Variants
+mapVariants f (VarFree vs)   = VarFree (f <$> vs)
+mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs)
+
+unvariants :: Variants -> [Value]
+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 (isCanonicalForm flat . snd) fs
+isCanonicalForm flat  (VR {})             = True
+isCanonicalForm flat  (VTable d cod)      = isCanonicalForm flat d && isCanonicalForm flat cod
+isCanonicalForm flat  (VT {})             = True
+isCanonicalForm flat  (VV {})             = True
+isCanonicalForm flat  (VSort {})          = True
+isCanonicalForm flat  (VInt {})           = True
+isCanonicalForm flat  (VFlt {})           = True
+isCanonicalForm flat  (VStr {})           = True
+isCanonicalForm flat  VEmpty              = True
+isCanonicalForm True  (VFV {})            = 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) vs
+isCanonicalForm flat  (VReset ctl v)      = isCanonicalForm flat v
+isCanonicalForm flat  _ = False
+
 data ConstValue a
   = Const a
   | CSusp MetaId (Value -> ConstValue a)
-  | CFV Choice [ConstValue a]
+  | CFV Choice (ConstVariants a)
   | RunTime
   | NonExist
 
+data ConstVariants a
+  = ConstFree [ConstValue a]
+  | ConstOpts Value [(Value, ConstValue a)]
+
+mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
+mapConstVs f (ConstFree vs)   = ConstFree (f <$> vs)
+mapConstVs f (ConstOpts n cs) = ConstOpts n (second f <$> cs)
+
+unconstVs :: ConstVariants a -> [ConstValue a]
+unconstVs (ConstFree vs)   = vs
+unconstVs (ConstOpts n cs) = snd <$> cs
+
 instance Functor ConstValue where
   fmap f (Const c) = Const (f c)
-  fmap f (CFV i vs) = CFV i (map (fmap f) vs)
+  fmap f (CFV i vs) = CFV i (mapConstVs (fmap f) vs)
   fmap f (CSusp i k) = CSusp i (fmap f . k)
   fmap f RunTime   = RunTime
   fmap f NonExist  = NonExist
@@ -89,8 +157,8 @@ instance Applicative ConstValue where
   pure = Const
 
   (Const f)     <*> (Const x)     = Const (f x)
-  (CFV s vs)    <*> v2            = CFV s [v1 <*> v2 | v1 <- vs]
-  v1            <*> (CFV s vs)    = CFV s [v1 <*> v2 | v2 <- vs]
+  (CFV s vs)    <*> v2            = CFV s (mapConstVs (<*> v2) vs)
+  v1            <*> (CFV s vs)    = CFV s (mapConstVs (v1 <*>) vs)
   (CSusp i k)   <*> v2            = CSusp i (\v -> k v <*> v2)
   v1            <*> (CSusp i k)   = CSusp i (\v -> v1 <*> k v)
   NonExist      <*> _             = NonExist
@@ -98,6 +166,14 @@ instance Applicative ConstValue where
   RunTime       <*>  _            = RunTime
   _             <*>  RunTime      = RunTime
 
+variants2consts :: (Value -> ConstValue a) -> Variants -> ConstVariants a
+variants2consts f (VarFree vs)   = ConstFree (f <$> vs)
+variants2consts f (VarOpts n os) = ConstOpts n (second f <$> os)
+
+consts2variants :: (ConstValue a -> Value) -> ConstVariants a -> Variants
+consts2variants f (ConstFree vs)   = VarFree (f <$> vs)
+consts2variants f (ConstOpts n os) = VarOpts n (second f <$> os)
+
 normalForm :: Globals -> Term -> Check Term
 normalForm g t = value2term g [] (bubble (eval g [] unit t []))
 
@@ -130,7 +206,7 @@ eval g env s (P t lbl)      vs  = let project (VR as)        = case lookup lbl a
                                                                  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 (map project fvs)
+                                      project (VFV s fvs)    = VFV s (mapVariants 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
@@ -139,8 +215,8 @@ 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) (VRecType as2)   = VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
-                                      extend (VFV i fvs)    v2               = VFV i [extend v1 v2 | v1 <- fvs]
-                                      extend v1             (VFV i fvs)      = VFV i [extend v1 v2 | v2 <- fvs]
+                                      extend (VFV i fvs)    v2               = VFV i (mapVariants (`extend` v2) fvs)
+                                      extend v1             (VFV i fvs)      = VFV i (mapVariants (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) []
@@ -168,37 +244,31 @@ eval g env s (S t1 t2)      vs  = let (!s1,!s2) = split s
                                                                                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 [select v1 | v1 <- fvs]
+                                      select (VFV i fvs)      = VFV i (mapVariants 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
                                           
-                                      empty = State Map.empty Map.empty
+                                      -- 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              = case Map.lookup id predef of
-                                  Nothing -> VApp q vs
-                                  Just fn -> let valueOf (Const res) = res
-                                                 valueOf (CFV i vs)  = VFV i (map valueOf vs)
-                                                 valueOf (CSusp i k) = VSusp i (valueOf . k) []
-                                                 valueOf RunTime     = VApp q vs
-                                                 valueOf NonExist    = VApp (cPredef,cNonExist) []
-                                             in valueOf (fn g c vs)
+  | m == cPredef              = evalPredef g c id vs
   | otherwise                 = case lookupResDef gr q of
                                   Ok t    -> eval g env c t vs
                                   Bad msg -> error msg
   where
     Gl gr predef = g
-eval g env s (QC q)         vs  = VApp q vs
+eval g env s (QC q)         vs  = VApp s q vs
 eval g env s (C t1 t2)      []  = let (!s1,!s2) = split s
 
                                       concat v1           VEmpty = v1
                                       concat VEmpty           v2 = v2
-                                      concat (VFV i fvs)      v2 = VFV i [concat v1 v2 | v1 <- fvs]
-                                      concat v1      (VFV i fvs) = VFV i [concat v1 v2 | v2 <- fvs]
+                                      concat (VFV i fvs)      v2 = VFV i (mapVariants (`concat` v2) fvs)
+                                      concat v1      (VFV i fvs) = VFV i (mapVariants (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) []
@@ -210,18 +280,18 @@ eval g env s (Glue t1 t2)   []  = let (!s1,!s2) = split s
 
                                       glue VEmpty        v             = v
                                       glue (VC v1 v2)    v             = VC v1 (glue v2 v)
-                                      glue (VApp q [])   v
-                                        | q == (cPredef,cNonExist)     = VApp q []
+                                      glue (VApp c q []) v
+                                        | q == (cPredef,cNonExist)     = VApp c q []
                                       glue v             VEmpty        = v
                                       glue v             (VC v1 v2)    = VC (glue v v1) v2
-                                      glue v             (VApp q [])
-                                        | q == (cPredef,cNonExist)     = VApp q []
+                                      glue v             (VApp c q [])
+                                        | q == (cPredef,cNonExist)     = VApp c q []
                                       glue (VStr s1)     (VStr s2)     = VStr (s1++s2)
                                       glue v             (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas]
                                       glue (VAlts d vas) (VStr s)      = pre d vas s
                                       glue (VAlts d vas) v             = glue d v
-                                      glue (VFV i fvs)   v2            = VFV i [glue v1 v2 | v1 <- fvs]
-                                      glue v1            (VFV i fvs)   = VFV i [glue v1 v2 | v2 <- fvs]
+                                      glue (VFV i fvs)   v2            = VFV i (mapVariants (`glue` v2) fvs)
+                                      glue v1            (VFV i fvs)   = VFV i (mapVariants (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) []
@@ -242,7 +312,7 @@ eval g env s (ELincat c ty) []  = let lbl = lockLabel c
 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 (mapC (\s t -> eval g env s t vs) s ts)
+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
@@ -256,25 +326,43 @@ eval g env c (Markup tag as ts) [] =
                               in (VMarkup tag vas vs)
 eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [])
 eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
+eval g env c t@(Opts n cs)  vs  = if null cs
+                                  then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
+                                  else let (c1,c2,c3) = split3 c
+                                           vn = eval g env c1 n []
+                                           vcs = mapC evalOpt c cs
+                                       in VFV c3 (VarOpts vn vcs)
+  where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
 eval g env c t              vs  = VError ("Cannot reduce term" <+> pp t)
 
+evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
+evalPredef g@(Gl gr pds) c n args =
+  case Map.lookup n pds of
+    Nothing  -> VApp c (cPredef,n) args
+    Just def -> let valueOf (Const res) = res
+                    valueOf (CFV i vs)  = VFV i (consts2variants valueOf vs)
+                    valueOf (CSusp i k) = VSusp i (valueOf . k) []
+                    valueOf RunTime     = VApp c (cPredef,n) args
+                    valueOf NonExist    = VApp c (cPredef,cNonExist) []
+                in valueOf (runPredef def g c args)
+
 stdPredef :: Globals -> PredefTable
 stdPredef g = Map.fromList
-  [(cLength, pdArity 1 $ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
-  ,(cTake,   pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
-  ,(cDrop,   pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
-  ,(cTk,     pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
-  ,(cDp,     pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
-  ,(cIsUpper,pdArity 1 $ \g c [v]     -> fmap toPBool (liftA (all isUpper) (value2string g v)))
-  ,(cToUpper,pdArity 1 $ \g c [v]     -> fmap string2value (liftA (map toUpper) (value2string g v)))
-  ,(cToLower,pdArity 1 $ \g c [v]     -> fmap string2value (liftA (map toLower) (value2string g v)))
-  ,(cEqStr,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
-  ,(cOccur,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
-  ,(cOccurs, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
-  ,(cEqInt,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
-  ,(cLessInt,pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
-  ,(cPlus,   pdArity 2 $ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
-  ,(cError,  pdArity 1 $ \g c [v]     -> fmap (VError . pp) (value2string g v))
+  [(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
+  ,(cTake,   pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
+  ,(cDrop,   pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
+  ,(cTk,     pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
+  ,(cDp,     pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
+  ,(cIsUpper,pdArity 1 $\ \g c [v]     -> fmap toPBool (liftA (all isUpper) (value2string g v)))
+  ,(cToUpper,pdArity 1 $\ \g c [v]     -> fmap string2value (liftA (map toUpper) (value2string g v)))
+  ,(cToLower,pdArity 1 $\ \g c [v]     -> fmap string2value (liftA (map toLower) (value2string g v)))
+  ,(cEqStr,  pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
+  ,(cOccur,  pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
+  ,(cOccurs, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
+  ,(cEqInt,  pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
+  ,(cLessInt,pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
+  ,(cPlus,   pdArity 2 $\ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
+  ,(cError,  pdArity 1 $\ \g c [v]     -> fmap (VError . pp) (value2string g v))
   ]
   where
     genericTk n = reverse . genericDrop n . reverse
@@ -282,16 +370,22 @@ stdPredef g = Map.fromList
 
 apply g (VMeta i vs0)                   vs  = VMeta i   (vs0++vs)
 apply g (VSusp i k vs0)                 vs  = VSusp i k (vs0++vs)
-apply g (VApp f  vs0)                   vs  = VApp f (vs0++vs)
+apply g (VApp c f@(m,n)  vs0)           vs
+  | m == cPredef                            = evalPredef g c n (vs0++vs)
+  | otherwise                               = VApp c f (vs0++vs)
 apply g (VGen i  vs0)                   vs  = VGen i (vs0++vs)
-apply g (VFV i fvs)                     vs  = VFV i [apply g v vs | v <- fvs]
+apply g (VFV i fvs)                     vs  = VFV i (mapVariants (\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 f vs) = liftL (VApp f) vs
+    bubble (VApp c f vs) = liftL (VApp c f) vs
     bubble (VMeta metaid vs) = liftL (VMeta metaid) vs
     bubble (VSusp metaid k vs) = liftL (VSusp metaid k) vs
     bubble (VGen i vs) = liftL (VGen i) vs
@@ -314,9 +408,12 @@ bubble v = snd (bubble v)
     bubble (VGlue v1 v2) = lift2 VGlue v1 v2
     bubble v@(VPatt _ _ _) = lift0 v
     bubble (VPattType v) = lift1 VPattType v
-    bubble (VFV c vs) =
+    bubble (VFV c (VarFree vs)) =
       let (union,vs') = mapAccumL descend Map.empty vs
-      in (Map.insert c (length vs,1) union, addVariants (VFV c vs') union)
+      in (Map.insert c (BubbleFree (length vs),1) union, addVariants (VFV c (VarFree vs')) union)
+    bubble (VFV c (VarOpts n os)) =
+      let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
+      in (Map.insert c (BubbleOpts n (fst <$> os),1) union, addVariants (VFV c (VarOpts n os')) union)
     bubble (VAlts v vs) = lift1L2 VAlts v vs
     bubble (VStrs vs) = liftL VStrs vs
     bubble (VMarkup tag attrs vs) =
@@ -379,7 +476,7 @@ bubble v = snd (bubble v)
       let (choices,v') = bubble v
       in (mergeChoices1 union choices,v')
 
-    descend' :: Map.Map Choice (Int,Int) -> (a,Value) -> (Map.Map Choice (Int,Int),(a,Value))
+    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'))
@@ -399,16 +496,18 @@ bubble v = snd (bubble v)
 
     addVariants v = Map.foldrWithKey addVariant v
       where
-        addVariant c (n,cnt) v
-          | cnt > 1   = VFV c (replicate n v)
+        addVariant c (bvs,cnt) v
+          | cnt > 1   = VFV c $ case bvs of
+                                  BubbleFree k    -> VarFree (replicate k v)
+                                  BubbleOpts n os -> VarOpts n ((,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 (cPredef,cPTrue)  []
-toPBool False = VApp (cPredef,cPFalse) []
+toPBool True  = VApp poison (cPredef,cPTrue)  []
+toPBool False = VApp poison (cPredef,cPFalse) []
 
 occur s1 []          = False
 occur s1 s2@(_:tail) = check s1 s2
@@ -451,8 +550,8 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
         (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 [match' env p ps eqs arg args | arg <- vs]
-        (PP q qs,    VApp r vs)
+        (p,           VFV s vs) -> VFV s (mapVariants (\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)
@@ -510,7 +609,7 @@ vtableSelect g v0 ty cs v2 vs =
   where
     select (Const (i,_)) = cs !! i
     select (CSusp i k)   = VSusp i (\v -> select (k v)) []
-    select (CFV s vs)    = VFV s (map select vs)
+    select (CFV s vs)    = VFV s (consts2variants select vs)
     select _             = v0
 
     value2index (VMeta i vs)      ty = CSusp i (\v -> value2index (apply g v vs) ty)
@@ -525,9 +624,9 @@ vtableSelect g v0 ty cs v2 vs =
                               (compute lbls)
             Nothing -> error (show ("Missing value for label" <+> pp lbl $$
                                     "among" <+> hsep (punctuate (pp ',') (map fst as))))
-    value2index (VApp q tnks) ty =
+    value2index (VApp c q args) ty =
       let (r ,ctxt,cnt ) = getIdxCnt q
-      in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt tnks)
+      in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args)
       where
         getIdxCnt q =
           let (_,ResValue (L _ ty) idx) = getInfo q
@@ -550,7 +649,7 @@ vtableSelect g v0 ty cs v2 vs =
         Gl gr _ = g
     value2index (VInt n)          ty
       | Just max <- isTypeInts ty    = Const (fromIntegral n,fromIntegral max+1)
-    value2index (VFV i vs)        ty = CFV i [value2index v ty | v <- vs]
+    value2index (VFV i vs)        ty = CFV i (variants2consts (\v -> value2index v ty) vs)
     value2index v ty = RunTime
 
 
@@ -566,11 +665,23 @@ data MetaState
   = Bound Scope Value
   | Narrowing   Type
   | Residuation Scope (Maybe Constraint)
+data OptionInfo
+  = OptionInfo
+      { optChoice  :: Choice
+      , optLabel   :: Value
+      , optChoices :: [Value]
+      }
+type ChoiceMap = Map.Map Choice Int
 data State
-  = State 
-      { choices  :: Map.Map Choice Int
+  = State
+      { choices  :: ChoiceMap
       , metaVars :: Map.Map MetaId MetaState
+      , options  :: [OptionInfo]
       }
+
+cleanOptions :: [OptionInfo] -> ChoiceMap -> ChoiceMap
+cleanOptions opts = Map.filterWithKey (\k _ -> any (\opt -> k == optChoice opt) opts)
+
 type Cont r = State -> r -> [Message] -> CheckResult r [Message]
 newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r)
 
@@ -606,46 +717,52 @@ runEvalM g (EvalM f) = Check $ \(es,ws) ->
     Fail   msg ws -> Fail msg (es,ws)
     Success xs ws -> Success (reverse xs) (es,ws)
   where
-    empty = State Map.empty Map.empty
+    empty = State Map.empty Map.empty []
+
+runEvalMWithOpts :: Globals -> ChoiceMap -> EvalM a -> Check [(a, ChoiceMap, [OptionInfo])]
+runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
+  case f g (\x (State cs mvs os) xs ws -> Success ((x,cs,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 cs 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
-  where
-    empty = State Map.empty Map.empty
 
 globals :: EvalM Globals
 globals = EvalM (\g k -> k g)
 
 variants :: Choice -> [a] -> EvalM a
-variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
+variants c xs = EvalM (\g k state@(State choices metas opts) r msgs ->
   case Map.lookup c choices of
     Just j  -> k (xs !! j) state r msgs
-    Nothing -> backtrack 0 xs k choices metas r msgs)
+    Nothing -> backtrack 0 xs k choices metas opts r msgs)
   where
-    backtrack j []     k choices metas r msgs = Success r msgs
-    backtrack j (x:xs) k choices metas r msgs =
-      case k x (State (Map.insert c j choices) metas) r msgs of
+    backtrack j []     k choices metas opts r msgs = Success r msgs
+    backtrack j (x:xs) k choices metas opts r msgs =
+      case k x (State (Map.insert c j choices) metas opts) r msgs of
         Fail    msg msgs -> Fail msg msgs
-        Success r   msgs -> backtrack (j+1) xs k choices metas r msgs
+        Success r   msgs -> backtrack (j+1) xs k choices metas opts r msgs
 
 variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term
-variants' c f xs = EvalM (\g k state@(State choices metas) r msgs ->
+variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
   case Map.lookup c choices of
     Just j  -> case f (xs !! j) of
                  EvalM f -> f g k state r msgs
-    Nothing -> case backtrack g 0 xs choices metas [] msgs of
+    Nothing -> case backtrack g 0 xs 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 []     choices metas ts msgs = Success ts msgs
-    backtrack g j (x:xs) choices metas ts msgs =
+    backtrack g j []     choices metas opts ts msgs = Success ts msgs
+    backtrack g j (x:xs) choices metas opts ts msgs =
       case f x of
-        EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State (Map.insert c j choices) metas) ts msgs of
+        EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State (Map.insert c j choices) metas opts) ts msgs of
                      Fail    msg msgs -> Fail msg msgs
-                     Success ts  msgs -> backtrack g (j+1) xs choices metas ts msgs
+                     Success ts  msgs -> backtrack g (j+1) xs choices metas opts ts msgs
 
 try :: (a -> EvalM b) -> [a] -> Message -> EvalM b
 try f xs msg = EvalM (\g k state r msgs ->
@@ -668,9 +785,9 @@ try f xs msg = EvalM (\g k state r msgs ->
         Success r msgs -> continue g k res r msgs
 
 newResiduation :: Scope -> EvalM MetaId
-newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
+newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
   let meta_id = Map.size metas+1
-  in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas)) r msgs)
+  in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas) opts) r msgs)
 
 getMeta :: MetaId -> EvalM MetaState
 getMeta i = EvalM (\g k state r msgs ->
@@ -679,12 +796,12 @@ getMeta i = EvalM (\g k state r msgs ->
     Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) 
 
 setMeta :: MetaId -> MetaState -> EvalM ()
-setMeta i ms = EvalM (\g k (State choices metas) r msgs ->
-  let state' = State choices (Map.insert i ms metas)
+setMeta i ms = EvalM (\g k (State choices metas opts) r msgs ->
+  let state' = State choices (Map.insert i ms metas) opts
   in k () state' r msgs)
 
 value2termM :: Bool -> [Ident] -> Value -> EvalM Term
-value2termM flat xs (VApp q vs) =
+value2termM flat xs (VApp c q vs) =
   foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs
 value2termM flat xs (VMeta i vs) = do
   mv <- getMeta i
@@ -788,11 +905,18 @@ value2termM flat xs (VGlue v1 v2) = do
   t1 <- value2termM flat xs v1
   t2 <- value2termM flat xs v2
   return (Glue t1 t2)
-value2termM flat xs (VFV i vs) =
-  case flat of
-    True  -> do v <- variants i vs
-                value2termM True xs v
-    False -> variants' i (value2termM False xs) vs
+value2termM True xs (VFV i (VarFree vs)) = do
+  v <- variants i vs
+  value2termM True xs v
+value2termM False xs (VFV i (VarFree vs)) = variants' i (value2termM False xs) vs
+value2termM flat xs (VFV i (VarOpts n os)) =
+  EvalM $ \g k (State choices metas opts) r msgs ->
+    let j = fromMaybe 0 (Map.lookup i choices)
+    in case os `maybeAt` j of
+         Just (l,t) -> case value2termM flat xs t of
+                         EvalM f -> let oi = OptionInfo i n (fst <$> os)
+                                    in f g k (State choices metas (oi: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)
@@ -855,7 +979,7 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
 pattVars st _            = st
 
 
-ppValue q d (VApp c vs) = prec d 4 (hsep (ppQIdent q c : map (ppValue q 5) vs))
+ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
 ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
 ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
 ppValue q d (VGen _ _) = pp "VGen"
@@ -882,7 +1006,7 @@ ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1
 ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+'  <+> ppValue q 2 v2)
 ppValue q d (VPatt _ _ _) = pp "VPatt"
 ppValue q d (VPattType _) = pp "VPattType"
-ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs))))
+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"
@@ -912,26 +1036,26 @@ 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 i vs)        = CFV i [concat v1 v2 | v2 <- vs]
+    concat v1 (CFV i vs)        = CFV i (mapConstVs (concat v1) vs)
     concat v1 res               = res
-value2string' g (VApp q []) b    ws      qs
+value2string' g (VApp c q []) b   ws     qs
   | q == (cPredef,cNonExist)              = NonExist
-value2string' g (VApp q []) b    ws      qs
+value2string' g (VApp c q []) b   ws     qs
   | q == (cPredef,cSOFT_SPACE)            = if null ws
                                               then Const (b,ws,q:qs)
                                               else Const (b,ws,qs)
-value2string' g (VApp q []) b     ws     qs
+value2string' g (VApp c q []) b   ws     qs
   | q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND) 
                                           = if null ws
                                               then Const (True,ws,q:qs)
                                               else Const (True,ws,qs)
-value2string' g (VApp q []) b     ws     qs
+value2string' g (VApp c q []) b   ws     qs
   | q == (cPredef,cCAPIT) = capit ws
   where
     capit []            = Const (b,[],q:qs)
     capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs)
     capit ws            = Const (b,ws,qs)
-value2string' g (VApp q []) b     ws     qs
+value2string' g (VApp c q []) b   ws     qs
   | q == (cPredef,cALL_CAPIT) = all_capit ws
   where
     all_capit []       = Const (b,[],q:qs)
@@ -946,7 +1070,7 @@ value2string' g (VAlts vd vas) b  ws     qs =
       | 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 [value2string' g v b ws qs | v <- vs]
+  CFV s (variants2consts (\v -> value2string' g v b ws qs) vs)
 value2string' _ _ _ _ _ = RunTime
 
 startsWith []          _ = True
@@ -963,17 +1087,24 @@ 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 (map (value2int g) vs)
+value2int g (VFV s vs)       = CFV s (variants2consts (value2int g) vs)
 value2int g _                = RunTime
 
-newtype Choice = Choice Integer deriving (Eq,Ord,Pretty,Show)
+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))
 
@@ -993,15 +1124,3 @@ mapCM f c (x:xs) = do
   y  <- f c1 x
   ys <- mapCM f c2 xs
   return (y:ys)
-
-pdArity :: Int -> PredefCombinator Value
-pdArity n def = \g c args ->
-  case splitAt' n args of
-    Nothing -> RunTime
-    Just (usedArgs, remArgs) ->
-      fmap (\v -> apply g v remArgs) (def g c usedArgs)
-  where
-    abstract i n t
-      | n <= 0    = t
-      | otherwise = let x = identV (rawIdentS "a") i
-                    in Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))
diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs
index b13dde7be..e9a909f6d 100644
--- a/src/compiler/api/GF/Compile/Repl.hs
+++ b/src/compiler/api/GF/Compile/Repl.hs
@@ -1,24 +1,40 @@
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LambdaCase, TupleSections, NamedFieldPuns #-}
 
 module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where
 
-import Control.Monad (unless, forM_, foldM)
+import Control.Monad (join, when, unless, forM_, foldM)
 import Control.Monad.IO.Class (MonadIO)
 import qualified Data.ByteString.Char8 as BS
 import Data.Char (isSpace)
 import Data.Function ((&))
 import Data.Functor ((<&>))
+import Data.List (find)
 import qualified Data.Map as Map
+import Data.Maybe (fromMaybe)
+import Text.Read (readMaybe)
 
 import System.Console.GetOpt (ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..), getOpt, usageInfo)
 import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn)
 import System.Directory (getAppUserDataDirectory)
 
 import GF.Compile (batchCompile)
-import GF.Compile.Compute.Concrete2 (Globals(Gl), stdPredef, normalFlatForm)
+import GF.Compile.Compute.Concrete2
+  ( Choice(..)
+  , ChoiceMap
+  , Globals(Gl)
+  , OptionInfo(..)
+  , stdPredef
+  , unit
+  , eval
+  , cleanOptions
+  , runEvalMWithOpts
+  , value2termM
+  , ppValue
+  )
 import GF.Compile.Rename (renameSourceTerm)
 import GF.Compile.TypeCheck.ConcreteNew (inferLType)
 import GF.Data.ErrM (Err(..))
+import GF.Data.Utilities (maybeAt, orLeft)
 import GF.Grammar.Grammar
   ( Grammar
   , mGrammar
@@ -33,7 +49,7 @@ import GF.Grammar.Grammar
   , Term(Typed)
   , prependModule
   )
-import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP)
+import GF.Grammar.Lexer (Posn(..), Lang(..), runLangP)
 import GF.Grammar.Parser (pTerm)
 import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm)
 import GF.Infra.CheckM (Check, runCheck)
@@ -41,14 +57,22 @@ import GF.Infra.Ident (moduleNameS)
 import GF.Infra.Option (noOptions)
 import GF.Infra.UseIO (justModuleName)
 import GF.Text.Pretty (render)
+import Debug.Trace
 
 data ReplOpts = ReplOpts
-  { noPrelude :: Bool
+  { lang :: Lang
+  , noPrelude :: Bool
   , inputFiles :: [String]
+  , evalToFlat :: Bool
   }
 
 defaultReplOpts :: ReplOpts
-defaultReplOpts = ReplOpts False []
+defaultReplOpts = ReplOpts
+  { lang = GF
+  , noPrelude = False
+  , inputFiles = []
+  , evalToFlat = True
+  }
 
 type Errs a = Either [String] a
 type ReplOptsOp = ReplOpts -> Errs ReplOpts
@@ -57,6 +81,14 @@ replOptDescrs :: [OptDescr ReplOptsOp]
 replOptDescrs =
   [ Option ['h'] ["help"] (NoArg $ \o -> Left [usageInfo "gfci" replOptDescrs]) "Display help."
   , Option [] ["no-prelude"] (flag $ \o -> o { noPrelude = True }) "Don't load the prelude."
+  , Option [] ["lang"] (ReqArg (\s o -> case s of
+                                          "gf"   -> Right (o { lang = GF })
+                                          "bnfc" -> Right (o { lang = BNFC })
+                                          "nlg"  -> Right (o { lang = NLG })
+                                          _      -> Left ["Unknown language variant: " ++ s])
+                               "{gf,bnfc,nlg}")
+           "Set the active language variant."
+  , Option [] ["no-flat"] (flag $ \o -> o { evalToFlat = False }) "Do not evaluate to flat form."
   ]
   where
     flag f = NoArg $ \o -> pure (f o)
@@ -68,12 +100,14 @@ getReplOpts args = case errs of
   where
     (flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args
 
-execCheck :: MonadIO m => Check a -> (a -> InputT m ()) -> InputT m ()
+execCheck :: MonadIO m => Check a -> (a -> InputT m b) -> InputT m (Maybe b)
 execCheck c k = case runCheck c of
   Ok (a, warn) -> do
     unless (null warn) $ outputStrLn warn
-    k a
-  Bad err -> outputStrLn err
+    Just <$> k a
+  Bad err -> do
+    outputStrLn err
+    return Nothing
 
 replModNameStr :: String
 replModNameStr = "<repl>"
@@ -81,47 +115,182 @@ replModNameStr = "<repl>"
 replModName :: ModuleName
 replModName = moduleNameS replModNameStr
 
-parseThen :: MonadIO m => Grammar -> String -> (Term -> InputT m ()) -> InputT m ()
-parseThen g s k = case runLangP GF pTerm (BS.pack s) of
-  Left (Pn l c, err) -> outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")"
+parseThen :: MonadIO m => Lang -> Grammar -> String -> (Term -> InputT m b) -> InputT m (Maybe b)
+parseThen l g s k = case runLangP l pTerm (BS.pack s) of
+  Left (Pn l c, err) -> do
+    outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")"
+    return Nothing
   Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t
 
-runRepl' :: Globals -> IO ()
-runRepl' gl@(Gl g _) = do
+data ResultState = ResultState
+  { srsResult  :: Term
+  , srsChoices :: ChoiceMap
+  , srsOptInfo :: [OptionInfo]
+  , srsOpts    :: ChoiceMap
+  }
+data OptionState = OptionState
+  { osTerm     :: Term
+  , osResults  :: [ResultState]
+  , osSelected :: Maybe ResultState
+  }
+newtype ReplState = ReplState
+  { rsOpts :: Maybe OptionState
+  }
+
+initState :: ReplState
+initState = ReplState Nothing
+
+runRepl' :: ReplOpts -> Globals -> IO ()
+runRepl' opts@ReplOpts { lang, evalToFlat } gl@(Gl g _) = do
   historyFile <- getAppUserDataDirectory "gfci_history"
-  runInputT (Settings noCompletion (Just historyFile) True) repl -- TODO tab completion
+  runInputT (Settings noCompletion (Just historyFile) True) (repl initState) -- TODO tab completion
   where
-    repl = do
+    repl st = do
       getInputLine "gfci> " >>= \case
-        Nothing -> repl
-        Just (':' : l) -> let (cmd, arg) = break isSpace l in command cmd (dropWhile isSpace arg)
-        Just code -> evalPrintLoop code
+        Nothing -> repl st
+        Just (':' : l) -> let (cmd, arg) = break isSpace l in command st cmd (dropWhile isSpace arg)
+        Just code -> evalPrintLoop st code
+
+    nlrepl st = outputStrLn "" >> repl st
 
-    command "t" arg = do
-      parseThen g arg $ \main ->
+    -- Show help text
+    command st "?" arg = do
+      outputStrLn ":? -- show help text."
+      outputStrLn ":t <expr> -- show the inferred type of <expr>."
+      outputStrLn ":r -- show the results of the last eval."
+      outputStrLn ":s <index> -- select the result at <index>."
+      outputStrLn ":c -- show the current selected result."
+      outputStrLn ":o <choice> <value> -- set option <choice> to <value>."
+      outputStrLn ":q -- quit the REPL."
+      nlrepl st
+
+    -- Show the inferred type of an expression
+    command st "t" arg = do
+      parseThen lang g arg $ \main ->
         execCheck (inferLType gl main) $ \res ->
           forM_ res $ \(t, ty) ->
             let t' = case t of
                        Typed _ _ -> t
                        t         -> Typed t ty
             in outputStrLn $ render (ppTerm Unqualified 0 t')
-      outputStrLn "" >> repl
+      nlrepl st
+    
+    -- Show the results of the last evaluated expression
+    command st "r" arg = do
+      case rsOpts st of
+        Nothing -> do
+          outputStrLn "No results to show!"
+        Just (OptionState t rs _) -> do
+          outputStrLn $ "> " ++ render (ppTerm Unqualified 0 t)
+          outputResults rs
+      nlrepl st
+
+    -- Select a result to "focus" by its index
+    command st "s" arg = do
+      let e = do (OptionState t rs _) <- orLeft "No results to select!" $ rsOpts st
+                 s <- orLeft "Could not parse result index!" $ readMaybe arg
+                 (ResultState r cs ois os) <- orLeft "Result index out of bounds!" $ rs `maybeAt` (s - 1)
+                 return (t, rs, r, cs, ois, os)
+      case e of
+        Left err -> do
+          outputStrLn err
+          nlrepl st
+        Right (t, rs, r, cs, ois, os) -> do
+          outputStrLn $ render (ppTerm Unqualified 0 r)
+          outputOptions ois os
+          nlrepl (st { rsOpts = Just (OptionState t rs (Just (ResultState r cs ois os))) })
+
+    -- Show the current selected result
+    command st "c" arg = do
+      let e = do (OptionState t _ sel) <- orLeft "No results to select!" $ rsOpts st
+                 (ResultState r _ ois os) <- orLeft "No result selected!" sel
+                 return (t, r, ois, os)
+      case e of
+        Left err -> outputStrLn err
+        Right (t, r, ois, os) -> do
+          outputStrLn $ "> " ++ render (ppTerm Unqualified 0 t)
+          outputStrLn $ render (ppTerm Unqualified 0 r)
+          outputOptions ois os
+      nlrepl st
+
+    -- Set an option for the selected result
+    command st "o" arg = do
+      let e = do (OptionState t _ sel) <- orLeft "No results to select!" $ rsOpts st
+                 (ResultState _ cs ois os) <- orLeft "No result selected!" sel
+                 (c, i) <- case words arg of
+                             [argc, argi] -> do
+                               c <- orLeft "Could not parse option choice!" $ readMaybe argc
+                               i <- orLeft "Could not parse option value!" $ readMaybe argi
+                               return (c, i)
+                             _ -> Left "Expected two arguments!"
+                 when (i < 1) $ Left "Option value must be positive!"
+                 oi <- orLeft "No such option!" $ find (\oi -> unchoice (optChoice oi) == c) ois
+                 when (i > length (optChoices oi)) $ Left "Option value out of bounds!"
+                 return (t, cs, ois, os, c, i)
+      case e of
+        Left err -> do
+          outputStrLn err
+          nlrepl st
+        Right (t, cs, ois, os, c, i) -> do
+          let os' = Map.insert (Choice c) (i - 1) os
+          nfs <- execCheck (doEval st t (Map.union os' cs)) pure
+          case nfs of
+            Nothing -> nlrepl st
+            Just [] -> do
+              outputStrLn "No results!"
+              nlrepl st
+            Just [(r, cs, ois')] -> do
+              outputStrLn $ render (ppTerm Unqualified 0 r)
+              let os'' = cleanOptions ois' os'
+              outputOptions ois' os''
+              let rst = ResultState r (Map.difference cs os') ois' os''
+              nlrepl (st { rsOpts = Just (OptionState t [rst] (Just rst)) })
+            Just rs -> do
+              let rsts = rs <&> \(r, cs, ois') ->
+                           ResultState r (Map.difference cs os') ois' (cleanOptions ois' os')
+              outputResults rsts
+              nlrepl (st { rsOpts = Just (OptionState t rsts Nothing) })
     
-    command "q" _ = outputStrLn "Bye!"
+    -- Quit the REPL
+    command _ "q" _ = outputStrLn "Bye!"
+
+    command st cmd _ = do
+      outputStrLn $ "Unknown REPL command \"" ++ cmd ++ "\"! Use :? for help."
+      nlrepl st
 
-    command cmd _ = do
-      outputStrLn $ "Unknown REPL command: " ++ cmd
-      outputStrLn "" >> repl
+    evalPrintLoop st code = do -- TODO bindings
+      c <- parseThen lang g code $ \main -> do
+        rsts <- execCheck (doEval st main Map.empty) $ \nfs -> do
+          if null nfs then do
+            outputStrLn "No results!"
+            return Nothing
+          else do
+            let rsts = nfs <&> \(r, cs, ois) -> ResultState r cs ois Map.empty
+            outputResults rsts
+            return $ Just rsts
+        return $ (main,) <$> join rsts
+      case join c of
+        Just (t, rs) -> nlrepl (ReplState (Just (OptionState t rs Nothing)))
+        Nothing      -> nlrepl st
 
-    evalPrintLoop code = do -- TODO bindings
-      parseThen g code $ \main ->
-        execCheck (inferLType gl main >>= \((t, _):_) -> normalFlatForm gl t) $ \nfs ->
-          forM_ (zip [1..] nfs) $ \(i, nf) ->
-            outputStrLn $ show i ++ ". " ++ render (ppTerm Unqualified 0 nf)
-      outputStrLn "" >> repl
+    doEval st t opts = inferLType gl t >>= \case
+      []          -> fail $ "No result while checking type: " ++ render (ppTerm Unqualified 0 t)
+      ((t', _):_) -> runEvalMWithOpts gl opts (value2termM evalToFlat [] (eval gl [] unit t' []))
+    
+    outputResults rs =
+      forM_ (zip [1..] rs) $ \(i, ResultState r _ opts _) ->
+        outputStrLn $ show i ++ (if null opts then ". " else "*. ") ++ render (ppTerm Unqualified 0 r)
+    
+    outputOptions ois os =
+      forM_ ois $ \(OptionInfo c n ls) -> do
+        outputStrLn ""
+        outputStrLn $ show (unchoice c) ++ ") " ++ render (ppValue Unqualified 0 n)
+        let sel = fromMaybe 0 (Map.lookup c os) + 1
+        forM_ (zip [1..] ls) $ \(i, l) ->
+          outputStrLn $ (if i == sel then "->" else "  ") ++ show i ++ ". " ++ render (ppValue Unqualified 0 l)
 
 runRepl :: ReplOpts -> IO ()
-runRepl (ReplOpts noPrelude inputFiles) = do
+runRepl opts@ReplOpts { noPrelude, inputFiles } = do
   -- TODO accept an ngf grammar
   let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles
   (g0, opens) <- case toLoad of
@@ -143,4 +312,4 @@ runRepl (ReplOpts noPrelude inputFiles) = do
       , jments  = Map.empty
       }
     g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g)
-  runRepl' g
+  runRepl' opts g
diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
index 44fee0401..1194ae4b3 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -21,6 +21,7 @@ import Data.STRef
 import Data.List (nub, (\\), tails)
 import qualified Data.Map as Map
 import Data.Maybe(fromMaybe,isNothing,mapMaybe)
+import Data.Bifunctor(second)
 import Data.Functor((<&>))
 import qualified Control.Monad.Fail as Fail
 
@@ -57,14 +58,14 @@ inferSigma scope s t = do                                      -- GEN1
   let forall_tvs = res_tvs \\ env_tvs
   quantify scope t forall_tvs ty
 
-vtypeInt   = VApp (cPredef,cInt) []
-vtypeFloat = VApp (cPredef,cFloat) []
-vtypeInts i= VApp (cPredef,cInts) [VInt i]
+vtypeInt   = VApp poison (cPredef,cInt) []
+vtypeFloat = VApp poison (cPredef,cFloat) []
+vtypeInts i= VApp poison (cPredef,cInts) [VInt i]
 vtypeStr   = VSort cStr
 vtypeStrs  = VSort cStrs
 vtypeType  = VSort cType
 vtypePType = VSort cPType
-vtypeMarkup= VApp (cPredef,cMarkup) []
+vtypeMarkup= VApp poison (cPredef,cMarkup) []
 
 tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
 tcRho scope s t@(EInt i)   mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT
@@ -90,7 +91,7 @@ tcRho scope c (Abs bt var body) Nothing = do                   -- ABS1
          in return (Abs bt var body, (VProd bt v arg_ty body_ty))
     else return (Abs bt var body, (VProd bt identW arg_ty body_ty))
   where
-    check m n st (VApp f vs)       = foldM (check m n) st vs
+    check m n st (VApp c f vs)     = foldM (check m n) st vs
     check m n st (VMeta i vs)      = do
       state <- getMeta i
       case state of
@@ -98,8 +99,8 @@ tcRho scope c (Abs bt var body) Nothing = do                   -- ABS1
                         check m n st (apply g v vs)
         _         -> foldM (check m n) st vs
     check m n st@(b,xs) (VGen i vs)
-      | i == m                     = return (True, xs)
-      | otherwise                  = return st
+      | i == m                       = return (True, xs)
+      | otherwise                    = return st
     check m n st (VClosure env c (Abs bt x t)) = do
       g <- globals
       check m (n+1) st (eval g ((x,VGen n []):env) c t [])
@@ -118,7 +119,7 @@ tcRho scope c (Abs bt var body) Nothing = do                   -- ABS1
       check m n st v1 >>= \st -> check m n st v2
     check m n st (VTable v1 v2)    =
       check m n st v1 >>= \st -> check m n st v2
-    check m n st (VT ty env c cs)    =
+    check m n st (VT ty env c cs) =
       check m n st ty    -- Traverse cs as well
     check m n st (VV ty cs)        =
       check m n st ty >>= \st -> foldM (check m n) st cs
@@ -186,17 +187,7 @@ tcRho scope c (Typed body ann_ty) mb_ty = do                   -- ANNOT
   (body,_) <- tcRho scope c3 body (Just v_ann_ty)
   instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty
 tcRho scope c (FV ts) mb_ty = do
-  (ty,subsume) <-
-    case mb_ty of
-      Just ty -> do return (ty, \t ty' -> return t)
-      Nothing -> do i <- newResiduation scope
-                    let ty = VMeta i []
-                    return (ty, \t ty' -> subsCheckRho scope t ty' ty)
-
-  let go c t = do (t, ty) <- tcRho scope c t mb_ty
-                  subsume t ty
-
-  ts <- mapCM go c ts
+  (ts,ty) <- tcUnifying scope c ts mb_ty
   return (FV ts, ty)
 tcRho scope s t@(Sort _) mb_ty = do
   instSigma scope s t vtypeType mb_ty
@@ -389,11 +380,17 @@ tcRho scope c (Reset ctl t) mb_ty =
        Limit n      -> do (t,_) <- tcRho scope c1 t Nothing
                           instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
        Coordination mb_mn@(Just mn) conj _
-                    -> do tcRho scope c1 (QC (mn,conj)) (Just (VApp (mn,identS "Conj") []))
+                    -> do tcRho scope c1 (QC (mn,conj)) (Just (VApp poison (mn,identS "Conj") []))
                           (t,ty) <- tcRho scope c2 t mb_ty
                           case ty of
-                            VApp id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
-                            _          -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
+                            VApp c id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
+                            _            -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
+tcRho scope s (Opts n cs) mb_ty = do
+  let (s1,s2,s3) = split3 s
+  (n,_) <- tcRho scope s1 n Nothing
+  (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
+  (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
+  return (Opts n (zip ls ts), ty)
 tcRho scope s t _ = unimplemented ("tcRho "++show t)
 
 evalCodomain :: Scope -> Ident -> Value -> EvalM Value
@@ -402,6 +399,21 @@ evalCodomain scope x (VClosure env c t) = do
   return (eval g ((x,VGen (length scope) []):env) c t [])
 evalCodomain scope x t = return t
 
+tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint)
+tcUnifying scope c ts mb_ty = do
+  (ty,subsume) <-
+    case mb_ty of
+      Just ty -> do return (ty, \t ty' -> return t)
+      Nothing -> do i <- newResiduation scope
+                    let ty = VMeta i []
+                    return (ty, \t ty' -> subsCheckRho scope t ty' ty)
+
+  let go c t = do (t, ty) <- tcRho scope c t mb_ty
+                  subsume t ty
+
+  ts <- mapCM go c ts
+  return (ts,ty)
+
 tcCases scope c []         p_ty res_ty = return []
 tcCases scope c ((p,t):cs) p_ty res_ty = do
   let (c1,c2,c3,c4) = split4 c
@@ -690,9 +702,9 @@ subsCheckRho scope t (VTable p1 r1) rho2 = do                 -- Rule TABLE
   subsCheckTbl scope t p1 r1 p2 r2
 subsCheckRho scope t (VSort s1) (VSort s2)                    -- Rule PTYPE
   | s1 == cPType && s2 == cType = return t
-subsCheckRho scope t (VApp p1 _) (VApp p2 _)                  -- Rule INT1
+subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _)              -- Rule INT1
   | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t
-subsCheckRho scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])        -- Rule INT2
+subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2
   | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do
       if i <= j
         then return t
@@ -736,10 +748,10 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
                           "there are no values for fields:" <+> hsep missing)
   rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]]
   return (mkWrap (R rs))
-subsCheckRho scope t tau1 (VFV c vs) = do
+subsCheckRho scope t tau1 (VFV c (VarFree vs)) = do
   tau2 <- variants c vs
   subsCheckRho scope t tau1 tau2
-subsCheckRho scope t (VFV c vs) tau2 = do
+subsCheckRho scope t (VFV c (VarFree vs)) tau2 = do
   tau1 <- variants c vs
   subsCheckRho scope t tau1 tau2
 subsCheckRho scope t tau1 tau2 = do                           -- Rule EQ
@@ -751,13 +763,13 @@ subsCheckFun scope t a1 r1 a2 r2 = do
   let v   = newVar scope
   vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1
   g  <- globals
-  let r1 = case r1 of
-             VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
-             r1                -> r1
-  let r2 = case r2 of
-             VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
-             r2                -> r2
-  t  <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1 r2
+  let r1' = case r1 of
+              VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
+              r1                -> r1
+      r2' = case r2 of
+              VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
+              r2                -> r2
+  t  <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2'
   return (Abs Explicit v t)
 
 subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho  -> EvalM Term
@@ -768,10 +780,10 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
   p2 <- value2termM True (scopeVars scope) p2
   return (T (TTyped p2) [(PV x,t)])
 
-subtype scope Nothing (VApp p [VInt i])
+subtype scope Nothing (VApp c p [VInt i])
   | p == (cPredef,cInts) = do
       return (VCInts Nothing (Just i))
-subtype scope (Just (VCInts i j)) (VApp p [VInt k])
+subtype scope (Just (VCInts i j)) (VApp c p [VInt k])
   | p == (cPredef,cInts) = do
       return (VCInts j (Just (maybe k (min k) i)))
 subtype scope Nothing (VRecType ltys) = do
@@ -793,10 +805,10 @@ subtype scope (Just ctr) ty = do
   unify scope ctr ty
   return ty
 
-supertype scope Nothing (VApp p [VInt i])
+supertype scope Nothing (VApp c p [VInt i])
   | p == (cPredef,cInts) = do
       return (VCInts (Just i) Nothing)
-supertype scope (Just (VCInts i j)) (VApp p [VInt k])
+supertype scope (Just (VCInts i j)) (VApp c p [VInt k])
   | p == (cPredef,cInts) = do
       return (VCInts (Just (maybe k (max k) i)) j)
 supertype scope Nothing (VRecType ltys) = do
@@ -823,9 +835,14 @@ supertype scope (Just ctr) ty = do
 unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho)
 unifyFun scope (VProd bt x arg res) =
   return (bt,x,arg,res)
-unifyFun scope (VFV c vs) = do
+unifyFun scope (VFV c (VarFree vs)) = do
   res <- mapM (unifyFun scope) vs
-  return (Explicit, identW, VFV c [sigma | (_,_,sigma,rho) <- res], VFV c [rho | (_,_,sigma,rho) <- res])
+  return
+    ( Explicit
+    , identW
+    , VFV c (VarFree [sigma | (_,_,sigma,rho) <- res])
+    , VFV c (VarFree [rho | (_,_,sigma,rho) <- res])
+    )
 unifyFun scope tau = do
   let mk_val i = VMeta i []
   arg <- fmap mk_val $ newResiduation scope
@@ -844,7 +861,7 @@ unifyTbl scope tau = do
   unify scope tau (VTable arg res)
   return (arg,res)
 
-unify scope (VApp f1 vs1) (VApp f2 vs2)
+unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2)
   | f1 == f2  = sequence_ (zipWith (unify scope) vs1 vs2)
 unify scope (VMeta i vs1) (VMeta j vs2)
   | i  == j   = sequence_ (zipWith (unify scope) vs1 vs2)
@@ -910,7 +927,7 @@ occursCheck scope' i0 scope v =
       n = length scope
   in check m n v
   where
-    check m n (VApp f vs) = mapM_ (check m n) vs
+    check m n (VApp c f vs) = mapM_ (check m n) vs
     check m n (VMeta i vs)
       | i0 == i  = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs)
                       ty2 <- value2termM False (scopeVars scope) v
@@ -964,7 +981,7 @@ occursCheck scope' i0 scope v =
     check m n (VPattType v) =
       check m n v
     check m n (VFV c vs) =
-      mapM_ (check m n) vs
+      mapM_ (check m n) (unvariants vs)
     check m n (VAlts v vs) =
       check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs
     check m n (VStrs vs) =
@@ -1019,9 +1036,9 @@ quantify scope t tvs ty = do
   where
     bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i []))
 
-    check m n xs (VApp f vs)       = do
+    check m n xs (VApp c f vs)     = do
       (xs,vs) <- mapAccumM (check m n) xs vs
-      return (xs,VApp f vs)
+      return (xs,VApp c f vs)
     check m n xs (VMeta i vs)      = do
       s <- getMeta i
       case s of
@@ -1090,9 +1107,12 @@ quantify scope t tvs ty = do
     check m n xs (VPattType v)     = do
       (xs,v) <- check m n xs v
       return (xs,VPattType v)
-    check m n xs (VFV c vs)       = do
+    check m n xs (VFV c (VarFree vs)) = do
       (xs,vs) <- mapAccumM (check m n) xs vs
-      return (xs,VFV c vs)
+      return (xs,VFV c (VarFree vs))
+    check m n xs (VFV c (VarOpts name os)) = do
+      (xs,os) <- mapAccumM (\acc (l,v) -> second (l,) <$> check m n acc v) xs os
+      return (xs,VFV c (VarOpts name os))
     check m n xs (VAlts v vs)      = do
       (xs,v)  <- check m n xs v
       (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1
@@ -1159,8 +1179,8 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
                                     Residuation _ Nothing  -> foldM go (m:acc) args
                                     Residuation _ (Just v) -> go acc v
                                     _                      -> return acc
-    go acc (VApp f args)     = foldM go acc args
-    go acc (VFV c vs)        = foldM go acc vs
+    go acc (VApp c f args)   = foldM go acc args
+    go acc (VFV c vs)        = foldM go acc (unvariants vs)
     go acc (VCRecType vs)    = foldM (\acc (lbl,b,v) -> go acc v) acc vs
     go acc (VCInts _ _)      = return acc
     go acc v                 = unimplemented ("go "++show (ppValue Unqualified 5 v))
diff --git a/src/compiler/api/GF/Data/Utilities.hs b/src/compiler/api/GF/Data/Utilities.hs
index c83070137..f8d76dd28 100644
--- a/src/compiler/api/GF/Data/Utilities.hs
+++ b/src/compiler/api/GF/Data/Utilities.hs
@@ -32,6 +32,11 @@ notLongerThan, longerThan :: Int -> [a] -> Bool
 notLongerThan n = null . snd . splitAt n
 longerThan    n = not . notLongerThan n
 
+maybeAt :: [a] -> Int -> Maybe a
+maybeAt xs i
+    | i >= 0 && i < length xs = Just (xs !! i)
+    | otherwise               = Nothing
+
 lookupList :: Eq a => a -> [(a, b)] -> [b]
 lookupList a [] = []
 lookupList a (p:ps) | a == fst p = snd p : lookupList a ps
@@ -171,6 +176,11 @@ anyM p = foldM (\b x -> if b then return True else p x) False
 
 -- * functions on Maybes
 
+-- | Returns the argument on the right, or a default value on the left.
+orLeft :: a -> Maybe b -> Either a b
+orLeft a (Just b) = Right b
+orLeft a Nothing  = Left a
+
 -- | Returns true if the argument is Nothing or Just []
 nothingOrNull :: Maybe [a] -> Bool
 nothingOrNull = maybe True null
diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs
index a16b59869..d2a7c6487 100644
--- a/src/compiler/api/GF/Grammar/Grammar.hs
+++ b/src/compiler/api/GF/Grammar/Grammar.hs
@@ -54,6 +54,7 @@ module GF.Grammar.Grammar (
         Equation,
         Labelling,
         Assign,
+        Option,
         Case,
         LocalDef,
         Param,
@@ -372,7 +373,9 @@ data Term =
  | R [Assign]                    -- ^ record:      @{ p = a ; ...}@
  | P Term Label                  -- ^ projection:  @r.p@
  | ExtR Term Term                -- ^ extension:   @R ** {x : A}@ (both types and terms)
- 
+
+ | Opts Term [Option]            -- ^ options:     @options s in { e => x ; ... }@
+
  | Table Term Term               -- ^ table type:  @P => A@
  | T TInfo [Case]                -- ^ table:       @table {p => c ; ...}@
  | V Type [Term]                 -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
@@ -471,6 +474,7 @@ type Equation = ([Patt],Term)
 
 type Labelling = (Label, Type) 
 type Assign = (Label, (Maybe Type, Term)) 
+type Option = (Term, Term)
 type Case = (Patt, Term) 
 --type Cases = ([Patt], Term) 
 type LocalDef = (Ident, (Maybe Type, Term))
diff --git a/src/compiler/api/GF/Grammar/Lexer.x b/src/compiler/api/GF/Grammar/Lexer.x
index d3f649002..1130aa0f1 100644
--- a/src/compiler/api/GF/Grammar/Lexer.x
+++ b/src/compiler/api/GF/Grammar/Lexer.x
@@ -41,7 +41,7 @@ $u = [.\n]                -- universal: any character
 "{-" ([$u # \-] | \- [$u # \}])* ("-")+ "}" ;
 
 $white+ ;
-@rsyms                          { tok ident }
+@rsyms                          { \lang -> tok (ident lang) lang }
 \< $white* @ident $white* (\/ | \>)
                                 { \lang inp@(AI pos s) inp' _ -> 
                                      let inp0 = AI (alexMove pos '<') (BS.tail s)
@@ -74,7 +74,7 @@ $white+ ;
                                               in POk (inp,inp0) T_less
                                      } }
 \' ([. # [\' \\ \n]] | (\\ (\' | \\)))+ \' { tok (T_Ident . identS . unescapeInitTail . unpack) }
-@ident   { tok ident }
+@ident   { \lang -> tok (ident lang) lang }
 
 \" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | $d+)))* \" { tok (T_String . unescapeInitTail . unpack) }
 
@@ -85,7 +85,7 @@ $white+ ;
 {
 unpack = UTF8.toString
 
-ident = res T_Ident . identC . rawIdentC
+ident lang = res lang T_Ident . identC . rawIdentC
 
 tok f _ inp@(AI _ s) inp' len = POk (inp,inp') (f (UTF8.take len s))
 
@@ -149,6 +149,7 @@ data Token
  | T_of
  | T_open
  | T_oper
+ | T_option
  | T_param
  | T_pattern
  | T_pre
@@ -174,16 +175,20 @@ data Token
  deriving Show -- debug
 
 res = eitherResIdent
-eitherResIdent :: (Ident -> Token) -> Ident -> Token
-eitherResIdent tv s =
-  case Map.lookup s resWords of
+eitherResIdent :: Lang -> (Ident -> Token) -> Ident -> Token
+eitherResIdent lang tv s =
+  case Map.lookup s (resWords lang) of
     Just t  -> t
     Nothing -> tv s
 
-isReservedWord :: Ident -> Bool
-isReservedWord ident = Map.member ident resWords
+isReservedWord :: Lang -> Ident -> Bool
+isReservedWord lang ident = Map.member ident (resWords lang)
 
-resWords = Map.fromList
+resWords :: Lang -> Map.Map Ident Token
+resWords NLG = nlgResWords
+resWords _   = coreResWords
+
+coreResWords = Map.fromList
  [ b "!"  T_exclmark
  , b "#"  T_patt
  , b "$"  T_int_label
@@ -255,13 +260,17 @@ resWords = Map.fromList
  , b "variants"   T_variants
  , b "where"      T_where
  , b "with"       T_with
- , b "coercions"  T_coercions
+ , b "coercions"  T_coercions -- FIXME ..
  , b "terminator" T_terminator
  , b "separator"  T_separator
  , b "nonempty"   T_nonempty
  ]
  where b s t = (identS s, t)
 
+-- bnfcResWords = _
+
+nlgResWords = Map.insert (identS "option") T_option coreResWords
+
 unescapeInitTail :: String -> String
 unescapeInitTail = unesc . tail where
   unesc s = case s of
diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y
index f9aa59a31..54b1fb755 100644
--- a/src/compiler/api/GF/Grammar/Parser.y
+++ b/src/compiler/api/GF/Grammar/Parser.y
@@ -101,6 +101,7 @@ import qualified Data.Map as Map
  'of'         { T_of        }
  'open'       { T_open      }
  'oper'       { T_oper      }
+ 'option'     { T_option    }
  'param'      { T_param     }
  'pattern'    { T_pattern   }
  'pre'        { T_pre       }
@@ -452,6 +453,7 @@ Exp4 :: { Term }
 Exp4
   : Exp4 Exp5                        { App $1 $2 }
   | Exp4 '{' Exp '}'                 { App $1 (ImplArg $3) } 
+  | 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
   | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
                                              Typed _ t -> TTyped t
                                              _         -> TRaw
@@ -608,6 +610,15 @@ ListPattTupleComp
   | Patt                       { [$1]    }
   | Patt ',' ListPattTupleComp { $1 : $3 }
 
+Opt :: { Option }
+Opt
+  : '(' Exp ')' '=>' Exp { ($2,$5) }
+
+ListOpt :: { [Option] }
+ListOpt
+  : Opt             { [$1]    }
+  | Opt ';' ListOpt { $1 : $3 }
+
 Case :: { Case }
 Case
   : Patt '=>' Exp { ($1,$3) }