1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 09:12:00 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 13:49:12 2010 +0200
1.3 @@ -6,7 +6,7 @@
1.4
1.5 signature CODE_PROLOG =
1.6 sig
1.7 - type code_options = {ensure_groundness : bool}
1.8 + type code_options = {ensure_groundness : bool, limited_types : (typ * int) list}
1.9 val options : code_options ref
1.10
1.11 datatype arith_op = Plus | Minus
1.12 @@ -42,9 +42,9 @@
1.13
1.14 (* code generation options *)
1.15
1.16 -type code_options = {ensure_groundness : bool}
1.17 +type code_options = {ensure_groundness : bool, limited_types : (typ * int) list}
1.18
1.19 -val options = Unsynchronized.ref {ensure_groundness = false};
1.20 +val options = Unsynchronized.ref {ensure_groundness = false, limited_types = []};
1.21
1.22 (* general string functions *)
1.23
1.24 @@ -284,7 +284,8 @@
1.25 apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
1.26 end
1.27
1.28 -(* add implementation for ground predicates *)
1.29 +(* implementation for fully enumerating predicates and
1.30 + for size-limited predicates for enumerating the values of a datatype upto a specific size *)
1.31
1.32 fun add_ground_typ (Conj prems) = fold add_ground_typ prems
1.33 | add_ground_typ (Ground (_, T)) = insert (op =) T
1.34 @@ -294,34 +295,58 @@
1.35 first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
1.36 | mk_relname _ = raise Fail "unexpected type"
1.37
1.38 +fun mk_lim_relname T = "lim_" ^ mk_relname T
1.39 +
1.40 (* This is copied from "pat_completeness.ML" *)
1.41 fun inst_constrs_of thy (T as Type (name, _)) =
1.42 map (fn (Cn,CT) =>
1.43 Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
1.44 (the (Datatype.get_constrs thy name))
1.45 | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
1.46 +
1.47 +fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
1.48
1.49 -fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
1.50 +fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
1.51 if member (op =) seen T then ([], (seen, constant_table))
1.52 else
1.53 let
1.54 - val rel_name = mk_relname T
1.55 - fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
1.56 + val (limited, size) = case AList.lookup (op =) limited_types T of
1.57 + SOME s => (true, s)
1.58 + | NONE => (false, 0)
1.59 + val rel_name = (if limited then mk_lim_relname else mk_relname) T
1.60 + fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
1.61 let
1.62 val constant_table' = declare_consts [constr_name] constant_table
1.63 + val Ts = binder_types cT
1.64 val (rec_clauses, (seen', constant_table'')) =
1.65 - fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
1.66 - val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))
1.67 - fun mk_prem v T = Rel (mk_relname T, [v])
1.68 + fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table')
1.69 + val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
1.70 + val lim_var =
1.71 + if limited then
1.72 + if recursive then [AppF ("suc", [Var "Lim"])]
1.73 + else [Var "Lim"]
1.74 + else []
1.75 + fun mk_prem v T' =
1.76 + if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
1.77 + else Rel (mk_relname T', [v])
1.78 val clause =
1.79 - ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
1.80 - Conj (map2 mk_prem vars (binder_types T)))
1.81 + ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
1.82 + Conj (map2 mk_prem vars Ts))
1.83 in
1.84 (clause :: flat rec_clauses, (seen', constant_table''))
1.85 end
1.86 val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
1.87 - in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
1.88 - | mk_ground_impl ctxt T (seen, constant_table) =
1.89 + val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
1.90 + |> (fn cs => filter_out snd cs @ filter snd cs)
1.91 + val (clauses, constant_table') =
1.92 + apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table))
1.93 + val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero")
1.94 + in
1.95 + ((if limited then
1.96 + cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"]))
1.97 + else I) clauses, constant_table')
1.98 + end
1.99 + | mk_ground_impl ctxt _ T (seen, constant_table) =
1.100 raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
1.101
1.102 fun replace_ground (Conj prems) = Conj (map replace_ground prems)
1.103 @@ -329,15 +354,16 @@
1.104 Rel (mk_relname T, [Var x])
1.105 | replace_ground p = p
1.106
1.107 -fun add_ground_predicates ctxt (p, constant_table) =
1.108 +fun add_ground_predicates ctxt limited_types (p, constant_table) =
1.109 let
1.110 val ground_typs = fold (add_ground_typ o snd) p []
1.111 - val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
1.112 + val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
1.113 val p' = map (apsnd replace_ground) p
1.114 in
1.115 ((flat grs) @ p', constant_table')
1.116 end
1.117 -
1.118 +
1.119 +
1.120 (* rename variables to prolog-friendly names *)
1.121
1.122 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
1.123 @@ -535,7 +561,9 @@
1.124 val ctxt'' = ProofContext.init_global thy'
1.125 val _ = tracing "Generating prolog program..."
1.126 val (p, constant_table) = generate options ctxt'' name
1.127 - |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I)
1.128 + |> (if #ensure_groundness options then
1.129 + add_ground_predicates ctxt'' (#limited_types options)
1.130 + else I)
1.131 val _ = tracing "Running prolog program..."
1.132 val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
1.133 val _ = tracing "Restoring terms..."
1.134 @@ -626,8 +654,8 @@
1.135 val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
1.136 val ctxt'' = ProofContext.init_global thy3
1.137 val _ = tracing "Generating prolog program..."
1.138 - val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
1.139 - |> add_ground_predicates ctxt''
1.140 + val (p, constant_table) = generate {ensure_groundness = true, limited_types = []} ctxt'' full_constname
1.141 + |> add_ground_predicates ctxt'' (#limited_types (!options))
1.142 val _ = tracing "Running prolog program..."
1.143 val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
1.144 (SOME 1)