# HG changeset patch # User haftmann # Date 1242851047 -7200 # Node ID c025f32afd4e0581fe6927f023a4f005e0a2b26c # Parent 29da4d396e1f7e08c1c6d03a5e573f36299d4fec experimental values command diff -r 29da4d396e1f -r c025f32afd4e src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Wed May 20 22:24:07 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Wed May 20 22:24:07 2009 +0200 @@ -7,39 +7,53 @@ setup {* Predicate_Compile.setup *} - text {* Experimental code *} -definition pred_map :: "('a \ 'b) \ 'a Predicate.pred \ 'b Predicate.pred" where - "pred_map f P = Predicate.bind P (Predicate.single o f)" - ML {* -structure Predicate = +structure Predicate_Compile = struct -open Predicate; - -val pred_ref = ref (NONE : (unit -> term Predicate.pred) option); +open Predicate_Compile; -fun eval_pred thy t = - Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy (HOLogic.mk_term_of (fastype_of t) t) []; +fun eval thy t_compr = + let + val t = Predicate_Compile.analyze_compr thy t_compr; + val Type (@{type_name Predicate.pred}, [T]) = fastype_of t; + fun mk_predT T = Type (@{type_name Predicate.pred}, [T]); + val T1 = T --> @{typ term}; + val T2 = T1 --> mk_predT T --> mk_predT @{typ term}; + val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*) + $ Const (@{const_name Code_Eval.term_of}, T1) $ t; + in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) @{code Predicate.map} thy t' []) end; -fun eval_pred_elems thy t T length = - t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T; +fun values ctxt k t_compr = + let + val thy = ProofContext.theory_of ctxt; + val (T, t') = eval thy t_compr; + in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end; -fun analyze_compr thy t = +fun values_cmd modes k raw_t state = let - val split = case t of (Const (@{const_name Collect}, _) $ t') => t' - | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t); - val (body, Ts, fp) = HOLogic.strip_split split; - val (t_pred, args) = strip_comb body; - val pred = case t_pred of Const (pred, _) => pred - | _ => error ("Not a constant: " ^ Syntax.string_of_term_global thy t_pred); - val mode = map is_Bound args; (*FIXME what about higher-order modes?*) - val args' = filter_out is_Bound args; - val T = HOLogic.mk_tupleT fp Ts; - val mk = HOLogic.mk_tuple' fp T; - in (((pred, mode), args), (mk, T)) end; + val ctxt = Toplevel.context_of state; + val t = Syntax.read_term ctxt raw_t; + val t' = values ctxt k t; + val ty' = Term.type_of t'; + val ctxt' = Variable.auto_fixes t' ctxt; + val p = PrintMode.with_modes 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')]) (); + in Pretty.writeln p end; + +end; + +local structure P = OuterParse in + +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; + +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag + (opt_modes -- Scan.optional P.nat ~1 -- P.term + >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep + (Predicate_Compile.values_cmd modes k t))); end; *} diff -r 29da4d396e1f -r c025f32afd4e src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Wed May 20 22:24:07 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed May 20 22:24:07 2009 +0200 @@ -12,7 +12,10 @@ thm even.equation -ML_val {* Predicate.yieldn 10 @{code even_0} *} +values "{x. even 2}" +values "{x. odd 2}" +values 10 "{n. even n}" +values 10 "{n. odd n}" inductive append :: "'a list \ 'a list \ 'a list \ bool" where @@ -24,7 +27,9 @@ thm append.equation -ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *} +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]}" inductive partition :: "('a \ bool) \ 'a list \ 'a list \ 'a list \ bool" @@ -38,10 +43,26 @@ thm partition.equation +(*FIXME values 10 "{(ys, zs). partition (\n. n mod 2 = 0) + [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*) + code_pred tranclp using assms by (rule tranclp.cases) thm tranclp.equation +inductive succ :: "nat \ nat \ bool" where + "succ 0 1" + | "succ m n \ succ (Suc m) (Suc n)" + +code_pred succ + using assms by (rule succ.cases) + +thm succ.equation + +values 20 "{n. tranclp succ 10 n}" +values "{n. tranclp succ n 10}" +values 20 "{(n, m). tranclp succ n m}" + end \ No newline at end of file diff -r 29da4d396e1f -r c025f32afd4e src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Wed May 20 22:24:07 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Wed May 20 22:24:07 2009 +0200 @@ -1,4 +1,4 @@ -(* Author: Lukas Bulwahn +(* Author: Lukas Bulwahn, TU Muenchen (Prototype of) A compiler from predicates specified by intro/elim rules to equations. @@ -13,14 +13,15 @@ val strip_intro_concl: term -> int -> term * (term list * term list) val modename_of: theory -> string -> mode -> string val modes_of: theory -> string -> mode list + val pred_intros: theory -> string -> thm list + val get_nparams: theory -> string -> int val setup: theory -> theory val code_pred: string -> Proof.context -> Proof.state val code_pred_cmd: string -> Proof.context -> Proof.state val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) val do_proofs: bool ref - val pred_intros : theory -> string -> thm list - val get_nparams : theory -> string -> int - val pred_term_of : theory -> term -> term option + val analyze_compr: theory -> term -> term + val eval_ref: (unit -> term Predicate.pred) option ref end; structure Predicate_Compile : PREDICATE_COMPILE = @@ -1425,29 +1426,37 @@ (*FIXME - Naming of auxiliary rules necessary? +- add default code equations P x y z = P_i_i_i x y z *) (* transformation for code generation *) -fun pred_term_of thy t = let - val (vars, body) = strip_abs t - val (pred, all_args) = strip_comb body - val (name, T) = dest_Const pred - val (params, args) = chop (get_nparams thy name) all_args - val user_mode = flat (map_index - (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1]) - args) - val (inargs, _) = get_args user_mode args - val all_modes = Symtab.dest (#modes (IndCodegenData.get thy)) - val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of_term all_modes (list_comb (pred, params))) - fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs) - in - case modes of - [] => (let val _ = error "No mode possible for this term" in NONE end) - | [m] => SOME (compile m) - | ms => (let val _ = warning "Multiple modes possible for this term" - in SOME (compile (hd ms)) end) - end; +val eval_ref = ref (NONE : (unit -> term Predicate.pred) option); + +fun analyze_compr thy t_compr = + let + 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_split split; + (*FIXME former order of tuple positions must be restored*) + val (pred as Const (name, T), all_args) = strip_comb body + val (params, args) = chop (get_nparams 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 (inargs, _) = get_args user_mode args; + val all_modes = Symtab.dest (#modes (IndCodegenData.get thy)); + val modes = filter (fn Mode (_, is, _) => is = user_mode) + (modes_of_term all_modes (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 t_eval = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), + inargs) + in t_eval end; end;