@@ -27,6 +27,7 @@ import qualified Data.Map as Map
2727import Data.Maybe (fromMaybe ,fromJust )
2828import Data.List
2929import Data.Char
30+ import Debug.Trace
3031
3132type Env = [(Ident ,Value )]
3233type Scope = [(Ident ,Value )]
@@ -37,8 +38,8 @@ data Globals = Gl Grammar PredefTable
3738
3839data Value
3940 = VApp QIdent [Value ]
40- | VMeta MetaId [Value ]
41- | VSusp MetaId (Value -> Value ) [Value ]
41+ | VMeta {- # UNPACK # -} ! MetaId [Value ]
42+ | VSusp {- # UNPACK # -} ! MetaId (Value -> Value ) [Value ]
4243 | VGen {- # UNPACK #-} !Int [Value ]
4344 | VClosure Env Choice Term
4445 | VProd BindType Ident Value Value
@@ -97,10 +98,10 @@ instance Applicative ConstValue where
9798 _ <*> RunTime = RunTime
9899
99100normalForm :: Globals -> Term -> Check Term
100- normalForm g t = value2term g [] (eval g [] unit t [] )
101+ normalForm g t = value2term g [] (bubble ( eval g [] unit t [] ) )
101102
102103normalFlatForm :: Globals -> Term -> Check [Term ]
103- normalFlatForm g t = runEvalM g (value2termM False [] (eval g [] unit t [] ))
104+ normalFlatForm g t = runEvalM g (value2termM True [] (eval g [] unit t [] ))
104105
105106eval :: Globals -> Env -> Choice -> Term -> [Value ] -> Value
106107eval g env s (Vr x) vs = case lookup x env of
@@ -280,6 +281,119 @@ apply g (VFV i fvs) vs = VFV i [apply g v vs | v <- fvs]
280281apply g (VClosure env s (Abs b x t)) (v: vs) = eval g ((x,v): env) s t vs
281282apply g v [] = v
282283
284+ bubble v = snd (bubble v)
285+ where
286+ bubble (VApp f vs) = liftL (VApp f) vs
287+ bubble (VMeta metaid vs) = liftL (VMeta metaid) vs
288+ bubble (VSusp metaid k vs) = liftL (VSusp metaid k) vs
289+ bubble (VGen i vs) = liftL (VGen i) vs
290+ bubble (VClosure env c t) = liftL' (\ env -> VClosure env c t) env
291+ bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2
292+ bubble (VRecType as) = liftL' VRecType as
293+ bubble (VR as) = liftL' VR as
294+ bubble (VP v l vs) = lift1L (\ v vs -> VP v l vs) v vs
295+ bubble (VExtR v1 v2) = lift2 VExtR v1 v2
296+ bubble (VTable v1 v2) = lift2 VTable v1 v2
297+ bubble (VT v env c cs) = lift1L' (\ v env -> VT v env c cs) v env
298+ bubble (VV v vs) = lift1L VV v vs
299+ bubble (VS v1 v2 vs) = lift2L VS v1 v2 vs
300+ bubble v@ (VSort _) = lift0 v
301+ bubble v@ (VInt _) = lift0 v
302+ bubble v@ (VFlt _) = lift0 v
303+ bubble v@ (VStr _) = lift0 v
304+ bubble v@ VEmpty = lift0 v
305+ bubble (VC v1 v2) = lift2 VC v1 v2
306+ bubble (VGlue v1 v2) = lift2 VGlue v1 v2
307+ bubble v@ (VPatt _ _ _) = lift0 v
308+ bubble (VPattType v) = lift1 VPattType v
309+ bubble (VFV c vs) =
310+ let (union,vs') = mapAccumL descend Map. empty vs
311+ in (Map. insert c (length vs,1 ) union, addVariants (VFV c vs') union)
312+ bubble (VAlts v vs) = lift1L2 VAlts v vs
313+ bubble (VStrs vs) = liftL VStrs vs
314+ bubble (VSymCat d i0 vs) =
315+ let (union,vs') = mapAccumL descendC Map. empty vs
316+ in (union, addVariants (VSymCat d i0 vs') union)
317+ bubble v@ (VError _) = lift0 v
318+ bubble v@ (VCRecType lbls) =
319+ let (union,lbls') = mapAccumL descendR Map. empty lbls
320+ in (union, addVariants (VCRecType lbls') union)
321+ bubble v@ (VCInts _ _) = lift0 v
322+
323+ lift0 v = (Map. empty, v)
324+
325+ lift1 f v =
326+ let (union,v') = bubble v
327+ in (union,f v')
328+
329+ liftL f vs =
330+ let (union,vs') = mapAccumL descend Map. empty vs
331+ in (union, addVariants (f vs') union)
332+
333+ liftL' f vs =
334+ let (union,vs') = mapAccumL descend' Map. empty vs
335+ in (union, addVariants (f vs') union)
336+
337+ lift1L f v vs =
338+ let (choices,v') = bubble v
339+ (union, vs') = mapAccumL descend (unitfy choices) vs
340+ in (union, addVariants (f v' vs') union)
341+
342+ lift1L' f v vs =
343+ let (choices,v') = bubble v
344+ (union, vs') = mapAccumL descend' (unitfy choices) vs
345+ in (union, addVariants (f v' vs') union)
346+
347+ lift1L2 f v vs =
348+ let (choices,v') = bubble v
349+ (union, vs') = mapAccumL descend2 (unitfy choices) vs
350+ in (union, addVariants (f v' vs') union)
351+
352+ lift2L f v1 v2 vs =
353+ let (choices1,v1') = bubble v1
354+ (choices2,v2') = bubble v2
355+ union = mergeChoices2 choices1 choices2
356+ (union', vs') = mapAccumL descend union vs
357+ in (union', addVariants (f v1' v2' vs') union')
358+
359+ lift2 f v1 v2 =
360+ let (choices1,v1') = bubble v1
361+ (choices2,v2') = bubble v2
362+ union = mergeChoices2 choices1 choices2
363+ in (union, addVariants (f v1' v2') union)
364+
365+ descend union v =
366+ let (choices,v') = bubble v
367+ in (mergeChoices1 union choices,v')
368+
369+ descend' :: Map. Map Choice (Int ,Int ) -> (a ,Value ) -> (Map. Map Choice (Int ,Int ),(a ,Value ))
370+ descend' union (x,v) =
371+ let (choices,v') = bubble v
372+ in (mergeChoices1 union choices,(x,v'))
373+
374+ descend2 union (v1,v2) =
375+ let (choices1,v1') = bubble v1
376+ (choices2,v2') = bubble v2
377+ in (mergeChoices1 (mergeChoices1 union choices1) choices2,(v1',v2'))
378+
379+ descendC union (i,(v,ty)) =
380+ let (choices,v') = bubble v
381+ in (mergeChoices1 union choices,(i,(v',ty)))
382+
383+ descendR union (l,b,v) =
384+ let (choices,v') = bubble v
385+ in (mergeChoices1 union choices,(l,b,v'))
386+
387+ addVariants v = Map. foldrWithKey addVariant v
388+ where
389+ addVariant c (n,cnt) v
390+ | cnt > 1 = VFV c (replicate n v)
391+ | otherwise = v
392+
393+ unitfy = fmap (\ (n,_) -> (n,1 ))
394+ mergeChoices1 = Map. mergeWithKey (\ c (n,cnt) _ -> Just (n,cnt+ 1 )) id unitfy
395+ mergeChoices2 = Map. mergeWithKey (\ c (n,cnt) _ -> Just (n,2 )) unitfy unitfy
396+
283397toPBool True = VApp (cPredef,cPTrue) []
284398toPBool False = VApp (cPredef,cPFalse) []
285399
@@ -497,6 +611,22 @@ variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
497611 Fail msg msgs -> Fail msg msgs
498612 Success r msgs -> backtrack (j+ 1 ) xs k choices metas r msgs
499613
614+ variants' :: Choice -> (a -> EvalM Term ) -> [a ] -> EvalM Term
615+ variants' c f xs = EvalM (\ g k state@ (State choices metas) r msgs ->
616+ case Map. lookup c choices of
617+ Just j -> case f (xs !! j) of
618+ EvalM f -> f g k state r msgs
619+ Nothing -> case backtrack g 0 xs choices metas [] msgs of
620+ Fail msg msgs -> Fail msg msgs
621+ Success ts msgs -> k (FV (reverse ts)) state r msgs)
622+ where
623+ backtrack g j [] choices metas ts msgs = Success ts msgs
624+ backtrack g j (x: xs) choices metas ts msgs =
625+ case f x of
626+ EvalM f -> case f g (\ t st ts msgs -> Success (t: ts) msgs) (State (Map. insert c j choices) metas) ts msgs of
627+ Fail msg msgs -> Fail msg msgs
628+ Success ts msgs -> backtrack g (j+ 1 ) xs choices metas ts msgs
629+
500630try :: (a -> EvalM b ) -> [a ] -> Message -> EvalM b
501631try f xs msg = EvalM (\ g k state r msgs ->
502632 let (res,msgs') = backtrack g xs state [] msgs
@@ -618,9 +748,11 @@ value2termM flat xs (VGlue v1 v2) = do
618748 t1 <- value2termM flat xs v1
619749 t2 <- value2termM flat xs v2
620750 return (Glue t1 t2)
621- value2termM flat xs (VFV i vs) = do
622- v <- variants i vs
623- value2termM flat xs v
751+ value2termM flat xs (VFV i vs) =
752+ case flat of
753+ True -> do v <- variants i vs
754+ value2termM True xs v
755+ False -> variants' i (value2termM False xs) vs
624756value2termM flat xs (VPatt min max p) = return (EPatt min max p)
625757value2termM flat xs (VPattType v) = do t <- value2termM flat xs v
626758 return (EPattType t)
@@ -766,7 +898,7 @@ value2int g (VInt n) = Const n
766898value2int g (VFV s vs) = CFV s (map (value2int g) vs)
767899value2int g _ = RunTime
768900
769- newtype Choice = Choice Integer deriving (Eq ,Ord ,Pretty )
901+ newtype Choice = Choice Integer deriving (Eq ,Ord ,Pretty , Show )
770902
771903unit :: Choice
772904unit = Choice 1
0 commit comments