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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
|
module PGF.Editor (
State, -- datatype -- type-annotated possibly open tree with a focus
Dict, -- datatype -- abstract syntax information optimized for editing
Position, -- datatype -- path from top to focus
new, -- :: Type -> State -- create new State
refine, -- :: Dict -> CId -> State -> State -- refine focus with CId
replace, -- :: Dict -> Tree -> State -> State -- replace focus with Tree
delete, -- :: State -> State -- replace focus with ?
goNextMeta, -- :: State -> State -- move focus to next ? node
goNext, -- :: State -> State -- move to next node
goTop, -- :: State -> State -- move focus to the top (=root)
goPosition, -- :: Position -> State -> State -- move focus to given position
mkPosition, -- :: [Int] -> Position -- list of choices (top = [])
showPosition,-- :: Position -> [Int] -- readable position
focusType, -- :: State -> Type -- get the type of focus
stateTree, -- :: State -> Tree -- get the current tree
isMetaFocus, -- :: State -> Bool -- whether focus is ?
allMetas, -- :: State -> [(Position,Type)] -- all ?s and their positions
prState, -- :: State -> String -- print state, focus marked *
refineMenu, -- :: Dict -> State -> [CId] -- get refinement menu
pgf2dict -- :: PGF -> Dict -- create editing Dict from PGF
) where
import PGF.Data
import PGF.CId
import qualified Data.Map as M
import Debug.Trace ----
-- API
new :: Type -> State
new (DTyp _ t _) = etree2state (uETree t)
refine :: Dict -> CId -> State -> State
refine dict f = replaceInState (mkRefinement dict f)
replace :: Dict -> Tree -> State -> State
replace dict t = replaceInState (tree2etree dict t)
delete :: State -> State
delete s = replaceInState (uETree (typ (tree s))) s
goNextMeta :: State -> State
goNextMeta s =
if isComplete s then s
else let s1 = goNext s in if isMetaFocus s1
then s1 else goNextMeta s1
isComplete :: State -> Bool
isComplete s = isc (tree s) where
isc t = case atom t of
AMeta _ -> False
ACon _ -> all isc (children t)
goTop :: State -> State
goTop = navigate (const top)
goPosition :: [Int] -> State -> State
goPosition p s = s{position = p}
mkPosition :: [Int] -> Position
mkPosition = id
refineMenu :: Dict -> State -> [CId]
refineMenu dict s = maybe [] (map fst) $ M.lookup (focusBType s) (refines dict)
focusType :: State -> Type
focusType s = btype2type (focusBType s)
stateTree :: State -> Tree
stateTree = etree2tree . tree
pgf2dict :: PGF -> Dict
pgf2dict pgf = Dict (M.fromAscList fus) refs where
fus = [(f,mkFType ty) | (f,(ty,_)) <- M.toList (funs abs)]
refs = M.fromAscList [(c, fusTo c) | (c,_) <- M.toList (cats abs)]
fusTo c = [(f,ty) | (f,ty@(_,k)) <- fus, k==c] ---- quadratic
mkFType (DTyp hyps c _) = ([k | Hyp _ (DTyp _ k _) <- hyps],c) ----dep types
abs = abstract pgf
etree2tree :: ETree -> Tree
etree2tree t = case atom t of
ACon f -> Fun f (map etree2tree (children t))
AMeta i -> Meta i
tree2etree :: Dict -> Tree -> ETree
tree2etree dict t = case t of
Fun f _ -> annot (look f) t
where
annot (tys,ty) tr = case tr of
Fun f trs -> ETree (ACon f) ty [annt t tr | (t,tr) <- zip tys trs]
Meta i -> ETree (AMeta i) ty []
annt ty tr = case tr of
Fun _ _ -> tree2etree dict tr
Meta _ -> annot ([],ty) tr
look f = maybe undefined id $ M.lookup f (functs dict)
prState :: State -> String
prState s = unlines [replicate i ' ' ++ f | (i,f) <- pr [] (tree s)] where
pr i t =
(ind i,prAtom i (atom t)) : concat [pr (sub j i) c | (j,c) <- zip [0..] (children t)]
prAtom i a = prFocus i ++ case a of
ACon f -> prCId f
AMeta i -> "?" ++ show i
prFocus i = if i == position s then "*" else ""
ind i = 2 * length i
sub j i = i ++ [j]
showPosition :: Position -> [Int]
showPosition = id
allMetas :: State -> [(Position,Type)]
allMetas s = [(reverse p, btype2type ty) | (p,ty) <- metas [] (tree s)] where
metas p t =
(if isMetaAtom (atom t) then [(p,typ t)] else []) ++
concat [metas (i:p) u | (i,u) <- zip [0..] (children t)]
---- Trees and navigation
data ETree = ETree {
atom :: Atom,
typ :: BType,
children :: [ETree]
}
deriving Show
data Atom =
ACon CId
| AMeta Int
deriving Show
btype2type :: BType -> Type
btype2type t = DTyp [] t []
uETree :: BType -> ETree
uETree ty = ETree (AMeta 0) ty []
data State = State {
position :: Position,
tree :: ETree
}
deriving Show
type Position = [Int]
top :: Position
top = []
up :: Position -> Position
up p = case p of
_:_ -> init p
_ -> p
down :: Position -> Position
down = (++[0])
left :: Position -> Position
left p = case p of
_:_ | last p > 0 -> init p ++ [last p - 1]
_ -> top
right :: Position -> Position
right p = case p of
_:_ -> init p ++ [last p + 1]
_ -> top
etree2state :: ETree -> State
etree2state = State top
doInState :: (ETree -> ETree) -> State -> State
doInState f s = s{tree = change (position s) (tree s)} where
change p t = case p of
[] -> f t
n:ns -> let (ts1,t0:ts2) = splitAt n (children t) in
t{children = ts1 ++ [change ns t0] ++ ts2}
subtree :: Position -> ETree -> ETree
subtree p t = case p of
[] -> t
n:ns -> subtree ns (children t !! n)
focus :: State -> ETree
focus s = subtree (position s) (tree s)
focusBType :: State -> BType
focusBType s = typ (focus s)
navigate :: (Position -> Position) -> State -> State
navigate p s = s{position = p (position s)}
-- p is a fix-point aspect of state change
untilFix :: Eq a => (State -> a) -> (State -> Bool) -> (State -> State) -> State -> State
untilFix p b f s =
if b s
then s
else let fs = f s in if p fs == p s
then s
else untilFix p b f fs
untilPosition :: (State -> Bool) -> (State -> State) -> State -> State
untilPosition = untilFix position
goNext :: State -> State
goNext s = case focus s of
st | not (null (children st)) -> navigate down s
_ -> findSister s
where
findSister s = case s of
s' | null (position s') -> s'
s' | hasYoungerSisters s' -> navigate right s'
s' -> findSister (navigate up s')
hasYoungerSisters s = case position s of
p@(_:_) -> length (children (focus (navigate up s))) > last p + 1
_ -> False
isMetaFocus :: State -> Bool
isMetaFocus s = isMetaAtom (atom (focus s))
isMetaAtom :: Atom -> Bool
isMetaAtom a = case a of
AMeta _ -> True
_ -> False
replaceInState :: ETree -> State -> State
replaceInState t = doInState (const t)
-------
type BType = CId ----dep types
type FType = ([BType],BType) ----dep types
data Dict = Dict {
functs :: M.Map CId FType,
refines :: M.Map BType [(CId,FType)]
}
mkRefinement :: Dict -> CId -> ETree
mkRefinement dict f = ETree (ACon f) val (map uETree args) where
(args,val) = maybe undefined id $ M.lookup f (functs dict)
|
