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
|
module PGF.Editor (
State, -- type-annotated possibly open tree with a position
Dict, -- abstract syntax in different views
new, -- :: Type -> State
refine, -- :: Dict -> CId -> State -> State
replace, -- :: Dict -> Tree -> State -> State
delete, -- :: State -> State
goNextMeta, -- :: State -> State
goNext, -- :: State -> State
goTop, -- :: State -> State
focusType, -- :: State -> Type
stateTree, -- :: State -> Tree
refineMenu, -- :: Dict -> State -> [CId]
pgf2dict -- :: PGF -> Dict
) 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)
refineMenu :: Dict -> State -> [CId]
refineMenu dict s = maybe [] (map fst) $ M.lookup (focusBType s) (refines dict)
focusType :: State -> Type
focusType s = DTyp [] (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)
---- TODO
-- getPosition :: Language -> Int -> ETree -> Position
---- Trees and navigation
data ETree = ETree {
atom :: Atom,
typ :: BType,
children :: [ETree]
}
deriving Show
data Atom =
ACon CId
| AMeta Int
deriving Show
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
(n:ns) | n > 0 -> n-1 : ns
_ -> top
right :: Position -> Position
right p = case p of
(n:ns) -> n+1 : ns
_ -> 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 = trace (show (position 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 = case atom (focus s) 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)
|
