# HG changeset patch # User haftmann # Date 1240587916 -7200 # Node ID 5b65835ccc920a87797c687d2b3f6f21af193ddf # Parent 7fbebf75b3ef6f6765efc6ee6d82ab13e117d230 some experiements towards user interface for predicate compiler diff -r 7fbebf75b3ef -r 5b65835ccc92 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Fri Apr 24 17:45:15 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Fri Apr 24 17:45:16 2009 +0200 @@ -1,20 +1,17 @@ theory Predicate_Compile -imports Complex_Main Code_Index Lattice_Syntax +imports Complex_Main Lattice_Syntax Code_Eval uses "predicate_compile.ML" begin +text {* Package setup *} + setup {* Predicate_Compile.setup *} -primrec "next" :: "('a Predicate.pred \ ('a \ 'a Predicate.pred) option) - \ 'a Predicate.seq \ ('a \ 'a Predicate.pred) option" where - "next yield Predicate.Empty = None" - | "next yield (Predicate.Insert x P) = Some (x, P)" - | "next yield (Predicate.Join P xq) = (case yield P - of None \ next yield xq | Some (x, Q) \ Some (x, Predicate.Seq (\_. Predicate.Join Q xq)))" + +text {* Experimental code *} -fun anamorph :: "('b \ ('a \ 'b) option) \ index \ 'b \ 'a list \ 'b" where - "anamorph f k x = (if k = 0 then ([], x) - else case f x of None \ ([], x) | Some (v, y) \ let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" +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 = @@ -22,11 +19,68 @@ open Predicate; -fun yield (Predicate.Seq f) = @{code next} yield (f ()); +val pred_ref = ref (NONE : (unit -> term Predicate.pred) option); + +fun eval_pred thy t = + t + |> Eval.mk_term_of (fastype_of t) + |> (fn t => Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy t []); + +fun eval_pred_elems thy t T length = + t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T; -fun yieldn k = @{code anamorph} yield k; +fun analyze_compr thy t = + 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; end; *} + +text {* Example(s) *} + +inductive even :: "nat \ bool" and odd :: "nat \ bool" where + "even 0" + | "even n \ odd (Suc n)" + | "odd n \ even (Suc n)" + +setup {* pred_compile "even" *} +thm even_codegen + + +inductive append :: "'a list \ 'a list \ 'a list \ bool" where + append_Nil: "append [] xs xs" + | append_Cons: "append xs ys zs \ append (x # xs) ys (x # zs)" + +setup {* pred_compile "append" *} +thm append_codegen + + +inductive partition :: "('a \ bool) \ 'a list \ 'a list \ 'a list \ bool" + for f where + "partition f [] [] []" + | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" + | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" + +setup {* pred_compile "partition" *} +thm partition_codegen + +setup {* pred_compile "tranclp" *} +thm tranclp_codegen + +ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *} +ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *} + +ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *} + end \ No newline at end of file diff -r 7fbebf75b3ef -r 5b65835ccc92 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Fri Apr 24 17:45:15 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Fri Apr 24 17:45:16 2009 +0200 @@ -6,38 +6,119 @@ signature PREDICATE_COMPILE = sig - val create_def_equation': string -> (int list option list * int list) option -> theory -> theory + type mode = int list option list * int list + val create_def_equation': string -> mode option -> theory -> theory val create_def_equation: string -> theory -> theory - val intro_rule: theory -> string -> (int list option list * int list) -> thm - val elim_rule: theory -> string -> (int list option list * int list) -> thm + val intro_rule: theory -> string -> mode -> thm + val elim_rule: theory -> string -> mode -> thm val strip_intro_concl : term -> int -> (term * (term list * term list)) val code_ind_intros_attrib : attribute val code_ind_cases_attrib : attribute + val print_alternative_rules : theory -> theory + val modename_of: theory -> string -> mode -> string + val modes_of: theory -> string -> mode list val setup : theory -> theory - val print_alternative_rules : theory -> theory val do_proofs: bool ref end; structure Predicate_Compile: PREDICATE_COMPILE = struct +(** auxiliary **) + +(* debug stuff *) + +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); + +fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); +fun debug_tac msg = (fn st => (tracing msg; Seq.single st)); + +val do_proofs = ref true; + + +(** fundamentals **) + +(* syntactic operations *) + +fun mk_eq (x, xs) = + let fun mk_eqs _ [] = [] + | mk_eqs a (b::cs) = + HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs + in mk_eqs x xs end; + +fun mk_tupleT [] = HOLogic.unitT + | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts; + +fun mk_tuple [] = HOLogic.unit + | mk_tuple ts = foldr1 HOLogic.mk_prod ts; + +fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = [] + | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2) + | dest_tuple t = [t] + +fun mk_pred_enumT T = Type ("Predicate.pred", [T]) + +fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T + | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []); + +fun mk_Enum f = + let val T as Type ("fun", [T', _]) = fastype_of f + in + Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f + end; + +fun mk_Eval (f, x) = + let val T = fastype_of x + in + Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x + end; + +fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T); + +fun mk_single t = + let val T = fastype_of t + in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end; + +fun mk_bind (x, f) = + let val T as Type ("fun", [_, U]) = fastype_of f + in + Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f + end; + +val mk_sup = HOLogic.mk_binop @{const_name sup}; + +fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred}, + HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) $ cond; + +fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT + in Const (@{const_name Predicate.not_pred}, T --> T) $ t end + + +(* data structures *) + +type mode = int list option list * int list; + +val mode_ord = prod_ord (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord); + structure PredModetab = TableFun( - type key = (string * (int list option list * int list)) - val ord = prod_ord fast_string_ord (prod_ord - (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord))) + type key = string * mode + val ord = prod_ord fast_string_ord mode_ord +); +(*FIXME scrap boilerplate*) + structure IndCodegenData = TheoryDataFun ( type T = {names : string PredModetab.table, - modes : ((int list option list * int list) list) Symtab.table, + modes : mode list Symtab.table, function_defs : Thm.thm Symtab.table, function_intros : Thm.thm Symtab.table, function_elims : Thm.thm Symtab.table, - intro_rules : (Thm.thm list) Symtab.table, + intro_rules : Thm.thm list Symtab.table, elim_rules : Thm.thm Symtab.table, nparams : int Symtab.table - }; + }; (*FIXME: better group tables according to key*) (* names: map from inductive predicate and mode to function name (string). modes: map from inductive predicates to modes function_defs: map from function name to definition @@ -115,26 +196,12 @@ intro_rules = #intro_rules x, elim_rules = #elim_rules x, nparams = f (#nparams x)}) thy -(* Debug stuff and tactics ***********************************************************) - -fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); -fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); - -fun debug_tac msg = (fn st => - (tracing msg; Seq.single st)); - (* removes first subgoal *) fun mycheat_tac thy i st = (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st -val (do_proofs : bool ref) = ref true; - (* Lightweight mode analysis **********************************************) -(* Hack for message from old code generator *) -val message = tracing; - - (**************************************************************************) (* source code from old code generator ************************************) @@ -153,7 +220,8 @@ | _ => false) in check end; -(**** check if a type is an equality type (i.e. doesn't contain fun) ****) +(**** check if a type is an equality type (i.e. doesn't contain fun) + FIXME this is only an approximation ****) fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts | is_eqT _ = true; @@ -165,7 +233,7 @@ | SOME js => enclose "[" "]" (commas (map string_of_int js))) (iss @ [SOME is])); -fun print_modes modes = message ("Inferred modes:\n" ^ +fun print_modes modes = tracing ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)); @@ -182,6 +250,7 @@ (get_args' is (i+1) ts) in get_args' is 1 ts end +(*FIXME this function should not be named merge... make it local instead*) fun merge xs [] = xs | merge [] ys = ys | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) @@ -197,7 +266,8 @@ fun cprods xss = foldr (map op :: o cprod) [[]] xss; -datatype mode = Mode of (int list option list * int list) * int list * mode option list; +datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand + why there is another mode type!?*) fun modes_of modes t = let @@ -285,11 +355,11 @@ in (p, List.filter (fn m => case find_index (not o check_mode_clause thy param_vs modes m) rs of ~1 => true - | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^ + | i => (tracing ("Clause " ^ string_of_int (i+1) ^ " of " ^ p ^ " violates mode " ^ string_of_mode m); false)) ms) end; -fun fixp f (x : (string * (int list option list * int list) list) list) = +fun fixp f (x : (string * mode list) list) = let val y = f x in if x = y then x else fixp f y end; @@ -306,66 +376,6 @@ (*****************************************************************************************) (**** term construction ****) -fun mk_eq (x, xs) = - let fun mk_eqs _ [] = [] - | mk_eqs a (b::cs) = - HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs - in mk_eqs x xs end; - -fun mk_tuple [] = HOLogic.unit - | mk_tuple ts = foldr1 HOLogic.mk_prod ts; - -fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = [] - | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2) - | dest_tuple t = [t] - -fun mk_tupleT [] = HOLogic.unitT - | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts; - -fun mk_pred_enumT T = Type ("Predicate.pred", [T]) - -fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T - | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []); - -fun mk_single t = - let val T = fastype_of t - in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end; - -fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T); - -fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred}, - HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) - $ cond - -fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT - in Const (@{const_name Predicate.not_pred}, T --> T) $ t end - -fun mk_bind (x, f) = - let val T as Type ("fun", [_, U]) = fastype_of f - in - Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f - end; - -fun mk_Enum f = - let val T as Type ("fun", [T', _]) = fastype_of f - in - Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f - end; - -fun mk_Eval (f, x) = - let val T = fastype_of x - in - Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x - end; - -fun mk_Eval' f = - let val T = fastype_of f - in - Const (@{const_name Predicate.eval}, T --> dest_pred_enumT T --> HOLogic.boolT) $ f - end; - -val mk_sup = HOLogic.mk_binop @{const_name sup}; - (* for simple modes (e.g. parameters) only: better call it param_funT *) (* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) fun funT_of T NONE = T @@ -424,13 +434,16 @@ (v', mk_empty U')])) end; -fun modename thy name mode = let +fun modename_of thy name mode = let val v = (PredModetab.lookup (#names (IndCodegenData.get thy)) (name, mode)) - in if (is_some v) then the v - else error ("fun modename - definition not found: name: " ^ name ^ " mode: " ^ (makestring mode)) + in if (is_some v) then the v (*FIXME use case here*) + else error ("fun modename_of - definition not found: name: " ^ name ^ " mode: " ^ (makestring mode)) end -(* function can be removed *) +fun modes_of thy = + these o Symtab.lookup ((#modes o IndCodegenData.get) thy); + +(*FIXME function can be removed*) fun mk_funcomp f t = let val names = Term.add_free_names t []; @@ -449,7 +462,7 @@ val f' = case f of Const (name, T) => if AList.defined op = modes name then - Const (modename thy name (iss, is'), funT'_of (iss, is') T) + Const (modename_of thy name (iss, is'), funT'_of (iss, is') T) else error "compile param: Not an inductive predicate with correct mode" | Free (name, T) => Free (name, funT_of T (SOME is')) in list_comb (f', params' @ args') end @@ -463,7 +476,7 @@ val (Ts, Us) = get_args is (curry Library.drop (length ms) (fst (strip_type T))) val params' = map (compile_param thy modes) (ms ~~ params) - val mode_id = modename thy name mode + val mode_id = modename_of thy name mode in list_comb (Const (mode_id, ((map fastype_of params') @ Ts) ---> mk_pred_enumT (mk_tupleT Us)), params') end @@ -556,7 +569,7 @@ val cl_ts = map (fn cl => compile_clause thy all_vs param_vs modes mode cl (mk_tuple xs)) cls; - val mode_id = modename thy s mode + val mode_id = modename_of thy s mode in HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (mode_id, (Ts1' @ Us1) ---> @@ -591,7 +604,7 @@ fold Term.add_consts intrs [] |> map fst |> filter_out (member (op =) preds) |> filter (is_ind_pred thy) -fun print_arities arities = message ("Arities:\n" ^ +fun print_arities arities = tracing ("Arities:\n" ^ cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ space_implode " -> " (map (fn NONE => "X" | SOME k' => string_of_int k') @@ -691,10 +704,10 @@ (* Proving equivalence of term *) -fun intro_rule thy pred mode = modename thy pred mode +fun intro_rule thy pred mode = modename_of thy pred mode |> Symtab.lookup (#function_intros (IndCodegenData.get thy)) |> the -fun elim_rule thy pred mode = modename thy pred mode +fun elim_rule thy pred mode = modename_of thy pred mode |> Symtab.lookup (#function_elims (IndCodegenData.get thy)) |> the fun pred_intros thy predname = let @@ -711,7 +724,7 @@ end fun function_definition thy pred mode = - modename thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the + modename_of thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the fun is_Type (Type _) = true | is_Type _ = false @@ -973,7 +986,7 @@ in nth (#elims (snd ind_result)) index end) fun prove_one_direction thy all_vs param_vs modes clauses ((pred, T), mode) = let - val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename thy pred mode)) + val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename_of thy pred mode)) (* val ind_result = InductivePackage.the_inductive (ProofContext.init thy) pred val index = find_index (fn s => s = pred) (#names (fst ind_result)) val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *) @@ -1225,7 +1238,7 @@ (* main function *********************************************************************) (*************************************************************************************) -fun create_def_equation' ind_name (mode : (int list option list * int list) option) thy = +fun create_def_equation' ind_name (mode : mode option) thy = let val _ = tracing ("starting create_def_equation' with " ^ ind_name) val (prednames, preds) = @@ -1249,6 +1262,7 @@ val _ = tracing ("calling preds: " ^ makestring name_of_calls) val _ = tracing "starting recursive compilations" fun rec_call name thy = + (*FIXME use member instead of infix mem*) if not (name mem (Symtab.keys (#modes (IndCodegenData.get thy)))) then create_def_equation name thy else thy val thy'' = fold rec_call name_of_calls thy'