summaryrefslogtreecommitdiff
path: root/src/compiler/GF/Compile/Compute
diff options
context:
space:
mode:
Diffstat (limited to 'src/compiler/GF/Compile/Compute')
-rw-r--r--src/compiler/GF/Compile/Compute/Abstract.hs138
-rw-r--r--src/compiler/GF/Compile/Compute/AppPredefined.hs157
-rw-r--r--src/compiler/GF/Compile/Compute/Concrete.hs461
3 files changed, 756 insertions, 0 deletions
diff --git a/src/compiler/GF/Compile/Compute/Abstract.hs b/src/compiler/GF/Compile/Compute/Abstract.hs
new file mode 100644
index 000000000..ef7974314
--- /dev/null
+++ b/src/compiler/GF/Compile/Compute/Abstract.hs
@@ -0,0 +1,138 @@
+----------------------------------------------------------------------
+-- |
+-- Module : GF.Compile.Abstract.Compute
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
+--
+-- computation in abstract syntax w.r.t. explicit definitions.
+--
+-- old GF computation; to be updated
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.Abstract (LookDef,
+ compute,
+ computeAbsTerm,
+ computeAbsTermIn,
+ beta
+ ) where
+
+import GF.Data.Operations
+
+import GF.Grammar
+import GF.Grammar.Lookup
+
+import Debug.Trace
+import Data.List(intersperse)
+import Control.Monad (liftM, liftM2)
+import Text.PrettyPrint
+
+-- for debugging
+tracd m t = t
+-- tracd = trace
+
+compute :: SourceGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: SourceGrammar -> Exp -> Err Exp
+computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
+
+-- | a hack to make compute work on source grammar as well
+type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where
+ compt vv t = case t of
+-- Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
+-- Abs x b -> liftM (Abs x) (compt (x:vv) b)
+ _ -> do
+ let t' = beta vv t
+ (yy,f,aa) <- termForm t'
+ let vv' = map snd yy ++ vv
+ aa' <- mapM (compt vv') aa
+ case look f of
+ Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $
+ case findMatch eqs aa' of
+ Ok (d,g) -> do
+ --- let (xs,ts) = unzip g
+ --- ts' <- alphaFreshAll vv' ts
+ let g' = g --- zip xs ts'
+ d' <- compt vv' $ substTerm vv' g' d
+ tracd (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
+ _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $
+ do
+ let v = mkApp f aa'
+ return $ mkAbs yy $ v
+ _ -> do
+ let t2 = mkAbs yy $ mkApp f aa'
+ tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
+
+ look t = case t of
+ (Q (m,f)) -> case lookd m f of
+ Ok (_,md) -> md
+ _ -> Nothing
+ _ -> Nothing
+
+beta :: [Ident] -> Exp -> Exp
+beta vv c = case c of
+ Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b)
+ App f a ->
+ let (a',f') = (beta vv a, beta vv f) in
+ case f' of
+ Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
+ _ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
+ Prod b x a t -> Prod b x (beta vv a) (beta (x:vv) t)
+ Abs b x t -> Abs b x (beta (x:vv) t)
+ _ -> c
+
+-- special version of pattern matching, to deal with comp under lambda
+
+findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
+findMatch cases terms = case cases of
+ [] -> Bad $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
+ (patts,_):_ | length patts /= length terms ->
+ Bad (render (text "wrong number of args for patterns :" <+>
+ hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
+ (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+ Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 val) val, concat substs)
+ _ -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do
+ t' <- termForm t
+ trym p t'
+ where
+
+ trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ----
+ case (p,t') of
+ (PW, _) | notMeta t -> return [] -- optimization with wildcard
+ (PV x, _) | notMeta t -> return [(x,t)]
+ (PString s, ([],K i,[])) | s==i -> return []
+ (PInt s, ([],EInt i,[])) | s==i -> return []
+ (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
+ (PP (q,p) pp, ([], QC (r,f), tt)) |
+ p `eqStrIdent` f && length pp == length tt -> do
+ matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ (PP (q,p) pp, ([], Q (r,f), tt)) |
+ p `eqStrIdent` f && length pp == length tt -> do
+ matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ (PT _ p',_) -> trym p' t'
+ (PAs x p',_) -> do
+ subst <- trym p' t'
+ return $ (x,t) : subst
+ _ -> Bad (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
+
+ notMeta e = case e of
+ Meta _ -> False
+ App f a -> notMeta f && notMeta a
+ Abs _ _ b -> notMeta b
+ _ -> True
+
+ prtm p g =
+ ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])
diff --git a/src/compiler/GF/Compile/Compute/AppPredefined.hs b/src/compiler/GF/Compile/Compute/AppPredefined.hs
new file mode 100644
index 000000000..94dc67022
--- /dev/null
+++ b/src/compiler/GF/Compile/Compute/AppPredefined.hs
@@ -0,0 +1,157 @@
+----------------------------------------------------------------------
+-- |
+-- Module : AppPredefined
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/06 14:21:34 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.13 $
+--
+-- Predefined function type signatures and definitions.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.AppPredefined (isInPredefined, typPredefined, appPredefined
+ ) where
+
+import GF.Infra.Ident
+import GF.Data.Operations
+import GF.Grammar.Predef
+import GF.Grammar.Grammar
+import GF.Grammar.Macros
+import GF.Grammar.Printer
+import qualified Data.ByteString.Char8 as BS
+import Text.PrettyPrint
+
+-- predefined function type signatures and definitions. AR 12/3/2003.
+
+isInPredefined :: Ident -> Bool
+isInPredefined = err (const True) (const False) . typPredefined
+
+typPredefined :: Ident -> Err Type
+typPredefined f
+ | f == cInt = return typePType
+ | f == cFloat = return typePType
+ | f == cErrorType = return typeType
+ | f == cInts = return $ mkFunType [typeInt] typePType
+ | f == cPBool = return typePType
+ | f == cError = return $ mkFunType [typeStr] typeError -- non-can. of empty set
+ | f == cPFalse = return $ typePBool
+ | f == cPTrue = return $ typePBool
+ | f == cDp = return $ mkFunType [typeInt,typeTok] typeTok
+ | f == cDrop = return $ mkFunType [typeInt,typeTok] typeTok
+ | f == cEqInt = return $ mkFunType [typeInt,typeInt] typePBool
+ | f == cLessInt = return $ mkFunType [typeInt,typeInt] typePBool
+ | f == cEqStr = return $ mkFunType [typeTok,typeTok] typePBool
+ | f == cLength = return $ mkFunType [typeTok] typeInt
+ | f == cOccur = return $ mkFunType [typeTok,typeTok] typePBool
+ | f == cOccurs = return $ mkFunType [typeTok,typeTok] typePBool
+ | f == cPlus = return $ mkFunType [typeInt,typeInt] (typeInt)
+---- "read" -> (P : Type) -> Tok -> P
+ | f == cShow = return $ mkProd -- (P : PType) -> P -> Tok
+ [(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
+ | f == cToStr = return $ mkProd -- (L : Type) -> L -> Str
+ [(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
+ | f == cMapStr = return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L
+ [(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
+ | f == cTake = return $ mkFunType [typeInt,typeTok] typeTok
+ | f == cTk = return $ mkFunType [typeInt,typeTok] typeTok
+ | otherwise = Bad (render (text "unknown in Predef:" <+> ppIdent f))
+
+varL :: Ident
+varL = identC (BS.pack "L")
+
+varP :: Ident
+varP = identC (BS.pack "P")
+
+appPredefined :: Term -> Err (Term,Bool)
+appPredefined t = case t of
+ App f x0 -> do
+ (x,_) <- appPredefined x0
+ case f of
+ -- one-place functions
+ Q (mod,f) | mod == cPredef ->
+ case x of
+ (K s) | f == cLength -> retb $ EInt $ length s
+ _ -> retb t
+
+ -- two-place functions
+ App (Q (mod,f)) z0 | mod == cPredef -> do
+ (z,_) <- appPredefined z0
+ case (norm z, norm x) of
+ (EInt i, K s) | f == cDrop -> retb $ K (drop i s)
+ (EInt i, K s) | f == cTake -> retb $ K (take i s)
+ (EInt i, K s) | f == cTk -> retb $ K (take (max 0 (length s - i)) s)
+ (EInt i, K s) | f == cDp -> retb $ K (drop (max 0 (length s - i)) s)
+ (K s, K t) | f == cEqStr -> retb $ if s == t then predefTrue else predefFalse
+ (K s, K t) | f == cOccur -> retb $ if substring s t then predefTrue else predefFalse
+ (K s, K t) | f == cOccurs -> retb $ if any (flip elem t) s then predefTrue else predefFalse
+ (EInt i, EInt j) | f == cEqInt -> retb $ if i==j then predefTrue else predefFalse
+ (EInt i, EInt j) | f == cLessInt -> retb $ if i<j then predefTrue else predefFalse
+ (EInt i, EInt j) | f == cPlus -> retb $ EInt $ i+j
+ (_, t) | f == cShow -> retb $ foldr C Empty $ map K $ words $ render (ppTerm Unqualified 0 t)
+ (_, K s) | f == cRead -> retb $ Cn (identC (BS.pack s)) --- because of K, only works for atomic tags
+ (_, t) | f == cToStr -> trm2str t >>= retb
+ _ -> retb t ---- prtBad "cannot compute predefined" t
+
+ -- three-place functions
+ App (App (Q (mod,f)) z0) y0 | mod == cPredef -> do
+ (y,_) <- appPredefined y0
+ (z,_) <- appPredefined z0
+ case (z, y, x) of
+ (ty,op,t) | f == cMapStr -> retf $ mapStr ty op t
+ _ -> retb t ---- prtBad "cannot compute predefined" t
+
+ _ -> retb t ---- prtBad "cannot compute predefined" t
+ _ -> retb t
+ ---- should really check the absence of arg variables
+ where
+ retb t = return (retc t,True) -- no further computing needed
+ retf t = return (retc t,False) -- must be computed further
+ retc t = case t of
+ K [] -> t
+ K s -> foldr1 C (map K (words s))
+ _ -> t
+ norm t = case t of
+ Empty -> K []
+ C u v -> case (norm u,norm v) of
+ (K x,K y) -> K (x +++ y)
+ _ -> t
+ _ -> t
+
+-- read makes variables into constants
+
+predefTrue = QC (cPredef,cPTrue)
+predefFalse = QC (cPredef,cPFalse)
+
+substring :: String -> String -> Bool
+substring s t = case (s,t) of
+ (c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds
+ ([],_) -> True
+ _ -> False
+
+trm2str :: Term -> Err Term
+trm2str t = case t of
+ R ((_,(_,s)):_) -> trm2str s
+ T _ ((_,s):_) -> trm2str s
+ V _ (s:_) -> trm2str s
+ C _ _ -> return $ t
+ K _ -> return $ t
+ S c _ -> trm2str c
+ Empty -> return $ t
+ _ -> Bad (render (text "cannot get Str from term" <+> ppTerm Unqualified 0 t))
+
+-- simultaneous recursion on type and term: type arg is essential!
+-- But simplify the task by assuming records are type-annotated
+-- (this has been done in type checking)
+mapStr :: Type -> Term -> Term -> Term
+mapStr ty f t = case (ty,t) of
+ _ | elem ty [typeStr,typeTok] -> App f t
+ (_, R ts) -> R [(l,mapField v) | (l,v) <- ts]
+ (Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs]
+ _ -> t
+ where
+ mapField (mty,te) = case mty of
+ Just ty -> (mty,mapStr ty f te)
+ _ -> (mty,te)
diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs
new file mode 100644
index 000000000..535bb9fcd
--- /dev/null
+++ b/src/compiler/GF/Compile/Compute/Concrete.hs
@@ -0,0 +1,461 @@
+----------------------------------------------------------------------
+-- |
+-- Module : GF.Compile.Concrete.Compute
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/01 15:39:12 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.19 $
+--
+-- Computation of source terms. Used in compilation and in @cc@ command.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.Concrete (computeConcrete, computeTerm,computeConcreteRec) where
+
+import GF.Data.Operations
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Infra.Modules
+import GF.Data.Str
+import GF.Grammar.Printer
+import GF.Grammar.Predef
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Compile.Refresh
+import GF.Grammar.PatternMatch
+import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
+
+import GF.Compile.Compute.AppPredefined
+
+import Data.List (nub,intersperse)
+import Control.Monad (liftM2, liftM)
+import Text.PrettyPrint
+
+-- | computation of concrete syntax terms into normal form
+-- used mainly for partial evaluation
+computeConcrete :: SourceGrammar -> Term -> Err Term
+computeConcrete g t = {- refreshTerm t >>= -} computeTerm g [] t
+computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
+
+computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
+computeTerm = computeTermOpt False
+
+-- rec=True is used if it cannot be assumed that looked-up constants
+-- have already been computed (mainly with -optimize=noexpand in .gfr)
+
+computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
+computeTermOpt rec gr = comput True where
+
+ comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging
+ case t of
+
+ Q (p,c) | p == cPredef -> return t
+ | otherwise -> look (p,c)
+
+ Vr x -> do
+ t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
+ case t' of
+ _ | t == t' -> return t
+ _ -> comp g t'
+
+ -- Abs x@(IA _) b -> do
+ Abs _ _ _ | full -> do
+ let (xs,b1) = termFormCnc t
+ b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
+ return $ mkAbs xs b'
+ -- b' <- comp (ext x (Vr x) g) b
+ -- return $ Abs x b'
+ Abs _ _ _ -> return t -- hnf
+
+ Let (x,(_,a)) b -> do
+ a' <- comp g a
+ comp (ext x a' g) b
+
+ Prod b x a t -> do
+ a' <- comp g a
+ t' <- comp (ext x (Vr x) g) t
+ return $ Prod b x a' t'
+
+ -- beta-convert
+ App f a -> case appForm t of
+ (h,as) | length as > 1 -> do
+ h' <- hnf g h
+ as' <- mapM (comp g) as
+ case h' of
+ _ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
+ c@(QC _) -> do
+ return $ mkApp c as'
+ Q (mod,f) | mod == cPredef -> do
+ (t',b) <- appPredefined (mkApp h' as')
+ if b then return t' else comp g t'
+
+ Abs _ _ _ -> do
+ let (xs,b) = termFormCnc h'
+ let g' = (zip (map snd xs) as') ++ g
+ let as2 = drop (length xs) as'
+ let xs2 = drop (length as') xs
+ b' <- comp g' (mkAbs xs2 b)
+ if null as2 then return b' else comp g (mkApp b' as2)
+
+ _ -> compApp g (mkApp h' as')
+ _ -> compApp g t
+
+ P t l | isLockLabel l -> return $ R []
+ ---- a workaround 18/2/2005: take this away and find the reason
+ ---- why earlier compilation destroys the lock field
+
+
+ P t l -> do
+ t' <- comp g t
+ case t' of
+ FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . variants
+ R r -> maybe (Bad (render (text "no value for label" <+> ppLabel l))) (comp g . snd) $
+ lookup l $ reverse r
+
+ ExtR a (R b) ->
+ case comp g (P (R b) l) of
+ Ok v -> return v
+ _ -> comp g (P a l)
+
+--- { - --- this is incorrect, since b can contain the proper value
+ ExtR (R a) b -> -- NOT POSSIBLE both a and b records!
+ case comp g (P (R a) l) of
+ Ok v -> return v
+ _ -> comp g (P b l)
+--- - } ---
+
+ S (T i cs) e -> prawitz g i (flip P l) cs e
+ S (V i cs) e -> prawitzV g i (flip P l) cs e
+
+ _ -> returnC $ P t' l
+
+ S t v -> do
+ t' <- compTable g t
+ v' <- comp g v
+ t1 <- case t' of
+---- V (RecType fs) _ -> uncurrySelect g fs t' v'
+---- T (TComp (RecType fs)) _ -> uncurrySelect g fs t' v'
+ _ -> return $ S t' v'
+ compSelect g t1
+
+ -- normalize away empty tokens
+ K "" -> return Empty
+
+ -- glue if you can
+ Glue x0 y0 -> do
+ 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
+
+ (S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
+ (s, S (T i cs) e) -> prawitz g i (Glue s) cs e
+ (S (V i cs) e, s) -> prawitzV g i (flip Glue s) cs e
+ (s, S (V i cs) e) -> prawitzV g i (Glue s) cs e
+ (_,Empty) -> return x
+ (Empty,_) -> return y
+ (K a, K b) -> return $ K (a ++ b)
+ (_, Alts d vs) -> do
+---- (K a, Alts (d,vs)) -> do
+ let glx = Glue x
+ comp g $ Alts (glx d) [(glx v,c) | (v,c) <- vs]
+ (Alts _ _, ka) -> checks [do
+ y' <- strsFromTerm ka
+---- (Alts _, K a) -> checks [do
+ x' <- strsFromTerm x -- this may fail when compiling opers
+ return $ variants [
+ foldr1 C (map K (str2strings (glueStr v u))) | v <- x', u <- y']
+---- foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
+ ,return $ Glue x y
+ ]
+ (C u v,_) -> comp g $ C u (Glue v y)
+
+ _ -> do
+ mapM_ checkNoArgVars [x,y]
+ r <- composOp (comp g) t
+ returnC r
+
+ Alts d aa -> do
+ d' <- comp g d
+ aa' <- mapM (compInAlts g) aa
+ returnC (Alts d' aa')
+
+ -- remove empty
+ C a b -> do
+ a' <- comp g a
+ b' <- comp g b
+ case (a',b') of
+ (Alts _ _, K a) -> checks [do
+ as <- strsFromTerm a' -- this may fail when compiling opers
+ return $ variants [
+ foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
+ ,
+ return $ C a' b'
+ ]
+ (Empty,_) -> returnC b'
+ (_,Empty) -> returnC a'
+ _ -> returnC $ C a' b'
+
+ -- reduce free variation as much as you can
+ FV ts -> mapM (comp g) ts >>= returnC . variants
+
+ -- merge record extensions if you can
+ ExtR r s -> do
+ r' <- comp g r
+ s' <- comp g s
+ case (r',s') of
+ (R rs, R ss) -> plusRecord r' s'
+ (RecType rs, RecType ss) -> plusRecType r' s'
+ _ -> return $ ExtR r' s'
+
+ ELin c r -> do
+ r' <- comp g r
+ unlockRecord c r'
+
+ T _ _ -> compTable g t
+ V _ _ -> compTable g t
+
+ -- otherwise go ahead
+ _ -> composOp (comp g) t >>= returnC
+
+ where
+
+ compApp g (App f a) = do
+ f' <- hnf 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'
+
+ (S (T i cs) e,_) -> prawitz g i (flip App a') cs e
+ (S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
+
+ _ -> do
+ (t',b) <- appPredefined (App f' a')
+ if b then return t' else comp g t'
+
+ hnf = comput False
+ comp = comput True
+
+ look c
+ | rec = lookupResDef gr c >>= comp []
+ | otherwise = lookupResDef gr c
+
+ ext x a g = (x,a):g
+
+ returnC = return --- . computed
+
+ variants ts = case nub ts of
+ [t] -> t
+ ts -> FV ts
+
+ isCan v = case v of
+ Con _ -> True
+ QC _ -> True
+ App f a -> isCan f && isCan a
+ R rs -> all (isCan . snd . snd) rs
+ _ -> False
+
+ compPatternMacro p = case p of
+ PM c -> case look c of
+ Ok (EPatt p') -> compPatternMacro p'
+ _ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
+ PAs x p -> do
+ p' <- compPatternMacro p
+ return $ PAs x p'
+ PAlt p q -> do
+ p' <- compPatternMacro p
+ q' <- compPatternMacro q
+ return $ PAlt p' q'
+ PSeq p q -> do
+ p' <- compPatternMacro p
+ q' <- compPatternMacro q
+ return $ PSeq p' q'
+ PRep p -> do
+ p' <- compPatternMacro p
+ return $ PRep p'
+ PNeg p -> do
+ p' <- compPatternMacro p
+ return $ PNeg p'
+ PR rs -> do
+ rs' <- mapPairsM compPatternMacro rs
+ return $ PR rs'
+
+ _ -> return p
+
+ compSelect g (S t' v') = case v' of
+ FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . variants
+
+---- S (T i cs) e -> prawitz g i (S t') cs e -- AR 8/7/2010 sometimes better
+---- S (V i cs) e -> prawitzV g i (S t') cs e -- sometimes much worse
+
+
+ _ -> case t' of
+ FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
+
+ T _ [(PW,c)] -> comp g c --- an optimization
+ T _ [(PT _ PW,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
+
+ -- course-of-values table: look up by index, no pattern matching needed
+
+ V ptyp ts -> do
+ vs <- allParamValues gr ptyp
+ case lookupR v' (zip vs [0 .. length vs - 1]) of
+ Just i -> comp g $ ts !! i
+ _ -> return $ S t' v' -- if v' is not canonical
+ T _ cc -> do
+ case matchPattern cc v' of
+ Ok (c,g') -> comp (g' ++ g) c
+ _ | isCan v' -> Bad (render (text "missing case" <+> ppTerm Unqualified 0 v' <+> text "in" <+> ppTerm Unqualified 0 t))
+ _ -> return $ S t' v' -- if v' is not canonical
+
+ S (T i cs) e -> prawitz g i (flip S v') cs e
+ S (V i cs) e -> prawitzV g i (flip S v') cs e
+ _ -> returnC $ S t' v'
+
+ --- needed to match records with and without type information
+ ---- todo: eliminate linear search in a list of records!
+ lookupR v vs = case v of
+ R rs -> lookup ([(x,y) | (x,(_,y)) <- rs])
+ [([(x,y) | (x,(_,y)) <- rs],v) | (R rs,v) <- vs]
+ _ -> lookup v vs
+
+ -- case-expand tables
+ -- if already expanded, don't expand again
+ compTable g t = case t of
+ T i@(TComp ty) cs -> do
+ -- if there are no variables, don't even go inside
+ cs' <- if (null g) then return cs else mapPairsM (comp g) cs
+---- return $ V ty (map snd cs')
+ return $ T i cs'
+ V ty cs -> do
+ ty' <- comp g ty
+ -- if there are no variables, don't even go inside
+ cs' <- if (null g) then return cs else mapM (comp g) cs
+ return $ V ty' cs'
+
+ T i cs -> do
+ pty0 <- getTableType i
+ ptyp <- comp g pty0
+ case allParamValues gr ptyp of
+ Ok vs0 -> do
+ let vs = vs0 ---- [Val v ptyp i | (v,i) <- zip vs0 [0..]]
+ ps0 <- mapM (compPatternMacro . fst) cs
+ cs' <- mapM (compBranchOpt g) (zip ps0 (map snd cs))
+ sts <- mapM (matchPattern cs') vs
+ ts <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
+ ps <- mapM term2patt vs
+ let ps' = ps --- PT ptyp (head ps) : tail ps
+---- return $ V ptyp ts -- to save space, just course of values
+ return $ T (TComp ptyp) (zip ps' ts)
+ _ -> do
+ ps0 <- mapM (compPatternMacro . fst) cs
+ cs' <- mapM (compBranch g) (zip ps0 (map snd cs))
+
+---- cs' <- mapM (compBranch g) cs
+ return $ T i cs' -- happens with variable types
+ _ -> comp g t
+
+ compBranch g (p,v) = do
+ let g' = contP p ++ g
+ v' <- comp g' v
+ return (p,v')
+
+ compBranchOpt g c@(p,v) = case contP p of
+ [] -> return c
+ _ -> err (const (return c)) return $ compBranch g c
+
+ contP p = case p of
+ PV x -> [(x,Vr x)]
+ PC _ ps -> concatMap contP ps
+ PP _ ps -> concatMap contP ps
+ PT _ p -> contP p
+ PR rs -> concatMap (contP . snd) rs
+
+ PAs x p -> (x,Vr x) : contP p
+
+ PSeq p q -> concatMap contP [p,q]
+ PAlt p q -> concatMap contP [p,q]
+ PRep p -> contP p
+ PNeg p -> contP p
+
+ _ -> []
+
+ prawitz g i f cs e = do
+ cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
+ return $ S (T i cs') e
+ prawitzV g i f cs e = do
+ cs' <- mapM (comp g) [(f v) | v <- cs]
+ return $ S (V i cs') e
+
+ compInAlts g (v,c) = do
+ v' <- comp g v
+ c' <- comp g c
+ c2 <- case c' of
+ EPatt p -> liftM Strs $ getPatts p
+ _ -> return c'
+ return (v',c2)
+ where
+ getPatts p = case p of
+ PAlt a b -> liftM2 (++) (getPatts a) (getPatts b)
+ PString s -> return [K s]
+ PSeq a b -> do
+ as <- getPatts a
+ bs <- getPatts b
+ return [K (s ++ t) | K s <- as, K t <- bs]
+ _ -> fail (render (text "not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))
+
+{- ----
+ uncurrySelect g fs t v = do
+ ts <- mapM (allParamValues gr . snd) fs
+ vs <- mapM (comp g) [P v r | r <- map fst fs]
+ return $ reorderSelect t fs ts vs
+
+ reorderSelect t fs pss vs = case (t,fs,pss,vs) of
+ (V _ ts, f:fs1, ps:pss1, v:vs1) ->
+ S (V (snd f)
+ [reorderSelect (V (RecType fs1) t) fs1 pss1 vs1 |
+ t <- segments (length ts `div` length ps) ts]) v
+ (T (TComp _) cs, f:fs1, ps:pss1, v:vs1) ->
+ S (T (TComp (snd f))
+ [(p,reorderSelect (T (TComp (RecType fs1)) c) fs1 pss1 vs1) |
+ (ep,c) <- zip ps (segments (length cs `div` length ps) cs),
+ let Ok p = term2patt ep]) v
+ _ -> t
+
+ segments i xs =
+ let (x0,xs1) = splitAt i xs in x0 : takeWhile (not . null) (segments i xs1)
+-}
+
+
+-- | argument variables cannot be glued
+checkNoArgVars :: Term -> Err Term
+checkNoArgVars t = case t of
+ Vr (IA _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t
+ Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t
+ _ -> composOp checkNoArgVars t
+
+glueErrorMsg s =
+ render (text "Cannot glue (+) term with run-time variable" <+> s <> char '.' $$
+ text "Use Prelude.bind instead.")
+
+getArgType t = case t of
+ V ty _ -> return ty
+ T (TComp ty) _ -> return ty
+ _ -> Bad (render (text "cannot get argument type of table" $$ nest 2 (ppTerm Unqualified 0 t)))