--- a/CONTRIBUTORS Thu Nov 12 15:10:27 2009 +0100
+++ b/CONTRIBUTORS Thu Nov 12 15:50:05 2009 +0100
@@ -6,7 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
-
+* November 2009: Lukas Bulwahn, TUM
+ Predicate Compiler: a compiler for inductive predicates to equational specfications
+
* November 2009: Sascha Boehme, TUM
HOL-Boogie: an interactive prover back-end for Boogie and VCC
--- a/NEWS Thu Nov 12 15:10:27 2009 +0100
+++ b/NEWS Thu Nov 12 15:50:05 2009 +0100
@@ -37,6 +37,9 @@
*** HOL ***
+* New commands "code_pred" and "values" to invoke the predicate compiler
+and to enumerate values of inductive predicates.
+
* Combined former theories Divides and IntDiv to one theory Divides
in the spirit of other number theory theories in HOL; some constants
(and to a lesser extent also facts) have been suffixed with _nat und _int
--- a/src/HOL/Code_Evaluation.thy Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy Thu Nov 12 15:50:05 2009 +0100
@@ -145,7 +145,7 @@
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
code_const "term_of \<Colon> String.literal \<Rightarrow> term"
- (Eval "HOLogic.mk'_message'_string")
+ (Eval "HOLogic.mk'_literal")
code_reserved Eval HOLogic
--- a/src/HOL/Datatype.thy Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Datatype.thy Thu Nov 12 15:50:05 2009 +0100
@@ -562,6 +562,14 @@
Sumr :: "('b => 'c) => 'a + 'b => 'c"
"Sumr == sum_case undefined"
+lemma [code]:
+ "Suml f (Inl x) = f x"
+ by (simp add: Suml_def)
+
+lemma [code]:
+ "Sumr f (Inr x) = f x"
+ by (simp add: Sumr_def)
+
lemma Suml_inject: "Suml f = Suml g ==> f = g"
by (unfold Suml_def) (erule sum_case_inject)
--- a/src/HOL/Predicate.thy Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Predicate.thy Thu Nov 12 15:50:05 2009 +0100
@@ -828,28 +828,6 @@
code_abort not_unique
-text {* dummy setup for @{text code_pred} and @{text values} keywords *}
-
-ML {*
-local
-
-structure P = OuterParse;
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-in
-
-val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
- OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
- OuterKeyword.diag ((opt_modes -- P.term)
- >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
- (K ())));
-
-end
-*}
-
no_notation
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
--- a/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 15:50:05 2009 +0100
@@ -10,7 +10,7 @@
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
- * Fixed soundness bug related to sets of sets
+ * Fixed soundness bugs related to sets and sets of sets
* Fixed monotonicity check
* Fixed error in display of uncurried constants
* Speeded up scope enumeration
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 15:50:05 2009 +0100
@@ -1448,7 +1448,7 @@
fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
| Op2 (Apply, _, R, u1, u2) =>
if is_Cst Unrep u2 andalso is_set_type (type_of u1)
- andalso not (is_opt_rep (rep_of u1)) then
+ andalso is_FreeName u1 then
false_atom
else
to_apply R u1 u2
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 15:50:05 2009 +0100
@@ -96,6 +96,7 @@
val nickname_of : nut -> string
val is_skolem_name : nut -> bool
val is_eval_name : nut -> bool
+ val is_FreeName : nut -> bool
val is_Cst : cst -> nut -> bool
val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
val map_nut : (nut -> nut) -> nut -> nut
@@ -367,6 +368,8 @@
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
+fun is_FreeName (FreeName _) = true
+ | is_FreeName _ = false
(* cst -> nut -> bool *)
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
@@ -764,9 +767,8 @@
(* A nut is said to be constructive if whenever it evaluates to unknown in our
three-valued logic, it would evaluate to a unrepresentable value ("unrep")
- according to the HOL semantics. For example, "Suc n" is
- constructive if "n" is representable or "Unrep", because unknown implies
- unrep. *)
+ according to the HOL semantics. For example, "Suc n" is constructive if "n"
+ is representable or "Unrep", because unknown implies unrep. *)
(* nut -> bool *)
fun is_constructive u =
is_Cst Unrep u orelse
@@ -830,13 +832,9 @@
else if is_Cst Unrep u2 then
if is_constructive u1 then
Cst (Unrep, T, R)
- else if is_boolean_type T andalso not (is_opt_rep (rep_of u1)) then
- (* Selectors are an unfortunate exception to the rule that non-"Opt"
- predicates return "False" for unrepresentable domain values. *)
- case u1 of
- ConstName (s, _, _) => if is_sel s then unknown_boolean T R
- else Cst (False, T, Formula Neut)
- | _ => Cst (False, T, Formula Neut)
+ else if is_boolean_type T then
+ if is_FreeName u1 then Cst (False, T, Formula Neut)
+ else unknown_boolean T R
else case u1 of
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
Cst (Unrep, T, R)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 15:50:05 2009 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML
Author: Lukas Bulwahn, TU Muenchen
-FIXME.
+Entry point for the predicate compiler; definition of Toplevel commands code_pred and values
*)
signature PREDICATE_COMPILE =
@@ -10,7 +10,7 @@
val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
end;
-structure Predicate_Compile : PREDICATE_COMPILE =
+structure Predicate_Compile (*: PREDICATE_COMPILE*) =
struct
(* options *)
@@ -105,12 +105,16 @@
(Graph.strong_conn gr) thy
end
-fun extract_options ((modes, raw_options), const) =
+fun extract_options (((expected_modes, proposed_modes), raw_options), const) =
let
fun chk s = member (op =) raw_options s
in
Options {
- expected_modes = Option.map (pair const) modes,
+ expected_modes = Option.map (pair const) expected_modes,
+ proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [],
+ proposed_names =
+ map_filter
+ (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes,
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
@@ -125,17 +129,18 @@
}
end
-fun code_pred_cmd ((modes, raw_options), raw_const) lthy =
+fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy =
let
val thy = ProofContext.theory_of lthy
val const = Code.read_const thy raw_const
- val options = extract_options ((modes, raw_options), const)
+ val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
in
if (is_inductify options) then
let
val lthy' = LocalTheory.theory (preprocess options const) lthy
|> LocalTheory.checkpoint
- val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
+ val const =
+ case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
SOME c => c
| NONE => const
val _ = print_step options "Starting Predicate Compile Core..."
@@ -146,7 +151,7 @@
Predicate_Compile_Core.code_pred_cmd options raw_const lthy
end
-val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
+val setup = Predicate_Compile_Core.setup
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
@@ -157,35 +162,25 @@
(* Parser for mode annotations *)
-(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
-datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
-
-val parse_argmode' =
- ((Args.$$$ "i" || Args.$$$ "o") >> Argmode) ||
- (Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple)
-
-fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss)
+fun parse_mode_basic_expr xs =
+ (Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
+ Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
+and parse_mode_tuple_expr xs =
+ (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
+ xs
+and parse_mode_expr xs =
+ (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
-val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]"
- >> (fn m => flat (map_index
- (fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else []
- | (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m))
-
-val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
- >> map (rpair (NONE : int list option))
-
-fun gen_parse_mode smode_parser =
- (Scan.optional
- ((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") [])
- -- smode_parser
-
-val parse_mode = gen_parse_mode parse_smode
-
-val parse_mode' = gen_parse_mode parse_smode'
+val mode_and_opt_proposal = parse_mode_expr --
+ Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
val opt_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
+ P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") []
+
+val opt_expected_modes =
+ Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
+ P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
(* Parser for options *)
@@ -198,10 +193,10 @@
val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME)
+val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE
+ P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
val value_options =
let
@@ -217,7 +212,8 @@
val _ = OuterSyntax.local_theory_to_proof "code_pred"
"prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+ OuterKeyword.thy_goal
+ (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
(opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 15:50:05 2009 +0100
@@ -21,6 +21,7 @@
(fn (i, is) =>
string_of_int i ^ (case is of NONE => ""
| SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js)
+(* FIXME: remove! *)
fun string_of_mode (iss, is) = space_implode " -> " (map
(fn NONE => "X"
@@ -28,10 +29,118 @@
(iss @ [SOME is]));
fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
- "predmode: " ^ (string_of_mode predmode) ^
+ "predmode: " ^ (string_of_mode predmode) ^
(if null param_modes then "" else
"; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
+(* new datatype for mode *)
+
+datatype mode' = Bool | Input | Output | Pair of mode' * mode' | Fun of mode' * mode'
+
+(* equality of instantiatedness with respect to equivalences:
+ Pair Input Input == Input and Pair Output Output == Output *)
+fun eq_mode' (Fun (m1, m2), Fun (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4)
+ | eq_mode' (Pair (m1, m2), Pair (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4)
+ | eq_mode' (Pair (m1, m2), Input) = eq_mode' (m1, Input) andalso eq_mode' (m2, Input)
+ | eq_mode' (Pair (m1, m2), Output) = eq_mode' (m1, Output) andalso eq_mode' (m2, Output)
+ | eq_mode' (Input, Pair (m1, m2)) = eq_mode' (Input, m1) andalso eq_mode' (Input, m2)
+ | eq_mode' (Output, Pair (m1, m2)) = eq_mode' (Output, m1) andalso eq_mode' (Output, m2)
+ | eq_mode' (Input, Input) = true
+ | eq_mode' (Output, Output) = true
+ | eq_mode' (Bool, Bool) = true
+ | eq_mode' _ = false
+
+(* name: binder_modes? *)
+fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
+ | strip_fun_mode Bool = []
+ | strip_fun_mode _ = error "Bad mode for strip_fun_mode"
+
+fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
+ | dest_fun_mode mode = [mode]
+
+fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
+ | dest_tuple_mode _ = []
+
+fun string_of_mode' mode' =
+ let
+ fun string_of_mode1 Input = "i"
+ | string_of_mode1 Output = "o"
+ | string_of_mode1 Bool = "bool"
+ | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")"
+ and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^ string_of_mode2 m2
+ | string_of_mode2 mode = string_of_mode1 mode
+ and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2
+ | string_of_mode3 mode = string_of_mode2 mode
+ in string_of_mode3 mode' end
+
+fun ascii_string_of_mode' mode' =
+ let
+ fun ascii_string_of_mode' Input = "i"
+ | ascii_string_of_mode' Output = "o"
+ | ascii_string_of_mode' Bool = "b"
+ | ascii_string_of_mode' (Pair (m1, m2)) =
+ "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+ | ascii_string_of_mode' (Fun (m1, m2)) =
+ "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
+ and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
+ ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
+ | ascii_string_of_mode'_Fun Bool = "B"
+ | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m
+ and ascii_string_of_mode'_Pair (Pair (m1, m2)) =
+ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+ | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
+ in ascii_string_of_mode'_Fun mode' end
+
+fun translate_mode T (iss, is) =
+ let
+ val Ts = binder_types T
+ val (Ts1, Ts2) = chop (length iss) Ts
+ fun translate_smode Ts is =
+ let
+ fun translate_arg (i, T) =
+ case AList.lookup (op =) is (i + 1) of
+ SOME NONE => Input
+ | SOME (SOME its) =>
+ let
+ fun translate_tuple (i, T) = if member (op =) its (i + 1) then Input else Output
+ in
+ foldr1 Pair (map_index translate_tuple (HOLogic.strip_tupleT T))
+ end
+ | NONE => Output
+ in map_index translate_arg Ts end
+ fun mk_mode arg_modes = foldr1 Fun (arg_modes @ [Bool])
+ val param_modes =
+ map (fn (T, NONE) => Input | (T, SOME is) => mk_mode (translate_smode (binder_types T) is))
+ (Ts1 ~~ iss)
+ in
+ mk_mode (param_modes @ translate_smode Ts2 is)
+ end;
+
+fun translate_mode' nparams mode' =
+ let
+ fun err () = error "translate_mode': given mode cannot be translated"
+ val (m1, m2) = chop nparams (strip_fun_mode mode')
+ val translate_to_tupled_mode =
+ (map_filter I) o (map_index (fn (i, m) =>
+ if eq_mode' (m, Input) then SOME (i + 1)
+ else if eq_mode' (m, Output) then NONE
+ else err ()))
+ val translate_to_smode =
+ (map_filter I) o (map_index (fn (i, m) =>
+ if eq_mode' (m, Input) then SOME (i + 1, NONE)
+ else if eq_mode' (m, Output) then NONE
+ else SOME (i + 1, SOME (translate_to_tupled_mode (dest_tuple_mode m)))))
+ fun translate_to_param_mode m =
+ case rev (dest_fun_mode m) of
+ Bool :: _ :: _ => SOME (translate_to_smode (strip_fun_mode m))
+ | _ => if eq_mode' (m, Input) then NONE else err ()
+ in
+ (map translate_to_param_mode m1, translate_to_smode m2)
+ end
+
+fun string_of_mode thy constname mode =
+ string_of_mode' (translate_mode (Sign.the_const_type thy constname) mode)
+
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
@@ -40,8 +149,6 @@
fun conjuncts t = conjuncts_aux t [];
-(* syntactic functions *)
-
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
| is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
| is_equationlike_term _ = false
@@ -70,8 +177,23 @@
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
| is_predT _ = false
-
+(* guessing number of parameters *)
+fun find_indexes pred xs =
+ let
+ fun find is n [] = is
+ | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
+ in rev (find [] 0 xs) end;
+
+fun guess_nparams T =
+ let
+ val argTs = binder_types T
+ val nparams = fold Integer.max
+ (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
+ in nparams end;
+
(*** check if a term contains only constructor functions ***)
+(* FIXME: constructor terms are supposed to be seen in the way the code generator
+ sees constructors.*)
fun is_constrt thy =
let
val cnstrs = flat (maps
@@ -159,7 +281,9 @@
(* Different options for compiler *)
datatype options = Options of {
- expected_modes : (string * mode list) option,
+ expected_modes : (string * mode' list) option,
+ proposed_modes : (string * mode' list) list,
+ proposed_names : ((string * mode') * string) list,
show_steps : bool,
show_proof_trace : bool,
show_intermediate_results : bool,
@@ -175,6 +299,10 @@
};
fun expected_modes (Options opt) = #expected_modes opt
+fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name
+fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode')
+ (#proposed_names opt) (name, mode)
+
fun show_steps (Options opt) = #show_steps opt
fun show_intermediate_results (Options opt) = #show_intermediate_results opt
fun show_proof_trace (Options opt) = #show_proof_trace opt
@@ -190,6 +318,8 @@
val default_options = Options {
expected_modes = NONE,
+ proposed_modes = [],
+ proposed_names = [],
show_steps = false,
show_intermediate_results = false,
show_proof_trace = false,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 15:50:05 2009 +0100
@@ -9,7 +9,7 @@
val setup : theory -> theory
val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
- val values_cmd : string list -> Predicate_Compile_Aux.smode option list option
+ val values_cmd : string list -> Predicate_Compile_Aux.mode' option list option
-> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
val register_predicate : (string * thm list * thm * int) -> theory -> theory
val register_intros : string * thm list -> theory -> theory
@@ -36,7 +36,7 @@
val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
option Unsynchronized.ref
- val code_pred_intros_attrib : attribute
+ val code_pred_intro_attrib : attribute
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
datatype compilation_funs = CompilationFuns of {
@@ -128,32 +128,25 @@
(* destruction of intro rules *)
(* FIXME: look for other place where this functionality was used before *)
-fun strip_intro_concl nparams intro = let
- val _ $ u = Logic.strip_imp_concl intro
- val (pred, all_args) = strip_comb u
- val (params, args) = chop nparams all_args
-in (pred, (params, args)) end
+fun strip_intro_concl nparams intro =
+ let
+ val _ $ u = Logic.strip_imp_concl intro
+ val (pred, all_args) = strip_comb u
+ val (params, args) = chop nparams all_args
+ in (pred, (params, args)) end
(** data structures **)
-(* new datatype for modes: *)
-(*
-datatype instantiation = Input | Output
-type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode
-type mode = arg_mode list
-type tmode = Mode of mode *
-*)
-
fun gen_split_smode (mk_tuple, strip_tuple) smode ts =
let
fun split_tuple' _ _ [] = ([], [])
| split_tuple' is i (t::ts) =
- (if i mem is then apfst else apsnd) (cons t)
+ (if member (op =) is i then apfst else apsnd) (cons t)
(split_tuple' is (i+1) ts)
fun split_tuple is t = split_tuple' is 1 (strip_tuple t)
fun split_smode' _ _ [] = ([], [])
| split_smode' smode i (t::ts) =
- (if i mem (map fst smode) then
+ (if member (op =) (map fst smode) i then
case (the (AList.lookup (op =) smode i)) of
NONE => apfst (cons t)
| SOME is =>
@@ -274,7 +267,7 @@
(AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode)
fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
- of NONE => error ("No function defined for mode " ^ string_of_mode mode ^
+ of NONE => error ("No function defined for mode " ^ string_of_mode thy name mode ^
" of predicate " ^ name)
| SOME data => data;
@@ -291,7 +284,7 @@
(AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode)
fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of
- NONE => error ("No random function defined for mode " ^ string_of_mode mode ^
+ NONE => error ("No random function defined for mode " ^ string_of_mode thy name mode ^
" of predicate " ^ name)
| SOME data => data
@@ -310,7 +303,7 @@
fun the_depth_limited_function_data thy name mode =
case lookup_depth_limited_function_data thy name mode of
- NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
+ NONE => error ("No depth-limited function defined for mode " ^ string_of_mode thy name mode
^ " of predicate " ^ name)
| SOME data => data
@@ -325,7 +318,7 @@
(AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode)
fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode
- of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode
+ of NONE => error ("No annotated function defined for mode " ^ string_of_mode thy name mode
^ " of predicate " ^ name)
| SOME data => data
@@ -337,17 +330,17 @@
(* diagnostic display functions *)
-fun print_modes options modes =
+fun print_modes options thy modes =
if show_modes options then
tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- string_of_mode ms)) modes))
+ (string_of_mode thy s) ms)) modes))
else ()
fun print_pred_mode_table string_of_entry thy pred_mode_table =
let
- fun print_mode pred (mode, entry) = "mode : " ^ (string_of_mode mode)
- ^ (string_of_entry pred mode entry)
+ fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode thy pred mode
+ ^ string_of_entry pred mode entry
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
val _ = tracing (cat_lines (map print_pred pred_mode_table))
@@ -417,25 +410,29 @@
fun print (pred, modes) u =
let
val _ = writeln ("predicate: " ^ pred)
- val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
- in u end
+ val _ = writeln ("modes: " ^ (commas (map (string_of_mode thy pred) modes)))
+ in u end
in
fold print (all_modes_of thy) ()
end
(* validity checks *)
-fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =
- case expected_modes options of
- SOME (s, ms) => (case AList.lookup (op =) modes s of
- SOME modes =>
- if not (eq_set (op =) (ms, modes)) then
- error ("expected modes were not inferred:\n"
- ^ "inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes)
- ^ "\n expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
- else ()
- | NONE => ())
- | NONE => ()
+fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes =
+ case expected_modes options of
+ SOME (s, ms) => (case AList.lookup (op =) modes s of
+ SOME modes =>
+ let
+ val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
+ in
+ if not (eq_set eq_mode' (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ()
(* importing introduction rules *)
@@ -464,7 +461,7 @@
val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred))
val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i))
(1 upto nparams)) ctxt'
- val params = map Free (param_names ~~ paramTs)
+ val params = map2 (curry Free) param_names paramTs
in (((outp_pred, params), []), ctxt') end
| import_intros inp_pred nparams (th :: ths) ctxt =
let
@@ -511,7 +508,7 @@
let
val (_, (_, args)) = strip_intro_concl nparams intro
val prems = Logic.strip_imp_prems intro
- val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
val frees = (fold o fold_aterms)
(fn t as Free _ =>
if member (op aconv) params t then I else insert (op aconv) t
@@ -567,25 +564,6 @@
Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
end;
-(* special case: predicate with no introduction rule *)
-fun noclause thy predname elim = let
- val T = (Logic.unvarifyT o Sign.the_const_type thy) predname
- val Ts = binder_types T
- val names = Name.variant_list []
- (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))
- val vs = map2 (curry Free) names Ts
- val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs))
- val intro_t = Logic.mk_implies (@{prop False}, clausehd)
- val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
- val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
- val intro = Goal.prove (ProofContext.init thy) names [] intro_t
- (fn _ => etac @{thm FalseE} 1)
- val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
- (fn _ => etac elim 1)
-in
- ([intro], elim)
-end
-
fun expand_tuples_elim th = th
(* updaters *)
@@ -617,7 +595,6 @@
val elim =
(Drule.standard o Skip_Proof.make_thm thy)
(mk_casesrule (ProofContext.init thy) pred nparams intros)
- val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
in
mk_pred_data ((intros, SOME elim, nparams), no_compilation)
end
@@ -653,23 +630,10 @@
end;
*)
-(* guessing number of parameters *)
-fun find_indexes pred xs =
- let
- fun find is n [] = is
- | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
- in rev (find [] 0 xs) end;
-
-fun guess_nparams T =
+fun add_intro thm thy =
let
- val argTs = binder_types T
- val nparams = fold Integer.max
- (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
- in nparams end;
-
-fun add_intro thm thy = let
- val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
- fun cons_intro gr =
+ val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
+ fun cons_intro gr =
case try (Graph.get_node gr) name of
SOME pred_data => Graph.map_node name (map_pred_data
(apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
@@ -680,13 +644,15 @@
in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end;
in PredData.map cons_intro thy end
-fun set_elim thm = let
+fun set_elim thm =
+ let
val (name, _) = dest_Const (fst
(strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
fun set (intros, _, nparams) = (intros, SOME thm, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-fun set_nparams name nparams = let
+fun set_nparams name nparams =
+ let
fun set (intros, elim, _ ) = (intros, elim, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
@@ -974,7 +940,6 @@
(iss ~~ args1)))
end
end)) (AList.lookup op = modes name)
-
in
case strip_comb (Envir.eta_contract t) of
(Const (name, _), args) => the_default default (mk_modes name args)
@@ -1081,7 +1046,7 @@
if show_mode_inference options then
let
val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m)
+ p ^ " violates mode " ^ string_of_mode thy p m)
val _ = tracing (string_of_clause thy p (nth rs i))
in () end
else ()
@@ -1170,10 +1135,6 @@
| mk_Eval_of additional_arguments ((x, T), SOME mode) names =
let
val Ts = binder_types T
- (*val argnames = Name.variant_list names
- (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- val args = map Free (argnames ~~ Ts)
- val (inargs, outargs) = split_smode mode args*)
fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
| mk_split_lambda [x] t = lambda x t
| mk_split_lambda xs t =
@@ -1200,7 +1161,7 @@
val vnames = Name.variant_list names
(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
(1 upto length Ts))
- val args = map Free (vnames ~~ Ts)
+ val args = map2 (curry Free) vnames Ts
fun split_args (i, arg) (ins, outs) =
if member (op =) pis i then
(arg::ins, outs)
@@ -1289,18 +1250,18 @@
let
val names = Term.add_free_names t [];
val Ts = binder_types (fastype_of t);
- val vs = map Free
- (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
+ val vs = map2 (curry Free)
+ (Name.variant_list names (replicate (length Ts) "x")) Ts
in
fold_rev lambda vs (f (list_comb (t, vs)))
end;
-fun compile_param compilation_modifiers compfuns thy (NONE, t) = t
- | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) =
+fun compile_param compilation_modifiers compfuns thy NONE t = t
+ | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms))) t =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, args') = chop (length ms) args
- val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+ val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params
val f' =
case f of
Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode,
@@ -1316,7 +1277,7 @@
case strip_comb t of
(Const (name, T), params) =>
let
- val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+ val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params
val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode
val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T
in
@@ -1428,8 +1389,12 @@
val vnames = Name.variant_list (all_vs @ param_vs)
(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
pis)
- in if null pis then []
- else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
+ in
+ if null pis then
+ []
+ else
+ [HOLogic.mk_tuple (map2 (curry Free) vnames (map (fn j => nth Ts (j - 1)) pis))]
+ end
val in_ts = maps mk_input_term (snd mode)
val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
@@ -1472,7 +1437,7 @@
map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
- val params = map Free (param_names ~~ Ts1')
+ val params = map2 (curry Free) param_names Ts1'
fun mk_args (i, T) argnames =
let
val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
@@ -1490,17 +1455,17 @@
val vnames = Name.variant_list (param_names @ argnames)
(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
(1 upto (length Ts)))
- in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ argnames) end
+ in (HOLogic.mk_tuple (map2 (curry Free) vnames Ts), vnames @ argnames) end
end
val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
val (inargs, outargs) = split_smode is args
val param_names' = Name.variant_list (param_names @ argnames)
(map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
- val param_vs = map Free (param_names' ~~ Ts1)
+ val param_vs = map2 (curry Free) param_names' Ts1
val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) []
val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args))
val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args))
- val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
+ val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) param_vs params'
val funargs = params @ inargs
val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
@@ -1520,24 +1485,20 @@
(introthm, elimthm)
end;
-fun create_constname_of_mode thy prefix name mode =
+fun create_constname_of_mode options thy prefix name T mode =
let
- fun string_of_mode mode = if null mode then "0"
- else space_implode "_"
- (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
- ^ space_implode "p" (map string_of_int pis)) mode)
- val HOmode = space_implode "_and_"
- (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
+ val system_proposal = prefix ^ (Long_Name.base_name name)
+ ^ "_" ^ ascii_string_of_mode' (translate_mode T mode)
+ val name = the_default system_proposal (proposed_names options name (translate_mode T mode))
in
- (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
- (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
+ Sign.full_bname thy name
end;
fun split_tupleT is T =
let
fun split_tuple' _ _ [] = ([], [])
| split_tuple' is i (T::Ts) =
- (if i mem is then apfst else apsnd) (cons T)
+ (if member (op =) is i then apfst else apsnd) (cons T)
(split_tuple' is (i+1) Ts)
in
split_tuple' is 1 (HOLogic.strip_tupleT T)
@@ -1550,7 +1511,8 @@
fun mk_proj i j t =
(if i = j then I else HOLogic.mk_fst)
(funpow (i - 1) HOLogic.mk_snd t)
- fun mk_arg' i (si, so) = if i mem pis then
+ fun mk_arg' i (si, so) =
+ if member (op =) pis i then
(mk_proj si ni xin, (si+1, so))
else
(mk_proj so (n - ni) xout, (si, so+1))
@@ -1559,12 +1521,12 @@
HOLogic.mk_tuple args
end
-fun create_definitions preds (name, modes) thy =
+fun create_definitions options preds (name, modes) thy =
let
val compfuns = PredicateCompFuns.compfuns
val T = AList.lookup (op =) preds name |> the
fun create_definition (mode as (iss, is)) thy = let
- val mode_cname = create_constname_of_mode thy "" name mode
+ val mode_cname = create_constname_of_mode options thy "" name T mode
val mode_cbasename = Long_Name.base_name mode_cname
val Ts = binder_types T
val (Ts1, Ts2) = chop (length iss) Ts
@@ -1573,16 +1535,9 @@
val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
val names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- (* old *)
- (*
- val xs = map Free (names ~~ (Ts1' @ Ts2))
- val (xparams, xargs) = chop (length iss) xs
- val (xins, xouts) = split_smode is xargs
- *)
- (* new *)
val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
- val xparams = map Free (param_names ~~ Ts1')
+ val xparams = map2 (curry Free) param_names Ts1'
fun mk_vars (i, T) names =
let
val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
@@ -1634,13 +1589,13 @@
fold create_definition modes thy
end;
-fun define_functions comp_modifiers compfuns preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
let
val T = AList.lookup (op =) preds name |> the
fun create_definition mode thy =
let
val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
- val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+ val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
in
thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
@@ -1672,8 +1627,8 @@
(* MAJOR FIXME: prove_params should be simple
- different form of introrule for parameters ? *)
-fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1)
- | prove_param thy (m as SOME (Mode (mode, is, ms)), t) =
+fun prove_param thy NONE t = TRY (rtac @{thm refl} 1)
+ | prove_param thy (m as SOME (Mode (mode, is, ms))) t =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, _) = chop (length ms) args
@@ -1690,7 +1645,7 @@
THEN print_tac "prove_param"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- THEN (EVERY (map (prove_param thy) (ms ~~ params)))
+ THEN (EVERY (map2 (prove_param thy) ms params))
THEN (REPEAT_DETERM (atac 1))
end
@@ -1711,7 +1666,7 @@
(* work with parameter arguments *)
THEN (atac 1)
THEN (print_tac "parameter goal")
- THEN (EVERY (map (prove_param thy) (ms ~~ args1)))
+ THEN (EVERY (map2 (prove_param thy) ms args1))
THEN (REPEAT_DETERM (atac 1))
end
| _ => rtac @{thm bindI} 1
@@ -1804,8 +1759,7 @@
THEN rtac @{thm not_predI} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN (REPEAT_DETERM (atac 1))
- (* FIXME: work with parameter arguments *)
- THEN (EVERY (map (prove_param thy) (param_modes ~~ params)))
+ THEN (EVERY (map2 (prove_param thy) param_modes params))
else
rtac @{thm not_predI'} 1)
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
@@ -1888,8 +1842,9 @@
*)
(* TODO: remove function *)
-fun prove_param2 thy (NONE, t) = all_tac
- | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let
+fun prove_param2 thy NONE t = all_tac
+ | prove_param2 thy (m as SOME (Mode (mode, is, ms))) t =
+ let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, _) = chop (length ms) args
val f_tac = case f of
@@ -1898,11 +1853,11 @@
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term"
- in
+ in
print_tac "before simplification in prove_args:"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- THEN (EVERY (map (prove_param2 thy) (ms ~~ params)))
+ THEN (EVERY (map2 (prove_param2 thy) ms params))
end
@@ -1916,7 +1871,7 @@
(prop_of (predfun_elim_of thy name mode))))
THEN (etac (predfun_elim_of thy name mode) 1)
THEN print_tac "prove_expr2"
- THEN (EVERY (map (prove_param2 thy) (ms ~~ args)))
+ THEN (EVERY (map2 (prove_param2 thy) ms args))
THEN print_tac "finished prove_expr2"
| _ => etac @{thm bindE} 1)
@@ -1987,7 +1942,7 @@
[predfun_definition_of thy (the name) (iss, is)]) 1
THEN etac @{thm not_predE} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
- THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
+ THEN (EVERY (map2 (prove_param2 thy) param_modes params))
else
etac @{thm not_predE'} 1)
THEN rec_tac
@@ -2078,7 +2033,7 @@
fun dest_prem thy params t =
(case strip_comb t of
- (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
+ (v as Free _, ts) => if member (op =) params v then Prem (ts, v) else Sidecond t
| (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
Prem (ts, t) => Negprem (ts, t)
| Negprem _ => error ("Double negation not allowed in premise: " ^
@@ -2091,7 +2046,7 @@
else Sidecond t
| _ => Sidecond t)
-fun prepare_intrs thy prednames intros =
+fun prepare_intrs options thy prednames intros =
let
val intrs = map prop_of intros
val nparams = nparams_of thy (hd prednames)
@@ -2108,7 +2063,7 @@
val (paramTs, _) = chop nparams (binder_types (snd (hd preds)))
val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
(1 upto length paramTs))
- in map Free (param_names ~~ paramTs) end
+ in map2 (curry Free) param_names paramTs end
| intr :: _ => fst (chop nparams
(snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))))
val param_vs = maps term_vs params
@@ -2151,7 +2106,11 @@
(Rs as _ :: _, Type ("bool", [])) =>
map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
end
- val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
+ val all_modes = map (fn (s, T) =>
+ case proposed_modes options s of
+ NONE => (s, modes_of_typ T)
+ | SOME modes' => (s, map (translate_mode' nparams) modes'))
+ preds
in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
(* sanity check of introduction rules *)
@@ -2160,14 +2119,15 @@
let
val concl = Logic.strip_imp_concl (prop_of intro)
val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
- val params = List.take (args, nparams_of thy (fst (dest_Const p)))
+ val params = fst (chop (nparams_of thy (fst (dest_Const p))) args)
fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
- if (length (HOLogic.strip_tuple arg) = length Ts) then true
+ if length (HOLogic.strip_tuple arg) = length Ts then
+ true
else
- error ("Format of introduction rule is invalid: tuples must be expanded:"
- ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
- (Display.string_of_thm_global thy intro))
+ error ("Format of introduction rule is invalid: tuples must be expanded:"
+ ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
+ (Display.string_of_thm_global thy intro))
| _ => true
val prems = Logic.strip_imp_prems (prop_of intro)
fun check_prem (Prem (args, _)) = forall check_arg args
@@ -2201,7 +2161,7 @@
fun add_code_equations thy nparams preds result_thmss =
let
- fun add_code_equation ((predname, T), (pred, result_thms)) =
+ fun add_code_equation (predname, T) (pred, result_thms) =
let
val full_mode = (replicate nparams NONE,
map (rpair NONE) (1 upto (length (binder_types T) - nparams)))
@@ -2211,7 +2171,7 @@
val Ts = binder_types T
val arg_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
- val args = map Free (arg_names ~~ Ts)
+ val args = map2 (curry Free) arg_names Ts
val predfun = Const (predfun_name_of thy predname full_mode,
Ts ---> PredicateCompFuns.mk_predT @{typ unit})
val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
@@ -2228,7 +2188,7 @@
(pred, result_thms)
end
in
- map add_code_equation (preds ~~ result_thmss)
+ map2 add_code_equation preds result_thmss
end
(** main function of predicate compiler **)
@@ -2237,7 +2197,7 @@
{
compile_preds : theory -> string list -> string list -> (string * typ) list
-> (moded_clause list) pred_mode_table -> term pred_mode_table,
- define_functions : (string * typ) list -> string * mode list -> theory -> theory,
+ define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
-> string list -> (string * (term list * indprem list) list) list
-> moded_clause list pred_mode_table,
@@ -2259,16 +2219,16 @@
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
- prepare_intrs thy prednames (maps (intros_of thy) prednames)
+ prepare_intrs options thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
val moded_clauses =
#infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
- val _ = check_expected_modes options modes
- val _ = print_modes options modes
+ val _ = check_expected_modes preds options modes
+ val _ = print_modes options thy modes
(*val _ = print_moded_clauses thy moded_clauses*)
val _ = print_step options "Defining executable functions..."
- val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
+ val thy' = fold (#define_functions (dest_steps steps) options preds) modes thy
|> Theory.checkpoint
val _ = print_step options "Compiling equations..."
val compiled_terms =
@@ -2373,7 +2333,7 @@
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
{function_name_of = random_function_name_of,
set_function_name = set_random_function_name,
- function_name_prefix = "random",
+ function_name_prefix = "random_",
funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
wrap_compilation = K (K (K (K (K I))))
@@ -2384,12 +2344,13 @@
val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
{function_name_of = annotated_function_name_of,
set_function_name = set_annotated_function_name,
- function_name_prefix = "annotated",
+ function_name_prefix = "annotated_",
funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = K [],
wrap_compilation =
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
- mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation,
+ mk_tracing ("calling predicate " ^ s ^
+ " with mode " ^ string_of_mode' (translate_mode T mode)) compilation,
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
@@ -2435,19 +2396,16 @@
fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-val code_pred_intros_attrib = attrib add_intro;
+val code_pred_intro_attrib = attrib add_intro;
(*FIXME
- Naming of auxiliary rules necessary?
-- add default code equations P x y z = P_i_i_i x y z
*)
val setup = PredData.put (Graph.empty) #>
- Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
+ Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro))
"adding alternative introduction rules for code generation of inductive predicates"
- (*FIXME name discrepancy in attribs and ML code*)
- (*FIXME intros should be better named intro*)
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
fun generic_code_pred prep_const options raw_const lthy =
@@ -2519,7 +2477,7 @@
val user_mode' = map (rpair NONE) user_mode
val all_modes_of = if random then all_random_modes_of else all_modes_of
fun fits_to is NONE = true
- | fits_to is (SOME pm) = (is = pm)
+ | fits_to is (SOME pm) = (is = (snd (translate_mode' 0 pm)))
fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) =
fits_to is pm andalso valid (ms @ ms') pms
| valid (NONE :: ms') pms = valid ms' pms
@@ -2593,14 +2551,7 @@
in if k = ~1 orelse length ts < k then elemsT
else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont
end;
- (*
-fun random_values ctxt k t =
- let
- val thy = ProofContext.theory_of ctxt
- val _ =
- in
- end;
- *)
+
fun values_cmd print_modes param_user_modes options k raw_t state =
let
val ctxt = Toplevel.context_of state;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 15:50:05 2009 +0100
@@ -186,9 +186,11 @@
@{const_name "False"},
@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
-@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
+@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
+@{const_name "HOL.zero_class.zero"},
@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
@{const_name Nat.ord_nat_inst.less_eq_nat},
+@{const_name Nat.ord_nat_inst.less_nat},
@{const_name number_nat_inst.number_of_nat},
@{const_name Int.Bit0},
@{const_name Int.Bit1},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 15:50:05 2009 +0100
@@ -6,29 +6,14 @@
signature PREDICATE_COMPILE_FUN =
sig
-val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
+ val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
val rewrite_intro : theory -> thm -> thm list
- val setup_oracle : theory -> theory
val pred_of_function : theory -> string -> string option
end;
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
struct
-
-(* Oracle for preprocessing *)
-
-val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
-
-fun the_oracle () =
- case !oracle of
- NONE => error "Oracle is not setup"
- | SOME (_, oracle) => oracle
-
-val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
- (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
-
-
fun is_funtype (Type ("fun", [_, _])) = true
| is_funtype _ = false;
@@ -393,9 +378,6 @@
in ([], thy) end
end
-(* preprocessing intro rules - uses oracle *)
-
-(* theory -> thm -> thm *)
fun rewrite_intro thy intro =
let
fun lookup_pred (Const (name, T)) =
@@ -435,7 +417,7 @@
|> map (fn (concl'::conclprems, _) =>
Logic.list_implies ((flat prems') @ conclprems, concl')))
in
- map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
- end;
+ map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
+ end
end;
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 15:50:05 2009 +0100
@@ -3,35 +3,21 @@
begin
section {* Set operations *}
-(*
-definition Empty where "Empty == {}"
-declare empty_def[symmetric, code_pred_inline]
-*)
+
declare eq_reflection[OF empty_def, code_pred_inline]
-(*
-definition Union where "Union A B == A Un B"
-
-lemma [code_pred_intros]: "A x ==> Union A B x"
-and [code_pred_intros] : "B x ==> Union A B x"
-unfolding Union_def Un_def Collect_def mem_def by auto
-
-code_pred Union
-unfolding Union_def Un_def Collect_def mem_def by auto
-
-declare Union_def[symmetric, code_pred_inline]
-*)
declare eq_reflection[OF Un_def, code_pred_inline]
+declare eq_reflection[OF UNION_def, code_pred_inline]
section {* Alternative list definitions *}
subsection {* Alternative rules for set *}
-lemma set_ConsI1 [code_pred_intros]:
+lemma set_ConsI1 [code_pred_intro]:
"set (x # xs) x"
unfolding mem_def[symmetric, of _ x]
by auto
-lemma set_ConsI2 [code_pred_intros]:
+lemma set_ConsI2 [code_pred_intro]:
"set xs x ==> set (x' # xs) x"
unfolding mem_def[symmetric, of _ x]
by auto
@@ -49,13 +35,12 @@
done
qed
-
subsection {* Alternative rules for list_all2 *}
-lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
by auto
-lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
by auto
code_pred list_all2
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 15:10:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 15:50:05 2009 +0100
@@ -6,31 +6,35 @@
inductive False' :: "bool"
-code_pred (mode : []) False' .
+code_pred (expected_modes: bool) False' .
code_pred [depth_limited] False' .
code_pred [random] False' .
inductive EmptySet :: "'a \<Rightarrow> bool"
-code_pred (mode: [], [1]) EmptySet .
+code_pred (expected_modes: o => bool, i => bool) EmptySet .
definition EmptySet' :: "'a \<Rightarrow> bool"
where "EmptySet' = {}"
-code_pred (mode: [], [1]) [inductify] EmptySet' .
+code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
+code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
code_pred
- (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2],
- [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2],
- [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2],
- [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2])
+ (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
+ (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
+ (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
+ (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
+ (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
+ (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
+ (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
+ (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
EmptyClosure .
thm EmptyClosure.equation
@@ -39,20 +43,21 @@
where
"False \<Longrightarrow> False''"
-code_pred (mode: []) False'' .
+code_pred (expected_modes: []) False'' .
inductive EmptySet'' :: "'a \<Rightarrow> bool"
where
"False \<Longrightarrow> EmptySet'' x"
-code_pred (mode: [1]) EmptySet'' .
-code_pred (mode: [], [1]) [inductify] EmptySet'' .
+code_pred (expected_modes: [1]) EmptySet'' .
+code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
*)
+
inductive True' :: "bool"
where
"True \<Longrightarrow> True'"
-code_pred (mode: []) True' .
+code_pred (expected_modes: bool) True' .
consts a' :: 'a
@@ -60,15 +65,29 @@
where
"Fact a' a'"
-code_pred (mode: [], [1], [2], [1, 2]) Fact .
+code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
inductive zerozero :: "nat * nat => bool"
where
"zerozero (0, 0)"
-code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero .
+code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
code_pred [random] zerozero .
+inductive JamesBond :: "nat => int => code_numeral => bool"
+where
+ "JamesBond 0 0 7"
+
+code_pred JamesBond .
+
+values "{(a, b, c). JamesBond a b c}"
+values "{(a, c, b). JamesBond a b c}"
+values "{(b, a, c). JamesBond a b c}"
+values "{(b, c, a). JamesBond a b c}"
+values "{(c, a, b). JamesBond a b c}"
+values "{(c, b, a). JamesBond a b c}"
+
+
subsection {* Alternative Rules *}
datatype char = C | D | E | F | G | H
@@ -77,22 +96,22 @@
where
"(x = C) \<or> (x = D) ==> is_C_or_D x"
-code_pred (mode: [1]) is_C_or_D .
+code_pred (expected_modes: i => bool) is_C_or_D .
thm is_C_or_D.equation
inductive is_D_or_E
where
"(x = D) \<or> (x = E) ==> is_D_or_E x"
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_D_or_E D"
by (auto intro: is_D_or_E.intros)
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_D_or_E E"
by (auto intro: is_D_or_E.intros)
-code_pred (mode: [], [1]) is_D_or_E
+code_pred (expected_modes: o => bool, i => bool) is_D_or_E
proof -
case is_D_or_E
from this(1) show thesis
@@ -115,11 +134,11 @@
where
"x = F \<or> x = G ==> is_F_or_G x"
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_F_or_G F"
by (auto intro: is_F_or_G.intros)
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_F_or_G G"
by (auto intro: is_F_or_G.intros)
@@ -130,7 +149,7 @@
text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
-code_pred (mode: [], [1]) is_FGH
+code_pred (expected_modes: o => bool, i => bool) is_FGH
proof -
case is_F_or_G
from this(1) show thesis
@@ -156,7 +175,7 @@
inductive zerozero' :: "nat * nat => bool" where
"equals (x, y) (0, 0) ==> zerozero' (x, y)"
-code_pred (mode: [1]) zerozero' .
+code_pred (expected_modes: i => bool) zerozero' .
lemma zerozero'_eq: "zerozero' x == zerozero x"
proof -
@@ -176,7 +195,7 @@
text {* if preprocessing fails, zerozero'' will not have all modes. *}
-code_pred (mode: [o], [(i, o)], [(o,i)], [i]) [inductify] zerozero'' .
+code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
subsection {* Numerals *}
@@ -214,7 +233,7 @@
| "even n \<Longrightarrow> odd (Suc n)"
| "odd n \<Longrightarrow> even (Suc n)"
-code_pred (mode: [], [1]) even .
+code_pred (expected_modes: i => bool, o => bool) even .
code_pred [depth_limited] even .
code_pred [random] even .
@@ -237,7 +256,7 @@
definition odd' where "odd' x == \<not> even x"
-code_pred (mode: [1]) [inductify] odd' .
+code_pred (expected_modes: i => bool) [inductify] odd' .
code_pred [inductify, depth_limited] odd' .
code_pred [inductify, random] odd' .
@@ -249,7 +268,7 @@
where
"n mod 2 = 0 \<Longrightarrow> is_even n"
-code_pred (mode: [1]) is_even .
+code_pred (expected_modes: i => bool) is_even .
subsection {* append predicate *}
@@ -257,7 +276,8 @@
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
+ i => o => i => bool as suffix) append .
code_pred [depth_limited] append .
code_pred [random] append .
code_pred [annotated] append .
@@ -270,11 +290,12 @@
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
-values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
-values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}"
-value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
-value [code] "Predicate.the (append_3 ([]::int list))"
+values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}"
+
+value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
+value [code] "Predicate.the (slice ([]::int list))"
text {* tricky case with alternative rules *}
@@ -287,9 +308,10 @@
lemma append2_Nil: "append2 [] (xs::'b list) xs"
by (simp add: append2.intros(1))
-lemmas [code_pred_intros] = append2_Nil append2.intros(2)
+lemmas [code_pred_intro] = append2_Nil append2.intros(2)
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2
+code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
+ i => o => i => bool, i => i => i => bool) append2
proof -
case append2
from append2(1) show thesis
@@ -309,13 +331,13 @@
"tupled_append ([], xs, xs)"
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) tupled_append .
code_pred [random] tupled_append .
thm tupled_append.equation
-(*
-TODO: values with tupled modes
-values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
-*)
+
+(*TODO: values with tupled modes*)
+(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*)
inductive tupled_append'
where
@@ -323,7 +345,8 @@
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) tupled_append' .
thm tupled_append'.equation
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -331,7 +354,8 @@
"tupled_append'' ([], xs, xs)"
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' .
thm tupled_append''.equation
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -339,7 +363,8 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' .
thm tupled_append'''.equation
subsection {* map_ofP predicate *}
@@ -349,7 +374,7 @@
"map_ofP ((a, b)#xs) a b"
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
-code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
+code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
thm map_ofP.equation
subsection {* filter predicate *}
@@ -361,7 +386,7 @@
| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
-code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 .
+code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
code_pred [depth_limited] filter1 .
code_pred [random] filter1 .
@@ -373,7 +398,7 @@
| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
-code_pred (mode: [1, 2, 3], [1, 2]) filter2 .
+code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 .
code_pred [depth_limited] filter2 .
code_pred [random] filter2 .
thm filter2.equation
@@ -384,7 +409,7 @@
where
"List.filter P xs = ys ==> filter3 P xs ys"
-code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 .
+code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 .
code_pred [depth_limited] filter3 .
thm filter3.depth_limited_equation
@@ -392,7 +417,7 @@
where
"List.filter P xs = ys ==> filter4 P xs ys"
-code_pred (mode: [1, 2], [1, 2, 3]) filter4 .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
code_pred [depth_limited] filter4 .
code_pred [random] filter4 .
@@ -402,7 +427,7 @@
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-code_pred (mode: [1], [2], [1, 2]) rev .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
thm rev.equation
@@ -412,7 +437,7 @@
"tupled_rev ([], [])"
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
-code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev .
+code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
thm tupled_rev.equation
subsection {* partition predicate *}
@@ -423,7 +448,8 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition .
+code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
+ (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) partition .
code_pred [depth_limited] partition .
code_pred [random] partition .
@@ -438,18 +464,21 @@
| "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
| "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
-code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition .
+code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
+ (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
thm tupled_partition.equation
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"r a b \<Longrightarrow> tranclp r a b"
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
by auto
subsection {* transitive predicate *}
-code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp
+code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
+ (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
+ (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
proof -
case tranclp
from this converse_tranclpE[OF this(1)] show thesis by metis
@@ -476,11 +505,10 @@
text {* values command needs mode annotation of the parameter succ
to disambiguate which mode is to be chosen. *}
-values [mode: [1]] 20 "{n. tranclp succ 10 n}"
-values [mode: [2]] 10 "{n. tranclp succ n 10}"
+values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
+values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
values 20 "{(n, m). tranclp succ n m}"
-
subsection {* IMP *}
types
@@ -548,9 +576,8 @@
values 5
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
-(* FIXME:
values 3 "{(a,q). step (par nil nil) a q}"
-*)
+
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
where
@@ -570,8 +597,8 @@
| "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
code_pred divmod_rel ..
-
-value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
+thm divmod_rel.equation
+value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
subsection {* Minimum *}
@@ -657,7 +684,7 @@
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-code_pred (mode: [1], [1, 2]) [inductify] set_of .
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
thm set_of.equation
code_pred [inductify] is_ord .
@@ -673,19 +700,15 @@
thm rel_comp.equation
code_pred [inductify] Image .
thm Image.equation
-(*TODO: *)
-
-declare Id_on_def[unfolded UNION_def, code_pred_def]
-
-code_pred [inductify] Id_on .
+code_pred (expected_modes: (o => bool) => o => bool, (o => bool) => i * o => bool,
+ (o => bool) => o * i => bool, (o => bool) => i => bool) [inductify] Id_on .
thm Id_on.equation
code_pred [inductify] Domain .
thm Domain.equation
code_pred [inductify] Range .
thm Range.equation
code_pred [inductify] Field .
-declare Sigma_def[unfolded UNION_def, code_pred_def]
-declare refl_on_def[unfolded UNION_def, code_pred_def]
+thm Field.equation
code_pred [inductify] refl_on .
thm refl_on.equation
code_pred [inductify] total_on .
@@ -708,21 +731,82 @@
(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
-code_pred [inductify] concat .
-code_pred [inductify] hd .
-code_pred [inductify] tl .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
+thm concatP.equation
+
+values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
+values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
+
+code_pred [inductify, depth_limited] List.concat .
+thm concatP.depth_limited_equation
+
+values [depth_limit = 3] 3
+ "{xs. concatP xs ([0] :: nat list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs ([1] :: int list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs ([1] :: nat list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs [(1::int), 2]}"
+
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
+thm hdP.equation
+values "{x. hdP [1, 2, (3::int)] x}"
+values "{(xs, x). hdP [1, 2, (3::int)] 1}"
+
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
+thm tlP.equation
+values "{x. tlP [1, 2, (3::nat)] x}"
+values "{x. tlP [1, 2, (3::int)] [3]}"
+
code_pred [inductify] last .
+thm lastP.equation
+
code_pred [inductify] butlast .
+thm butlastP.equation
+
code_pred [inductify] take .
+thm takeP.equation
+
code_pred [inductify] drop .
+thm dropP.equation
code_pred [inductify] zip .
+thm zipP.equation
+
(*code_pred [inductify] upt .*)
code_pred [inductify] remdups .
+thm remdupsP.equation
+code_pred [inductify, depth_limited] remdups .
+values [depth_limit = 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
+
code_pred [inductify] remove1 .
+thm remove1P.equation
+values "{xs. remove1P 1 xs [2, (3::int)]}"
+
code_pred [inductify] removeAll .
+thm removeAllP.equation
+code_pred [inductify, depth_limited] removeAll .
+
+values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
+
code_pred [inductify] distinct .
+thm distinct.equation
+
code_pred [inductify] replicate .
+thm replicateP.equation
+values 5 "{(n, xs). replicateP n (0::int) xs}"
+
code_pred [inductify] splice .
+thm splice.simps
+thm spliceP.equation
+
+values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
+(* TODO: correct error messages:*)
+(* values {(xs, ys, zs). spliceP xs ... } *)
+
code_pred [inductify] List.rev .
code_pred [inductify] map .
code_pred [inductify] foldr .
@@ -786,7 +870,7 @@
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
-code_pred (mode: [], [1]) S\<^isub>4p .
+code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
subsection {* Lambda *}
@@ -838,10 +922,58 @@
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
-code_pred (mode: [1, 2], [1, 2, 3]) typing .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
thm typing.equation
-code_pred (mode: [1], [1, 2]) beta .
+code_pred (modes: i => o => bool as reduce') beta .
thm beta.equation
+values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
+
+definition "reduce t = Predicate.the (reduce' t)"
+
+value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
+
+code_pred [random] typing .
+
+values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
+
+subsection {* A minimal example of yet another semantics *}
+
+text {* thanks to Elke Salecker *}
+
+types
+vname = nat
+vvalue = int
+var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
+
+datatype ir_expr =
+ IrConst vvalue
+| ObjAddr vname
+| Add ir_expr ir_expr
+
+datatype val =
+ IntVal vvalue
+
+record configuration =
+Env :: var_assign
+
+inductive eval_var ::
+"ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
+where
+ irconst: "eval_var (IrConst i) conf (IntVal i)"
+| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
+| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
+
+(* TODO: breaks if code_pred_intro is used? *)
+(*
+lemmas [code_pred_intro] = irconst objaddr plus
+*)
+thm eval_var.cases
+
+code_pred eval_var . (*by (rule eval_var.cases)*)
+thm eval_var.equation
+
+values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
+
end
\ No newline at end of file