equal
deleted
inserted
replaced
466 val satisfies_ref : (unit -> bool) option ref = ref NONE; |
466 val satisfies_ref : (unit -> bool) option ref = ref NONE; |
467 |
467 |
468 fun satisfies thy ct witnesses = |
468 fun satisfies thy ct witnesses = |
469 let |
469 let |
470 fun evl code ((vs, ty), t) deps ct = |
470 fun evl code ((vs, ty), t) deps ct = |
471 let |
471 eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref) |
472 val t0 = Thm.term_of ct |
472 code (t, ty) witnesses; |
473 val _ = (Term.map_types o Term.map_atyps) (fn _ => |
|
474 error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type")) |
|
475 t0; |
|
476 in |
|
477 eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref) |
|
478 code (t, ty) witnesses |
|
479 end; |
|
480 in eval_term thy evl ct end; |
473 in eval_term thy evl ct end; |
481 |
474 |
482 fun filter_generatable thy consts = |
475 fun filter_generatable thy consts = |
483 let |
476 let |
484 val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |
477 val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |