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
|
----------------------------------------------------------------------
-- |
-- Module : AbsCompute
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- computation in abstract syntax with def definitions.
--
-- modified from src GF computation
-----------------------------------------------------------------------------
module PGF.AbsCompute (
compute
) where
import PGF.Data
import PGF.Macros (lookDef,isData)
import PGF.Expr
import PGF.CId
compute :: PGF -> Tree -> Tree
compute pgf = computeAbsTermIn pgf []
computeAbsTermIn :: PGF -> [CId] -> Tree -> Tree
computeAbsTermIn pgf vv = expr2tree . compt vv . tree2expr where
compt vv t =
let
t' = beta vv t
(yy,f,aa) = exprForm t'
vv' = yy ++ vv
aa' = map (compt vv') aa
in
mkAbs yy $ case look f of
Left (EEq eqs) -> case match eqs aa' of
Just (d,g) -> compt vv' $ subst vv' g d
_ -> mkApp f aa'
Left (EMeta _) -> mkApp f aa' -- canonical or primitive
Left d -> compt vv' $ mkApp d aa'
_ -> mkApp f aa' -- literal
look f = case f of
EVar c -> Left $ lookDef pgf c
_ -> Right f
match = findMatch pgf
beta :: [CId] -> Expr -> Expr
beta vv c = case c of
EApp f a ->
let (a',f') = (beta vv a, beta vv f) in
case f' of
EAbs x b -> beta vv $ subst vv [(x,a')] (beta (x:vv) b)
_ -> (if a'==a && f'==f then id else beta vv) $ EApp f' a'
EAbs x b -> EAbs x (beta (x:vv) b)
_ -> c
subst :: [CId] -> Subst -> Expr -> Expr
subst xs g e = case e of
EAbs x b -> EAbs x (subst (x:xs) g e) ---- TODO: refresh variables
EApp f a -> EApp (substg f) (substg a)
EVar x -> maybe e id $ lookup x g
_ -> e
where
substg = subst xs g
type Subst = [(CId,Expr)]
type Patt = Expr
exprForm :: Expr -> ([CId],Expr,[Expr])
exprForm exp = upd ([],exp,[]) where
upd (xs,f,es) = case f of
EAbs x b -> upd (x:xs,b,es)
EApp c a -> upd (xs,c,a:es)
_ -> (reverse xs,f,es)
mkAbs xs b = foldr EAbs b xs
mkApp f es = foldl EApp f es
-- special version of pattern matching, to deal with comp under lambda
findMatch :: PGF -> [Equation] -> [Expr] -> Maybe (Expr, Subst)
findMatch pgf cases terms = case cases of
[] -> Nothing
(Equ patts _):_ | length patts /= length terms -> Nothing
(Equ patts val):cc -> case mapM tryMatch (zip patts terms) of
Just substs -> return (val, concat substs)
_ -> findMatch pgf cc terms
where
tryMatch (p,t) = case (exprForm p, exprForm t) of
(([],EVar c,[]),_) | constructor c -> if p==t then return [] else Nothing
(([],EVar x,[]),_) | notMeta t -> return [(x,t)]
(([],p, pp), ([], f, tt)) | p == f && length pp == length tt -> do
matches <- mapM tryMatch (zip pp tt)
return (concat matches)
_ -> if p==t then return [] else Nothing
notMeta e = case e of
EMeta _ -> False
EApp f a -> notMeta f && notMeta a
EAbs _ b -> notMeta b
_ -> True
constructor = isData pgf
|
