@@ -64,6 +64,7 @@ data Value
6464 | VAlts Value [(Value , Value )]
6565 | VStrs [Value ]
6666 | VMarkup Ident [(Ident ,Value )] [Value ]
67+ | VReset Control Value
6768 | VSymCat Int LIndex [(LIndex , (Value , Type ))]
6869 | VError Doc
6970 -- These two constructors are only used internally
@@ -254,10 +255,7 @@ eval g env c (Markup tag as ts) [] =
254255 vas = mapC (\ c (id ,t) -> (id ,eval g env c t [] )) c1 as
255256 vs = mapC (\ c t -> eval g env c t [] ) c2 ts
256257 in (VMarkup tag vas vs)
257- eval g env c (Reset ctl t) [] =
258- let limit All = id
259- limit (Limit n) = fmap (genericTake n)
260- in (VMarkup identW [] [eval g env c t [] ])
258+ eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [] )
261259eval g env c (TSymCat d r rs) [] = VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
262260eval g env c t vs = VError (" Cannot reduce term" <+> pp t)
263261
@@ -325,6 +323,7 @@ bubble v = snd (bubble v)
325323 let (union1,attrs') = mapAccumL descend' Map. empty attrs
326324 (union2,vs') = mapAccumL descend union1 vs
327325 in (union2, VMarkup tag attrs' vs')
326+ bubble (VReset ctl v) = lift1 (VReset ctl) v
328327 bubble (VSymCat d i0 vs) =
329328 let (union,vs') = mapAccumL descendC Map. empty vs
330329 in (union, addVariants (VSymCat d i0 vs') union)
@@ -610,6 +609,14 @@ runEvalM g (EvalM f) = Check $ \(es,ws) ->
610609 where
611610 empty = State Map. empty Map. empty
612611
612+ reset :: EvalM a -> EvalM [a ]
613+ reset (EvalM f) = EvalM $ \ g k state r ws ->
614+ case f g (\ x state xs ws -> Success (x: xs) ws) state [] ws of
615+ Fail msg ws -> Fail msg ws
616+ Success xs ws -> k (reverse xs) state r ws
617+ where
618+ empty = State Map. empty Map. empty
619+
613620globals :: EvalM Globals
614621globals = EvalM (\ g k -> k g)
615622
@@ -784,6 +791,29 @@ value2termM flat xs (VMarkup tag as vs) = do
784791 as <- mapM (\ (id ,v) -> value2termM flat xs v >>= \ t -> return (id ,t)) as
785792 ts <- mapM (value2termM flat xs) vs
786793 return (Markup tag as ts)
794+ value2termM flat xs (VReset ctl v) = do
795+ ts <- reset (value2termM True xs v)
796+ case ctl of
797+ All -> case ts of
798+ [t] -> return t
799+ ts -> return (Markup identW [] ts)
800+ One -> case ts of
801+ [] -> mzero
802+ (t: ts) -> return t
803+ Limit n -> case genericTake n ts of
804+ [t] -> return t
805+ ts -> return (Markup identW [] ts)
806+ Coordination (Just mn) conj id ->
807+ case ts of
808+ [] -> mzero
809+ [t] -> return t
810+ ts -> do let cat = showIdent id
811+ t <- listify mn cat ts
812+ return (App (App (QC (mn,identS (" Conj" ++ cat))) (QC (mn,conj))) t)
813+ where
814+ listify mn cat [t1,t2] = do return (App (App (QC (mn,identS (" Base" ++ cat))) t1) t2)
815+ listify mn cat (t1: ts) = do t2 <- listify mn id ts
816+ return (App (App (QC (mn,identS (" Cons" ++ cat))) t1) t2)
787817value2termM flat xs (VError msg) = evalError msg
788818value2termM flat xs (VCRecType lbls) = do
789819 lbls <- mapM (\ (lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
0 commit comments