# HG changeset patch # User bulwahn # Date 1282823352 -7200 # Node ID d171840881fddd0fb537009f154e635da6cd228d # Parent 14c1085dec028961f6a7bb4c595be63ddbaee0e6 added generation of predicates for size-limited enumeration of values diff -r 14c1085dec02 -r d171840881fd src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 13:49:12 2010 +0200 @@ -6,7 +6,7 @@ signature CODE_PROLOG = sig - type code_options = {ensure_groundness : bool} + type code_options = {ensure_groundness : bool, limited_types : (typ * int) list} val options : code_options ref datatype arith_op = Plus | Minus @@ -42,9 +42,9 @@ (* code generation options *) -type code_options = {ensure_groundness : bool} +type code_options = {ensure_groundness : bool, limited_types : (typ * int) list} -val options = Unsynchronized.ref {ensure_groundness = false}; +val options = Unsynchronized.ref {ensure_groundness = false, limited_types = []}; (* general string functions *) @@ -284,7 +284,8 @@ apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table) end -(* add implementation for ground predicates *) +(* implementation for fully enumerating predicates and + for size-limited predicates for enumerating the values of a datatype upto a specific size *) fun add_ground_typ (Conj prems) = fold add_ground_typ prems | add_ground_typ (Ground (_, T)) = insert (op =) T @@ -294,34 +295,58 @@ first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs) | mk_relname _ = raise Fail "unexpected type" +fun mk_lim_relname T = "lim_" ^ mk_relname T + (* This is copied from "pat_completeness.ML" *) fun inst_constrs_of thy (T as Type (name, _)) = map (fn (Cn,CT) => Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) (the (Datatype.get_constrs thy name)) | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) + +fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T -fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) = +fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) = if member (op =) seen T then ([], (seen, constant_table)) else let - val rel_name = mk_relname T - fun mk_impl (Const (constr_name, T)) (seen, constant_table) = + val (limited, size) = case AList.lookup (op =) limited_types T of + SOME s => (true, s) + | NONE => (false, 0) + val rel_name = (if limited then mk_lim_relname else mk_relname) T + fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) = let val constant_table' = declare_consts [constr_name] constant_table + val Ts = binder_types cT val (rec_clauses, (seen', constant_table'')) = - fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table') - val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T))) - fun mk_prem v T = Rel (mk_relname T, [v]) + fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table') + val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts)) + val lim_var = + if limited then + if recursive then [AppF ("suc", [Var "Lim"])] + else [Var "Lim"] + else [] + fun mk_prem v T' = + if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v]) + else Rel (mk_relname T', [v]) val clause = - ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]), - Conj (map2 mk_prem vars (binder_types T))) + ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]), + Conj (map2 mk_prem vars Ts)) in (clause :: flat rec_clauses, (seen', constant_table'')) end val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T - in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end - | mk_ground_impl ctxt T (seen, constant_table) = + val constrs' = (constrs ~~ map (is_recursive_constr T) constrs) + |> (fn cs => filter_out snd cs @ filter snd cs) + val (clauses, constant_table') = + apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table)) + val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero") + in + ((if limited then + cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"])) + else I) clauses, constant_table') + end + | mk_ground_impl ctxt _ T (seen, constant_table) = raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T) fun replace_ground (Conj prems) = Conj (map replace_ground prems) @@ -329,15 +354,16 @@ Rel (mk_relname T, [Var x]) | replace_ground p = p -fun add_ground_predicates ctxt (p, constant_table) = +fun add_ground_predicates ctxt limited_types (p, constant_table) = let val ground_typs = fold (add_ground_typ o snd) p [] - val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table) + val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table) val p' = map (apsnd replace_ground) p in ((flat grs) @ p', constant_table') end - + + (* rename variables to prolog-friendly names *) fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) @@ -535,7 +561,9 @@ val ctxt'' = ProofContext.init_global thy' val _ = tracing "Generating prolog program..." val (p, constant_table) = generate options ctxt'' name - |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I) + |> (if #ensure_groundness options then + add_ground_predicates ctxt'' (#limited_types options) + else I) val _ = tracing "Running prolog program..." val tss = run p (translate_const constant_table name) (map first_upper vnames) soln val _ = tracing "Restoring terms..." @@ -626,8 +654,8 @@ val thy3 = Predicate_Compile.preprocess preprocess_options const thy2 val ctxt'' = ProofContext.init_global thy3 val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname - |> add_ground_predicates ctxt'' + val (p, constant_table) = generate {ensure_groundness = true, limited_types = []} ctxt'' full_constname + |> add_ground_predicates ctxt'' (#limited_types (!options)) val _ = tracing "Running prolog program..." val [ts] = run p (translate_const constant_table full_constname) (map fst vs') (SOME 1)