# HG changeset patch # User bulwahn # Date 1264170389 -3600 # Node ID dcd0fa5cc6d3e165903a20bc54271ad9d68b83ac # Parent 3b1957113753dfe3a6cec48e3ae9ae578454df5f# Parent e1b8f273640415617663d88ded5403cd6ca6d7dc merged diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/DSequence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/DSequence.thy Fri Jan 22 15:26:29 2010 +0100 @@ -0,0 +1,112 @@ + +(* Author: Lukas Bulwahn, TU Muenchen *) + +header {* Depth-Limited Sequences with failure element *} + +theory DSequence +imports Lazy_Sequence Code_Numeral +begin + +types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option" + +definition empty :: "'a dseq" +where + "empty = (%i pol. Some Lazy_Sequence.empty)" + +definition single :: "'a => 'a dseq" +where + "single x = (%i pol. Some (Lazy_Sequence.single x))" + +fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option" +where + "eval f i pol = f i pol" + +definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" +where + "yield dseq i pol = (case eval dseq i pol of + None => None + | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))" + +definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq" +where + "yieldn n dseq i pol = (case eval dseq i pol of + None => ([], %i pol. None) + | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))" + +fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq" +where + "map_seq f xq i pol = (case Lazy_Sequence.yield xq of + None => Some Lazy_Sequence.empty + | Some (x, xq') => (case eval (f x) i pol of + None => None + | Some yq => (case map_seq f xq' i pol of + None => None + | Some zq => Some (Lazy_Sequence.append yq zq))))" + +definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq" +where + "bind x f = (%i pol. + if i = 0 then + (if pol then Some Lazy_Sequence.empty else None) + else + (case x (i - 1) pol of + None => None + | Some xq => map_seq f xq i pol))" + +definition union :: "'a dseq => 'a dseq => 'a dseq" +where + "union x y = (%i pol. case (x i pol, y i pol) of + (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq) + | _ => None)" + +definition if_seq :: "bool => unit dseq" +where + "if_seq b = (if b then single () else empty)" + +definition not_seq :: "unit dseq => unit dseq" +where + "not_seq x = (%i pol. case x i (\pol) of + None => Some Lazy_Sequence.empty + | Some xq => (case Lazy_Sequence.yield xq of + None => Some (Lazy_Sequence.single ()) + | Some _ => Some (Lazy_Sequence.empty)))" + +definition map :: "('a => 'b) => 'a dseq => 'b dseq" +where + "map f g = (%i pol. case g i pol of + None => None + | Some xq => Some (Lazy_Sequence.map f xq))" + +ML {* +signature DSEQUENCE = +sig + type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option + val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option + val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq + val map : ('a -> 'b) -> 'a dseq -> 'b dseq +end; + +structure DSequence : DSEQUENCE = +struct + +type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option + +val yieldn = @{code yieldn} +val yield = @{code yield} +val map = @{code map} + +end; +*} + +code_reserved Eval DSequence +(* +hide type Sequence.seq + +hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single + Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq +*) +hide (open) const empty single eval map_seq bind union if_seq not_seq map +hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def + if_seq_def not_seq_def map_def + +end diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Jan 22 15:26:29 2010 +0100 @@ -247,10 +247,12 @@ Code_Evaluation.thy \ Code_Numeral.thy \ Divides.thy \ + DSequence.thy \ Equiv_Relations.thy \ Groebner_Basis.thy \ Hilbert_Choice.thy \ Int.thy \ + Lazy_Sequence.thy \ List.thy \ Main.thy \ Map.thy \ @@ -261,6 +263,7 @@ Predicate_Compile.thy \ Quickcheck.thy \ Random.thy \ + Random_Sequence.thy \ Recdef.thy \ SetInterval.thy \ String.thy \ diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Lazy_Sequence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lazy_Sequence.thy Fri Jan 22 15:26:29 2010 +0100 @@ -0,0 +1,158 @@ + +(* Author: Lukas Bulwahn, TU Muenchen *) + +header {* Lazy sequences *} + +theory Lazy_Sequence +imports List Code_Numeral +begin + +datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence" + +definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence" +where + "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)" + +code_datatype Lazy_Sequence + +primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option" +where + "yield Empty = None" +| "yield (Insert x xq) = Some (x, xq)" + +fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence" +where + "yieldn i S = (if i = 0 then ([], S) else + case yield S of + None => ([], S) + | Some (x, S') => let + (xs, S'') = yieldn (i - 1) S' + in (x # xs, S''))" + +lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq" +by (cases xq) auto + +lemma yield_Seq [code]: + "yield (Lazy_Sequence f) = f ()" +unfolding Lazy_Sequence_def by (cases "f ()") auto + +lemma Seq_yield: + "Lazy_Sequence (%u. yield f) = f" +unfolding Lazy_Sequence_def by (cases f) auto + +lemma lazy_sequence_size_code [code]: + "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)" +by (cases xq) auto + +lemma size_code [code]: + "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)" +by (cases xq) auto + +lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of + (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \ (eq_class.eq xq yq) | _ => False)" +apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) +apply (cases yq) apply (auto simp add: eq_class.eq_equals) done + +lemma seq_case [code]: + "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')" +by (cases xq) auto + +lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))" +by (cases xq) auto + +definition empty :: "'a lazy_sequence" +where + [code]: "empty = Lazy_Sequence (%u. None)" + +definition single :: "'a => 'a lazy_sequence" +where + [code]: "single x = Lazy_Sequence (%u. Some (x, empty))" + +primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence" +where + "append Empty yq = yq" +| "append (Insert x xq) yq = Insert x (append xq yq)" + +lemma [code]: + "append xq yq = Lazy_Sequence (%u. case yield xq of + None => yield yq + | Some (x, xq') => Some (x, append xq' yq))" +unfolding Lazy_Sequence_def +apply (cases "xq") +apply auto +apply (cases "yq") +apply auto +done + +primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence" +where + "flat Empty = Empty" +| "flat (Insert xq xqq) = append xq (flat xqq)" + +lemma [code]: + "flat xqq = Lazy_Sequence (%u. case yield xqq of + None => None + | Some (xq, xqq') => yield (append xq (flat xqq')))" +apply (cases "xqq") +apply (auto simp add: Seq_yield) +unfolding Lazy_Sequence_def +by auto + +primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence" +where + "map f Empty = Empty" +| "map f (Insert x xq) = Insert (f x) (map f xq)" + +lemma [code]: + "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))" +apply (cases xq) +apply (auto simp add: Seq_yield) +unfolding Lazy_Sequence_def +apply auto +done + +definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence" +where + [code]: "bind xq f = flat (map f xq)" + +definition if_seq :: "bool => unit lazy_sequence" +where + "if_seq b = (if b then single () else empty)" + +definition not_seq :: "unit lazy_sequence => unit lazy_sequence" +where + "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)" + +subsection {* Code setup *} + +ML {* +signature LAZY_SEQUENCE = +sig + datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option + val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option + val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence) +end; + +structure Lazy_Sequence : LAZY_SEQUENCE = +struct + +@{code_datatype lazy_sequence = Lazy_Sequence} + +val yield = @{code yield} + +val yieldn = @{code yieldn} + +end; +*} + +code_reserved Eval Lazy_Sequence + +code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence") + +code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence") + +hide (open) type lazy_sequence +hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq +hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def + +end diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Predicate_Compile.thy --- a/src/HOL/Predicate_Compile.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Predicate_Compile.thy Fri Jan 22 15:26:29 2010 +0100 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports Quickcheck +imports Random_Sequence Quickcheck uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_core.ML" @@ -18,4 +18,4 @@ setup Predicate_Compile.setup -end \ No newline at end of file +end diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Random_Sequence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Random_Sequence.thy Fri Jan 22 15:26:29 2010 +0100 @@ -0,0 +1,61 @@ + +(* Author: Lukas Bulwahn, TU Muenchen *) + +theory Random_Sequence +imports Quickcheck DSequence +begin + +types 'a random_dseq = "code_numeral \ code_numeral \ Random.seed \ ('a DSequence.dseq \ Random.seed)" + +definition empty :: "'a random_dseq" +where + "empty = (%nrandom size. Pair (DSequence.empty))" + +definition single :: "'a => 'a random_dseq" +where + "single x = (%nrandom size. Pair (DSequence.single x))" + +definition bind :: "'a random_dseq => ('a \ 'b random_dseq) \ 'b random_dseq" +where + "bind R f = (\nrandom size s. let + (P, s') = R nrandom size s; + (s1, s2) = Random.split_seed s' + in (DSequence.bind P (%a. fst (f a nrandom size s1)), s2))" + +definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq" +where + "union R1 R2 = (\nrandom size s. let + (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s' + in (DSequence.union S1 S2, s''))" + +definition if_random_dseq :: "bool => unit random_dseq" +where + "if_random_dseq b = (if b then single () else empty)" + +definition not_random_dseq :: "unit random_dseq => unit random_dseq" +where + "not_random_dseq R = (\nrandom size s. let + (S, s') = R nrandom size s + in (DSequence.not_seq S, s'))" + +fun Random :: "(code_numeral \ Random.seed \ (('a \ (unit \ term)) \ Random.seed)) \ 'a random_dseq" +where + "Random g nrandom = (%size. if nrandom <= 0 then (Pair DSequence.empty) else + (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (DSequence.union (DSequence.single (fst r)) rs)))))" + +definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq" +where + "map f P = bind P (single o f)" + +(* +hide const DSequence.empty DSequence.single DSequence.eval + DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq + DSequence.map +*) + +hide (open) const empty single bind union if_random_dseq not_random_dseq Random map + +hide type DSequence.dseq random_dseq +hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def + +end \ No newline at end of file diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Function/function.ML Fri Jan 22 15:26:29 2010 +0100 @@ -164,6 +164,7 @@ simps=SOME simps, inducts=SOME inducts, termination=termination } in Local_Theory.declaration false (add_function_data o morph_function_data info') + #> Spec_Rules.add Spec_Rules.Equational (fs, simps) end) end in diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Jan 22 15:26:29 2010 +0100 @@ -69,14 +69,19 @@ (intross3 @ new_intross, thy'''') end -fun preprocess_strong_conn_constnames options gr constnames thy = +fun preprocess_strong_conn_constnames options gr ts thy = let - val get_specs = map (fn k => (k, Graph.get_node gr k)) - val _ = print_step options ("Preprocessing scc of " ^ commas constnames) - val (prednames, funnames) = List.partition (is_pred thy) constnames + fun get_specs ts = map_filter (fn t => + TermGraph.get_node gr t |> + (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths))) + ts + val _ = print_step options ("Preprocessing scc of " ^ + commas (map (Syntax.string_of_term_global thy) ts)) + val (prednames, funnames) = List.partition (fn t => body_type (fastype_of t) = @{typ bool}) ts (* untangle recursion by defining predicates for all functions *) val _ = print_step options - ("Compiling functions (" ^ commas funnames ^ ") to predicates...") + ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^ + ") to predicates...") val (fun_pred_specs, thy') = if not (null funnames) then Predicate_Compile_Fun.define_predicates (get_specs funnames) thy else ([], thy) @@ -95,17 +100,19 @@ thy'''' end; -fun preprocess options const thy = +fun preprocess options t thy = let val _ = print_step options "Fetching definitions from theory..." - val table = Predicate_Compile_Data.make_const_spec_table options thy - val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const - val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr - in fold_rev (preprocess_strong_conn_constnames options gr) - (Graph.strong_conn gr) thy + val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" + (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t + |> (fn gr => TermGraph.subgraph (member (op =) (TermGraph.all_succs gr [t])) gr)) + in + Output.cond_timeit (!Quickcheck.timing) "preprocess-process" + (fn () => (fold_rev (preprocess_strong_conn_constnames options gr) + (TermGraph.strong_conn gr) thy)) end -fun extract_options (((expected_modes, proposed_modes), raw_options), const) = +fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) = let fun chk s = member (op =) raw_options s in @@ -123,9 +130,7 @@ show_compilation = chk "show_compilation", skip_proof = chk "skip_proof", inductify = chk "inductify", - random = chk "random", - depth_limited = chk "depth_limited", - annotated = chk "annotated" + compilation = compilation } end @@ -133,11 +138,13 @@ let val thy = ProofContext.theory_of lthy val const = Code.read_const thy raw_const + val T = Sign.the_const_type thy const + val t = Const (const, T) val options = extract_options (((expected_modes, proposed_modes), raw_options), const) in if (is_inductify options) then let - val lthy' = Local_Theory.theory (preprocess options const) lthy + val lthy' = Local_Theory.theory (preprocess options t) lthy |> Local_Theory.checkpoint val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of @@ -153,10 +160,6 @@ 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", - "annotated"] - local structure P = OuterParse in @@ -187,8 +190,11 @@ val scan_options = let val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options) + val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names) in - Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") [] + Scan.optional (P.$$$ "[" |-- Scan.optional scan_compilation Pred + -- P.enum "," scan_bool_option --| P.$$$ "]") + (Pred, []) end val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; @@ -200,12 +206,15 @@ val value_options = let - val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE - val random = Scan.optional (Args.$$$ "random" >> K true) false - val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false + val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE + val scan_compilation = + Scan.optional + (foldl1 (op ||) + (map (fn (s, c) => Args.$$$ s -- P.enum "," P.int >> (fn (_, ps) => (c, ps))) + compilation_names)) + (Pred, []) in - Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]") - (NONE, (false, false)) + Scan.optional (P.$$$ "[" |-- expected_values -- scan_compilation --| P.$$$ "]") (NONE, (Pred, [])) end (* code_pred command and values command *) @@ -217,7 +226,7 @@ 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 - >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.no_timing o Toplevel.keep + >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep (Predicate_Compile_Core.values_cmd print_modes param_modes options k t))); end diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Jan 22 15:26:29 2010 +0100 @@ -6,49 +6,45 @@ (* FIXME proper signature *) +structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord); + structure Predicate_Compile_Aux = struct +(* general functions *) + +fun apfst3 f (x, y, z) = (f x, y, z) +fun apsnd3 f (x, y, z) = (x, f y, z) +fun aptrd3 f (x, y, z) = (x, y, f z) + +fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2)) + | comb_option f (NONE, SOME x2) = SOME x2 + | comb_option f (SOME x1, NONE) = SOME x1 + | comb_option f (NONE, NONE) = NONE + +fun map2_optional f (x :: xs) (y :: ys) = (f x (SOME y)) :: (map2_optional f xs ys) + | map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs []) + | map2_optional f [] [] = [] + +fun find_indices f xs = + map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs) (* mode *) -type smode = (int * int list option) list -type mode = smode option list * smode -datatype tmode = Mode of mode * smode * tmode option list; - -fun string_of_smode js = - commas (map - (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" - | SOME js => enclose "[" "]" (string_of_smode js)) - (iss @ [SOME is])); - -fun string_of_tmode (Mode (predmode, termmode, param_modes)) = - "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' +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 +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' @@ -61,7 +57,153 @@ fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode' | dest_tuple_mode _ = [] -fun string_of_mode' mode' = +fun all_modes_of_typ (T as Type ("fun", _)) = + let + val (S, U) = strip_type T + in + if U = HOLogic.boolT then + fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) + (map all_modes_of_typ S) [Bool] + else + [Input, Output] + end + | all_modes_of_typ (Type ("*", [T1, T2])) = + map_product (curry Pair) (all_modes_of_typ T1) (all_modes_of_typ T2) + | all_modes_of_typ (Type ("bool", [])) = [Bool] + | all_modes_of_typ _ = [Input, Output] + +fun extract_params arg = + case fastype_of arg of + (T as Type ("fun", _)) => + (if (body_type T = HOLogic.boolT) then + (case arg of + Free _ => [arg] | _ => error "extract_params: Unexpected term") + else []) + | (Type ("*", [T1, T2])) => + let + val (t1, t2) = HOLogic.dest_prod arg + in + extract_params t1 @ extract_params t2 + end + | _ => [] + +fun ho_arg_modes_of mode = + let + fun ho_arg_mode (m as Fun _) = [m] + | ho_arg_mode (Pair (m1, m2)) = ho_arg_mode m1 @ ho_arg_mode m2 + | ho_arg_mode _ = [] + in + maps ho_arg_mode (strip_fun_mode mode) + end + +fun ho_args_of mode ts = + let + fun ho_arg (Fun _) (SOME t) = [t] + | ho_arg (Fun _) NONE = error "ho_arg_of" + | ho_arg (Pair (m1, m2)) (SOME (Const ("Pair", _) $ t1 $ t2)) = + ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2) + | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE + | ho_arg _ _ = [] + in + flat (map2_optional ho_arg (strip_fun_mode mode) ts) + end + +(* temporary function should be replaced by unsplit_input or so? *) +fun replace_ho_args mode hoargs ts = + let + fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs') + | replace (Pair (m1, m2), Const ("Pair", T) $ t1 $ t2) hoargs = + let + val (t1', hoargs') = replace (m1, t1) hoargs + val (t2', hoargs'') = replace (m2, t2) hoargs' + in + (Const ("Pair", T) $ t1' $ t2', hoargs'') + end + | replace (_, t) hoargs = (t, hoargs) + in + fst (fold_map replace ((strip_fun_mode mode) ~~ ts) hoargs) + end + +fun ho_argsT_of mode Ts = + let + fun ho_arg (Fun _) T = [T] + | ho_arg (Pair (m1, m2)) (Type ("*", [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2 + | ho_arg _ _ = [] + in + flat (map2 ho_arg (strip_fun_mode mode) Ts) + end + +(* splits mode and maps function to higher-order argument types *) +fun split_map_mode f mode ts = + let + fun split_arg_mode' (m as Fun _) t = f m t + | split_arg_mode' (Pair (m1, m2)) (Const ("Pair", _) $ t1 $ t2) = + let + val (i1, o1) = split_arg_mode' m1 t1 + val (i2, o2) = split_arg_mode' m2 t2 + in + (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) + end + | split_arg_mode' Input t = (SOME t, NONE) + | split_arg_mode' Output t = (NONE, SOME t) + | split_arg_mode' _ _ = error "split_map_mode: mode and term do not match" + in + (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) + end + +(* splits mode and maps function to higher-order argument types *) +fun split_map_modeT f mode Ts = + let + fun split_arg_mode' (m as Fun _) T = f m T + | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) = + let + val (i1, o1) = split_arg_mode' m1 T1 + val (i2, o2) = split_arg_mode' m2 T2 + in + (comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2)) + end + | split_arg_mode' Input T = (SOME T, NONE) + | split_arg_mode' Output T = (NONE, SOME T) + | split_arg_mode' _ _ = error "split_modeT': mode and type do not match" + in + (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) + end + +fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts + +fun fold_map_aterms_prodT comb f (Type ("*", [T1, T2])) s = + let + val (x1, s') = fold_map_aterms_prodT comb f T1 s + val (x2, s'') = fold_map_aterms_prodT comb f T2 s' + in + (comb x1 x2, s'') + end + | fold_map_aterms_prodT comb f T s = f T s + +fun map_filter_prod f (Const ("Pair", _) $ t1 $ t2) = + comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2) + | map_filter_prod f t = f t + +(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *) + +fun split_modeT' mode Ts = + let + fun split_arg_mode' (Fun _) T = ([], []) + | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) = + let + val (i1, o1) = split_arg_mode' m1 T1 + val (i2, o2) = split_arg_mode' m2 T2 + in + (i1 @ i2, o1 @ o2) + end + | split_arg_mode' Input T = ([T], []) + | split_arg_mode' Output T = ([], [T]) + | split_arg_mode' _ _ = error "split_modeT': mode and type do not match" + in + (pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) + end + +fun string_of_mode mode = let fun string_of_mode1 Input = "i" | string_of_mode1 Output = "o" @@ -71,9 +213,9 @@ | 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 + in string_of_mode3 mode end -fun ascii_string_of_mode' mode' = +fun ascii_string_of_mode mode' = let fun ascii_string_of_mode' Input = "i" | ascii_string_of_mode' Output = "o" @@ -91,55 +233,10 @@ | 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; +(* premises *) -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) +datatype indprem = Prem of term | Negprem of term | Sidecond of term + | Generator of (string * typ); (* general syntactic functions *) @@ -162,9 +259,9 @@ val is_pred_equation = is_pred_equation_term o prop_of fun is_intro_term constname t = - case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of + the_default false (try (fn t => case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of Const (c, _) => c = constname - | _ => false + | _ => false) t) fun is_intro constname t = is_intro_term constname (prop_of t) @@ -177,21 +274,8 @@ 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 ***) +(* TODO: another copy in the core! *) (* FIXME: constructor terms are supposed to be seen in the way the code generator sees constructors.*) fun is_constrt thy = @@ -206,7 +290,34 @@ | _ => false) | _ => false) in check end; - + +fun is_funtype (Type ("fun", [_, _])) = true + | is_funtype _ = false; + +fun is_Type (Type _) = true + | is_Type _ = false + +(* returns true if t is an application of an datatype constructor *) +(* which then consequently would be splitted *) +(* else false *) +(* +fun is_constructor thy t = + if (is_Type (fastype_of t)) then + (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of + NONE => false + | SOME info => (let + val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) + val (c, _) = strip_comb t + in (case c of + Const (name, _) => name mem_string constr_consts + | _ => false) end)) + else false +*) + +(* must be exported in code.ML *) +(* TODO: is there copy in the core? *) +fun is_constr thy = is_some o Code.get_datatype_of_constr thy; + fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = let val (xTs, t') = strip_ex t @@ -224,7 +335,6 @@ val t'' = Term.subst_bounds (rev vs, t'); in ((ps', t''), nctxt') end; - (* introduction rule combinators *) (* combinators to apply a function to all literals of an introduction rules *) @@ -280,10 +390,23 @@ (* Different options for compiler *) +datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated | Random_DSeq + +fun string_of_compilation c = case c of + Pred => "" + | Random => "random" + | Depth_Limited => "depth limited" + | DSeq => "dseq" + | Annotated => "annotated" + | Random_DSeq => "random dseq" + +(*datatype compilation_options = + Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*) + datatype options = Options of { - expected_modes : (string * mode' list) option, - proposed_modes : (string * mode' list) option, - proposed_names : ((string * mode') * string) list, + expected_modes : (string * mode list) option, + proposed_modes : (string * mode list) option, + proposed_names : ((string * mode) * string) list, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, @@ -293,14 +416,12 @@ skip_proof : bool, inductify : bool, - random : bool, - depth_limited : bool, - annotated : bool + compilation : compilation }; fun expected_modes (Options opt) = #expected_modes opt fun proposed_modes (Options opt) = #proposed_modes opt -fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode') +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 @@ -312,9 +433,8 @@ fun skip_proof (Options opt) = #skip_proof opt fun is_inductify (Options opt) = #inductify opt -fun is_random (Options opt) = #random opt -fun is_depth_limited (Options opt) = #depth_limited opt -fun is_annotated (Options opt) = #annotated opt + +fun compilation (Options opt) = #compilation opt val default_options = Options { expected_modes = NONE, @@ -326,14 +446,18 @@ show_modes = false, show_mode_inference = false, show_compilation = false, - skip_proof = false, + skip_proof = true, inductify = false, - random = false, - depth_limited = false, - annotated = false + compilation = Pred } +val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", + "show_mode_inference", "show_compilation", "skip_proof", "inductify"] + +val compilation_names = [("pred", Pred), + (*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*) + ("dseq", DSeq), ("random_dseq", Random_DSeq)] fun print_step options s = if show_steps options then tracing s else () diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jan 22 15:26:29 2010 +0100 @@ -9,36 +9,41 @@ 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.mode' option list option - -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit - val register_predicate : (string * thm list * thm * int) -> theory -> theory + val values_cmd : string list -> Predicate_Compile_Aux.mode option list option + -> (string option * (Predicate_Compile_Aux.compilation * int list)) + -> int -> string -> Toplevel.state -> unit + val register_predicate : (string * thm list * thm) -> theory -> theory val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool + val function_name_of : Predicate_Compile_Aux.compilation -> theory + -> string -> Predicate_Compile_Aux.mode -> string val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm - val predfun_name_of: theory -> string -> Predicate_Compile_Aux.mode -> string val all_preds_of : theory -> string list - val modes_of: theory -> string -> Predicate_Compile_Aux.mode list - val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list - val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string - val random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list - val random_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string - val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list + val modes_of: Predicate_Compile_Aux.compilation + -> theory -> string -> Predicate_Compile_Aux.mode list + val all_modes_of : Predicate_Compile_Aux.compilation + -> theory -> (string * Predicate_Compile_Aux.mode list) list val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list val intros_of : theory -> string -> thm list - val nparams_of : theory -> string -> int val add_intro : thm -> theory -> theory val set_elim : thm -> theory -> theory - val set_nparams : string -> int -> theory -> theory + val preprocess_intro : theory -> thm -> thm val print_stored_rules : theory -> unit - val print_all_modes : theory -> unit - val mk_casesrule : Proof.context -> term -> int -> thm list -> term + val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit + val mk_casesrule : Proof.context -> term -> thm list -> term + 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 dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref + val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) + option Unsynchronized.ref val code_pred_intro_attrib : attribute + (* used by Quickcheck_Generator *) (* temporary for testing of the compilation *) + datatype compilation_funs = CompilationFuns of { mk_predT : typ -> typ, dest_predT : typ -> typ, @@ -50,12 +55,11 @@ mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term }; + val pred_compfuns : compilation_funs val randompred_compfuns : compilation_funs val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory - val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory - val add_depth_limited_equations : Predicate_Compile_Aux.options - -> string list -> theory -> theory + val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val mk_tracing : string -> term -> term end; @@ -75,6 +79,8 @@ fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) +fun assert b = if not b then error "Assertion failed" else warning "Assertion holds" + datatype assertion = Max_number_of_subgoals of int fun assert_tac (Max_number_of_subgoals i) st = if (nprems_of st <= i) then Seq.single st @@ -97,7 +103,7 @@ val T = fastype_of t val U = fastype_of u val [A] = binder_types T - val D = body_type U + val D = body_type U in Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u end; @@ -121,96 +127,92 @@ Const(@{const_name Code_Evaluation.tracing}, @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t -(* destruction of intro rules *) +val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) + +(* derivation trees for modes of premises *) + +datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode + | Mode_Pair of mode_derivation * mode_derivation | Term of mode -(* 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 string_of_derivation (Mode_App (m1, m2)) = + "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")" + | string_of_derivation (Mode_Pair (m1, m2)) = + "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")" + | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")" + | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")" -(** data structures **) - -fun gen_split_smode (mk_tuple, strip_tuple) smode ts = +fun strip_mode_derivation deriv = let - fun split_tuple' _ _ [] = ([], []) - | split_tuple' is i (t::ts) = - (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 member (op =) (map fst smode) i then - case (the (AList.lookup (op =) smode i)) of - NONE => apfst (cons t) - | SOME is => - let - val (ts1, ts2) = split_tuple is t - fun cons_tuple ts = if null ts then I else cons (mk_tuple ts) - in (apfst (cons_tuple ts1)) o (apsnd (cons_tuple ts2)) end - else apsnd (cons t)) - (split_smode' smode (i+1) ts) - in split_smode' smode 1 ts end + fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds) + | strip deriv ds = (deriv, ds) + in + strip deriv [] + end + +fun mode_of (Context m) = m + | mode_of (Term m) = m + | mode_of (Mode_App (d1, d2)) = + (case mode_of d1 of Fun (m, m') => + (if m = mode_of d2 then m' else error "mode_of") + | _ => error "mode_of2") + | mode_of (Mode_Pair (d1, d2)) = + Pair (mode_of d1, mode_of d2) + +fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv)) -fun split_smode smode ts = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple) smode ts -fun split_smodeT smode ts = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT) smode ts - -fun gen_split_mode split_smode (iss, is) ts = +fun param_derivations_of deriv = let - val (t1, t2) = chop (length iss) ts - in (t1, split_smode is t2) end + val (_, argument_derivs) = strip_mode_derivation deriv + fun param_derivation (Mode_Pair (m1, m2)) = + param_derivation m1 @ param_derivation m2 + | param_derivation (Term _) = [] + | param_derivation m = [m] + in + maps param_derivation argument_derivs + end -fun split_mode (iss, is) ts = gen_split_mode split_smode (iss, is) ts -fun split_modeT (iss, is) ts = gen_split_mode split_smodeT (iss, is) ts +fun collect_context_modes (Mode_App (m1, m2)) = + collect_context_modes m1 @ collect_context_modes m2 + | collect_context_modes (Mode_Pair (m1, m2)) = + collect_context_modes m1 @ collect_context_modes m2 + | collect_context_modes (Context m) = [m] + | collect_context_modes (Term _) = [] -datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term - | Generator of (string * typ); +(* representation of inferred clauses with modes *) -type moded_clause = term list * (indprem * tmode) list +type moded_clause = term list * (indprem * mode_derivation) list + type 'a pred_mode_table = (string * (mode * 'a) list) list +(* book-keeping *) + datatype predfun_data = PredfunData of { - name : string, definition : thm, intro : thm, elim : thm }; fun rep_predfun_data (PredfunData data) = data; -fun mk_predfun_data (name, definition, intro, elim) = - PredfunData {name = name, definition = definition, intro = intro, elim = elim} -datatype function_data = FunctionData of { - name : string, - equation : thm option (* is not used at all? *) -}; - -fun rep_function_data (FunctionData data) = data; -fun mk_function_data (name, equation) = - FunctionData {name = name, equation = equation} +fun mk_predfun_data (definition, intro, elim) = + PredfunData {definition = definition, intro = intro, elim = elim} datatype pred_data = PredData of { intros : thm list, elim : thm option, - nparams : int, - functions : bool * (mode * predfun_data) list, - random_functions : bool * (mode * function_data) list, - depth_limited_functions : bool * (mode * function_data) list, - annotated_functions : bool * (mode * function_data) list + function_names : (compilation * (mode * string) list) list, + predfun_data : (mode * predfun_data) list, + needs_random : mode list }; fun rep_pred_data (PredData data) = data; -fun mk_pred_data ((intros, elim, nparams), - (functions, random_functions, depth_limited_functions, annotated_functions)) = - PredData {intros = intros, elim = elim, nparams = nparams, - functions = functions, random_functions = random_functions, - depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions} -fun map_pred_data f (PredData {intros, elim, nparams, - functions, random_functions, depth_limited_functions, annotated_functions}) = - mk_pred_data (f ((intros, elim, nparams), (functions, random_functions, - depth_limited_functions, annotated_functions))) + +fun mk_pred_data ((intros, elim), (function_names, predfun_data, needs_random)) = + PredData {intros = intros, elim = elim, + function_names = function_names, predfun_data = predfun_data, needs_random = needs_random} + +fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) = + mk_pred_data (f ((intros, elim), (function_names, predfun_data, needs_random))) fun eq_option eq (NONE, NONE) = true | eq_option eq (SOME x, SOME y) = eq (x, y) @@ -218,8 +220,7 @@ fun eq_pred_data (PredData d1, PredData d2) = eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso - eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso - #nparams d1 = #nparams d2 + eq_option (Thm.eq_thm) (#elim d1, #elim d2) structure PredData = Theory_Data ( @@ -238,7 +239,7 @@ of NONE => error ("No such predicate " ^ quote name) | SOME data => data; -val is_registered = is_some oo lookup_pred_data +val is_registered = is_some oo lookup_pred_data val all_preds_of = Graph.keys o PredData.get @@ -250,24 +251,38 @@ val has_elim = is_some o #elim oo the_pred_data; -val nparams_of = #nparams oo the_pred_data - -val modes_of = (map fst) o snd o #functions oo the_pred_data +fun function_names_of compilation thy name = + case AList.lookup (op =) (#function_names (the_pred_data thy name)) compilation of + NONE => error ("No " ^ string_of_compilation compilation + ^ "functions defined for predicate " ^ quote name) + | SOME fun_names => fun_names -fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) +fun function_name_of compilation thy name mode = + case AList.lookup (op =) (function_names_of compilation thy name) mode of + NONE => error ("No " ^ string_of_compilation compilation + ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name) + | SOME function_name => function_name + +fun modes_of compilation thy name = map fst (function_names_of compilation thy name) -val defined_functions = fst o #functions oo the_pred_data +fun all_modes_of compilation thy = + map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name)) + (all_preds_of thy) + +val all_random_modes_of = all_modes_of Random + +fun defined_functions compilation thy name = + AList.defined (op =) (#function_names (the_pred_data thy name)) compilation fun lookup_predfun_data thy name mode = Option.map rep_predfun_data - (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode) + (AList.lookup (op =) (#predfun_data (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 thy name mode ^ - " of predicate " ^ name) - | SOME data => data; - -val predfun_name_of = #name ooo the_predfun_data +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 predicate " ^ name) + | SOME data => data; val predfun_definition_of = #definition ooo the_predfun_data @@ -275,102 +290,32 @@ val predfun_elim_of = #elim ooo the_predfun_data -fun lookup_random_function_data thy name mode = - Option.map rep_function_data - (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 thy name mode ^ - " of predicate " ^ name) - | SOME data => data - -val random_function_name_of = #name ooo the_random_function_data - -val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data - -val defined_random_functions = fst o #random_functions oo the_pred_data - -fun all_random_modes_of thy = - map (fn name => (name, random_modes_of thy name)) (all_preds_of thy) - -fun lookup_depth_limited_function_data thy name mode = - Option.map rep_function_data - (AList.lookup (op =) (snd (#depth_limited_functions (the_pred_data thy name))) mode) - -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 thy name mode - ^ " of predicate " ^ name) - | SOME data => data - -val depth_limited_function_name_of = #name ooo the_depth_limited_function_data - -val depth_limited_modes_of = (map fst) o snd o #depth_limited_functions oo the_pred_data - -val defined_depth_limited_functions = fst o #depth_limited_functions oo the_pred_data - -fun lookup_annotated_function_data thy name mode = - Option.map rep_function_data - (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 thy name mode - ^ " of predicate " ^ name) - | SOME data => data - -val annotated_function_name_of = #name ooo the_annotated_function_data - -val annotated_modes_of = (map fst) o snd o #annotated_functions oo the_pred_data - -val defined_annotated_functions = fst o #annotated_functions oo the_pred_data - (* diagnostic display functions *) 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 thy s) ms)) modes)) + string_of_mode 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 thy pred mode + fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode 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)) in () end; -fun string_of_prem thy (Prem (ts, p)) = - (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)" - | string_of_prem thy (Negprem (ts, p)) = - (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)" +fun string_of_prem thy (Prem t) = + (Syntax.string_of_term_global thy t) ^ "(premise)" + | string_of_prem thy (Negprem t) = + (Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)" | string_of_prem thy (Sidecond t) = (Syntax.string_of_term_global thy t) ^ "(sidecondition)" | string_of_prem thy _ = error "string_of_prem: unexpected input" -fun string_of_moded_prem thy (Prem (ts, p), tmode) = - (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ - "(" ^ (string_of_tmode tmode) ^ ")" - | string_of_moded_prem thy (Generator (v, T), _) = - "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T) - | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) = - (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ - "(negative mode: " ^ string_of_smode is ^ ")" - | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) = - (Syntax.string_of_term_global thy t) ^ - "(sidecond mode: " ^ string_of_smode is ^ ")" - | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented" - -fun print_moded_clauses thy = - let - fun string_of_clause pred mode clauses = - cat_lines (map (fn (ts, prems) => (space_implode " --> " - (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " " - ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses) - in print_pred_mode_table string_of_clause thy end; - fun string_of_clause thy pred (ts, prems) = (space_implode " --> " (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " " @@ -386,7 +331,6 @@ val preds = (Graph.keys o PredData.get) thy fun print pred () = let val _ = writeln ("predicate: " ^ pred) - val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred)) val _ = writeln ("introrules: ") val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm)) (rev (intros_of thy pred)) () @@ -400,16 +344,16 @@ fold print preds () end; -fun print_all_modes thy = +fun print_all_modes compilation thy = let val _ = writeln ("Inferred modes:") fun print (pred, modes) u = let val _ = writeln ("predicate: " ^ pred) - val _ = writeln ("modes: " ^ (commas (map (string_of_mode thy pred) modes))) + val _ = writeln ("modes: " ^ (commas (map string_of_mode modes))) in u end in - fold print (all_modes_of thy) () + fold print (all_modes_of compilation thy) () end (* validity checks *) @@ -420,12 +364,12 @@ 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 + val modes' = modes in - if not (eq_set eq_mode' (ms, modes')) then + 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)) + ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n" + ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms)) else () end | NONE => ()) @@ -437,12 +381,12 @@ SOME inferred_ms => let val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes)) - val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) inferred_ms + val modes' = inferred_ms in - if not (eq_set eq_mode' (ms, modes')) then + 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) ^ "\n" + ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n" + ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n" ^ "For the following clauses, the following modes could not be inferred: " ^ "\n" ^ cat_lines errors ^ (if not (null preds_without_modes) then @@ -474,58 +418,88 @@ end) handle Type.TUNIFY => (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); -fun import_intros inp_pred nparams [] ctxt = +fun import_intros inp_pred [] ctxt = let - val ([outp_pred], ctxt') = Variable.import_terms false [inp_pred] ctxt - 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 ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt + val T = fastype_of outp_pred + (* TODO: put in a function for this next line! *) + val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T) + val (param_names, ctxt'') = Variable.variant_fixes + (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' val params = map2 (curry Free) param_names paramTs - in (((outp_pred, params), []), ctxt') end - | import_intros inp_pred nparams (th :: ths) ctxt = + in + (((outp_pred, params), []), ctxt') + end + | import_intros inp_pred (th :: ths) ctxt = let - val ((_, [th']), ctxt') = Variable.import false [th] ctxt + val ((_, [th']), ctxt') = Variable.import true [th] ctxt val thy = ProofContext.theory_of ctxt' - val (pred, (params, args)) = strip_intro_concl nparams (prop_of th') - val ho_args = filter (is_predT o fastype_of) args + val (pred, args) = strip_intro_concl th' + val T = fastype_of pred + val ho_args = ho_args_of (hd (all_modes_of_typ T)) args fun subst_of (pred', pred) = let val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end fun instantiate_typ th = let - val (pred', _) = strip_intro_concl 0 (prop_of th) + val (pred', _) = strip_intro_concl th val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then error "Trying to instantiate another predicate" else () in Thm.certify_instantiate (subst_of (pred', pred), []) th end; fun instantiate_ho_args th = let - val (_, (params', args')) = strip_intro_concl nparams (prop_of th) - val ho_args' = map dest_Var (filter (is_predT o fastype_of) args') - in Thm.certify_instantiate ([], map dest_Var params' ~~ params) th end + val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th + val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args') + in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end val outp_pred = Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred val ((_, ths'), ctxt1) = Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' in - (((outp_pred, params), th' :: ths'), ctxt1) + (((outp_pred, ho_args), th' :: ths'), ctxt1) end (* generation of case rules from user-given introduction rules *) -fun mk_casesrule ctxt pred nparams introrules = +fun mk_args2 (Type ("*", [T1, T2])) st = + let + val (t1, st') = mk_args2 T1 st + val (t2, st'') = mk_args2 T2 st' + in + (HOLogic.mk_prod (t1, t2), st'') + end + | mk_args2 (T as Type ("fun", _)) (params, ctxt) = + let + val (S, U) = strip_type T + in + if U = HOLogic.boolT then + (hd params, (tl params, ctxt)) + else + let + val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt + in + (Free (x, T), (params, ctxt')) + end + end + | mk_args2 T (params, ctxt) = + let + val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt + in + (Free (x, T), (params, ctxt')) + end + +fun mk_casesrule ctxt pred introrules = let - val (((pred, params), intros_th), ctxt1) = import_intros pred nparams introrules ctxt + val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt val intros = map prop_of intros_th val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) - val (_, argsT) = chop nparams (binder_types (fastype_of pred)) - val (argnames, ctxt3) = Variable.variant_fixes - (map (fn i => "a" ^ string_of_int i) (1 upto length argsT)) ctxt2 - val argvs = map2 (curry Free) argnames argsT + val argsT = binder_types (fastype_of pred) + val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2) fun mk_case intro = let - val (_, (_, args)) = strip_intro_concl nparams intro + val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro val prems = Logic.strip_imp_prems intro val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args val frees = (fold o fold_aterms) @@ -533,11 +507,11 @@ if member (op aconv) params t then I else insert (op aconv) t | _ => I) (args @ prems) [] in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end - val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs)) + val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs)) val cases = map mk_case intros in Logic.list_implies (assm :: cases, prop) end; -(** preprocessing rules **) +(** preprocessing rules **) fun imp_prems_conv cv ct = case Thm.term_of ct of @@ -555,7 +529,7 @@ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) (Thm.transfer thy rule) -fun preprocess_elim thy nparams elimrule = +fun preprocess_elim thy elimrule = let fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) @@ -563,7 +537,7 @@ val ctxt = ProofContext.init thy val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt val prems = Thm.prems_of elimrule - val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams + val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) fun preprocess_case t = let val params = Logic.strip_params t @@ -585,15 +559,7 @@ fun expand_tuples_elim th = th -(* updaters *) - -fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4) -fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4) -fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4) -fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4) -fun appair f g (x, y) = (f x, g x) - -val no_compilation = ((false, []), (false, []), (false, []), (false, [])) +val no_compilation = ([], [], []) fun fetch_pred_data thy name = case try (Inductive.the_inductive (ProofContext.init thy)) name of @@ -608,20 +574,19 @@ val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index val pred = nth (#preds result) index - val nparams = length (Inductive.params_of (#raw_induct result)) (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams (expand_tuples_elim pre_elim))*) val elim = (Drule.standard o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init thy) pred nparams intros) + (mk_casesrule (ProofContext.init thy) pred intros) in - mk_pred_data ((intros, SOME elim, nparams), no_compilation) + mk_pred_data ((intros, SOME elim), no_compilation) end | NONE => error ("No such predicate: " ^ quote name) -fun add_predfun name mode data = +fun add_predfun_data name mode data = let - val add = (apsnd o apfst4) (fn (x, y) => (true, cons (mode, mk_predfun_data data) y)) + val add = (apsnd o apsnd3) (cons (mode, mk_predfun_data data)) in PredData.map (Graph.map_node name (map_pred_data add)) end fun is_inductive_predicate thy name = @@ -636,96 +601,74 @@ (is_inductive_predicate thy c orelse is_registered thy c)) end; - -(* code dependency graph *) -(* -fun dependencies_of thy name = - let - val (intros, elim, nparams) = fetch_pred_data thy name - val data = mk_pred_data ((intros, SOME elim, nparams), ([], [], [])) - val keys = depending_preds_of thy intros - in - (data, keys) - end; -*) - fun add_intro thm thy = let - val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) + val (name, T) = dest_Const (fst (strip_intro_concl 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 - | NONE => - let - val nparams = the_default (guess_nparams T) - (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) - in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end; + (apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr + | NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr in PredData.map cons_intro thy end 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) + fun set (intros, _) = (intros, SOME thm) in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end -fun set_nparams name nparams = +fun register_predicate (constname, pre_intros, pre_elim) thy = let - fun set (intros, elim, _ ) = (intros, elim, nparams) - in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end - -fun register_predicate (constname, pre_intros, pre_elim, nparams) thy = - let - (* preprocessing *) val intros = map (preprocess_intro thy) pre_intros - val elim = preprocess_elim thy nparams pre_elim + val elim = preprocess_elim thy pre_elim in if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map (Graph.new_node (constname, - mk_pred_data ((intros, SOME elim, nparams), no_compilation))) thy + mk_pred_data ((intros, SOME elim), no_compilation))) thy else thy end fun register_intros (constname, pre_intros) thy = let val T = Sign.the_const_type thy constname - fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr)))) + fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr))) val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then error ("register_intros: Introduction rules of different constants are used\n" ^ "expected rules for " ^ constname ^ ", but received rules for " ^ commas (map constname_of_intro pre_intros)) else () val pred = Const (constname, T) - val nparams = guess_nparams T val pre_elim = (Drule.standard o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init thy) pred nparams pre_intros) - in register_predicate (constname, pre_intros, pre_elim, nparams) thy end + (mk_casesrule (ProofContext.init thy) pred pre_intros) + in register_predicate (constname, pre_intros, pre_elim) thy end -fun set_random_function_name pred mode name = +fun defined_function_of compilation pred = let - val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) + val set = (apsnd o apfst3) (cons (compilation, [])) in PredData.map (Graph.map_node pred (map_pred_data set)) end -fun set_depth_limited_function_name pred mode name = +fun set_function_name compilation pred mode name = let - val set = (apsnd o aptrd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) + val set = (apsnd o apfst3) + (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name))) in PredData.map (Graph.map_node pred (map_pred_data set)) end -fun set_annotated_function_name pred mode name = +fun set_needs_random name modes = let - val set = (apsnd o apfourth4) - (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) + val set = (apsnd o aptrd3) (K modes) in - PredData.map (Graph.map_node pred (map_pred_data set)) + PredData.map (Graph.map_node name (map_pred_data set)) end +(* datastructures and setup for generic compilation *) + datatype compilation_funs = CompilationFuns of { mk_predT : typ -> typ, dest_predT : typ -> typ, @@ -789,6 +732,8 @@ Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x end; +fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) + fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp; @@ -811,7 +756,7 @@ fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) fun mk_single t = - let + let val T = fastype_of t in Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t @@ -840,54 +785,119 @@ mk_not = mk_not, mk_map = mk_map}; end; + +structure DSequence_CompFuns = +struct + +fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, + Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])]) + +fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, + Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])) = T + | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []); + +fun mk_bot T = Const ("DSequence.empty", mk_dseqT T); + +fun mk_single t = + let val T = fastype_of t + in Const("DSequence.single", T --> mk_dseqT T) $ t end; + +fun mk_bind (x, f) = + let val T as Type ("fun", [_, U]) = fastype_of f + in + Const ("DSequence.bind", fastype_of x --> T --> U) $ x $ f + end; + +val mk_sup = HOLogic.mk_binop "DSequence.union"; + +fun mk_if cond = Const ("DSequence.if_seq", + HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond; + +fun mk_not t = let val T = mk_dseqT HOLogic.unitT + in Const ("DSequence.not_seq", T --> T) $ t end + +fun mk_map T1 T2 tf tp = Const ("DSequence.map", + (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp + +val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT, + mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + mk_not = mk_not, mk_map = mk_map} + +end; + +structure Random_Sequence_CompFuns = +struct + +fun mk_random_dseqT T = + @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed}) + +fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, + Type ("fun", [@{typ Random.seed}, + Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T + | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); + +fun mk_bot T = Const ("Random_Sequence.empty", mk_random_dseqT T); + +fun mk_single t = + let val T = fastype_of t + in Const("Random_Sequence.single", T --> mk_random_dseqT T) $ t end; + +fun mk_bind (x, f) = + let + val T as Type ("fun", [_, U]) = fastype_of f + in + Const ("Random_Sequence.bind", fastype_of x --> T --> U) $ x $ f + end; + +val mk_sup = HOLogic.mk_binop "Random_Sequence.union"; + +fun mk_if cond = Const ("Random_Sequence.if_random_dseq", + HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond; + +fun mk_not t = let val T = mk_random_dseqT HOLogic.unitT + in Const ("Random_Sequence.not_random_dseq", T --> T) $ t end + +fun mk_map T1 T2 tf tp = Const ("Random_Sequence.map", + (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp + +val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT, + mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + mk_not = mk_not, mk_map = mk_map} + +end; + + + +fun mk_random T = + let + val random = Const ("Quickcheck.random_class.random", + @{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) + in + Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> + Random_Sequence_CompFuns.mk_random_dseqT T) $ random + end; + + + (* for external use with interactive mode *) val pred_compfuns = PredicateCompFuns.compfuns -val randompred_compfuns = RandomPredCompFuns.compfuns; - -fun lift_random random = - let - val T = dest_randomT (fastype_of random) - in - Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} --> - HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> - RandomPredCompFuns.mk_randompredT T) $ random - end; +val randompred_compfuns = Random_Sequence_CompFuns.compfuns; (* function types and names of different compilations *) -fun funT_of compfuns (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs - in - (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) - end; - -fun depth_limited_funT_of compfuns (iss, is) T = +fun funT_of compfuns mode T = let val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = - map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs + val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts in - (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) - ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) + inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs)) end; -fun random_function_funT_of (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs - in - (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> - (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) - end +(** mode analysis **) -(* Mode analysis *) - -(*** check if a term contains only constructor functions ***) fun is_constrt thy = let val cnstrs = flat (maps @@ -924,235 +934,347 @@ val is = subsets (i+1) j in merge (map (fn ks => i::ks) is) is end else [[]]; - -(* FIXME: should be in library - cprod = map_prod I *) -fun cprod ([], ys) = [] - | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); - -fun cprods xss = List.foldr (map op :: o cprod) [[]] xss; - -fun cprods_subset [] = [[]] - | cprods_subset (xs :: xss) = - let - val yss = (cprods_subset xss) - in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end - -fun modes_of_term modes t = - let - val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t)); - val default = [Mode (([], ks), ks, [])]; - fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => - let - val (args1, args2) = - if length args < length iss then - error ("Too few arguments for inductive predicate " ^ name) - else chop (length iss) args; - val k = length args2; - val prfx = map (rpair NONE) (1 upto k) - in - if not (is_prefix op = prfx is) then [] else - let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k)) - in map (fn x => Mode (m, is', x)) (cprods (map - (fn (NONE, _) => [NONE] - | (SOME js, arg) => map SOME (filter - (fn Mode (_, js', _) => js=js') (modes_of_term modes arg))) - (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) - | (Var ((name, _), _), args) => the (mk_modes name args) - | (Free (name, _), args) => the (mk_modes name args) - | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *) - | _ => default - end - -fun select_mode_prem thy modes vs ps = - find_first (is_some o snd) (ps ~~ map - (fn Prem (us, t) => find_first (fn Mode (_, is, _) => - let - val (in_ts, out_ts) = split_smode is us; - val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts; - val vTs = maps term_vTs out_ts'; - val dupTs = map snd (duplicates (op =) vTs) @ - map_filter (AList.lookup (op =) vTs) vs; - in - subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso - forall (is_eqT o fastype_of) in_ts' andalso - subset (op =) (term_vs t, vs) andalso - forall is_eqT dupTs - end) - (modes_of_term modes t handle Option => - error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) - | Negprem (us, t) => find_first (fn Mode (_, is, _) => - is = map (rpair NONE) (1 upto length us) andalso - subset (op =) (terms_vs us, vs) andalso - subset (op =) (term_vs t, vs)) - (modes_of_term modes t handle Option => - error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) - | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], [])) - else NONE - ) ps); - -fun fold_prem f (Prem (args, _)) = fold f args - | fold_prem f (Negprem (args, _)) = fold f args - | fold_prem f (Sidecond t) = f t - -fun all_subsets [] = [[]] - | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end - -fun generator vTs v = - let - val T = the (AList.lookup (op =) vTs v) - in - (Generator (v, T), Mode (([], []), [], [])) - end; - -fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) = - let - val modes' = modes @ map_filter - (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) - (param_vs ~~ iss); - val gen_modes' = gen_modes @ map_filter - (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) - (param_vs ~~ iss); - val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts [])) - val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps []) - fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs) - | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of - NONE => - (if with_generator then - (case select_mode_prem thy gen_modes' vs ps of - SOME (p as Prem _, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) - (filter_out (equal p) ps) - | _ => - let - val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) - |> sort (int_ord o (pairself length)) - in - case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) - all_generator_vs) of - SOME generator_vs => check_mode_prems - ((map (generator vTs) generator_vs) @ acc_ps) - (union (op =) vs generator_vs) ps - | NONE => NONE - end) - else - NONE) - | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) - (filter_out (equal p) ps)) - val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); - val in_vs = terms_vs in_ts; - val concl_vs = terms_vs ts - in - if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso - forall (is_eqT o fastype_of) in_ts' then - case check_mode_prems [] (union (op =) param_vs in_vs) ps of - NONE => NONE - | SOME (acc_ps, vs) => - if with_generator then - SOME (ts, (rev acc_ps) @ (map (generator vTs) (subtract (op =) vs concl_vs))) - else - if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE - else NONE - end; fun print_failed_mode options thy modes p m rs is = if show_mode_inference options then let val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ - p ^ " violates mode " ^ string_of_mode thy p m) + p ^ " violates mode " ^ string_of_mode m) in () end else () -fun error_of thy p m is = +fun error_of p m is = (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ - p ^ " violates mode " ^ string_of_mode thy p m) + p ^ " violates mode " ^ string_of_mode m) + +fun is_all_input mode = + let + fun is_all_input' (Fun _) = true + | is_all_input' (Pair (m1, m2)) = is_all_input' m1 andalso is_all_input' m2 + | is_all_input' Input = true + | is_all_input' Output = false + in + forall is_all_input' (strip_fun_mode mode) + end + +fun all_input_of T = + let + val (Ts, U) = strip_type T + fun input_of (Type ("*", [T1, T2])) = Pair (input_of T1, input_of T2) + | input_of _ = Input + in + if U = HOLogic.boolT then + fold_rev (curry Fun) (map input_of Ts) Bool + else + error "all_input_of: not a predicate" + end + +fun partial_hd [] = NONE + | partial_hd (x :: xs) = SOME x + +fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm []; +val terms_vs = distinct (op =) o maps term_vs; + +fun input_mode T = + let + val (Ts, U) = strip_type T + in + fold_rev (curry Fun) (map (K Input) Ts) Input + end + +fun output_mode T = + let + val (Ts, U) = strip_type T + in + fold_rev (curry Fun) (map (K Output) Ts) Output + end + +fun is_invertible_function thy (Const (f, _)) = is_constr thy f + | is_invertible_function thy _ = false + +fun non_invertible_subterms thy (Free _) = [] + | non_invertible_subterms thy t = + case (strip_comb t) of (f, args) => + if is_invertible_function thy f then + maps (non_invertible_subterms thy) args + else + [t] -fun find_indices f xs = - map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs) +fun collect_non_invertible_subterms thy (f as Free _) (names, eqs) = (f, (names, eqs)) + | collect_non_invertible_subterms thy t (names, eqs) = + case (strip_comb t) of (f, args) => + if is_invertible_function thy f then + let + val (args', (names', eqs')) = + fold_map (collect_non_invertible_subterms thy) args (names, eqs) + in + (list_comb (f, args'), (names', eqs')) + end + else + let + val s = Name.variant names "x" + val v = Free (s, fastype_of t) + in + (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs)) + end +(* + if is_constrt thy t then (t, (names, eqs)) else + let + val s = Name.variant names "x" + val v = Free (s, fastype_of t) + in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; +*) + +fun is_possible_output thy vs t = + forall + (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t)) + (non_invertible_subterms thy t) -fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = +fun vars_of_destructable_term thy (Free (x, _)) = [x] + | vars_of_destructable_term thy t = + case (strip_comb t) of (f, args) => + if is_invertible_function thy f then + maps (vars_of_destructable_term thy) args + else + [] + +fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t) + +fun missing_vars vs t = subtract (op =) vs (term_vs t) + +fun derivations_of thy modes vs t Input = + [(Term Input, missing_vars vs t)] + | derivations_of thy modes vs t Output = + if is_possible_output thy vs t then [(Term Output, [])] else [] + | derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) = + map_product + (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) + (derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2) + | derivations_of thy modes vs t m = + (case try (all_derivations_of thy modes vs) t of + SOME derivs => filter (fn (d, mvars) => mode_of d = m) derivs + | NONE => (if is_all_input m then [(Context m, [])] else [])) +and all_derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) = + let + val derivs1 = all_derivations_of thy modes vs t1 + val derivs2 = all_derivations_of thy modes vs t2 + in + map_product + (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) + derivs1 derivs2 + end + | all_derivations_of thy modes vs (t1 $ t2) = let - val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] - fun invalid_mode m = - case find_indices - (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of - [] => NONE - | is => SOME (error_of thy p m is) - val res = map (fn m => (m, invalid_mode m)) ms - val ms' = map_filter (fn (m, NONE) => SOME m | _ => NONE) res - val errors = map_filter snd res + val derivs1 = all_derivations_of thy modes vs t1 + in + maps (fn (d1, mvars1) => + case mode_of d1 of + Fun (m', _) => map (fn (d2, mvars2) => + (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m') + | _ => error "Something went wrong") derivs1 + end + | all_derivations_of thy modes vs (Const (s, T)) = + (case (AList.lookup (op =) modes s) of + SOME ms => map (fn m => (Context m, [])) ms + | NONE => error ("No mode for constant " ^ s)) + | all_derivations_of _ modes vs (Free (x, _)) = + (case (AList.lookup (op =) modes x) of + SOME ms => map (fn m => (Context m , [])) ms + | NONE => error ("No mode for parameter variable " ^ x)) + | all_derivations_of _ modes vs _ = error "all_derivations_of" + +fun rev_option_ord ord (NONE, NONE) = EQUAL + | rev_option_ord ord (NONE, SOME _) = GREATER + | rev_option_ord ord (SOME _, NONE) = LESS + | rev_option_ord ord (SOME x, SOME y) = ord (x, y) + +fun term_of_prem (Prem t) = t + | term_of_prem (Negprem t) = t + | term_of_prem (Sidecond t) = t + +fun random_mode_in_deriv modes t deriv = + case try dest_Const (fst (strip_comb t)) of + SOME (s, _) => + (case AList.lookup (op =) modes s of + SOME ms => + (case AList.lookup (op =) ms (head_mode_of deriv) of + SOME r => r + | NONE => false) + | NONE => false) + | NONE => false + +fun number_of_output_positions mode = + let + val args = strip_fun_mode mode + fun contains_output (Fun _) = false + | contains_output Input = false + | contains_output Output = true + | contains_output (Pair (m1, m2)) = contains_output m1 orelse contains_output m2 + in + length (filter contains_output args) + end + +fun lex_ord ord1 ord2 (x, x') = + case ord1 (x, x') of + EQUAL => ord2 (x, x') + | ord => ord + +fun deriv_ord2' thy modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) = + let + fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) = + int_ord (length mvars1, length mvars2) + fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) = + int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0, + if random_mode_in_deriv modes t1 deriv1 then 1 else 0) + fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) = + int_ord (number_of_output_positions (head_mode_of deriv1), + number_of_output_positions (head_mode_of deriv2)) + in + lex_ord mvars_ord (lex_ord random_mode_ord output_mode_ord) + ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) + end + +fun deriv_ord2 thy modes t = deriv_ord2' thy modes t t + +fun deriv_ord ((deriv1, mvars1), (deriv2, mvars2)) = + int_ord (length mvars1, length mvars2) + +fun premise_ord thy modes ((prem1, a1), (prem2, a2)) = + rev_option_ord (deriv_ord2' thy modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2) + +fun print_mode_list modes = + tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^ + commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes))) + +fun select_mode_prem' thy modes vs ps = + let + val modes' = map (fn (s, ms) => (s, map fst ms)) modes + in + partial_hd (sort (premise_ord thy modes) (ps ~~ map + (fn Prem t => + partial_hd + (sort (deriv_ord2 thy modes t) (all_derivations_of thy modes' vs t)) + | Sidecond t => SOME (Context Bool, missing_vars vs t) + | Negprem t => + partial_hd + (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d)) + (all_derivations_of thy modes' vs t))) + | p => error (string_of_prem thy p)) + ps)) + end + +fun check_mode_clause' use_random thy param_vs modes mode (ts, ps) = + let + val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts [])) + val modes' = modes @ (param_vs ~~ map (fn x => [(x, false)]) (ho_arg_modes_of mode)) + val (in_ts, out_ts) = split_mode mode ts + val in_vs = maps (vars_of_destructable_term thy) in_ts + val out_vs = terms_vs out_ts + fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd) + | check_mode_prems acc_ps rnd vs ps = + (case select_mode_prem' thy modes' vs ps of + SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd (*TODO: uses random? *) + (case p of + Prem t => union (op =) vs (term_vs t) + | Sidecond t => vs + | Negprem t => union (op =) vs (term_vs t) + | _ => error "I do not know") + (filter_out (equal p) ps) + | SOME (p, SOME (deriv, missing_vars)) => + if use_random then + check_mode_prems ((p, deriv) :: (map + (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) missing_vars) + @ acc_ps) true + (case p of + Prem t => union (op =) vs (term_vs t) + | Sidecond t => union (op =) vs (term_vs t) + | Negprem t => union (op =) vs (term_vs t) + | _ => error "I do not know") + (filter_out (equal p) ps) + else NONE + | SOME (p, NONE) => NONE + | NONE => NONE) + in + case check_mode_prems [] false in_vs ps of + NONE => NONE + | SOME (acc_ps, vs, rnd) => + if forall (is_constructable thy vs) (in_ts @ out_ts) then + SOME (ts, rev acc_ps, rnd) + else + if use_random then + let + val generators = map + (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) + (subtract (op =) vs (terms_vs out_ts)) + in + SOME (ts, rev (generators @ acc_ps), true) + end + else + NONE + end + +datatype result = Success of bool | Error of string + +fun check_modes_pred' use_random options thy param_vs clauses modes (p, ms) = + let + fun split xs = + let + fun split' [] (ys, zs) = (rev ys, rev zs) + | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs) + | split' ((m, Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs) + in + split' xs ([], []) + end + val rs = these (AList.lookup (op =) clauses p) + fun check_mode m = + let + val res = map (check_mode_clause' use_random thy param_vs modes m) rs + in + case find_indices is_none res of + [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res) + | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)) + end + val res = map (fn (m, _) => (m, check_mode m)) ms + val (ms', errors) = split res in ((p, ms'), errors) end; -fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) = +fun get_modes_pred' use_random thy param_vs clauses modes (p, ms) = let - val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] + val rs = these (AList.lookup (op =) clauses p) in - (p, map (fn m => - (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms) + (p, map (fn (m, rnd) => + (m, map ((fn (ts, ps, rnd) => (ts, ps)) o the o check_mode_clause' use_random thy param_vs modes m) rs)) ms) end; -fun fixp f (x : (string * mode list) list) = +fun fixp f x = let val y = f x in if x = y then x else fixp f y end; -fun fixp_with_state f ((x : (string * mode list) list), state) = +fun fixp_with_state f (x, state) = let val (y, state') = f (x, state) in if x = y then (y, state') else fixp_with_state f (y, state') end -fun infer_modes options thy extra_modes all_modes param_vs clauses = +fun infer_modes use_random options preds extra_modes param_vs clauses thy = let + val all_modes = map (fn (s, T) => (s, map (rpair false) (all_modes_of_typ T))) preds + fun needs_random s m = (m, member (op =) (#needs_random (the_pred_data thy s)) m) + val extra_modes = map (fn (s, ms) => (s, map (needs_random s) ms)) extra_modes val (modes, errors) = fixp_with_state (fn (modes, errors) => let val res = map - (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes + (check_modes_pred' use_random options thy param_vs clauses (modes @ extra_modes)) modes in (map fst res, errors @ maps snd res) end) (all_modes, []) + val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then + set_needs_random s (map fst (filter (fn (_, rnd) => rnd = true) ms)) else I) modes thy in - (map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes, errors) - end; - -fun remove_from rem [] = [] - | remove_from rem ((k, vs) :: xs) = - (case AList.lookup (op =) rem k of - NONE => (k, vs) - | SOME vs' => (k, subtract (op =) vs' vs)) - :: remove_from rem xs - -fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses = - let - val prednames = map fst clauses - val extra_modes' = all_modes_of thy - val gen_modes = all_random_modes_of thy - |> filter_out (fn (name, _) => member (op =) prednames name) - val starting_modes = remove_from extra_modes' all_modes - fun eq_mode (m1, m2) = (m1 = m2) - val (modes, errors) = - fixp_with_state (fn (modes, errors) => - let - val res = map - (check_modes_pred options true thy param_vs clauses extra_modes' - (gen_modes @ modes)) modes - in (map fst res, errors @ maps snd res) end) (starting_modes, []) - val moded_clauses = - map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes - val (moded_clauses', _) = infer_modes options thy extra_modes all_modes param_vs clauses - val join_moded_clauses_table = AList.join (op =) - (fn _ => fn ((mps1, mps2)) => - merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2)) - in - (join_moded_clauses_table (moded_clauses', moded_clauses), errors) + ((map (get_modes_pred' use_random thy param_vs clauses (modes @ extra_modes)) modes, errors), thy') end; (* term construction *) @@ -1231,10 +1353,9 @@ datatype comp_modifiers = Comp_Modifiers of { - function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, - set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory, + compilation : compilation, function_name_prefix : string, - funT_of : compilation_funs -> mode -> typ -> typ, + compfuns : compilation_funs, additional_arguments : string list -> term list, wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term, transform_additional_arguments : indprem -> term list -> term list @@ -1242,25 +1363,27 @@ fun dest_comp_modifiers (Comp_Modifiers c) = c -val function_name_of = #function_name_of o dest_comp_modifiers -val set_function_name = #set_function_name o dest_comp_modifiers +val compilation = #compilation o dest_comp_modifiers val function_name_prefix = #function_name_prefix o dest_comp_modifiers -val funT_of = #funT_of o dest_comp_modifiers +val compfuns = #compfuns o dest_comp_modifiers +val funT_of = funT_of o compfuns val additional_arguments = #additional_arguments o dest_comp_modifiers val wrap_compilation = #wrap_compilation o dest_comp_modifiers val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers end; +(* TODO: uses param_vs -- change necessary for compilation with new modes *) fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg = let fun map_params (t as Free (f, T)) = if member (op =) param_vs f then - case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of + case (AList.lookup (op =) (param_vs ~~ iss) f) of SOME is => let - val T' = Comp_Mod.funT_of compilation_modifiers compfuns ([], is) T - in fst (mk_Eval_of additional_arguments ((Free (f, T'), T), SOME is) []) end + val _ = error "compile_arg: A parameter in a input position -- do we have a test case?" + val T' = Comp_Mod.funT_of compilation_modifiers is T + in t(*fst (mk_Eval_of additional_arguments ((Free (f, T'), T), is) [])*) end | NONE => t else t | map_params t = t @@ -1291,104 +1414,83 @@ (v', mk_bot compfuns U')])) end; -(*FIXME function can be removed*) -fun mk_funcomp f t = +fun compile_expr compilation_modifiers compfuns thy (t, deriv) additional_arguments = let - val names = Term.add_free_names t []; - val Ts = binder_types (fastype_of t); - val vs = map2 (curry Free) - (Name.variant_list names (replicate (length Ts) "x")) Ts + fun expr_of (t, deriv) = + (case (t, deriv) of + (t, Term Input) => SOME t + | (t, Term Output) => NONE + | (Const (name, T), Context mode) => + SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name mode, + Comp_Mod.funT_of compilation_modifiers mode T)) + | (Free (s, T), Context m) => + SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T)) + | (t, Context m) => + let + val bs = map (pair "x") (binder_types (fastype_of t)) + val bounds = map Bound (rev (0 upto (length bs) - 1)) + in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end + | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) => + (case (expr_of (t1, d1), expr_of (t2, d2)) of + (NONE, NONE) => NONE + | (NONE, SOME t) => SOME t + | (SOME t, NONE) => SOME t + | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2))) + | (t1 $ t2, Mode_App (deriv1, deriv2)) => + (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of + (SOME t, NONE) => SOME t + | (SOME t, SOME u) => SOME (t $ u) + | _ => error "something went wrong here!")) 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 = - let - val (f, args) = strip_comb (Envir.eta_contract t) - val (params, args') = chop (length ms) args - 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, - Comp_Mod.funT_of compilation_modifiers compfuns mode T) - | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T) - | _ => error ("PredicateCompiler: illegal parameter term") - in - list_comb (f', params' @ args') - end - -fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) - inargs additional_arguments = - case strip_comb t of - (Const (name, T), params) => - let - 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 - (list_comb (Const (name', T'), params' @ inargs @ additional_arguments)) - end - | (Free (name, T), params) => - list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T), - params @ inargs @ additional_arguments) + the (expr_of (t, deriv)) + end fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments - (iss, is) inp (ts, moded_ps) = + mode inp (ts, moded_ps) = let + val iss = ho_arg_modes_of mode val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy - fun check_constrt t (names, eqs) = - if is_constrt thy t then (t, (names, eqs)) else - let - val s = Name.variant names "x" - val v = Free (s, fastype_of t) - in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; - - val (in_ts, out_ts) = split_smode is ts; + val (in_ts, out_ts) = split_mode mode ts; val (in_ts', (all_vs', eqs)) = - fold_map check_constrt in_ts (all_vs, []); - + fold_map (collect_non_invertible_subterms thy) in_ts (all_vs, []); fun compile_prems out_ts' vs names [] = let val (out_ts'', (names', eqs')) = - fold_map check_constrt out_ts' (names, []); + fold_map (collect_non_invertible_subterms thy) out_ts' (names, []); val (out_ts''', (names'', constr_vs)) = fold_map distinct_v out_ts'' (names', map (rpair []) vs); in compile_match constr_vs (eqs @ eqs') out_ts''' (mk_single compfuns (HOLogic.mk_tuple out_ts)) end - | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) = + | compile_prems out_ts vs names ((p, deriv) :: ps) = let val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); val (out_ts', (names', eqs)) = - fold_map check_constrt out_ts (names, []) + fold_map (collect_non_invertible_subterms thy) out_ts (names, []) val (out_ts'', (names'', constr_vs')) = fold_map distinct_v out_ts' ((names', map (rpair []) vs)) + val mode = head_mode_of deriv val additional_arguments' = Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments val (compiled_clause, rest) = case p of - Prem (us, t) => + Prem t => let - val (in_ts, out_ts''') = split_smode is us; - val in_ts = map (compile_arg compilation_modifiers compfuns - additional_arguments thy param_vs iss) in_ts val u = compile_expr compilation_modifiers compfuns thy - (mode, t) in_ts additional_arguments' + (t, deriv) additional_arguments' + val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) end - | Negprem (us, t) => + | Negprem t => let - val (in_ts, out_ts''') = split_smode is us - val in_ts = map (compile_arg compilation_modifiers compfuns - additional_arguments thy param_vs iss) in_ts val u = mk_not compfuns (compile_expr compilation_modifiers compfuns thy - (mode, t) in_ts additional_arguments') + (t, deriv) additional_arguments') + val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1403,8 +1505,7 @@ end | Generator (v, T) => let - val [size] = additional_arguments - val u = lift_random (HOLogic.mk_random T size) + val u = mk_random T val rest = compile_prems [Free (v, T)] vs' names'' ps; in (u, rest) @@ -1418,47 +1519,45 @@ mk_bind compfuns (mk_single compfuns inp, prem_t) end -fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls = +fun compile_pred compilation_modifiers thy all_vs param_vs s T mode moded_cls = let - val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) - val (Us1, Us2) = split_smodeT (snd mode) Ts2 - val Ts1' = - map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) - (fst mode) Ts1 - fun mk_input_term (i, NONE) = - [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] - | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of - [] => error "strange unit input" - | [T] => [Free (Name.variant (all_vs @ param_vs) - ("x" ^ string_of_int i), nth Ts2 (i - 1))] - | Ts => let - 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 (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 + (* TODO: val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs) + *) + val compfuns = Comp_Mod.compfuns compilation_modifiers + fun is_param_type (T as Type ("fun",[_ , T'])) = + is_some (try (dest_predT compfuns) T) orelse is_param_type T' + | is_param_type T = is_some (try (dest_predT compfuns) T) + val additional_arguments = [] + val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode + (binder_types T) + val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs) + val funT = Comp_Mod.funT_of compilation_modifiers mode T + + val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod) + (fn T => fn (param_vs, names) => + if is_param_type T then + (Free (hd param_vs, T), (tl param_vs, names)) + else + let + val new = Name.variant names "x" + in (Free (new, T), (param_vs, new :: names)) end)) inpTs + (param_vs, (all_vs @ param_vs)) + val in_ts' = map_filter (map_filter_prod + (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts val cl_ts = map (compile_clause compilation_modifiers compfuns - thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls; + thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls; val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments (if null cl_ts then - mk_bot compfuns (HOLogic.mk_tupleT Us2) + mk_bot compfuns (HOLogic.mk_tupleT outTs) else foldr1 (mk_sup compfuns) cl_ts) val fun_const = - Const (Comp_Mod.function_name_of compilation_modifiers thy s mode, - Comp_Mod.funT_of compilation_modifiers compfuns mode T) + Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s mode, funT) in HOLogic.mk_Trueprop - (HOLogic.mk_eq (list_comb (fun_const, params @ in_ts @ additional_arguments), compilation)) + (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation)) end; (* special setup for simpset *) @@ -1474,152 +1573,108 @@ (fn NONE => "X" | SOME k' => string_of_int k') (ks @ [SOME k]))) arities)); -fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy = -let - val Ts = binder_types (fastype_of pred) - val funtrm = Const (mode_id, funT) - val (Ts1, Ts2) = chop (length iss) Ts; - val Ts1' = - 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 = map2 (curry Free) param_names Ts1' - fun mk_args (i, T) argnames = +fun split_lambda (x as Free _) t = lambda x t + | split_lambda (Const ("Pair", _) $ t1 $ t2) t = + HOLogic.mk_split (split_lambda t1 (split_lambda t2 t)) + | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t) + | split_lambda t _ = raise (TERM ("split_lambda", [t])) + +fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t + | strip_split_abs (Abs (_, _, t)) = strip_split_abs t + | strip_split_abs t = t + +fun mk_args is_eval (Pair (m1, m2), Type ("*", [T1, T2])) names = let - val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i)) - val default = (Free (vname, T), vname :: argnames) + val (t1, names') = mk_args is_eval (m1, T1) names + val (t2, names'') = mk_args is_eval (m2, T2) names' + in + (HOLogic.mk_prod (t1, t2), names'') + end + | mk_args is_eval ((m as Fun _), T) names = + let + val funT = funT_of PredicateCompFuns.compfuns m T + val x = Name.variant names "x" + val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names) + val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args + val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval + (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs)) + in + (if is_eval then t else Free (x, funT), x :: names) + end + | mk_args is_eval (_, T) names = + let + val x = Name.variant names "x" in - case AList.lookup (op =) is i of - NONE => default - | SOME NONE => default - | SOME (SOME pis) => - case HOLogic.strip_tupleT T of - [] => default - | [_] => default - | Ts => - let - 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 (map2 (curry Free) vnames Ts), vnames @ argnames) end + (Free (x, T), x :: names) 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 = 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 = 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)) - val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), - HOLogic.mk_tuple outargs)) - val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) - val simprules = [defthm, @{thm eval_pred}, - @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] - val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 - val introthm = Goal.prove (ProofContext.init thy) - (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac) - val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); - val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) - val elimthm = Goal.prove (ProofContext.init thy) - (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac) -in - (introthm, elimthm) -end; + +fun create_intro_elim_rule mode defthm mode_id funT pred thy = + let + val funtrm = Const (mode_id, funT) + val Ts = binder_types (fastype_of pred) + val (args, argnames) = fold_map (mk_args true) (strip_fun_mode mode ~~ Ts) [] + fun strip_eval _ t = + let + val t' = strip_split_abs t + val (r, _) = PredicateCompFuns.dest_Eval t' + in (SOME (fst (strip_comb r)), NONE) end + val (inargs, outargs) = split_map_mode strip_eval mode args + val eval_hoargs = ho_args_of mode args + val hoargTs = ho_argsT_of mode Ts + val hoarg_names' = + Name.variant_list argnames ((map (fn i => "x" ^ string_of_int i)) (1 upto (length hoargTs))) + val hoargs' = map2 (curry Free) hoarg_names' hoargTs + val args' = replace_ho_args mode hoargs' args + val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args')) + val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args)) + val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs' + val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs), + if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs)) + val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs), + HOLogic.mk_tuple outargs)) + val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) + val simprules = [defthm, @{thm eval_pred}, + @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] + val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 + val introthm = Goal.prove (ProofContext.init thy) + (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac) + val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); + val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) + val elimthm = Goal.prove (ProofContext.init thy) + (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac) + in + (introthm, elimthm) + end fun create_constname_of_mode options thy prefix name T mode = let 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)) + ^ "_" ^ ascii_string_of_mode mode + val name = the_default system_proposal (proposed_names options name mode) in Sign.full_bname thy name end; -fun split_tupleT is T = - let - fun split_tuple' _ _ [] = ([], []) - | split_tuple' is i (T::Ts) = - (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) - end - -fun mk_arg xin xout pis T = - let - val n = length (HOLogic.strip_tupleT T) - val ni = length pis - 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 member (op =) pis i then - (mk_proj si ni xin, (si+1, so)) - else - (mk_proj so (n - ni) xout, (si, so+1)) - val (args, _) = fold_map mk_arg' (1 upto n) (1, 1) - in - HOLogic.mk_tuple args - end - 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 = + fun create_definition mode thy = let 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 - val (Us1, Us2) = split_smodeT is Ts2 - val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1 - 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))); - val param_names = Name.variant_list [] - (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1'))) - val xparams = map2 (curry Free) param_names Ts1' - fun mk_vars (i, T) names = + val funT = funT_of compfuns mode T + val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) [] + fun strip_eval m t = let - val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i)) - in - case AList.lookup (op =) is i of - NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names) - | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names) - | SOME (SOME pis) => - let - val (Tins, Touts) = split_tupleT pis T - val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in") - val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out") - val xin = Free (name_in, HOLogic.mk_tupleT Tins) - val xout = Free (name_out, HOLogic.mk_tupleT Touts) - val xarg = mk_arg xin xout pis T - in - (((if null Tins then [] else [xin], - if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end - end - val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names - val (xinout, xargs) = split_list xinoutargs - val (xins, xouts) = pairself flat (split_list xinout) - val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names - 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 = - let - fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) - | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) - in - mk_split_lambda' xs t - end; - val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts - (list_comb (Const (name, T), xparams' @ xargs))) - val lhs = list_comb (Const (mode_cname, funT), xparams @ xins) + val t' = strip_split_abs t + val (r, _) = PredicateCompFuns.dest_Eval t' + in (SOME (fst (strip_comb r)), NONE) end + val (inargs, outargs) = split_map_mode strip_eval mode args + val predterm = fold_rev split_lambda inargs + (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs) + (list_comb (Const (name, T), args)))) + val lhs = Const (mode_cname, funT) val def = Logic.mk_equals (lhs, predterm) val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> @@ -1627,13 +1682,14 @@ val (intro, elim) = create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy' in thy' - |> add_predfun name mode (mode_cname, definition, intro, elim) + |> set_function_name Pred name mode mode_cname + |> add_predfun_data name mode (definition, intro, elim) |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd |> Theory.checkpoint end; in - fold create_definition modes thy + thy |> defined_function_of Pred name |> fold create_definition modes end; fun define_functions comp_modifiers compfuns options preds (name, modes) thy = @@ -1643,13 +1699,15 @@ let val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers 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 + val funT = Comp_Mod.funT_of comp_modifiers mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname + |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname end; in - fold create_definition modes thy + thy + |> defined_function_of (Comp_Mod.compilation comp_modifiers) name + |> fold create_definition modes end; (* Proving equivalence of term *) @@ -1674,11 +1732,13 @@ (* MAJOR FIXME: prove_params should be simple - different form of introrule for parameters ? *) -fun prove_param options thy NONE t = TRY (rtac @{thm refl} 1) - | prove_param options thy (m as SOME (Mode (mode, is, ms))) t = + +fun prove_param options thy t deriv = let val (f, args) = strip_comb (Envir.eta_contract t) - val (params, _) = chop (length ms) args + val mode = head_mode_of deriv + val param_derivations = param_derivations_of deriv + val ho_args = ho_args_of mode args val f_tac = case f of Const (name, T) => simp_tac (HOL_basic_ss addsimps ([@{thm eval_pred}, (predfun_definition_of thy name mode), @@ -1691,19 +1751,20 @@ THEN print_tac' options "prove_param" THEN f_tac THEN print_tac' options "after simplification in prove_args" - THEN (EVERY (map2 (prove_param options thy) ms params)) THEN (REPEAT_DETERM (atac 1)) + THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations)) end -fun prove_expr options thy (Mode (mode, is, ms), t, us) (premposition : int) = +fun prove_expr options thy (premposition : int) (t, deriv) = case strip_comb t of - (Const (name, T), args) => + (Const (name, T), args) => let + val mode = head_mode_of deriv val introrule = predfun_intro_of thy name mode - val (args1, args2) = chop (length ms) args + val param_derivations = param_derivations_of deriv + val ho_args = ho_args_of mode args in - rtac @{thm bindI} 1 - THEN print_tac' options "before intro rule:" + print_tac' options "before intro rule:" (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule) @@ -1712,39 +1773,58 @@ (* work with parameter arguments *) THEN atac 1 THEN print_tac' options "parameter goal" - THEN (EVERY (map2 (prove_param options thy) ms args1)) + THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations)) THEN (REPEAT_DETERM (atac 1)) end - | _ => rtac @{thm bindI} 1 - THEN asm_full_simp_tac + | _ => + asm_full_simp_tac (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1 THEN (atac 1) THEN print_tac' options "after prove parameter call" - + -fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; +fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st -fun prove_match thy (out_ts : term list) = let - fun get_case_rewrite t = - if (is_constructor thy t) then let - val case_rewrites = (#case_rewrites (Datatype.the_info thy - ((fst o dest_Type o fastype_of) t))) - in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end - else [] - val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts -(* replace TRY by determining if it necessary - are there equations when calling compile match? *) -in - (* make this simpset better! *) - asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1 - THEN print_tac "after prove_match:" - THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1 - THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1)))) - THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))) - THEN print_tac "after if simplification" -end; +fun check_format thy st = + let + val concl' = Logic.strip_assums_concl (hd (prems_of st)) + val concl = HOLogic.dest_Trueprop concl' + val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl))) + fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true + | valid_expr (Const (@{const_name Predicate.single}, _)) = true + | valid_expr _ = false + in + if valid_expr expr then + ((*tracing "expression is valid";*) Seq.single st) + else + ((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*) + end + +fun prove_match options thy (out_ts : term list) = + let + fun get_case_rewrite t = + if (is_constructor thy t) then let + val case_rewrites = (#case_rewrites (Datatype.the_info thy + ((fst o dest_Type o fastype_of) t))) + in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end + else [] + val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts + (* replace TRY by determining if it necessary - are there equations when calling compile match? *) + in + (* make this simpset better! *) + asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1 + THEN print_tac' options "after prove_match:" + THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1 + THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1)))) + THEN print_tac' options "if condition to be solved:" + THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:")) + THEN check_format thy + THEN print_tac' options "after if simplification - a TRY block"))) + THEN print_tac' options "after if simplification" + end; (* corresponds to compile_fun -- maybe call that also compile_sidecond? *) @@ -1758,7 +1838,7 @@ val preds = preds_of t [] val defs = map (fn (pred, T) => predfun_definition_of thy pred - ([], map (rpair NONE) (1 upto (length (binder_types T))))) + (all_input_of T)) preds in (* remove not_False_eq_True when simpset in prove_match is better *) @@ -1767,63 +1847,74 @@ (* need better control here! *) end -fun prove_clause options thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) = +fun prove_clause options thy nargs modes mode (_, clauses) (ts, moded_ps) = let - val (in_ts, clause_out_ts) = split_smode is ts; + val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems out_ts [] = - (prove_match thy out_ts) + (prove_match options thy out_ts) THEN print_tac' options "before simplifying assumptions" THEN asm_full_simp_tac HOL_basic_ss' 1 THEN print_tac' options "before single intro rule" THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) - | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) = + | prove_prems out_ts ((p, deriv) :: ps) = let val premposition = (find_index (equal p) clauses) + nargs - val rest_tac = (case p of Prem (us, t) => + val mode = head_mode_of deriv + val rest_tac = + rtac @{thm bindI} 1 + THEN (case p of Prem t => let - val (_, out_ts''') = split_smode is us + val (_, us) = strip_comb t + val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems out_ts''' ps in print_tac' options "before clause:" - THEN asm_simp_tac HOL_basic_ss 1 + (*THEN asm_simp_tac HOL_basic_ss 1*) THEN print_tac' options "before prove_expr:" - THEN prove_expr options thy (mode, t, us) premposition + THEN prove_expr options thy premposition (t, deriv) THEN print_tac' options "after prove_expr:" THEN rec_tac end - | Negprem (us, t) => + | Negprem t => let - val (_, out_ts''') = split_smode is us + val (t, args) = strip_comb t + val (_, out_ts''') = split_mode mode args val rec_tac = prove_prems out_ts''' ps val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) - val (_, params) = strip_comb t + val param_derivations = param_derivations_of deriv + val params = ho_args_of mode args in - rtac @{thm bindI} 1 - THEN print_tac' options "before prove_neg_expr:" + print_tac' options "before prove_neg_expr:" + THEN full_simp_tac (HOL_basic_ss addsimps + [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, + @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then print_tac' options ("before unfolding definition " ^ (Display.string_of_thm_global thy - (predfun_definition_of thy (the name) (iss, is)))) + (predfun_definition_of thy (the name) mode))) + THEN simp_tac (HOL_basic_ss addsimps - [predfun_definition_of thy (the name) (iss, is)]) 1 + [predfun_definition_of thy (the name) mode]) 1 THEN rtac @{thm not_predI} 1 THEN print_tac' options "after applying rule not_predI" - THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 + THEN full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}, + @{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, + @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (REPEAT_DETERM (atac 1)) - THEN (EVERY (map2 (prove_param options thy) param_modes params)) + THEN (EVERY (map2 (prove_param options thy) params param_derivations)) + THEN (REPEAT_DETERM (atac 1)) else rtac @{thm not_predI'} 1) THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN rec_tac end | Sidecond t => - rtac @{thm bindI} 1 - THEN rtac @{thm if_predI} 1 + rtac @{thm if_predI} 1 THEN print_tac' options "before sidecond:" THEN prove_sidecond thy modes t THEN print_tac' options "after sidecond:" THEN prove_prems [] ps) - in (prove_match thy out_ts) + in (prove_match options thy out_ts) THEN rest_tac end; val prems_tac = prove_prems in_ts moded_ps @@ -1841,7 +1932,7 @@ fun prove_one_direction options thy clauses preds modes pred mode moded_clauses = let val T = the (AList.lookup (op =) preds pred) - val nargs = length (binder_types T) - nparams_of thy pred + val nargs = length (binder_types T) val pred_case_rule = the_elim_of thy pred in REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) @@ -1893,11 +1984,12 @@ *) (* TODO: remove function *) -fun prove_param2 thy NONE t = all_tac - | prove_param2 thy (m as SOME (Mode (mode, is, ms))) t = +fun prove_param2 thy t deriv = let - val (f, args) = strip_comb (Envir.eta_contract t) - val (params, _) = chop (length ms) args + val (f, args) = strip_comb (Envir.eta_contract t) + val mode = head_mode_of deriv + val param_derivations = param_derivations_of deriv + val ho_args = ho_args_of mode args val f_tac = case f of Const (name, T) => full_simp_tac (HOL_basic_ss addsimps (@{thm eval_pred}::(predfun_definition_of thy name mode) @@ -1908,24 +2000,29 @@ print_tac "before simplification in prove_args:" THEN f_tac THEN print_tac "after simplification in prove_args" - THEN (EVERY (map2 (prove_param2 thy) ms params)) + THEN EVERY (map2 (prove_param2 thy) ho_args param_derivations) end - -fun prove_expr2 thy (Mode (mode, is, ms), t) = +fun prove_expr2 thy (t, deriv) = (case strip_comb t of - (Const (name, T), args) => - etac @{thm bindE} 1 - THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) - THEN print_tac "prove_expr2-before" - THEN (debug_tac (Syntax.string_of_term_global thy - (prop_of (predfun_elim_of thy name mode)))) - THEN (etac (predfun_elim_of thy name mode) 1) - THEN print_tac "prove_expr2" - THEN (EVERY (map2 (prove_param2 thy) ms args)) - THEN print_tac "finished prove_expr2" - | _ => etac @{thm bindE} 1) - + (Const (name, T), args) => + let + val mode = head_mode_of deriv + val param_derivations = param_derivations_of deriv + val ho_args = ho_args_of mode args + in + etac @{thm bindE} 1 + THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) + THEN print_tac "prove_expr2-before" + THEN (debug_tac (Syntax.string_of_term_global thy + (prop_of (predfun_elim_of thy name mode)))) + THEN (etac (predfun_elim_of thy name mode) 1) + THEN print_tac "prove_expr2" + THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations)) + THEN print_tac "finished prove_expr2" + end + | _ => etac @{thm bindE} 1) + (* FIXME: what is this for? *) (* replace defined by has_mode thy pred *) (* TODO: rewrite function *) @@ -1938,7 +2035,7 @@ val preds = preds_of t [] val defs = map (fn (pred, T) => predfun_definition_of thy pred - ([], map (rpair NONE) (1 upto (length (binder_types T))))) + (all_input_of T)) preds in (* only simplify the one assumption *) @@ -1947,10 +2044,10 @@ THEN print_tac "after sidecond2 simplification" end -fun prove_clause2 thy modes pred (iss, is) (ts, ps) i = +fun prove_clause2 thy modes pred mode (ts, ps) i = let val pred_intro_rule = nth (intros_of thy pred) (i - 1) - val (in_ts, clause_out_ts) = split_smode is ts; + val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems2 out_ts [] = print_tac "before prove_match2 - last call:" THEN prove_match2 thy out_ts @@ -1969,31 +2066,35 @@ [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1) THEN print_tac "state after simp_tac:")))) - | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) = + | prove_prems2 out_ts ((p, deriv) :: ps) = let + val mode = head_mode_of deriv val rest_tac = (case p of - Prem (us, t) => + Prem t => let - val (_, out_ts''') = split_smode is us + val (_, us) = strip_comb t + val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems2 out_ts''' ps in - (prove_expr2 thy (mode, t)) THEN rec_tac + (prove_expr2 thy (t, deriv)) THEN rec_tac end - | Negprem (us, t) => + | Negprem t => let - val (_, out_ts''') = split_smode is us + val (_, args) = strip_comb t + val (_, out_ts''') = split_mode mode args val rec_tac = prove_prems2 out_ts''' ps val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) - val (_, params) = strip_comb t + val param_derivations = param_derivations_of deriv + val ho_args = ho_args_of mode args in print_tac "before neg prem 2" THEN etac @{thm bindE} 1 THEN (if is_some name then full_simp_tac (HOL_basic_ss addsimps - [predfun_definition_of thy (the name) (iss, is)]) 1 + [predfun_definition_of thy (the name) mode]) 1 THEN etac @{thm not_predE} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 - THEN (EVERY (map2 (prove_param2 thy) param_modes params)) + THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations)) else etac @{thm not_predE'} 1) THEN rec_tac @@ -2066,10 +2167,10 @@ fun maps_modes preds_modes_table = map (fn (pred, modes) => - (pred, map (fn (mode, value) => value) modes)) preds_modes_table + (pred, map (fn (mode, value) => value) modes)) preds_modes_table -fun compile_preds comp_modifiers compfuns thy all_vs param_vs preds moded_clauses = - map_preds_modes (fn pred => compile_pred comp_modifiers compfuns thy all_vs param_vs pred +fun compile_preds comp_modifiers thy all_vs param_vs preds moded_clauses = + map_preds_modes (fn pred => compile_pred comp_modifiers thy all_vs param_vs pred (the (AList.lookup (op =) preds pred))) moded_clauses fun prove options thy clauses preds modes moded_clauses compiled_terms = @@ -2084,89 +2185,58 @@ fun dest_prem thy params t = (case strip_comb t of - (v as Free _, ts) => if member (op =) params v then Prem (ts, v) else Sidecond t + (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of - Prem (ts, t) => Negprem (ts, t) + Prem t => Negprem t | Negprem _ => error ("Double negation not allowed in premise: " ^ Syntax.string_of_term_global thy (c $ t)) | Sidecond t => Sidecond (c $ t)) | (c as Const (s, _), ts) => - if is_registered thy s then - let val (ts1, ts2) = chop (nparams_of thy s) ts - in Prem (ts2, list_comb (c, ts1)) end - else Sidecond t + if is_registered thy s then Prem t else Sidecond t | _ => Sidecond t) - -fun prepare_intrs options thy prednames intros = + +fun prepare_intrs options compilation thy prednames intros = let val intrs = map prop_of intros - val nparams = nparams_of thy (hd prednames) val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames val (preds, intrs) = unify_consts thy preds intrs val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy) val preds = map dest_Const preds - val extra_modes = all_modes_of thy - |> filter_out (fn (name, _) => member (op =) prednames name) - val params = case intrs of + val extra_modes = + all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name) + val all_vs = terms_vs intrs + val params = + case intrs of [] => let - val (paramTs, _) = chop nparams (binder_types (snd (hd preds))) + val T = snd (hd preds) + val paramTs = + ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T) val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs)) - 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 - val all_vs = terms_vs intrs - fun add_clause intr (clauses, arities) = - let - val _ $ t = Logic.strip_imp_concl intr; - val (Const (name, T), ts) = strip_comb t; - val (ts1, ts2) = chop nparams ts; - val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr); - val (Ts, Us) = chop nparams (binder_types T) - in - (AList.update op = (name, these (AList.lookup op = clauses name) @ - [(ts2, prems)]) clauses, - AList.update op = (name, (map (fn U => (case strip_type U of - (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs) - | _ => NONE)) Ts, - length Us)) arities) - end; - val (clauses, arities) = fold add_clause intrs ([], []); - fun modes_of_arities arities = - (map (fn (s, (ks, k)) => (s, cprod (cprods (map - (fn NONE => [NONE] - | SOME k' => map SOME (map (map (rpair NONE)) (subsets 1 k'))) ks), - map (map (rpair NONE)) (subsets 1 k)))) arities) - fun modes_of_typ T = + in + map2 (curry Free) param_names paramTs + end + | (intr :: _) => maps extract_params + (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))) + val param_vs = map (fst o dest_Free) params + fun add_clause intr clauses = let - val (Ts, Us) = chop nparams (binder_types T) - fun all_smodes_of_typs Ts = cprods_subset ( - map_index (fn (i, U) => - case HOLogic.strip_tupleT U of - [] => [(i + 1, NONE)] - | [U] => [(i + 1, NONE)] - | Us => (i + 1, NONE) :: - (map (pair (i + 1) o SOME) - (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us))))) - Ts) + val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)) + val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr) in - cprod (cprods (map (fn T => case strip_type T of - (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) => - case proposed_modes options of - NONE => (s, modes_of_typ T) - | SOME (s', modes') => - if s = s' then (s, map (translate_mode' nparams) modes') else (s, modes_of_typ T)) - preds - in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; + AList.update op = (name, these (AList.lookup op = clauses name) @ + [(ts, prems)]) clauses + end; + val clauses = fold add_clause intrs [] + in + (preds, all_vs, param_vs, extra_modes, clauses) + end; (* sanity check of introduction rules *) - +(* TODO: rethink check with new modes *) +(* fun check_format_of_intro_rule thy intro = let val concl = Logic.strip_imp_concl (prop_of intro) @@ -2182,14 +2252,14 @@ (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 - | check_prem (Negprem (args, _)) = forall check_arg args + fun check_prem (Prem t) = forall check_arg args + | check_prem (Negprem t) = forall check_arg args | check_prem _ = true in forall check_arg args andalso forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems end - +*) (* fun check_intros_elim_match thy prednames = let @@ -2211,20 +2281,19 @@ (* create code equation *) -fun add_code_equations thy nparams preds result_thmss = +fun add_code_equations thy preds result_thmss = let 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))) + val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool in - if member (op =) (modes_of thy predname) full_mode then + if member (op =) (modes_of Pred thy predname) full_mode then let 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 = map2 (curry Free) arg_names Ts - val predfun = Const (predfun_name_of thy predname full_mode, + val predfun = Const (function_name_of Pred thy predname full_mode, Ts ---> PredicateCompFuns.mk_predT @{typ unit}) val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) val eq_term = HOLogic.mk_Trueprop @@ -2247,22 +2316,19 @@ datatype steps = Steps of { - compile_preds : theory -> string list -> string list -> (string * typ) list - -> (moded_clause list) pred_mode_table -> term pred_mode_table, define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory, - infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list + infer_modes : options -> (string * typ) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list - -> moded_clause list pred_mode_table * string list, + -> theory -> ((moded_clause list pred_mode_table * string list) * theory), prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list -> (string * mode list) list -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, - add_code_equations : theory -> int -> (string * typ) list + add_code_equations : theory -> (string * typ) list -> (string * thm list) list -> (string * thm list) list, - defined : theory -> string -> bool, + comp_modifiers : Comp_Mod.comp_modifiers, qname : bstring } - fun add_equations_of steps options prednames thy = let fun dest_steps (Steps s) = s @@ -2270,37 +2336,37 @@ ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") (*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 options thy prednames (maps (intros_of thy) prednames) + val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) + val (preds, all_vs, param_vs, extra_modes, clauses) = + prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." - val (moded_clauses, errors) = - #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses + val ((moded_clauses, errors), thy') = + #infer_modes (dest_steps steps) options preds extra_modes param_vs clauses thy val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes preds options modes val _ = check_proposed_modes preds options modes extra_modes errors - val _ = print_modes options thy modes - (*val _ = print_moded_clauses thy moded_clauses*) + val _ = print_modes options thy' modes val _ = print_step options "Defining executable functions..." - val thy' = fold (#define_functions (dest_steps steps) options 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 = - #compile_preds (dest_steps steps) thy' all_vs param_vs preds moded_clauses - val _ = print_compiled_terms options thy' compiled_terms + compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses + val _ = print_compiled_terms options thy'' compiled_terms val _ = print_step options "Proving equations..." - val result_thms = #prove (dest_steps steps) options thy' clauses preds (extra_modes @ modes) + val result_thms = #prove (dest_steps steps) options thy'' clauses preds (extra_modes @ modes) moded_clauses compiled_terms - val result_thms' = #add_code_equations (dest_steps steps) thy' nparams preds + val result_thms' = #add_code_equations (dest_steps steps) thy'' preds (maps_modes result_thms) val qname = #qname (dest_steps steps) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) - val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss + val thy''' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib thy ])] thy)) - result_thms' thy' |> Theory.checkpoint + result_thms' thy'' |> Theory.checkpoint in - thy'' + thy''' end fun extend' value_of edges_of key (G, visited) = @@ -2320,36 +2386,27 @@ fun gen_add_equations steps options names thy = let fun dest_steps (Steps s) = s + val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) val thy' = thy |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) |> Theory.checkpoint; fun strong_conn_of gr keys = Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) val scc = strong_conn_of (PredData.get thy') names + val thy'' = fold_rev (fn preds => fn thy => - if not (forall (#defined (dest_steps steps) thy) preds) then + if not (forall (defined thy) preds) then add_equations_of steps options preds thy else thy) scc thy' |> Theory.checkpoint in thy'' end - -(* different instantiantions of the predicate compiler *) - -val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers - {function_name_of = predfun_name_of : (theory -> string -> mode -> string), - set_function_name = (fn _ => fn _ => fn _ => I), - function_name_prefix = "", - funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), - additional_arguments = K [], - wrap_compilation = K (K (K (K (K I)))) - : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), - transform_additional_arguments = K I : (indprem -> term list -> term list) - } - +(* val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers - {function_name_of = depth_limited_function_name_of, - set_function_name = set_depth_limited_function_name, + { + compilation = Depth_Limited, + function_name_of = function_name_of Depth_Limited, + set_function_name = set_function_name Depth_Limited, funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ), function_name_prefix = "depth_limited_", additional_arguments = fn names => @@ -2384,8 +2441,10 @@ } val random_comp_modifiers = Comp_Mod.Comp_Modifiers - {function_name_of = random_function_name_of, - set_function_name = set_random_function_name, + { + compilation = Random, + function_name_of = function_name_of Random, + set_function_name = set_function_name 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})], @@ -2393,55 +2452,106 @@ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), transform_additional_arguments = K I : (indprem -> term list -> term list) } +*) +(* different instantiantions of the predicate compiler *) + +val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = Pred, + function_name_prefix = "", + compfuns = PredicateCompFuns.compfuns, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + +val add_equations = gen_add_equations + (Steps {infer_modes = infer_modes false, + define_functions = create_definitions, + prove = prove, + add_code_equations = add_code_equations, + comp_modifiers = predicate_comp_modifiers, + qname = "equation"}) val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers - {function_name_of = annotated_function_name_of, - set_function_name = set_annotated_function_name, + { + compilation = Annotated, function_name_prefix = "annotated_", - funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), + compfuns = PredicateCompFuns.compfuns, 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' (translate_mode T mode)) compilation, + " with mode " ^ string_of_mode mode) compilation, transform_additional_arguments = K I : (indprem -> term list -> term list) } -val add_equations = gen_add_equations - (Steps {infer_modes = infer_modes, - define_functions = create_definitions, - compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, - prove = prove, - add_code_equations = add_code_equations, - defined = defined_functions, - qname = "equation"}) +val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = DSeq, + function_name_prefix = "dseq_", + compfuns = DSequence_CompFuns.compfuns, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } +val random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = Random_DSeq, + function_name_prefix = "random_dseq_", + compfuns = Random_Sequence_CompFuns.compfuns, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + +(* val add_depth_limited_equations = gen_add_equations (Steps {infer_modes = infer_modes, define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns, compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, - add_code_equations = K (K (K I)), - defined = defined_depth_limited_functions, + add_code_equations = K (K I), + defined = defined_functions Depth_Limited, qname = "depth_limited_equation"}) - +*) val add_annotated_equations = gen_add_equations - (Steps {infer_modes = infer_modes, + (Steps {infer_modes = infer_modes false, define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns, - compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, - add_code_equations = K (K (K I)), - defined = defined_annotated_functions, + add_code_equations = K (K I), + comp_modifiers = annotated_comp_modifiers, qname = "annotated_equation"}) - +(* val add_quickcheck_equations = gen_add_equations (Steps {infer_modes = infer_modes_with_generator, define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns, compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, - add_code_equations = K (K (K I)), - defined = defined_random_functions, + add_code_equations = K (K I), + defined = defined_functions Random, qname = "random_equation"}) +*) +val add_dseq_equations = gen_add_equations + (Steps {infer_modes = infer_modes false, + define_functions = define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns, + prove = prove_by_skip, + add_code_equations = K (K I), + comp_modifiers = dseq_comp_modifiers, + qname = "dseq_equation"}) + +val add_random_dseq_equations = gen_add_equations + (Steps {infer_modes = infer_modes true, + define_functions = define_functions random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns, + prove = prove_by_skip, + add_code_equations = K (K I), + comp_modifiers = random_dseq_comp_modifiers, + qname = "random_dseq_equation"}) + (** user interface **) @@ -2474,9 +2584,8 @@ let val T = Sign.the_const_type thy const val pred = Const (const, T) - val nparams = nparams_of thy' const val intros = intros_of thy' const - in mk_casesrule lthy' pred nparams intros end + in mk_casesrule lthy' pred intros end val cases_rules = map mk_cases preds val cases = map (fn case_rule => Rule_Cases.Case {fixes = [], @@ -2492,15 +2601,15 @@ (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms) in goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #> - (if is_random options then - (add_equations options [const] #> - add_quickcheck_equations options [const]) - else if is_depth_limited options then - add_depth_limited_equations options [const] - else if is_annotated options then - add_annotated_equations options [const] - else - add_equations options [const])) + ((case compilation options of + Pred => add_equations + | DSeq => add_dseq_equations + | Random_DSeq => add_random_dseq_equations + | compilation => error ("Compilation not supported") + (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs) + | Depth_Limited => add_depth_limited_equations + | Annotated => add_annotated_equations*) + ) options [const])) end in Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' @@ -2514,104 +2623,161 @@ val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); val random_eval_ref = Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); +val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option); +val random_dseq_eval_ref = + Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) -(* TODO: make analyze_compr generic with respect to the compilation modifiers*) -fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) t_compr = +fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr = let + val all_modes_of = all_modes_of compilation val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr); val (body, Ts, fp) = HOLogic.strip_psplits split; - val (pred as Const (name, T), all_args) = strip_comb body; - val (params, args) = chop (nparams_of thy name) all_args; - val user_mode = map_filter I (map_index - (fn (i, t) => case t of Bound j => if j < length Ts then NONE - else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*) - 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 = (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 - | valid [] [] = true - | valid [] _ = error "Too many mode annotations" - | valid (SOME _ :: _) [] = error "Not enough mode annotations" - val modes = filter (fn Mode (_, is, ms) => is = user_mode' - andalso (the_default true (Option.map (valid ms) param_user_modes))) - (modes_of_term (all_modes_of thy) (list_comb (pred, params))); - val m = case modes - of [] => error ("No mode possible for comprehension " - ^ Syntax.string_of_term_global thy t_compr) - | [m] => m - | m :: _ :: _ => (warning ("Multiple modes possible for comprehension " - ^ Syntax.string_of_term_global thy t_compr); m); - val (inargs, outargs) = split_smode user_mode' args; - val additional_arguments = - case depth_limit of - NONE => (if random then [@{term "5 :: code_numeral"}] else []) - | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d] - val comp_modifiers = - case depth_limit of - NONE => - (if random then random_comp_modifiers else - if annotated then annotated_comp_modifiers else predicate_comp_modifiers) - | SOME _ => depth_limited_comp_modifiers - val t_pred = compile_expr comp_modifiers compfuns thy - (m, list_comb (pred, params)) inargs additional_arguments; - val t_eval = if null outargs then t_pred else + val output_names = Name.variant_list (Term.add_free_names body []) + (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) + val output_frees = map2 (curry Free) output_names Ts + val body = subst_bounds (output_frees, body) + val T_compr = HOLogic.mk_ptupleT fp (rev Ts) + val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees) + val (pred as Const (name, T), all_args) = strip_comb body + in + if defined_functions compilation thy name then let - val outargs_bounds = map (fn Bound i => i) outargs; - val outargsTs = map (nth Ts) outargs_bounds; - val T_pred = HOLogic.mk_tupleT outargsTs; - val T_compr = HOLogic.mk_ptupleT fp (rev Ts); - val k = length outargs - 1; - val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds - |> sort (prod_ord (K EQUAL) int_ord) - |> map fst; - val (outargsTs', outargsT) = split_last outargsTs; - val (arrange, _) = fold_rev (fn U => fn (t, T) => - (HOLogic.split_const (U, T, T_compr) $ Abs ("", U, t), - HOLogic.mk_prodT (U, T))) - outargsTs' (Abs ("", outargsT, - HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)), outargsT) - in mk_map compfuns T_pred T_compr arrange t_pred end - in t_eval end; + fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2) + | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input + | extract_mode _ = Input + val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool + fun valid modes1 modes2 = + case int_ord (length modes1, length modes2) of + GREATER => error "Not enough mode annotations" + | LESS => error "Too many mode annotations" + | EQUAL => forall (fn (m, NONE) => true | (m, SOME m2) => eq_mode (m, m2)) + (modes1 ~~ modes2) + fun mode_instance_of (m1, m2) = + let + fun instance_of (Fun _, Input) = true + | instance_of (Input, Input) = true + | instance_of (Output, Output) = true + | instance_of (Pair (m1, m2), Pair (m1', m2')) = + instance_of (m1, m1') andalso instance_of (m2, m2') + | instance_of (Pair (m1, m2), Input) = + instance_of (m1, Input) andalso instance_of (m2, Input) + | instance_of (Pair (m1, m2), Output) = + instance_of (m1, Output) andalso instance_of (m2, Output) + | instance_of _ = false + in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end + val derivs = all_derivations_of thy (all_modes_of thy) [] body + |> filter (fn (d, missing_vars) => + let + val (p_mode :: modes) = collect_context_modes d + in + null missing_vars andalso + mode_instance_of (p_mode, user_mode) andalso + the_default true (Option.map (valid modes) param_user_modes) + end) + |> map fst + val deriv = case derivs of + [] => error ("No mode possible for comprehension " + ^ Syntax.string_of_term_global thy t_compr) + | [d] => d + | d :: _ :: _ => (warning ("Multiple modes possible for comprehension " + ^ Syntax.string_of_term_global thy t_compr); d); + val (_, outargs) = split_mode (head_mode_of deriv) all_args + val additional_arguments = + case compilation of + Pred => [] + | Random => [@{term "5 :: code_numeral"}] + | Annotated => [] + | Depth_Limited => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} (hd arguments)] + | DSeq => [] + | Random_DSeq => [] + val comp_modifiers = + case compilation of + Pred => predicate_comp_modifiers + (*| Random => random_comp_modifiers + | Depth_Limited => depth_limited_comp_modifiers + | Annotated => annotated_comp_modifiers*) + | DSeq => dseq_comp_modifiers + | Random_DSeq => random_dseq_comp_modifiers + val t_pred = compile_expr comp_modifiers compfuns thy (body, deriv) additional_arguments; + val T_pred = dest_predT compfuns (fastype_of t_pred) + val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple + in + if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred + end + else + error "Evaluation with values is not possible because compilation with code_pred was not invoked" + end -fun eval thy param_user_modes (options as (depth_limit, (random, annotated))) t_compr = +fun eval thy param_user_modes (options as (compilation, arguments)) k t_compr = let - val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns + val compfuns = + case compilation of + Random => RandomPredCompFuns.compfuns + | DSeq => DSequence_CompFuns.compfuns + | Random_DSeq => Random_Sequence_CompFuns.compfuns + | _ => PredicateCompFuns.compfuns val t = analyze_compr thy compfuns param_user_modes options t_compr; val T = dest_predT compfuns (fastype_of t); val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; - val eval = - if random then - Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref) + val ts = + case compilation of + Random => + fst (Predicate.yieldn k + (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref) (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' [] - |> Random_Engine.run - else - Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' [] - in (T, eval) end; + |> Random_Engine.run)) + | Random_DSeq => + let + val [nrandom, size, depth] = arguments + in + fst (DSequence.yieldn k + (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref) + (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc) + thy t' [] nrandom size + |> Random_Engine.run) + depth true) + end + | DSeq => + fst (DSequence.yieldn k + (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref) + DSequence.map thy t' []) (the_single arguments) true) + | _ => + fst (Predicate.yieldn k + (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) + Predicate.map thy t' [])) + in (T, ts) end; -fun values ctxt param_user_modes options k t_compr = +fun values ctxt param_user_modes (raw_expected, comp_options) k t_compr = let - val thy = ProofContext.theory_of ctxt; - val (T, ts) = eval thy param_user_modes options t_compr; - val (ts, _) = Predicate.yieldn k ts; - val setT = HOLogic.mk_setT T; - val elemsT = HOLogic.mk_set T ts; + val thy = ProofContext.theory_of ctxt + val (T, ts) = eval thy param_user_modes comp_options k t_compr + val setT = HOLogic.mk_setT T + val elems = HOLogic.mk_set T ts val cont = Free ("...", setT) - in if k = ~1 orelse length ts < k then elemsT - else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont + (* check expected values *) + val () = + case raw_expected of + NONE => () + | SOME s => + if eq_set (op =) (HOLogic.dest_set (Syntax.read_term ctxt s), ts) then () + else + error ("expected and computed values do not match:\n" ^ + "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^ + "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n") + in + if k = ~1 orelse length ts < k then elems + else Const (@{const_name Set.union}, setT --> setT --> setT) $ elems $ cont end; fun values_cmd print_modes param_user_modes options k raw_t state = let - val ctxt = Toplevel.context_of state; - val t = Syntax.read_term ctxt raw_t; - val t' = values ctxt param_user_modes options k t; - val ty' = Term.type_of t'; - val ctxt' = Variable.auto_fixes t' ctxt; + val ctxt = Toplevel.context_of state + val t = Syntax.read_term ctxt raw_t + val t' = values ctxt param_user_modes options k t + val ty' = Term.type_of t' + val ctxt' = Variable.auto_fixes t' ctxt val p = PrintMode.with_modes print_modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Jan 22 15:26:29 2010 +0100 @@ -7,10 +7,10 @@ signature PREDICATE_COMPILE_DATA = sig type specification_table; - val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table - val get_specification : specification_table -> string -> thm list - val obtain_specification_graph : Predicate_Compile_Aux.options -> theory -> - specification_table -> string -> thm list Graph.T + (*val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table*) + val get_specification : theory -> term -> thm list + val obtain_specification_graph : + Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T val normalize_equation : theory -> thm -> thm end; @@ -37,16 +37,17 @@ type specification_table = thm list Symtab.table -fun defining_const_of_introrule_term t = +fun defining_term_of_introrule_term t = let val _ $ u = Logic.strip_imp_concl t - val (pred, all_args) = strip_comb u + in fst (strip_comb u) end +(* in case pred of Const (c, T) => c | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) end - -val defining_const_of_introrule = defining_const_of_introrule_term o prop_of +*) +val defining_term_of_introrule = defining_term_of_introrule_term o prop_of (*TODO*) fun is_introlike_term t = true @@ -66,14 +67,20 @@ val check_equation_format = check_equation_format_term o prop_of -fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) = - (case fst (strip_comb u) of - Const (c, _) => c - | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t])) - | defining_const_of_equation_term t = + +fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u) + | defining_term_of_equation_term t = raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) -val defining_const_of_equation = defining_const_of_equation_term o prop_of +val defining_term_of_equation = defining_term_of_equation_term o prop_of + +fun defining_const_of_equation th = + case defining_term_of_equation th + of Const (c, _) => c + | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]) + + + (* Normalizing equations *) @@ -125,7 +132,7 @@ |> split_all_pairs thy |> tap check_equation_format -fun inline_equations options thy th = +fun inline_equations thy th = let val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy) val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th @@ -136,7 +143,7 @@ in th' end - +(* fun store_thm_in_table options ignore thy th= let val th = th @@ -150,7 +157,7 @@ in (defining_const_of_equation eq, eq) end - else if (is_introlike th) then (defining_const_of_introrule th, th) + else if is_introlike th then (defining_const_of_introrule th, th) else error "store_thm: unexpected definition format" in if ignore const then I else Symtab.cons_list (const, th) @@ -160,15 +167,15 @@ let fun store ignore f = fold (store_thm_in_table options ignore thy) - (map (Thm.transfer thy) (f (ProofContext.init thy))) + (map (Thm.transfer thy) (f )) val table = Symtab.empty |> store (K false) Predicate_Compile_Alternative_Defs.get val ignore = Symtab.defined table in table |> store ignore (fn ctxt => maps - (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else []) - (Spec_Rules.get ctxt)) + else []) + |> store ignore Nitpick_Simps.get |> store ignore Nitpick_Intros.get end @@ -177,28 +184,56 @@ case Symtab.lookup table constname of SOME thms => thms | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") +*) + +fun get_specification thy t = + Output.cond_timeit true "get_specification" (fn () => + let + val ctxt = ProofContext.init thy + fun filtering th = + if is_equationlike th andalso + defining_const_of_equation (normalize_equation thy th) = (fst (dest_Const t)) then + SOME (normalize_equation thy th) + else + if is_introlike th andalso defining_term_of_introrule th = t then + SOME th + else + NONE + in + case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt)) + of [] => (case Spec_Rules.retrieve ctxt t + of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt))) + | ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths) + | ths => rev ths + end) val logic_operator_names = - [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, + [@{const_name "=="}, + @{const_name "==>"}, + @{const_name "Trueprop"}, + @{const_name "Not"}, + @{const_name "op ="}, + @{const_name "op -->"}, + @{const_name "All"}, + @{const_name "Ex"}, @{const_name "op &"}] -val special_cases = member (op =) [ - @{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.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}, +fun special_cases (c, T) = member (op =) [ + @{const_name "Product_Type.Unity"}, + @{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.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}, @{const_name Int.Pls}, -@{const_name "Int.zero_int_inst.zero_int"}, -@{const_name "List.filter"}] - -fun case_consts thy s = is_some (Datatype.info_of_case thy s) + @{const_name "Int.zero_int_inst.zero_int"}, + @{const_name "List.filter"}] c fun print_specification options thy constname specs = if show_intermediate_results options then @@ -206,26 +241,32 @@ cat_lines (map (Display.string_of_thm_global thy) specs)) else () -fun obtain_specification_graph options thy table constname = +fun obtain_specification_graph options thy t = let - fun is_nondefining_constname c = member (op =) logic_operator_names c - val is_defining_constname = member (op =) (Symtab.keys table) - fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) + fun is_nondefining_const (c, T) = member (op =) logic_operator_names c + fun has_code_pred_intros (c, T) = is_some (try (Predicate_Compile_Core.intros_of thy) c) + fun case_consts (c, T) = is_some (Datatype.info_of_case thy c) + fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T)) fun defiants_of specs = - fold (Term.add_const_names o prop_of) specs [] - |> filter is_defining_constname - |> filter_out is_nondefining_constname + fold (Term.add_consts o prop_of) specs [] + |> filter_out is_datatype_constructor + |> filter_out is_nondefining_const |> filter_out has_code_pred_intros - |> filter_out (case_consts thy) + |> filter_out case_consts |> filter_out special_cases - fun extend constname = + |> map Const + (* + |> filter is_defining_constname*) + fun extend t = let - val specs = get_specification table constname - val _ = print_specification options thy constname specs + val specs = get_specification thy t + |> map (inline_equations thy) + (*|> Predicate_Compile_Set.unfold_set_notation*) + (*val _ = print_specification options thy constname specs*) in (specs, defiants_of specs) end; in - Graph.extend extend constname Graph.empty + TermGraph.extend extend t TermGraph.empty end; - + end; diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Jan 22 15:26:29 2010 +0100 @@ -14,31 +14,7 @@ structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = struct -fun is_funtype (Type ("fun", [_, _])) = true - | is_funtype _ = false; - -fun is_Type (Type _) = true - | is_Type _ = false - -(* returns true if t is an application of an datatype constructor *) -(* which then consequently would be splitted *) -(* else false *) -(* -fun is_constructor thy t = - if (is_Type (fastype_of t)) then - (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of - NONE => false - | SOME info => (let - val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) - val (c, _) = strip_comb t - in (case c of - Const (name, _) => name mem_string constr_consts - | _ => false) end)) - else false -*) - -(* must be exported in code.ML *) -fun is_constr thy = is_some o Code.get_datatype_of_constr thy; +open Predicate_Compile_Aux; (* Table from constant name (string) to term of inductive predicate *) structure Pred_Compile_Preproc = Theory_Data @@ -364,7 +340,8 @@ val prednames = map (fst o dest_Const) (#preds ind_result) (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) (* add constants to my table *) - val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames + val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) + (#intrs ind_result))) prednames val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' in (specs, thy'') diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Jan 22 15:26:29 2010 +0100 @@ -112,8 +112,9 @@ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}]) val rewrite_intros = - Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) - +(* Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) *) + Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm not_not}]) + fun preprocess (constname, specs) thy = let val ctxt = ProofContext.init thy diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Jan 22 15:26:29 2010 +0100 @@ -8,7 +8,8 @@ sig val quickcheck : Proof.context -> term -> int -> term list option val test_ref : - ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref + ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref + val tracing : bool Unsynchronized.ref; end; structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = @@ -17,7 +18,9 @@ open Predicate_Compile_Aux; val test_ref = - Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) + Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option); + +val tracing = Unsynchronized.ref false; val target = "Quickcheck" @@ -28,15 +31,12 @@ show_steps = true, show_intermediate_results = true, show_proof_trace = false, - show_modes = true, + show_modes = false, show_mode_inference = false, - show_compilation = true, + show_compilation = false, skip_proof = false, - - inductify = false, - random = false, - depth_limited = false, - annotated = false + compilation = Random, + inductify = false } fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs @@ -65,7 +65,11 @@ fun quickcheck ctxt t = let - val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) + (*val () = + if !tracing then + tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) + else + ()*) val ctxt' = ProofContext.theory (Context.copy_thy) ctxt val thy = (ProofContext.theory_of ctxt') val (vs, t') = strip_abs t @@ -75,42 +79,47 @@ val constname = "pred_compile_quickcheck" val full_constname = Sign.full_bname thy constname val constT = map snd vs' ---> @{typ bool} - val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy + val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy + val const = Const (full_constname, constT) val t = Logic.list_implies - (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), + (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) - val tac = fn _ => Skip_Proof.cheat_tac thy' - val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac - val _ = tracing (Display.string_of_thm ctxt' intro) - val thy'' = thy' - |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) - |> Predicate_Compile.preprocess options full_constname - |> Predicate_Compile_Core.add_equations options [full_constname] - (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) - |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname] - val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname - val modes = Predicate_Compile_Core.random_modes_of thy'' full_constname + val tac = fn _ => Skip_Proof.cheat_tac thy1 + val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac + (*val _ = tracing (Display.string_of_thm ctxt' intro)*) + val thy2 = (*Output.cond_timeit (!Quickcheck.timing) "predicate intros" + (fn () => *)(Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1) + val thy3 = (*Output.cond_timeit (!Quickcheck.timing) "predicate preprocessing" + (fn () =>*) (Predicate_Compile.preprocess options const thy2) + val thy4 = Output.cond_timeit (!Quickcheck.timing) "random_dseq compilation" + (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3) + (*val depth_limited_modes = Predicate_Compile_Core.modes_of Depth_Limited thy'' full_constname*) + val modes = Predicate_Compile_Core.modes_of Random_DSeq thy4 full_constname + val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool val prog = - if member (op =) modes ([], []) then + if member eq_mode modes output_mode then let - val name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], []) - val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) - in Const (name, T) $ Bound 0 end + val name = Predicate_Compile_Core.function_name_of Random_DSeq thy4 full_constname output_mode + val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) + in + Const (name, T) + end (*else if member (op =) depth_limited_modes ([], []) then let val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) in lift_pred (Const (name, T) $ Bound 0) end*) else error "Predicate Compile Quickcheck failed" - val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, + val qc_term = mk_bind (prog, mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} - (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) - val _ = tracing (Syntax.string_of_term ctxt' qc_term) - val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) - (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) - thy'' qc_term [] + (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) + val compilation = + Code_Eval.eval NONE ("Predicate_Compile_Quickcheck.test_ref", test_ref) + (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc) + thy4 qc_term [] in - ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) + (fn size => + Option.map fst (DSequence.yield (compilation size size |> Random_Engine.run) size true)) end end; diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/old_primrec.ML Fri Jan 22 15:26:29 2010 +0100 @@ -281,11 +281,14 @@ thy' |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps); val simps'' = maps snd simps'; + fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))) + val specs = (distinct (op =) (map dest_eqn simps''), simps'') in thy'' |> note (("simps", [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'') |> snd + |> Spec_Rules.add_global Spec_Rules.Equational specs |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd |> Sign.parent_path diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/primrec.ML Fri Jan 22 15:26:29 2010 +0100 @@ -265,6 +265,15 @@ local +fun specs_of simps = + let + val eqns = maps snd simps + fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))) + val t = distinct (op =) (map dest_eqn eqns) + in + (t, eqns) + end + fun gen_primrec prep_spec raw_fixes raw_spec lthy = let val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); @@ -277,7 +286,8 @@ lthy |> add_primrec_simple fixes (map snd spec) |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps) - #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps'))) + #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps') + ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps')))) |>> snd end; diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/recdef.ML Fri Jan 22 15:26:29 2010 +0100 @@ -204,13 +204,13 @@ val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute] else []; - val ((simps' :: rules', [induct']), thy) = thy |> Sign.add_path bname |> PureThy.add_thmss (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) - ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]; + ||>> PureThy.add_thms [((Binding.name "induct", induct), [])] + ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules); val result = {simps = simps', rules = rules', induct = induct', tcs = tcs}; val thy = thy diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Word/WordBitwise.thy Fri Jan 22 15:26:29 2010 +0100 @@ -204,7 +204,7 @@ lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" unfolding to_bl_def word_log_defs - by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) + by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric] bin_to_bl_def[symmetric]) lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" unfolding to_bl_def word_log_defs bl_xor_bin diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Fri Jan 22 15:26:29 2010 +0100 @@ -1,13 +1,19 @@ theory Predicate_Compile_Alternative_Defs -imports Main +imports "../Predicate_Compile" begin section {* Set operations *} -declare eq_reflection[OF empty_def, code_pred_inline] +declare Collect_def[code_pred_inline] +declare mem_def[code_pred_inline] + +declare eq_reflection[OF empty_def, code_pred_inline] +declare insert_code[code_pred_def] 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 *} @@ -22,13 +28,13 @@ unfolding mem_def[symmetric, of _ x] by auto -code_pred set +code_pred [skip_proof] set proof - case set from this show thesis - apply (case_tac a1) + apply (case_tac xb) apply auto - unfolding mem_def[symmetric, of _ a2] + unfolding mem_def[symmetric, of _ xc] apply auto unfolding mem_def apply fastsimp @@ -43,15 +49,15 @@ 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 +code_pred [skip_proof] list_all2 proof - case list_all2 from this show thesis apply - - apply (case_tac a1) - apply (case_tac a2) + apply (case_tac xa) + apply (case_tac xb) apply auto - apply (case_tac a2) + apply (case_tac xb) apply auto done qed diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/ex/Predicate_Compile_Quickcheck.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Fri Jan 22 15:26:29 2010 +0100 @@ -3,10 +3,34 @@ header {* A Prototype of Quickcheck based on the Predicate Compiler *} theory Predicate_Compile_Quickcheck -imports Main +imports "../Predicate_Compile" uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" begin setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *} +(* +datatype alphabet = a | b +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where + "[] \ S\<^isub>1" +| "w \ A\<^isub>1 \ b # w \ S\<^isub>1" +| "w \ B\<^isub>1 \ a # w \ S\<^isub>1" +| "w \ S\<^isub>1 \ a # w \ A\<^isub>1" +| "w \ S\<^isub>1 \ b # w \ S\<^isub>1" +| "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" + +ML {* set Toplevel.debug *} + +declare mem_def[code_pred_inline] Collect_def[code_pred_inline] + +lemma + "w \ S\<^isub>1p \ w = []" +quickcheck[generator = predicate_compile, iterations=1] +oops + +theorem S\<^isub>1_sound: +"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[generator=predicate_compile, size=15] +oops +*) end \ No newline at end of file diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Jan 22 15:26:29 2010 +0100 @@ -3,39 +3,43 @@ Predicate_Compile_Alternative_Defs begin -section {* Sets *} +ML {* Predicate_Compile_Alternative_Defs.get *} +section {* Sets *} +(* lemma "x \ {(1::nat)} ==> False" +quickcheck[generator=predicate_compile, iterations=10] +oops +*) +(* TODO: some error with doubled negation *) +(* +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x \ Suc 0" quickcheck[generator=predicate_compile] oops - -(* TODO: some error with doubled negation *) -lemma "x \ {Suc 0, Suc (Suc 0)} ==> x \ Suc 0" +*) +(* +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x = Suc 0" +quickcheck[generator=predicate_compile] +oops +*) +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" (*quickcheck[generator=predicate_compile]*) oops -lemma "x \ {Suc 0, Suc (Suc 0)} ==> x = Suc 0" -quickcheck[generator=predicate_compile] -oops - -lemma "x \ {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" -quickcheck[generator=predicate_compile] -oops - section {* Numerals *} - +(* lemma "x \ {1, 2, (3::nat)} ==> x = 1 \ x = 2" quickcheck[generator=predicate_compile] oops - +*) lemma "x \ {1, 2, (3::nat)} ==> x < 3" (*quickcheck[generator=predicate_compile]*) oops lemma "x \ {1, 2} \ {3, 4} ==> x = (1::nat) \ x = (2::nat)" -quickcheck[generator=predicate_compile] +(*quickcheck[generator=predicate_compile]*) oops section {* Context Free Grammar *} @@ -49,10 +53,33 @@ | "w \ S\<^isub>1 \ a # w \ A\<^isub>1" | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" +(* +code_pred [random_dseq inductify] "S\<^isub>1p" . +*) +(*thm B\<^isub>1p.random_dseq_equation*) +(* +values [random_dseq 2, 2, 4] 10 "{x. S\<^isub>1p x}" +values [random_dseq 1, 1, 5] 20 "{x. S\<^isub>1p x}" + +ML {* set ML_Context.trace *} +*) +ML {* set Toplevel.debug *} +(* +quickcheck[generator = predicate_compile, size = 10, iterations = 1] +oops +*) +ML {* Spec_Rules.get *} +ML {* Item_Net.retrieve *} +local_setup {* Local_Theory.checkpoint *} +ML {* Predicate_Compile_Data.get_specification @{theory} @{term "append"} *} +lemma + "w \ S\<^isub>1p \ w = []" +quickcheck[generator = predicate_compile, iterations=1] +oops theorem S\<^isub>1_sound: "w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=predicate_compile, size=15]*) +quickcheck[generator=predicate_compile, size=15] oops @@ -64,37 +91,37 @@ | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -code_pred [inductify, random] S\<^isub>2 . -thm S\<^isub>2.random_equation -thm A\<^isub>2.random_equation -thm B\<^isub>2.random_equation +code_pred [random_dseq inductify] S\<^isub>2 . +thm S\<^isub>2.random_dseq_equation +thm A\<^isub>2.random_dseq_equation +thm B\<^isub>2.random_dseq_equation -values [random] 10 "{x. S\<^isub>2 x}" +values [random_dseq 1, 2, 8] 10 "{x. S\<^isub>2 x}" lemma "w \ S\<^isub>2 ==> w \ [] ==> w \ [b, a] ==> w \ {}" -quickcheck[generator=predicate_compile] +quickcheck[generator=predicate_compile, size=8] oops lemma "[x <- w. x = a] = []" quickcheck[generator=predicate_compile] oops +declare list.size(3,4)[code_pred_def] +(* lemma "length ([x \ w. x = a]) = (0::nat)" -(*quickcheck[generator=predicate_compile]*) +quickcheck[generator=predicate_compile] oops - - +*) lemma -"w \ S\<^isub>2 ==> length [x \ w. x = a] < Suc (Suc 0)" -(*quickcheck[generator=predicate_compile]*) +"w \ S\<^isub>2 ==> length [x \ w. x = a] <= Suc (Suc 0)" +quickcheck[generator=predicate_compile, size = 10, iterations = 1] oops - theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=predicate_compile, size=15, iterations=100]*) +quickcheck[generator=predicate_compile, size=15, iterations=1] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -107,23 +134,24 @@ code_pred [inductify] S\<^isub>3 . thm S\<^isub>3.equation +(* +values 10 "{x. S\<^isub>3 x}" +*) -values 10 "{x. S\<^isub>3 x}" lemma S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=predicate_compile, size=10, iterations=1]*) +quickcheck[generator=predicate_compile, size=10, iterations=10] oops - lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -(*quickcheck[size=10, generator = pred_compile]*) +quickcheck[size=10, generator = predicate_compile] oops theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" (*quickcheck[generator=SML]*) -(*quickcheck[generator=predicate_compile, size=10, iterations=100]*) +quickcheck[generator=predicate_compile, size=10, iterations=100] oops @@ -138,13 +166,205 @@ theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator = predicate_compile, size=2, iterations=1]*) +quickcheck[generator = predicate_compile, size=5, iterations=1] oops theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -(*quickcheck[generator = pred_compile, size=5, iterations=1]*) +quickcheck[generator = predicate_compile, size=5, iterations=1] +oops + +hide const b + +subsection {* Lexicographic order *} +lemma + "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" + +subsection {* IMP *} + +types + var = nat + state = "int list" + +datatype com = + Skip | + Ass var "int" | + Seq com com | + IF "state list" com com | + While "state list" com + +inductive exec :: "com => state => state => bool" where + "exec Skip s s" | + "exec (Ass x e) s (s[x := e])" | + "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | + "s \ set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec (While b c) s s" | + "s1 \ set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" + +code_pred [random_dseq] exec . + +values [random_dseq 1, 2, 3] 10 "{(c, s, s'). exec c s s'}" + +lemma + "exec c s s' ==> exec (Seq c c) s s'" +quickcheck[generator = predicate_compile, size=3, iterations=1] +oops + +subsection {* Lambda *} + +datatype type = + Atom nat + | Fun type type (infixr "\" 200) + +datatype dB = + Var nat + | App dB dB (infixl "\" 200) + | Abs type dB + +primrec + nth_el :: "'a list \ nat \ 'a option" ("_\_\" [90, 0] 91) +where + "[]\i\ = None" +| "(x # xs)\i\ = (case i of 0 \ Some x | Suc j \ xs \j\)" + +inductive nth_el' :: "'a list \ nat \ 'a \ bool" +where + "nth_el' (x # xs) 0 x" +| "nth_el' xs i y \ nth_el' (x # xs) (Suc i) y" + +inductive typing :: "type list \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) + where + Var [intro!]: "nth_el' env x T \ env \ Var x : T" + | Abs [intro!]: "T # env \ t : U \ env \ Abs T t : (T \ U)" + | App [intro!]: "env \ s : U \ T \ env \ t : T \ env \ (s \ t) : U" + +primrec + lift :: "[dB, nat] => dB" +where + "lift (Var i) k = (if i < k then Var i else Var (i + 1))" + | "lift (s \ t) k = lift s k \ lift t k" + | "lift (Abs T s) k = Abs T (lift s (k + 1))" + +primrec + subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) +where + subst_Var: "(Var i)[s/k] = + (if k < i then Var (i - 1) else if i = k then s else Var i)" + | subst_App: "(t \ u)[s/k] = t[s/k] \ u[s/k]" + | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" + +inductive beta :: "[dB, dB] => bool" (infixl "\\<^sub>\" 50) + where + beta [simp, intro!]: "Abs T s \ t \\<^sub>\ s[t/0]" + | appL [simp, intro!]: "s \\<^sub>\ t ==> s \ u \\<^sub>\ t \ u" + | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t" + | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" + +lemma + "\ \ t : U \ t \\<^sub>\ t' \ \ \ t' : U" +quickcheck[generator = predicate_compile, size = 7, iterations = 10] oops +(* +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . +thm typing.equation + +code_pred (modes: i => i => bool, i => o => bool as reduce') beta . +thm beta.equation + +values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \\<^sub>\ x}" + +definition "reduce t = Predicate.the (reduce' t)" + +value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" + +code_pred [random] typing . +code_pred [random_dseq] typing . + +(*values [random] 1 "{(\, t, T). \ \ t : T}" +*)*) + +subsection {* JAD *} + +definition matrix :: "('a :: semiring_0) list list \ nat \ nat \ bool" where + "matrix M rs cs \ (\ row \ set M. length row = cs) \ length M = rs" +(* +code_pred [random_dseq inductify] matrix . +thm matrix.random_dseq_equation + +thm matrix_aux.random_dseq_equation + +values [random_dseq 3, 2] 10 "{(M, rs, cs). matrix (M:: int list list) rs cs}" +*) +lemma [code_pred_intro]: + "matrix [] 0 m" + "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m" +sorry + +code_pred [random_dseq inductify] matrix sorry + + +values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" + +definition "scalar_product v w = (\ (x, y)\zip v w. x * y)" + +definition mv :: "('a \ semiring_0) list list \ 'a list \ 'a list" + where [simp]: "mv M v = map (scalar_product v) M" +text {* + This defines the matrix vector multiplication. To work properly @{term +"matrix M m n \ length v = n"} must hold. +*} + +subsection "Compressed matrix" + +definition "sparsify xs = [i \ zip [0.. 0]" +(* +lemma sparsify_length: "(i, x) \ set (sparsify xs) \ i < length xs" + by (auto simp: sparsify_def set_zip) + +lemma listsum_sparsify[simp]: + fixes v :: "('a \ semiring_0) list" + assumes "length w = length v" + shows "(\x\sparsify w. (\(i, x). v ! i) x * snd x) = scalar_product v w" + (is "(\x\_. ?f x) = _") + unfolding sparsify_def scalar_product_def + using assms listsum_map_filter[where f="?f" and P="\ i. snd i \ (0::'a)"] + by (simp add: listsum_setsum) +*) +definition [simp]: "unzip w = (map fst w, map snd w)" + +primrec insert :: "('a \ 'b \ linorder) => 'a \ 'a list => 'a list" where + "insert f x [] = [x]" | + "insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)" + +primrec sort :: "('a \ 'b \ linorder) \ 'a list => 'a list" where + "sort f [] = []" | + "sort f (x # xs) = insert f x (sort f xs)" + +definition + "length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)" + +definition + "transpose M = [map (\ xs. xs ! i) (takeWhile (\ xs. i < length xs) M). i \ [0 ..< length (M ! 0)]]" + +definition + "inflate upds = foldr (\ (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)" + +definition + "jad = apsnd transpose o length_permutate o map sparsify" + +definition + "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\ (i, x). v ! i * x)))" +ML {* ML_Context.trace := false *} + +lemma "matrix (M::int list list) rs cs \ False" +quickcheck[generator = predicate_compile, size = 6] +oops + +lemma + "\ matrix M rs cs ; length v = cs \ \ jad_mv v (jad M) = mv M v" +(*quickcheck[generator = predicate_compile]*) +oops end \ No newline at end of file diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Jan 22 15:26:29 2010 +0100 @@ -1,5 +1,5 @@ theory Predicate_Compile_ex -imports Main Predicate_Compile_Alternative_Defs +imports Predicate_Compile_Alternative_Defs begin subsection {* Basic predicates *} @@ -7,8 +7,35 @@ inductive False' :: "bool" code_pred (expected_modes: bool) False' . -code_pred [depth_limited] False' . -code_pred [random] False' . +code_pred [dseq] False' . +code_pred [random_dseq] False' . + +values [expected "{}" pred] "{x. False'}" +values [expected "{}" dseq 1] "{x. False'}" +values [expected "{}" random_dseq 1, 1, 1] "{x. False'}" + +value "False'" + + +inductive True' :: "bool" +where + "True ==> True'" + +code_pred True' . +code_pred [dseq] True' . +code_pred [random_dseq] True' . + +thm True'.equation +thm True'.dseq_equation +thm True'.random_dseq_equation +values [expected "{()}" ]"{x. True'}" +values [expected "{}" dseq 0] "{x. True'}" +values [expected "{()}" dseq 1] "{x. True'}" +values [expected "{()}" dseq 2] "{x. True'}" +values [expected "{}" random_dseq 1, 1, 0] "{x. True'}" +values [expected "{}" random_dseq 1, 1, 1] "{x. True'}" +values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}" +values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}" inductive EmptySet :: "'a \ bool" @@ -38,6 +65,7 @@ EmptyClosure . thm EmptyClosure.equation + (* TODO: inductive package is broken! inductive False'' :: "bool" where @@ -53,12 +81,6 @@ code_pred (expected_modes: [], [1]) [inductify] EmptySet'' . *) -inductive True' :: "bool" -where - "True \ True'" - -code_pred (expected_modes: bool) True' . - consts a' :: 'a inductive Fact :: "'a \ 'a \ bool" @@ -72,7 +94,30 @@ "zerozero (0, 0)" code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . -code_pred [random] zerozero . +code_pred [dseq] zerozero . +code_pred [random_dseq] zerozero . + +thm zerozero.equation +thm zerozero.dseq_equation +thm zerozero.random_dseq_equation + +text {* We expect the user to expand the tuples in the values command. +The following values command is not supported. *} +(*values "{x. zerozero x}" *) +text {* Instead, the user must type *} +values "{(x, y). zerozero (x, y)}" + +values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}" +values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}" +values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}" +values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}" +values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}" + +inductive nested_tuples :: "((int * int) * int * int) => bool" +where + "nested_tuples ((0, 1), 2, 3)" + +code_pred nested_tuples . inductive JamesBond :: "nat => int => code_numeral => bool" where @@ -80,16 +125,17 @@ 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}" +values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}" +values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}" +values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}" +values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}" +values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}" +values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}" -values "{(a, b). JamesBond 0 b a}" -values "{(c, a). JamesBond a 0 c}" -values "{(a, c). JamesBond a 0 c}" +values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}" +values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}" +values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}" + subsection {* Alternative Rules *} @@ -119,14 +165,14 @@ case is_D_or_E from this(1) show thesis proof - fix x - assume x: "a1 = x" - assume "x = D \ x = E" + fix xa + assume x: "x = xa" + assume "xa = D \ xa = E" from this show thesis proof - assume "x = D" from this x is_D_or_E(2) show thesis by simp + assume "xa = D" from this x is_D_or_E(2) show thesis by simp next - assume "x = E" from this x is_D_or_E(3) show thesis by simp + assume "xa = E" from this x is_D_or_E(3) show thesis by simp qed qed qed @@ -157,15 +203,15 @@ case is_F_or_G from this(1) show thesis proof - fix x - assume x: "a1 = x" - assume "x = F \ x = G" + fix xa + assume x: "x = xa" + assume "xa = F \ xa = G" from this show thesis proof - assume "x = F" + assume "xa = F" from this x is_F_or_G(2) show thesis by simp next - assume "x = G" + assume "xa = G" from this x is_F_or_G(3) show thesis by simp qed qed @@ -200,15 +246,16 @@ code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . -subsection {* Numerals *} +subsection {* Sets and Numerals *} definition - "one_or_two == {Suc 0, (Suc (Suc 0))}" + "one_or_two = {Suc 0, (Suc (Suc 0))}" -(*code_pred [inductify] one_or_two .*) -code_pred [inductify, random] one_or_two . -(*values "{x. one_or_two x}"*) -values [random] "{x. one_or_two x}" +code_pred [inductify] one_or_two . +code_pred [dseq] one_or_two . +(*code_pred [random_dseq] one_or_two .*) +values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}" +(*values [random_dseq 1,1,2] "{x. one_or_two x}"*) inductive one_or_two' :: "nat => bool" where @@ -222,13 +269,12 @@ definition one_or_two'': "one_or_two'' == {1, (2::nat)}" - -code_pred [inductify] one_or_two'' . +ML {* prop_of @{thm one_or_two''} *} +(*code_pred [inductify] one_or_two'' . thm one_or_two''.equation values "{x. one_or_two'' x}" - - +*) subsection {* even predicate *} inductive even :: "nat \ bool" and odd :: "nat \ bool" where @@ -237,35 +283,55 @@ | "odd n \ even (Suc n)" code_pred (expected_modes: i => bool, o => bool) even . -code_pred [depth_limited] even . -code_pred [random] even . +code_pred [dseq] even . +code_pred [random_dseq] even . thm odd.equation thm even.equation -thm odd.depth_limited_equation -thm even.depth_limited_equation -thm even.random_equation -thm odd.random_equation +thm odd.dseq_equation +thm even.dseq_equation +thm odd.random_dseq_equation +thm even.random_dseq_equation values "{x. even 2}" values "{x. odd 2}" values 10 "{n. even n}" values 10 "{n. odd n}" -values [depth_limit = 2] "{x. even 6}" -values [depth_limit = 7] "{x. even 6}" -values [depth_limit = 2] "{x. odd 7}" -values [depth_limit = 8] "{x. odd 7}" -values [depth_limit = 7] 10 "{n. even n}" +values [expected "{}" dseq 2] "{x. even 6}" +values [expected "{}" dseq 6] "{x. even 6}" +values [expected "{()}" dseq 7] "{x. even 6}" +values [dseq 2] "{x. odd 7}" +values [dseq 6] "{x. odd 7}" +values [dseq 7] "{x. odd 7}" +values [expected "{()}" dseq 8] "{x. odd 7}" + +values [expected "{}" dseq 0] 8 "{x. even x}" +values [expected "{0::nat}" dseq 1] 8 "{x. even x}" +values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}" +values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}" +values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}" + +values [random_dseq 1, 1, 0] 8 "{x. even x}" +values [random_dseq 1, 1, 1] 8 "{x. even x}" +values [random_dseq 1, 1, 2] 8 "{x. even x}" +values [random_dseq 1, 1, 3] 8 "{x. even x}" +values [random_dseq 1, 1, 6] 8 "{x. even x}" + +values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}" +values [random_dseq 1, 1, 8] "{x. odd 7}" +values [random_dseq 1, 1, 9] "{x. odd 7}" definition odd' where "odd' x == \ even x" code_pred (expected_modes: i => bool) [inductify] odd' . -code_pred [inductify, depth_limited] odd' . -code_pred [inductify, random] odd' . +code_pred [dseq inductify] odd' . +code_pred [random_dseq inductify] odd' . -thm odd'.depth_limited_equation -values [depth_limit = 2] "{x. odd' 7}" -values [depth_limit = 9] "{x. odd' 7}" +values [expected "{}" dseq 2] "{x. odd' 7}" +values [expected "{()}" dseq 9] "{x. odd' 7}" +values [expected "{}" dseq 2] "{x. odd' 8}" +values [expected "{}" dseq 10] "{x. odd' 8}" + inductive is_even :: "nat \ bool" where @@ -280,22 +346,28 @@ | "append xs ys zs \ append (x # xs) ys (x # zs)" 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 . + i => o => i => bool as suffix, i => i => i => bool) append . +code_pred [dseq] append . +code_pred [random_dseq] append . thm append.equation -thm append.depth_limited_equation -thm append.random_equation -thm append.annotated_equation +thm append.dseq_equation +thm append.random_dseq_equation 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] 1 "{(ys, zs). append [1::nat, 2] ys zs}" +values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}" +values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" +values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" +values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" +values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}" value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (slice ([]::int list))" @@ -320,11 +392,11 @@ from append2(1) show thesis proof fix xs - assume "a1 = []" "a2 = xs" "a3 = xs" + assume "xa = []" "xb = xs" "xc = xs" from this append2(2) show thesis by simp next fix xs ys zs x - assume "a1 = x # xs" "a2 = ys" "a3 = x # zs" "append2 xs ys zs" + assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs" from this append2(3) show thesis by fastsimp qed qed @@ -336,11 +408,10 @@ 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 . +code_pred [random_dseq] tupled_append . thm tupled_append.equation -(*TODO: values with tupled modes*) -(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*) +values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}" inductive tupled_append' where @@ -358,7 +429,7 @@ | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" 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'' . + i * o * i => bool, i * i * i => bool) tupled_append'' . thm tupled_append''.equation inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" @@ -367,7 +438,7 @@ | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" 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''' . + i * o * i => bool, i * i * i => bool) tupled_append''' . thm tupled_append'''.equation subsection {* map_ofP predicate *} @@ -390,39 +461,46 @@ | "\ P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . -code_pred [depth_limited] filter1 . -code_pred [random] filter1 . +code_pred [dseq] filter1 . +code_pred [random_dseq] filter1 . thm filter1.equation +values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" +values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" +values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" + inductive filter2 where "filter2 P [] []" | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" | "\ P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" -code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 . -code_pred [depth_limited] filter2 . -code_pred [random] filter2 . +code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 . +code_pred [dseq] filter2 . +code_pred [random_dseq] filter2 . + thm filter2.equation -thm filter2.random_equation +thm filter2.random_dseq_equation +(* inductive filter3 for P where "List.filter P xs = ys ==> filter3 P xs ys" -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 +code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 . +code_pred [dseq] filter3 . +thm filter3.dseq_equation +*) inductive filter4 where "List.filter P xs = ys ==> filter4 P xs ys" -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . -code_pred [depth_limited] filter4 . -code_pred [random] filter4 . +(*code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .*) +(*code_pred [depth_limited] filter4 .*) +(*code_pred [random] filter4 .*) subsection {* reverse predicate *} @@ -452,9 +530,10 @@ | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" 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 . + (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) + partition . +code_pred [dseq] partition . +code_pred [random_dseq] partition . values 10 "{(ys, zs). partition is_even [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" @@ -489,19 +568,44 @@ from this converse_tranclpE[OF this(1)] show thesis by metis qed -code_pred [depth_limited] tranclp . -code_pred [random] tranclp . + +code_pred [dseq] tranclp . +code_pred [random_dseq] tranclp . thm tranclp.equation -thm tranclp.random_equation +thm tranclp.random_dseq_equation + +inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" +where + "rtrancl' x x r" +| "r x y ==> rtrancl' y z r ==> rtrancl' x z r" + +code_pred [random_dseq] rtrancl' . + +thm rtrancl'.random_dseq_equation + +inductive rtrancl'' :: "('a * 'a * ('a \ 'a \ bool)) \ bool" +where + "rtrancl'' (x, x, r)" +| "r x y \ rtrancl'' (y, z, r) \ rtrancl'' (x, z, r)" + +code_pred rtrancl'' . + +inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" +where + "rtrancl''' (x, (x, x), r)" +| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)" + +code_pred rtrancl''' . + inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" -code_pred succ . -code_pred [random] succ . +code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ . +code_pred [random_dseq] succ . thm succ.equation -thm succ.random_equation +thm succ.random_dseq_equation values 10 "{(m, n). succ n m}" values "{m. succ 0 m}" @@ -531,10 +635,55 @@ code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph . thm not_reachable_in_example_graph.equation - +thm tranclp.equation value "not_reachable_in_example_graph 0 3" value "not_reachable_in_example_graph 4 8" value "not_reachable_in_example_graph 5 6" +text {* rtrancl compilation is strange! *} +(* +value "not_reachable_in_example_graph 0 4" +value "not_reachable_in_example_graph 1 6" +value "not_reachable_in_example_graph 8 4"*) + +code_pred [dseq] not_reachable_in_example_graph . + +values [dseq 6] "{x. tranclp example_graph 0 3}" + +values [dseq 0] "{x. not_reachable_in_example_graph 0 3}" +values [dseq 0] "{x. not_reachable_in_example_graph 0 4}" +values [dseq 20] "{x. not_reachable_in_example_graph 0 4}" +values [dseq 6] "{x. not_reachable_in_example_graph 0 3}" +values [dseq 3] "{x. not_reachable_in_example_graph 4 2}" +values [dseq 6] "{x. not_reachable_in_example_graph 4 2}" + + +inductive not_reachable_in_example_graph' :: "int => int => bool" +where "\ (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y" + +code_pred not_reachable_in_example_graph' . + +value "not_reachable_in_example_graph' 0 3" +(* value "not_reachable_in_example_graph' 0 5" would not terminate *) + + +(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*) +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*) +(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) + +code_pred [dseq] not_reachable_in_example_graph' . + +(*thm not_reachable_in_example_graph'.dseq_equation*) + +(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*) +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}" +values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) + subsection {* IMP *} @@ -564,6 +713,7 @@ (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) [3,5] t}" + inductive tupled_exec :: "(com \ state \ state) \ bool" where "tupled_exec (Skip, s, s)" | "tupled_exec (Ass x e, s, s[x := e(s)])" | @@ -575,6 +725,8 @@ code_pred tupled_exec . +values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}" + subsection {* CCS *} text{* This example formalizes finite CCS processes without communication or @@ -633,13 +785,16 @@ where "Min s r x \ s x \ (\y. r x y \ x = y)" code_pred [inductify] Min . +thm Min.equation subsection {* Lexicographic order *} +declare lexord_def[code_pred_def] code_pred [inductify] lexord . -code_pred [inductify, random] lexord . +code_pred [random_dseq inductify] lexord . + thm lexord.equation -thm lexord.random_equation +thm lexord.random_dseq_equation inductive less_than_nat :: "nat * nat => bool" where @@ -648,38 +803,100 @@ code_pred less_than_nat . -code_pred [depth_limited] less_than_nat . -code_pred [random] less_than_nat . +code_pred [dseq] less_than_nat . +code_pred [random_dseq] less_than_nat . inductive test_lexord :: "nat list * nat list => bool" where "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" -code_pred [random] test_lexord . -code_pred [depth_limited] test_lexord . -thm test_lexord.depth_limited_equation -thm test_lexord.random_equation +code_pred test_lexord . +code_pred [dseq] test_lexord . +code_pred [random_dseq] test_lexord . +thm test_lexord.dseq_equation +thm test_lexord.random_dseq_equation values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" -values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" +(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*) +declare list.size(3,4)[code_pred_def] lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv - +(* code_pred [inductify] lexn . thm lexn.equation +*) +(* +code_pred [random_dseq inductify] lexn . +thm lexn.random_dseq_equation -code_pred [random] lexn . +values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" +*) +inductive has_length +where + "has_length [] 0" +| "has_length xs i ==> has_length (x # xs) (Suc i)" + +lemma has_length: + "has_length xs n = (length xs = n)" +proof (rule iffI) + assume "has_length xs n" + from this show "length xs = n" + by (rule has_length.induct) auto +next + assume "length xs = n" + from this show "has_length xs n" + by (induct xs arbitrary: n) (auto intro: has_length.intros) +qed -thm lexn.random_equation +lemma lexn_intros [code_pred_intro]: + "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)" + "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)" +proof - + assume "has_length xs i" "has_length ys i" "r (x, y)" + from this has_length show "lexn r (Suc i) (x # xs, y # ys)" + unfolding lexn_conv Collect_def mem_def + by fastsimp +next + assume "lexn r i (xs, ys)" + thm lexn_conv + from this show "lexn r (Suc i) (x#xs, x#ys)" + unfolding Collect_def mem_def lexn_conv + apply auto + apply (rule_tac x="x # xys" in exI) + by auto +qed + +code_pred [random_dseq inductify] lexn +proof - + fix n xs ys + assume 1: "lexn r n (xs, ys)" + assume 2: "\i x xs' y ys'. r = r ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r (x, y) ==> thesis" + assume 3: "\i x xs' ys'. r = r ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r i (xs', ys') ==> thesis" + from 1 2 3 show thesis + unfolding lexn_conv Collect_def mem_def + apply (auto simp add: has_length) + apply (case_tac xys) + apply auto + apply fastsimp + apply fastsimp done +qed + + +values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" + code_pred [inductify] lenlex . thm lenlex.equation -code_pred [inductify, random] lenlex . -thm lenlex.random_equation +code_pred [random_dseq inductify] lenlex . +thm lenlex.random_dseq_equation +values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" +thm lists.intros +(* code_pred [inductify] lists . -thm lists.equation +*) +(*thm lists.equation*) subsection {* AVL Tree *} @@ -693,12 +910,14 @@ "avl ET = True" "avl (MKT x l r h) = ((height l = height r \ height l = 1 + height r \ height r = 1+height l) \ h = max (height l) (height r) + 1 \ avl l \ avl r)" - +(* code_pred [inductify] avl . -thm avl.equation +thm avl.equation*) -code_pred [random] avl . -thm avl.random_equation +code_pred [random_dseq inductify] avl . +thm avl.random_dseq_equation + +values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}" fun set_of where @@ -714,30 +933,57 @@ code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of . thm set_of.equation -code_pred [inductify] is_ord . +code_pred (expected_modes: i => bool) [inductify] is_ord . thm is_ord_aux.equation thm is_ord.equation subsection {* Definitions about Relations *} +term "converse" +code_pred (modes: + (i * i => bool) => i * i => bool, + (i * o => bool) => o * i => bool, + (i * o => bool) => i * i => bool, + (o * i => bool) => i * o => bool, + (o * i => bool) => i * i => bool, + (o * o => bool) => o * o => bool, + (o * o => bool) => i * o => bool, + (o * o => bool) => o * i => bool, + (o * o => bool) => i * i => bool) [inductify] converse . -code_pred [inductify] converse . thm converse.equation code_pred [inductify] rel_comp . thm rel_comp.equation code_pred [inductify] Image . thm Image.equation -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 . +declare singleton_iff[code_pred_inline] +declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def] + +code_pred (expected_modes: + (o => bool) => o => bool, + (o => bool) => i * o => bool, + (o => bool) => o * i => bool, + (o => bool) => i => bool, + (i => bool) => i * o => bool, + (i => bool) => o * i => bool, + (i => bool) => i => bool) [inductify] Id_on . thm Id_on.equation -code_pred [inductify] Domain . +thm Domain_def +code_pred (modes: + (o * o => bool) => o => bool, + (o * o => bool) => i => bool, + (i * o => bool) => i => bool) [inductify] Domain . thm Domain.equation -code_pred [inductify] Range . +code_pred (modes: + (o * o => bool) => o => bool, + (o * o => bool) => i => bool, + (o * i => bool) => i => bool) [inductify] Range . thm Range.equation code_pred [inductify] Field . thm Field.equation +(*thm refl_on_def code_pred [inductify] refl_on . -thm refl_on.equation +thm refl_on.equation*) code_pred [inductify] total_on . thm total_on.equation code_pred [inductify] antisym . @@ -751,11 +997,11 @@ subsection {* Inverting list functions *} -code_pred [inductify] length . -code_pred [inductify, random] length . +(*code_pred [inductify] length . +code_pred [random inductify] length . thm size_listP.equation thm size_listP.random_equation - +*) (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*) code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat . @@ -764,19 +1010,19 @@ 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 +code_pred [dseq inductify] List.concat . +thm concatP.dseq_equation -values [depth_limit = 3] 3 +values [dseq 3] 3 "{xs. concatP xs ([0] :: nat list)}" -values [depth_limit = 5] 3 +values [dseq 5] 3 "{xs. concatP xs ([1] :: int list)}" -values [depth_limit = 5] 3 +values [dseq 5] 3 "{xs. concatP xs ([1] :: nat list)}" -values [depth_limit = 5] 3 +values [dseq 5] 3 "{xs. concatP xs [(1::int), 2]}" code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd . @@ -803,11 +1049,11 @@ code_pred [inductify] zip . thm zipP.equation -(*code_pred [inductify] upt .*) +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 [dseq inductify] remdups . +values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}" code_pred [inductify] remove1 . thm remove1P.equation @@ -815,13 +1061,12 @@ code_pred [inductify] removeAll . thm removeAllP.equation -code_pred [inductify, depth_limited] removeAll . +code_pred [dseq inductify] removeAll . -values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}" +values [dseq 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}" @@ -837,7 +1082,7 @@ code_pred [inductify] foldr . code_pred [inductify] foldl . code_pred [inductify] filter . -code_pred [inductify, random] filter . +code_pred [random_dseq inductify] filter . subsection {* Context Free Grammar *} @@ -852,11 +1097,11 @@ | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" code_pred [inductify] S\<^isub>1p . -code_pred [inductify, random] S\<^isub>1p . +code_pred [random_dseq inductify] S\<^isub>1p . thm S\<^isub>1p.equation -thm S\<^isub>1p.random_equation +thm S\<^isub>1p.random_dseq_equation -values [random] 5 "{x. S\<^isub>1p x}" +values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}" inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" @@ -866,12 +1111,12 @@ | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -code_pred [inductify, random] S\<^isub>2 . -thm S\<^isub>2.random_equation -thm A\<^isub>2.random_equation -thm B\<^isub>2.random_equation +code_pred [random_dseq inductify] S\<^isub>2p . +thm S\<^isub>2p.random_dseq_equation +thm A\<^isub>2p.random_dseq_equation +thm B\<^isub>2p.random_dseq_equation -values [random] 10 "{x. S\<^isub>2 x}" +values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}" inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where "[] \ S\<^isub>3" @@ -881,10 +1126,10 @@ | "w \ S\<^isub>3 \ b # w \ B\<^isub>3" | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" -code_pred [inductify] S\<^isub>3 . -thm S\<^isub>3.equation +code_pred [inductify] S\<^isub>3p . +thm S\<^isub>3p.equation -values 10 "{x. S\<^isub>3 x}" +values 10 "{x. S\<^isub>3p x}" inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" @@ -950,7 +1195,7 @@ code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . thm typing.equation -code_pred (modes: i => o => bool as reduce') beta . +code_pred (modes: i => i => bool, i => o => bool as reduce') beta . thm beta.equation values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \\<^sub>\ x}" @@ -959,18 +1204,19 @@ value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" -code_pred [random] typing . +code_pred [dseq] typing . +code_pred [random_dseq] typing . -values [random] 1 "{(\, t, T). \ \ t : T}" +values [random_dseq 1,1,5] 10 "{(\, t, T). \ \ t : T}" subsection {* A minimal example of yet another semantics *} text {* thanks to Elke Salecker *} types -vname = nat -vvalue = int -var_assign = "vname \ vvalue" --"variable assignment" + vname = nat + vvalue = int + var_assign = "vname \ vvalue" --"variable assignment" datatype ir_expr = IrConst vvalue @@ -981,10 +1227,10 @@ IntVal vvalue record configuration = -Env :: var_assign + Env :: var_assign inductive eval_var :: -"ir_expr \ configuration \ val \ bool" + "ir_expr \ configuration \ val \ bool" where irconst: "eval_var (IrConst i) conf (IntVal i)" | objaddr: "\ Env conf n = i \ \ eval_var (ObjAddr n) conf (IntVal i)" diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/Pure/Isar/spec_rules.ML Fri Jan 22 15:26:29 2010 +0100 @@ -12,6 +12,8 @@ type spec = rough_classification * (term list * thm list) val get: Proof.context -> spec list val get_global: theory -> spec list + val retrieve: Proof.context -> term -> spec list + val retrieve_global: theory -> term -> spec list val add: rough_classification -> term list * thm list -> local_theory -> local_theory val add_global: rough_classification -> term list * thm list -> theory -> theory end; @@ -41,6 +43,9 @@ val get = Item_Net.content o Rules.get o Context.Proof; val get_global = Item_Net.content o Rules.get o Context.Theory; +val retrieve = Item_Net.retrieve o Rules.get o Context.Proof; +val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory; + fun add class (ts, ths) lthy = let val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts; diff -r e1b8f2736404 -r dcd0fa5cc6d3 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/Tools/quickcheck.ML Fri Jan 22 15:26:29 2010 +0100 @@ -7,6 +7,7 @@ signature QUICKCHECK = sig val auto: bool Unsynchronized.ref + val timing : bool Unsynchronized.ref val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory @@ -21,6 +22,8 @@ val auto = Unsynchronized.ref false; +val timing = Unsynchronized.ref false; + val _ = ProofGeneralPgip.add_preference Preferences.category_tracing (setmp_CRITICAL auto true (fn () => @@ -97,9 +100,10 @@ fun test_term ctxt quiet generator_name size i t = let val (names, t') = prep_test_term t; - val testers = case generator_name - of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' - | SOME name => [mk_tester_select name ctxt t']; + val testers = (*cond_timeit (!timing) "quickcheck compilation" + (fn () => *)(case generator_name + of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' + | SOME name => [mk_tester_select name ctxt t']); fun iterate f 0 = NONE | iterate f j = case f () handle Match => (if quiet then () else warning "Exception Match raised during quickcheck"; NONE) @@ -113,9 +117,11 @@ else (if quiet then () else priority ("Test data size: " ^ string_of_int k); case with_testers k testers of NONE => with_size (k + 1) | SOME q => SOME q); - in case with_size 1 - of NONE => NONE - | SOME ts => SOME (names ~~ ts) + in + cond_timeit (!timing) "quickcheck execution" + (fn () => case with_size 1 + of NONE => NONE + | SOME ts => SOME (names ~~ ts)) end; fun monomorphic_term thy insts default_T =