143 fun report [] _ _ = () |
145 fun report [] _ _ = () |
144 | report ps markup x = |
146 | report ps markup x = |
145 let val m = markup x |
147 let val m = markup x |
146 in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end; |
148 in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end; |
147 |
149 |
148 val env0 = ([], [], []); |
150 fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = |
149 |
|
150 fun decode (env as (ps, qs, bs)) (Const ("_constrain", _) $ t $ typ) = |
|
151 (case decode_position typ of |
151 (case decode_position typ of |
152 SOME p => decode (p :: ps, qs, bs) t |
152 SOME p => decode (p :: ps) qs bs t |
153 | NONE => Type.constraint (decodeT typ) (decode env t)) |
153 | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) |
154 | decode (env as (ps, qs, bs)) (Const ("_constrainAbs", _) $ t $ typ) = |
154 | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = |
155 (case decode_position typ of |
155 (case decode_position typ of |
156 SOME q => decode (ps, q :: qs, bs) t |
156 SOME q => decode ps (q :: qs) bs t |
157 | NONE => Type.constraint (decodeT typ --> dummyT) (decode env t)) |
157 | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) |
158 | decode (_, qs, bs) (Abs (x, T, t)) = |
158 | decode _ qs bs (Abs (x, T, t)) = |
159 let |
159 let |
160 val id = serial_string (); |
160 val id = serial_string (); |
161 val _ = report qs markup_bound id; |
161 val _ = report qs (markup_bound true) id; |
162 in Abs (x, T, decode ([], [], (qs, id) :: bs) t) end |
162 in Abs (x, T, decode [] [] (id :: bs) t) end |
163 | decode _ (t $ u) = decode env0 t $ decode env0 u |
163 | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u |
164 | decode (ps, _, _) (Const (a, T)) = |
164 | decode ps _ _ (Const (a, T)) = |
165 (case try Lexicon.unmark_fixed a of |
165 (case try Lexicon.unmark_fixed a of |
166 SOME x => (report ps markup_free x; Free (x, T)) |
166 SOME x => (report ps markup_free x; Free (x, T)) |
167 | NONE => |
167 | NONE => |
168 let |
168 let |
169 val c = |
169 val c = |
170 (case try Lexicon.unmark_const a of |
170 (case try Lexicon.unmark_const a of |
171 SOME c => c |
171 SOME c => c |
172 | NONE => snd (map_const a)); |
172 | NONE => snd (map_const a)); |
173 val _ = report ps markup_const c; |
173 val _ = report ps markup_const c; |
174 in Const (c, T) end) |
174 in Const (c, T) end) |
175 | decode (ps, _, _) (Free (a, T)) = |
175 | decode ps _ _ (Free (a, T)) = |
176 (case (map_free a, map_const a) of |
176 (case (map_free a, map_const a) of |
177 (SOME x, _) => (report ps markup_free x; Free (x, T)) |
177 (SOME x, _) => (report ps markup_free x; Free (x, T)) |
178 | (_, (true, c)) => (report ps markup_const c; Const (c, T)) |
178 | (_, (true, c)) => (report ps markup_const c; Const (c, T)) |
179 | (_, (false, c)) => |
179 | (_, (false, c)) => |
180 if Long_Name.is_qualified c |
180 if Long_Name.is_qualified c |
181 then (report ps markup_const c; Const (c, T)) |
181 then (report ps markup_const c; Const (c, T)) |
182 else (report ps markup_free c; Free (c, T))) |
182 else (report ps markup_free c; Free (c, T))) |
183 | decode (ps, _, _) (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) |
183 | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) |
184 | decode (_, _, bs) (t as Bound i) = |
184 | decode ps _ bs (t as Bound i) = |
185 (case try (nth bs) i of |
185 (case try (nth bs) i of |
186 SOME (qs, id) => (report qs markup_bound id; t) |
186 SOME id => (report ps (markup_bound false) id; t) |
187 | NONE => t); |
187 | NONE => t); |
188 |
188 |
189 val tm' = decode env0 tm; |
189 val tm' = decode [] [] [] tm; |
190 in (! reports, tm') end; |
190 in (! reports, tm') end; |
191 |
191 |
192 |
192 |
193 |
193 |
194 (** output utils **) |
194 (** output utils **) |