semantics of variants

This commit is contained in:
aarne
2007-01-10 21:03:18 +00:00
parent 61e932e797
commit 9b1fb0c1c0
3 changed files with 31 additions and 13 deletions

View File

@@ -125,8 +125,22 @@ allParamValues cnc ptyp = case ptyp of
-- runtime computation on GFC objects
ccompute :: CanonGrammar -> [Term] -> Term -> Err Term
ccompute cnc = comp []
ccompute cnc = vcomp
where
vcomp xs t = do
let xss = variations xs
ts <- mapM (\xx -> comp [] xx t) xss
return $ variants ts
variations xs = combinations [getVariants t | t <- xs]
variants ts = case ts of
[t] -> t
_ -> FV ts
getVariants t = case t of
FV ts -> ts
_ -> [t]
comp g xs t = case t of
Arg (A _ i) -> err (const (return t)) return $ xs !? fromInteger i
Arg (AB _ _ i) -> err (const (return t)) return $ xs !? fromInteger i

View File

@@ -154,8 +154,8 @@ partEval opts gr (context, val) trm = errIn ("parteval" +++ prt_ trm) $ do
subst = [(v, Vr v) | v <- vars]
trm1 = mkApp trm args
trm3 <- if globalTable
then etaExpand trm1 >>= comp subst >>= outCase subst
else etaExpand trm1 >>= comp subst
then etaExpand subst trm1 >>= outCase subst
else etaExpand subst trm1
return $ mkAbs vars trm3
where
@@ -164,7 +164,7 @@ partEval opts gr (context, val) trm = errIn ("parteval" +++ prt_ trm) $ do
comp g t = {- refreshTerm t >>= -} computeTerm gr g t
etaExpand t = recordExpand val t --- >>= caseEx -- done by comp
etaExpand su t = comp su t >>= recordExpand val >>= comp su
outCase subst t = do
pts <- getParams context

View File

@@ -80,10 +80,12 @@ computeTermOpt rec gr = comp where
f' <- comp g f
a' <- comp g a
case (f',a') of
(Abs x b, FV as) ->
mapM (\c -> comp (ext x c g) b) as >>= return . variants
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
(Abs x b,_) -> comp (ext x a' g) b
(QC _ _,_) -> returnC $ App f' a'
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
(Alias _ _ d, _) -> comp g (App d a')
@@ -140,13 +142,14 @@ computeTermOpt rec gr = comp where
t' <- comp g t
v' <- comp g v
case t' of
FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
T _ [(PV IW,c)] -> comp g c --- an optimization
T _ [(PT _ (PV IW),c)] -> comp g c
T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
V ptyp ts -> do
vs <- allParamValues gr ptyp
@@ -180,6 +183,13 @@ computeTermOpt rec gr = comp where
x <- comp g x0
y <- comp g y0
case (x,y) of
(FV ks,_) -> do
kys <- mapM (comp g . flip Glue y) ks
return $ variants kys
(_,FV ks) -> do
xks <- mapM (comp g . Glue x) ks
return $ variants xks
(Alias _ _ d, y) -> comp g $ Glue d y
(x, Alias _ _ d) -> comp g $ Glue x d
@@ -201,12 +211,6 @@ computeTermOpt rec gr = comp where
---- foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
,return $ Glue x y
]
(FV ks,_) -> do
kys <- mapM (comp g . flip Glue y) ks
return $ variants kys
(_,FV ks) -> do
xks <- mapM (comp g . Glue x) ks
return $ variants xks
_ -> do
mapM_ checkNoArgVars [x,y]