equal
deleted
inserted
replaced
23 |
23 |
24 val discard : computer -> unit |
24 val discard : computer -> unit |
25 |
25 |
26 val setup : theory -> theory |
26 val setup : theory -> theory |
27 |
27 |
|
28 val print_encoding : bool ref |
|
29 |
28 end |
30 end |
29 |
31 |
30 structure Compute :> COMPUTE = struct |
32 structure Compute :> COMPUTE = struct |
|
33 |
|
34 val print_encoding = ref false |
31 |
35 |
32 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
36 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
33 |
37 |
34 (* Terms are mapped to integer codes *) |
38 (* Terms are mapped to integer codes *) |
35 structure Encode :> |
39 structure Encode :> |
259 BARRAS => ProgBarras (AM_Interpreter.compile rules) |
263 BARRAS => ProgBarras (AM_Interpreter.compile rules) |
260 | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules) |
264 | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules) |
261 | HASKELL => ProgHaskell (AM_GHC.compile rules) |
265 | HASKELL => ProgHaskell (AM_GHC.compile rules) |
262 | SML => ProgSML (AM_SML.compile rules) |
266 | SML => ProgSML (AM_SML.compile rules) |
263 |
267 |
264 (* val _ = print (Encode.fold (fn x => fn s => x::s) encoding [])*) |
|
265 |
|
266 fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
268 fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
267 |
269 |
268 val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable |
270 val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable |
269 |
271 |
270 in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end |
272 in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end |
288 | run (ProgHaskell p) = AM_GHC.run p |
290 | run (ProgHaskell p) = AM_GHC.run p |
289 | run (ProgSML p) = AM_SML.run p |
291 | run (ProgSML p) = AM_SML.run p |
290 val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct |
292 val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct |
291 val thy = Theory.merge (Theory.deref rthy, ctthy) |
293 val thy = Theory.merge (Theory.deref rthy, ctthy) |
292 val (encoding, t) = report "remove_types" (fn () => remove_types encoding t) |
294 val (encoding, t) = report "remove_types" (fn () => remove_types encoding t) |
|
295 val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else () |
293 val t = report "run" (fn () => run prog t) |
296 val t = report "run" (fn () => run prog t) |
294 val t = report "infer_types" (fn () => infer_types naming encoding ty t) |
297 val t = report "infer_types" (fn () => infer_types naming encoding ty t) |
295 in |
298 in |
296 t |
299 t |
297 end |
300 end |
338 (* theory setup *) |
341 (* theory setup *) |
339 |
342 |
340 fun compute_oracle (thy, Param (r, naming, ct)) = |
343 fun compute_oracle (thy, Param (r, naming, ct)) = |
341 let |
344 let |
342 val _ = Theory.assert_super (theory_of r) thy |
345 val _ = Theory.assert_super (theory_of r) thy |
343 val t' = compute r naming ct |
346 val t' = timeit (fn () => compute r naming ct) |
344 val eq = Logic.mk_equals (term_of ct, t') |
347 val eq = Logic.mk_equals (term_of ct, t') |
345 val hyps = hyps_of r |
348 val hyps = hyps_of r |
346 val shyptab = shyptab_of r |
349 val shyptab = shyptab_of r |
347 fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab |
350 fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab |
348 fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab |
351 fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab |