src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
changeset 39800 17e29ddd538e
parent 39725 4f4dd39a1e58
child 40924 a9be7f26b4e6
equal deleted inserted replaced
39799:fdbea66eae4b 39800:17e29ddd538e
    98 
    98 
    99 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    99 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
   100 
   100 
   101 setup {* Code_Prolog.map_code_options (K 
   101 setup {* Code_Prolog.map_code_options (K 
   102   {ensure_groundness = true,
   102   {ensure_groundness = true,
       
   103    limit_globally = NONE,
   103    limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
   104    limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
   104    limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
   105    limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
   105     (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
   106     (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
   106    replacing =
   107    replacing =
   107      [(("repP", "limited_repP"), "lim_repIntPa"),
   108      [(("repP", "limited_repP"), "lim_repIntPa"),