Mercurial > urweb

comparison src/elab_util.sml @ 6:38bf996e1c2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Check for leftover kind unifs
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 16:44:39 -0500
parents 258261a53842
children a455a9f85cc3
comparison
equal deleted inserted replaced
5:258261a53842 6:38bf996e1c2e
31 31
32 structure S = Search 32 structure S = Search
33 33
34 structure Kind = struct 34 structure Kind = struct
35 35
36 fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'state, 'abort) S.mapfolder = 36 fun mapfold f =
37 let 37 let
38 fun mfk k acc = 38 fun mfk k acc =
39 S.bindP (mfk' k acc, f) 39 S.bindP (mfk' k acc, f)
40 40
41 and mfk' (kAll as (k, loc)) = 41 and mfk' (kAll as (k, loc)) =
63 in 63 in
64 mfk 64 mfk
65 end 65 end
66 66
67 fun exists f k = 67 fun exists f k =
68 case mapfold (fn (k, ()) => 68 case mapfold (fn k => fn () =>
69 if f k then 69 if f k then
70 S.Return () 70 S.Return ()
71 else 71 else
72 S.Continue (k, ())) k () of 72 S.Continue (k, ())) k () of
73 S.Return _ => true
74 | S.Continue _ => false
75
76 end
77
78 structure Con = struct
79
80 fun mapfold {kind = fk, con = fc} =
81 let
82 val mfk = Kind.mapfold fk
83
84 fun mfc c acc =
85 S.bindP (mfc' c acc, fc)
86
87 and mfc' (cAll as (c, loc)) =
88 case c of
89 TFun (c1, c2) =>
90 S.bind2 (mfc c1,
91 fn c1' =>
92 S.map2 (mfc c2,
93 fn c2' =>
94 (TFun (c1', c2'), loc)))
95 | TCFun (e, x, k, c) =>
96 S.bind2 (mfk k,
97 fn k' =>
98 S.map2 (mfc c,
99 fn c' =>
100 (TCFun (e, x, k', c'), loc)))
101 | TRecord c =>
102 S.map2 (mfc c,
103 fn c' =>
104 (TRecord c', loc))
105
106 | CRel _ => S.return2 cAll
107 | CNamed _ => S.return2 cAll
108 | CApp (c1, c2) =>
109 S.bind2 (mfc c1,
110 fn c1' =>
111 S.map2 (mfc c2,
112 fn c2' =>
113 (CApp (c1', c2'), loc)))
114 | CAbs (e, x, k, c) =>
115 S.bind2 (mfk k,
116 fn k' =>
117 S.map2 (mfc c,
118 fn c' =>
119 (CAbs (e, x, k', c'), loc)))
120
121 | CName _ => S.return2 cAll
122
123 | CRecord (k, xcs) =>
124 S.bind2 (mfk k,
125 fn k' =>
126 S.map2 (ListUtil.mapfold (fn (x, c) =>
127 S.bind2 (mfc x,
128 fn x' =>
129 S.map2 (mfc c,
130 fn c' =>
131 (x', c'))))
132 xcs,
133 fn xcs' =>
134 (CRecord (k', xcs'), loc)))
135 | CConcat (c1, c2) =>
136 S.bind2 (mfc c1,
137 fn c1' =>
138 S.map2 (mfc c2,
139 fn c2' =>
140 (CConcat (c1', c2'), loc)))
141
142 | CError => S.return2 cAll
143 | CUnif (_, _, ref (SOME c)) => mfc' c
144 | CUnif _ => S.return2 cAll
145 in
146 mfc
147 end
148
149 fun exists {kind, con} k =
150 case mapfold {kind = fn k => fn () =>
151 if kind k then
152 S.Return ()
153 else
154 S.Continue (k, ()),
155 con = fn c => fn () =>
156 if con c then
157 S.Return ()
158 else
159 S.Continue (c, ())} k () of
73 S.Return _ => true 160 S.Return _ => true
74 | S.Continue _ => false 161 | S.Continue _ => false
75 162
76 end 163 end
77 164