# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 4785ef554dccdc104a469f8e5f7f2e25a03f837b # Parent 0f6e30b87cf19c0fd424e9ff50736dcf48dcc181 added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex diff -r 0f6e30b87cf1 -r 4785ef554dcc src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200 @@ -8,6 +8,7 @@ val define_predicates : (string * thm list) list -> theory -> theory val rewrite_intro : theory -> thm -> thm list val setup_oracle : theory -> theory + val pred_of_function : theory -> string -> string option end; structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = @@ -63,6 +64,8 @@ fun merge _ = Symtab.merge (op =); ) +fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name + fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) @@ -246,6 +249,8 @@ let val _ = tracing ("Flattening term " ^ (Syntax.string_of_term_global thy t)) val (f, args) = strip_comb t + (* TODO: special procedure for higher-order functions: split arguments in + simple types and function types *) val resname = Name.variant names "res" val resvar = Free (resname, body_type (fastype_of t)) val names' = resname :: names @@ -356,7 +361,7 @@ Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) end fun mk_rewr_thm (func, pred) = @{thm refl} - in + in case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of NONE => thy | SOME intr_ts => let diff -r 0f6e30b87cf1 -r 4785ef554dcc src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 @@ -64,9 +64,9 @@ val thy'' = thy' |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) |> Predicate_Compile.preprocess full_constname - |> Predicate_Compile_Core.add_equations [full_constname] - |> Predicate_Compile_Core.add_sizelim_equations [full_constname] - |> Predicate_Compile_Core.add_quickcheck_equations [full_constname] + |> Predicate_Compile_Core.add_equations NONE [full_constname] + |> Predicate_Compile_Core.add_sizelim_equations NONE [full_constname] + |> Predicate_Compile_Core.add_quickcheck_equations NONE [full_constname] val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname val prog = diff -r 0f6e30b87cf1 -r 4785ef554dcc src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -135,28 +135,38 @@ (Graph.strong_conn gr) thy end -fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy = +fun code_pred_cmd (((modes, inductify_all), rpred), raw_const) lthy = if inductify_all then let val thy = ProofContext.theory_of lthy val const = Code.read_const thy raw_const val lthy' = LocalTheory.theory (preprocess const) lthy |> LocalTheory.checkpoint + + val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + SOME c => c + | NONE => const val _ = tracing "Starting Predicate Compile Core..." - in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end + in Predicate_Compile_Core.code_pred modes rpred const lthy' end else - Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy + Predicate_Compile_Core.code_pred_cmd modes rpred raw_const lthy val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"] +val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred", "mode"] local structure P = OuterParse in +val opt_modes = + Scan.optional (P.$$$ "(" |-- P.$$$ "mode" |-- P.$$$ ":" |-- + P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") + --| P.$$$ ")" >> SOME) NONE + val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd) + OuterKeyword.thy_goal (opt_modes -- + P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd) end diff -r 0f6e30b87cf1 -r 4785ef554dcc src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -7,8 +7,8 @@ signature PREDICATE_COMPILE_CORE = sig val setup: theory -> theory - val code_pred: bool -> string -> Proof.context -> Proof.state - val code_pred_cmd: bool -> string -> Proof.context -> Proof.state + val code_pred: int list list option -> bool -> string -> Proof.context -> Proof.state + val code_pred_cmd: int list list option -> bool -> string -> Proof.context -> Proof.state type smode = (int * int list option) list type mode = smode option list * smode datatype tmode = Mode of mode * smode * tmode option list; @@ -39,7 +39,7 @@ val mk_casesrule : Proof.context -> int -> thm list -> term val analyze_compr: theory -> term -> term val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref - val add_equations : string list -> theory -> theory + val add_equations : int list list option -> string list -> theory -> theory val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) (*val funT_of : mode -> typ -> typ @@ -90,8 +90,8 @@ val rpred_compfuns : compilation_funs val dest_funT : typ -> typ * typ (* val depending_preds_of : theory -> thm list -> string list *) - val add_quickcheck_equations : string list -> theory -> theory - val add_sizelim_equations : string list -> theory -> theory + val add_quickcheck_equations : int list list option -> string list -> theory -> theory + val add_sizelim_equations : int list list option -> string list -> theory -> theory val is_inductive_predicate : theory -> string -> bool val terms_vs : term list -> string list val subsets : int -> int -> int list list @@ -197,6 +197,13 @@ (** data structures **) +(* new datatype for modes: *) +(* +datatype instantiation = Input | Output +type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode +type mode = arg_mode list +type tmode = Mode of mode * +*) type smode = (int * int list option) list type mode = smode option list * smode; datatype tmode = Mode of mode * smode * tmode option list; @@ -2193,7 +2200,8 @@ fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of (Ts as _ :: _ :: _) => if (length (HOLogic.strip_tuple arg) = length Ts) then true - else error ("Format of introduction rule is invalid: tuples must be expanded:" + else + error ("Format of introduction rule is invalid: tuples must be expanded:" ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ (Display.string_of_thm_global thy intro)) | _ => true @@ -2210,16 +2218,21 @@ (** main function of predicate compiler **) -fun add_equations_of steps prednames thy = +fun add_equations_of steps expected_modes prednames thy = let val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) - val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames) + (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = prepare_intrs thy prednames (maps (intros_of thy) prednames) val _ = Output.tracing "Infering modes..." val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses - val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses + val modes : (string * ((int * int list option) list option list * (int * int list option) list) list) list = map (fn (p, mps) => (p, map fst mps)) moded_clauses + val all_smodes : (((int * int list option) list) list) list = map (map snd) (map snd modes) + val _ = case expected_modes of + SOME ms => if not (forall (fn smodes => eq_set (map (map (rpair NONE)) ms, smodes)) all_smodes) then + error ("expected modes were not inferred - " ^ commas (map string_of_smode (flat all_smodes))) else () + | NONE => () val _ = print_modes modes val _ = print_moded_clauses thy moded_clauses val _ = Output.tracing "Defining executable functions..." @@ -2258,7 +2271,7 @@ fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) -fun gen_add_equations steps names thy = +fun gen_add_equations steps expected_modes names thy = let val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy |> Theory.checkpoint; @@ -2267,7 +2280,7 @@ val scc = strong_conn_of (PredData.get thy') names val thy'' = fold_rev (fn preds => fn thy => - if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy) + if #are_not_defined steps thy preds then add_equations_of steps expected_modes preds thy else thy) scc thy' |> Theory.checkpoint in thy'' end @@ -2323,7 +2336,7 @@ (*FIXME why distinguished attribute for cases?*) (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *) -fun generic_code_pred prep_const rpred raw_const lthy = +fun generic_code_pred prep_const modes rpred raw_const lthy = let val thy = ProofContext.theory_of lthy val const = prep_const thy raw_const @@ -2353,9 +2366,9 @@ in goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> (if rpred then - (add_equations [const] #> - add_sizelim_equations [const] #> add_quickcheck_equations [const]) - else add_equations [const])) + (add_equations NONE [const] #> + add_sizelim_equations NONE [const] #> add_quickcheck_equations NONE [const]) + else add_equations modes [const])) end in Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' @@ -2442,7 +2455,6 @@ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; - local structure P = OuterParse in val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; diff -r 0f6e30b87cf1 -r 4785ef554dcc src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -7,11 +7,28 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred even . +code_pred (mode: [], [1]) even . thm odd.equation thm even.equation +(* +lemma unit: "unit_case f = (\x. f)" +apply (rule ext) +apply (case_tac x) +apply (simp only: unit.cases) +done +lemma "even_1 (Suc (Suc n)) = even_1 n" +thm even.equation(2) +unfolding even.equation(1)[of "Suc (Suc n)"] +unfolding odd.equation +unfolding single_bind +apply simp +apply (simp add: unit) +unfolding bind_single +apply (rule refl) +done +*) values "{x. even 2}" values "{x. odd 2}" values 10 "{n. even n}" @@ -21,7 +38,9 @@ "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" -code_pred append . +code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . +thm append.equation + code_pred (inductify_all) (rpred) append . thm append.equation @@ -57,7 +76,7 @@ code_pred (inductify_all) tupled_append' . thm tupled_append'.equation -(* TODO: Missing a few modes! *) +(* TODO: Modeanalysis returns mode [2] ?? *) inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" where @@ -68,7 +87,7 @@ code_pred (inductify_all) tupled_append'' . thm tupled_append''.equation -(* TODO: Missing a few modes *) +(* TODO: Modeanalysis returns mode [2] ?? *) inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" where @@ -78,9 +97,7 @@ code_pred (inductify_all) tupled_append''' . thm tupled_append'''.equation (* TODO: Missing a few modes *) -thm fst_conv snd_conv -thm map_of.simps -term "map_of" + inductive map_ofP :: "('a \ 'b) list \ 'a \ 'b \ bool" where "map_ofP ((a, b)#xs) a b" @@ -367,6 +384,33 @@ code_pred (inductify_all) Domain . thm Domain.equation +section {* List functions *} + +code_pred (inductify_all) length . +thm size_listP.equation + +code_pred (inductify_all) concat . +thm concatP.equation + +code_pred (inductify_all) hd . +code_pred (inductify_all) tl . +code_pred (inductify_all) last . +code_pred (inductify_all) butlast . +(*code_pred (inductify_all) listsum .*) +code_pred (inductify_all) take . +code_pred (inductify_all) drop . +code_pred (inductify_all) zip . +code_pred (inductify_all) upt . +code_pred set sorry +code_pred (inductify_all) remdups . +code_pred (inductify_all) remove1 . +code_pred (inductify_all) removeAll . +code_pred (inductify_all) distinct . +code_pred (inductify_all) replicate . +code_pred (inductify_all) splice . +code_pred (inductify_all) List.rev . +thm revP.equation + section {* Context Free Grammar *}