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
|
module PGF.Editor where
import PGF.Data
import PGF.CId
import qualified Data.Map as M
-- API
new :: Type -> State
new (DTyp _ t _) = etree2state (uETree t)
refine :: Dict -> CId -> State -> State
refine dict f = replace (mkRefinement dict f)
replace :: ETree -> State -> State
replace t = doInState (const t)
delete :: State -> State
delete s = replace (uETree (typ (tree s))) s
goNextMeta :: State -> State
goNextMeta = untilPosition isMetaFocus goNext
goTop :: State -> State
goTop = navigate (const top)
refineMenu :: Dict -> State -> [(CId,FType)]
refineMenu dict s = maybe [] id $ M.lookup (focusType s) (refines dict)
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 :: Tree -> ETree
---- 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 = tail
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)
focusType :: State -> BType
focusType 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
_ -> navigate right (untilPosition hasYoungerSisters (navigate up) s)
where
hasYoungerSisters s = case position s of
n:ns -> length (children (subtree ns (tree s))) > n + 1
isMetaFocus :: State -> Bool
isMetaFocus s = case atom (focus s) of
AMeta _ -> True
_ -> False
-------
type BType = CId ----
type FType = ([BType],BType) ----
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)
|
