143 val prelude = |
147 val prelude = |
144 "#!/usr/bin/swipl -q -t main -f\n\n" ^ |
148 "#!/usr/bin/swipl -q -t main -f\n\n" ^ |
145 ":- style_check(-singleton).\n\n" ^ |
149 ":- style_check(-singleton).\n\n" ^ |
146 "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ |
150 "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ |
147 "main :- halt(1).\n" |
151 "main :- halt(1).\n" |
|
152 |
|
153 (* parsing prolog solution *) |
|
154 |
|
155 val scan_atom = |
|
156 Scan.repeat (Scan.one (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s)) |
|
157 |
|
158 val scan_var = |
|
159 Scan.repeat (Scan.one |
|
160 (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)) |
|
161 |
|
162 fun dest_Char (Symbol.Char s) = s |
|
163 |
|
164 val string_of = concat o map (dest_Char o Symbol.decode) |
|
165 |
|
166 val scan_term = |
|
167 scan_atom >> (Cons o string_of) || scan_var >> (Var o rpair dummyT o string_of) |
|
168 |
|
169 val parse_term = fst o Scan.finite Symbol.stopper |
|
170 (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) |
|
171 scan_term) |
|
172 o explode |
|
173 |
|
174 fun parse_solution sol = |
|
175 let |
|
176 fun dest_eq s = (tracing s; tracing(commas (space_explode "=" s)); case space_explode "=" s of |
|
177 (l :: r :: []) => parse_term (unprefix " " r) |
|
178 | _ => raise Fail "unexpected equation in prolog output") |
|
179 in |
|
180 map dest_eq (fst (split_last (space_explode "\n" sol))) |
|
181 end |
148 |
182 |
149 (* calling external interpreter and getting results *) |
183 (* calling external interpreter and getting results *) |
150 |
184 |
151 fun run p query_rel vnames = |
185 fun run p query_rel vnames = |
152 let |
186 let |
153 val cmd = Path.named_root |
187 val cmd = Path.named_root |
154 val prog = prelude ^ query_first query_rel vnames ^ write_program p |
188 val prog = prelude ^ query_first query_rel vnames ^ write_program p |
155 val prolog_file = File.tmp_path (Path.basic "prolog_file") |
189 val prolog_file = File.tmp_path (Path.basic "prolog_file") |
156 val _ = File.write prolog_file prog |
190 val _ = File.write prolog_file prog |
157 val (solution, _) = bash_output ("/usr/bin/swipl -f " ^ File.shell_path prolog_file) |
191 val (solution, _) = bash_output ("/usr/bin/swipl -f " ^ File.shell_path prolog_file) |
158 in |
192 val ts = parse_solution solution |
159 tracing ("Prolog returns result:\n" ^ solution) |
193 val _ = tracing (commas (map string_of_prol_term ts)) |
160 end |
194 in |
|
195 ts |
|
196 end |
|
197 |
|
198 (* values command *) |
|
199 |
|
200 fun mk_term (Var (s, T)) = Free (s, T) |
|
201 | mk_term (Cons s) = Const (s, dummyT) |
|
202 | mk_term (AppF (f, args)) = list_comb (Const (f, dummyT), map mk_term args) |
|
203 |
|
204 fun values ctxt soln t_compr = |
|
205 let |
|
206 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |
|
207 | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); |
|
208 val (body, Ts, fp) = HOLogic.strip_psplits split; |
|
209 val output_names = Name.variant_list (Term.add_free_names body []) |
|
210 (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) |
|
211 val output_frees = map2 (curry Free) output_names (rev Ts) |
|
212 val body = subst_bounds (output_frees, body) |
|
213 val (pred as Const (name, T), all_args) = |
|
214 case strip_comb body of |
|
215 (Const (name, T), all_args) => (Const (name, T), all_args) |
|
216 | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) |
|
217 val vnames = |
|
218 case try (map (fst o dest_Free)) all_args of |
|
219 SOME vs => vs |
|
220 | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args)) |
|
221 val ts = run (generate ctxt [name]) (translate_const name) (map first_upper vnames) |
|
222 in |
|
223 HOLogic.mk_tuple (map mk_term ts) |
|
224 end |
|
225 |
|
226 fun values_cmd print_modes soln raw_t state = |
|
227 let |
|
228 val ctxt = Toplevel.context_of state |
|
229 val t = Syntax.read_term ctxt raw_t |
|
230 val t' = values ctxt soln t |
|
231 val ty' = Term.type_of t' |
|
232 val ctxt' = Variable.auto_fixes t' ctxt |
|
233 val p = Print_Mode.with_modes print_modes (fn () => |
|
234 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
|
235 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
|
236 in Pretty.writeln p end; |
|
237 |
|
238 |
|
239 (* renewing the values command for Prolog queries *) |
|
240 |
|
241 val opt_print_modes = |
|
242 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) []; |
|
243 |
|
244 val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag |
|
245 (opt_print_modes -- Scan.optional Parse.nat ~1 -- Parse.term |
|
246 >> (fn ((print_modes, soln), t) => Toplevel.keep |
|
247 (values_cmd print_modes soln t))); |
161 |
248 |
162 end; |
249 end; |