1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
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 GF.Text.Pretty
-- for debugging
tracd m t = t
-- tracd = trace
compute :: SourceGrammar -> Term -> Err Term
compute = computeAbsTerm
computeAbsTerm :: SourceGrammar -> Term -> Err Term
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] -> Term -> Err Term
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])
|
