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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
module GF.Compile.PGFtoLProlog(grammar2lambdaprolog_mod, grammar2lambdaprolog_sig) where
import PGF.CId
import PGF.Data hiding (ppExpr, ppType, ppHypo)
import PGF.Macros
import Data.List
import Data.Maybe
import Text.PrettyPrint
import qualified Data.Map as Map
import Debug.Trace
grammar2lambdaprolog_mod pgf = render $
text "module" <+> ppCId (absname pgf) <> char '.' $$
space $$
vcat [ppClauses cat fns | (cat,(_,fs,_)) <- Map.toList (cats (abstract pgf)),
let fns = [(f,fromJust (Map.lookup f (funs (abstract pgf)))) | (_,f) <- fs]]
where
ppClauses cat fns =
text "/*" <+> ppCId cat <+> text "*/" $$
vcat [snd (ppClause (abstract pgf) 0 1 [] f ty) <> dot | (f,(ty,_,Nothing,_,_)) <- fns] $$
space $$
vcat [vcat (map (\eq -> equation2clause (abstract pgf) f eq <> dot) eqs) | (f,(_,_,Just eqs,_,_)) <- fns] $$
space
grammar2lambdaprolog_sig pgf = render $
text "sig" <+> ppCId (absname pgf) <> char '.' $$
space $$
vcat [ppCat c hyps <> dot | (c,(hyps,_,_)) <- Map.toList (cats (abstract pgf))] $$
space $$
vcat [ppFun f ty <> dot | (f,(ty,_,Nothing,_,_)) <- Map.toList (funs (abstract pgf))] $$
space $$
vcat [ppExport c hyps <> dot | (c,(hyps,_,_)) <- Map.toList (cats (abstract pgf))] $$
vcat [ppFunPred f (hyps ++ [(Explicit,wildCId,DTyp [] c es)]) <> dot | (f,(DTyp hyps c es,_,Just _,_,_)) <- Map.toList (funs (abstract pgf))]
ppCat :: CId -> [Hypo] -> Doc
ppCat c hyps = text "kind" <+> ppKind c <+> text "type"
ppFun :: CId -> Type -> Doc
ppFun f ty = text "type" <+> ppCId f <+> ppType 0 ty
ppExport :: CId -> [Hypo] -> Doc
ppExport c hyps = text "exportdef" <+> ppPred c <+> foldr (\hyp doc -> ppHypo 1 hyp <+> text "->" <+> doc) (text "o") (hyp:hyps)
where
hyp = (Explicit,wildCId,DTyp [] c [])
ppFunPred :: CId -> [Hypo] -> Doc
ppFunPred c hyps = text "exportdef" <+> ppCId c <+> foldr (\hyp doc -> ppHypo 1 hyp <+> text "->" <+> doc) (text "o") hyps
ppClause :: Abstr -> Int -> Int -> [CId] -> CId -> Type -> (Int,Doc)
ppClause abstr d i scope f ty@(DTyp hyps cat args)
| null hyps = let res = EFun f
(goals,i',head) = ppRes i scope cat (res : args)
in (i',(if null goals
then empty
else hsep (punctuate comma (map (ppExpr 0 i' scope) goals)) <> comma)
<+>
head)
| otherwise = let (i',vars,scope',hdocs) = ppHypos i [] scope hyps (depType [] ty)
res = foldl EApp (EFun f) (map EFun (reverse vars))
quants = if d > 0
then hsep (map (\v -> text "pi" <+> ppCId v <+> char '\\') vars)
else empty
(goals,i'',head) = ppRes i' scope' cat (res : args)
docs = map (ppExpr 0 i'' scope') goals ++ hdocs
in (i'',ppParens (d > 0) (quants <+> head <+>
(if null docs
then empty
else text ":-" <+> hsep (punctuate comma docs))))
where
ppRes i scope cat es =
let ((goals,i'),es') = mapAccumL (\(goals,i) e -> let (goals',i',e') = expr2goal abstr scope goals i e []
in ((goals',i'),e')) ([],i) es
in (goals,i',ppParens (d > 3) (ppPred cat <+> hsep (map (ppExpr 4 i' scope) es')))
ppHypos :: Int -> [CId] -> [CId] -> [(BindType,CId,Type)] -> [Int] -> (Int,[CId],[CId],[Doc])
ppHypos i vars scope [] []
= (i,vars,scope,[])
ppHypos i vars scope ((_,x,typ):hyps) (c:cs)
| x /= wildCId = let v = mkVar i
(i',doc) = ppClause abstr 1 (i+1) scope v typ
(i'',vars',scope',docs) = ppHypos i' (v:vars) (v:scope) hyps cs
in (i'',vars',scope',if c == 0 then doc : docs else docs)
ppHypos i vars scope ((_,x,typ):hyps) cs
= let v = mkVar i
(i',doc) = ppClause abstr 1 (i+1) scope v typ
(i'',vars',scope',docs) = ppHypos i' (v:vars) scope hyps cs
in (i'',vars',scope',doc : docs)
mkVar i = mkCId ("X_"++show i)
ppPred :: CId -> Doc
ppPred cat = text "p_" <> ppCId cat
ppKind :: CId -> Doc
ppKind cat = text "k_" <> ppCId cat
ppType :: Int -> Type -> Doc
ppType d (DTyp hyps cat args)
| null hyps = ppKind cat
| otherwise = ppParens (d > 0) (foldr (\hyp doc -> ppHypo 1 hyp <+> text "->" <+> doc) (ppKind cat) hyps)
ppHypo d (_,_,typ) = ppType d typ
ppExpr d i scope (EAbs b x e) = let v = mkVar i
in ppParens (d > 1) (ppCId v <+> char '\\' <+> ppExpr 1 (i+1) (v:scope) e)
ppExpr d i scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 i scope e1) <+> (ppExpr 4 i scope e2))
ppExpr d i scope (ELit l) = ppLit l
ppExpr d i scope (EMeta n) = ppMeta n
ppExpr d i scope (EFun f) = ppCId f
ppExpr d i scope (EVar j) = ppCId (scope !! j)
ppExpr d i scope (ETyped e ty)= ppExpr d i scope e
ppExpr d i scope (EImplArg e) = ppExpr 0 i scope e
dot = char '.'
depType counts (DTyp hyps cat es) =
foldl' depExpr (foldl' depHypo counts hyps) es
depHypo counts (_,x,ty)
| x == wildCId = depType counts ty
| otherwise = 0:depType counts ty
depExpr counts (EAbs b x e) = tail (depExpr (0:counts) e)
depExpr counts (EApp e1 e2) = depExpr (depExpr counts e1) e2
depExpr counts (ELit l) = counts
depExpr counts (EMeta n) = counts
depExpr counts (EFun f) = counts
depExpr counts (EVar j) = let (xs,c:ys) = splitAt j counts
in xs++(c+1):ys
depExpr counts (ETyped e ty)= depExpr counts e
depExpr counts (EImplArg e) = depExpr counts e
equation2clause abstr f (Equ ps e) =
let scope0 = foldl pattScope [] ps
scope = [mkVar i | i <- [0..n-1]]
n = length scope0
es = map (patt2expr scope0) ps
(goals,_,goal) = expr2goal abstr scope [] n e []
in ppCId f <+> hsep (map (ppExpr 4 n scope) (es++[goal])) <+>
if null goals
then empty
else text ":-" <+> hsep (punctuate comma (map (ppExpr 0 n scope) (reverse goals)))
patt2expr scope (PApp f ps) = foldl EApp (EFun f) (map (patt2expr scope) ps)
patt2expr scope (PLit l) = ELit l
patt2expr scope (PVar x) = case findIndex (==x) scope of
Just i -> EVar i
Nothing -> error ("unknown variable "++showCId x)
patt2expr scope (PImplArg p)= EImplArg (patt2expr scope p)
expr2goal abstr scope goals i (EApp e1 e2) args =
let (goals',i',e2') = expr2goal abstr scope goals i e2 []
in expr2goal abstr scope goals' i' e1 (e2':args)
expr2goal abstr scope goals i (EFun f) args =
case Map.lookup f (funs abstr) of
Just (_,_,Just _,_,_) -> let e = EFun (mkVar i)
in (foldl EApp (EFun f) (args++[e]) : goals, i+1, e)
_ -> (goals,i,foldl EApp (EFun f) args)
expr2goal abstr scope goals i (EVar j) args =
(goals,i,foldl EApp (EVar j) args)
|
