--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 29 11:56:02 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,437 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-Preprocessing functions to predicates
-*)
-
-signature PREDICATE_COMPILE_FUN =
-sig
-val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
- val rewrite_intro : theory -> thm -> thm list
- val setup_oracle : theory -> theory
- val pred_of_function : theory -> string -> string option
-end;
-
-structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
-struct
-
-
-(* Oracle for preprocessing *)
-
-val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
-
-fun the_oracle () =
- case !oracle of
- NONE => error "Oracle is not setup"
- | SOME (_, oracle) => oracle
-
-val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
- (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
-
-
-fun is_funtype (Type ("fun", [_, _])) = true
- | is_funtype _ = false;
-
-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;
-
-(* Table from constant name (string) to term of inductive predicate *)
-structure Pred_Compile_Preproc = TheoryDataFun
-(
- type T = string Symtab.table;
- val empty = Symtab.empty;
- val copy = I;
- val extend = I;
- 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)
-
-
-fun transform_ho_typ (T as Type ("fun", _)) =
- let
- val (Ts, T') = strip_type T
- in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
-| transform_ho_typ t = t
-
-fun transform_ho_arg arg =
- case (fastype_of arg) of
- (T as Type ("fun", _)) =>
- (case arg of
- Free (name, _) => Free (name, transform_ho_typ T)
- | _ => error "I am surprised")
-| _ => arg
-
-fun pred_type T =
- let
- val (Ts, T') = strip_type T
- val Ts' = map transform_ho_typ Ts
- in
- (Ts' @ [T']) ---> HOLogic.boolT
- end;
-
-(* FIXME: create new predicate name -- does not avoid nameclashing *)
-fun pred_of f =
- let
- val (name, T) = dest_Const f
- in
- if (body_type T = @{typ bool}) then
- (Free (Long_Name.base_name name ^ "P", T))
- else
- (Free (Long_Name.base_name name ^ "P", pred_type T))
- end
-
-fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
- | mk_param thy lookup_pred t =
- let
- val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
- in if Predicate_Compile_Aux.is_predT (fastype_of t) then
- t
- else
- let
- val (vs, body) = strip_abs t
- val names = Term.add_free_names body []
- val vs_names = Name.variant_list names (map fst vs)
- val vs' = map2 (curry Free) vs_names (map snd vs)
- val body' = subst_bounds (rev vs', body)
- val (f, args) = strip_comb body'
- val resname = Name.variant (vs_names @ names) "res"
- val resvar = Free (resname, body_type (fastype_of body'))
- (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
- val pred_body = list_comb (P, args @ [resvar])
- *)
- val pred_body = HOLogic.mk_eq (body', resvar)
- val param = fold_rev lambda (vs' @ [resvar]) pred_body
- in param end
- end
-(* creates the list of premises for every intro rule *)
-(* theory -> term -> (string list, term list list) *)
-
-fun dest_code_eqn eqn = let
- val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
- val (func, args) = strip_comb lhs
-in ((func, args), rhs) end;
-
-fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
-
-fun string_of_term t =
- case t of
- Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
- | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
- | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
- | Bound i => "Bound " ^ string_of_int i
- | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
- | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
-
-fun ind_package_get_nparams thy name =
- case try (Inductive.the_inductive (ProofContext.init thy)) name of
- SOME (_, result) => length (Inductive.params_of (#raw_induct result))
- | NONE => error ("No such predicate: " ^ quote name)
-
-(* TODO: does not work with higher order functions yet *)
-fun mk_rewr_eq (func, pred) =
- let
- val (argTs, resT) = (strip_type (fastype_of func))
- val nctxt =
- Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
- val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
- val ([resname], nctxt'') = Name.variants ["r"] nctxt'
- val args = map Free (argnames ~~ argTs)
- val res = Free (resname, resT)
- in Logic.mk_equals
- (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
- end;
-
-fun has_split_rule_cname @{const_name "nat_case"} = true
- | has_split_rule_cname @{const_name "list_case"} = true
- | has_split_rule_cname _ = false
-
-fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
- | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
- | has_split_rule_term thy _ = false
-
-fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
- | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
- | has_split_rule_term' thy c = has_split_rule_term thy c
-
-fun prepare_split_thm ctxt split_thm =
- (split_thm RS @{thm iffD2})
- |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
- @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
-
-fun find_split_thm thy (Const (name, typ)) =
- let
- fun split_name str =
- case first_field "." str
- of (SOME (field, rest)) => field :: split_name rest
- | NONE => [str]
- val splitted_name = split_name name
- in
- if length splitted_name > 0 andalso
- String.isSuffix "_case" (List.last splitted_name)
- then
- (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
- |> space_implode "."
- |> PureThy.get_thm thy
- |> SOME
- handle ERROR msg => NONE
- else NONE
- end
- | find_split_thm _ _ = NONE
-
-fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
- | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
- | find_split_thm' thy c = find_split_thm thy c
-
-fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-
-fun folds_map f xs y =
- let
- fun folds_map' acc [] y = [(rev acc, y)]
- | folds_map' acc (x :: xs) y =
- maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
- in
- folds_map' [] xs y
- end;
-
-fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
- let
- fun mk_prems' (t as Const (name, T)) (names, prems) =
- if is_constr thy name orelse (is_none (try lookup_pred t)) then
- [(t, (names, prems))]
- else [(lookup_pred t, (names, prems))]
- | mk_prems' (t as Free (f, T)) (names, prems) =
- [(lookup_pred t, (names, prems))]
- | mk_prems' (t as Abs _) (names, prems) =
- if Predicate_Compile_Aux.is_predT (fastype_of t) then
- [(t, (names, prems))] else error "mk_prems': Abs "
- (* mk_param *)
- | mk_prems' t (names, prems) =
- if Predicate_Compile_Aux.is_constrt thy t then
- [(t, (names, prems))]
- else
- if has_split_rule_term' thy (fst (strip_comb t)) then
- let
- val (f, args) = strip_comb t
- val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
- (* TODO: contextify things - this line is to unvarify the split_thm *)
- (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
- val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
- fun mk_prems_of_assm assm =
- let
- val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
- val var_names = Name.variant_list names (map fst vTs)
- val vars = map Free (var_names ~~ (map snd vTs))
- val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
- val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
- in
- mk_prems' inner_t (var_names @ names, prems' @ prems)
- end
- in
- maps mk_prems_of_assm assms
- end
- else
- let
- 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
- fun mk_prems'' (t as Const (c, _)) =
- if is_constr thy c orelse (is_none (try lookup_pred t)) then
- folds_map mk_prems' args (names', prems) |>
- map
- (fn (argvs, (names'', prems')) =>
- let
- val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
- in (names'', prem :: prems') end)
- else
- let
- val pred = lookup_pred t
- val nparams = get_nparams pred
- val (params, args) = chop nparams args
- val params' = map (mk_param thy lookup_pred) params
- in
- folds_map mk_prems' args (names', prems)
- |> map (fn (argvs, (names'', prems')) =>
- let
- val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
- in (names'', prem :: prems') end)
- end
- | mk_prems'' (t as Free (_, _)) =
- let
- (* higher order argument call *)
- val pred = lookup_pred t
- in
- folds_map mk_prems' args (resname :: names, prems)
- |> map (fn (argvs, (names', prems')) =>
- let
- val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
- in (names', prem :: prems') end)
- end
- | mk_prems'' t =
- error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
- in
- map (pair resvar) (mk_prems'' f)
- end
- in
- mk_prems' t (names, prems)
- end;
-
-(* assumption: mutual recursive predicates all have the same parameters. *)
-fun define_predicates specs thy =
- if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
- ([], thy)
- else
- let
- val consts = map fst specs
- val eqns = maps snd specs
- (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
- (* create prednames *)
- val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
- val argss' = map (map transform_ho_arg) argss
- val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss'))
- val preds = map pred_of funs
- val prednames = map (fst o dest_Free) preds
- val funnames = map (fst o dest_Const) funs
- val fun_pred_names = (funnames ~~ prednames)
- (* mapping from term (Free or Const) to term *)
- fun lookup_pred (Const (name, T)) =
- (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
- SOME c => Const (c, pred_type T)
- | NONE =>
- (case AList.lookup op = fun_pred_names name of
- SOME f => Free (f, pred_type T)
- | NONE => Const (name, T)))
- | lookup_pred (Free (name, T)) =
- if member op = (map fst pnames) name then
- Free (name, transform_ho_typ T)
- else
- Free (name, T)
- | lookup_pred t =
- error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
-
- (* mapping from term (predicate term, not function term!) to int *)
- fun get_nparams (Const (name, _)) =
- the_default 0 (try (ind_package_get_nparams thy) name)
- | get_nparams (Free (name, _)) =
- (if member op = prednames name then
- length pnames
- else 0)
- | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
-
- (* create intro rules *)
-
- fun mk_intros ((func, pred), (args, rhs)) =
- if (body_type (fastype_of func) = @{typ bool}) then
- (*TODO: preprocess predicate definition of rhs *)
- [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
- else
- let
- val names = Term.add_free_names rhs []
- in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
- |> map (fn (resultt, (names', prems)) =>
- Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
- end
- fun mk_rewr_thm (func, pred) = @{thm refl}
- in
- case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
- NONE => ([], thy)
- | SOME intr_ts =>
- if is_some (try (map (cterm_of thy)) intr_ts) then
- let
- val (ind_result, thy') =
- Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
- alt_name = Binding.empty, coind = false, no_elim = false,
- no_ind = false, skip_mono = false, fork_mono = false}
- (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
- pnames
- (map (fn x => (Attrib.empty_binding, x)) intr_ts)
- [] thy
- 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 thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
- in
- (specs, thy'')
- end
- else
- let
- val _ = tracing "Introduction rules of function_predicate are not welltyped"
- in ([], thy) end
- end
-
-(* preprocessing intro rules - uses oracle *)
-
-(* theory -> thm -> thm *)
-fun rewrite_intro thy intro =
- let
- fun lookup_pred (Const (name, T)) =
- (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
- SOME c => Const (c, pred_type T)
- | NONE => error ("Function " ^ name ^ " is not inductified"))
- | lookup_pred (Free (name, T)) = Free (name, T)
- | lookup_pred _ = error "lookup function is not defined!"
-
- fun get_nparams (Const (name, _)) =
- the_default 0 (try (ind_package_get_nparams thy) name)
- | get_nparams (Free _) = 0
- | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
-
- val intro_t = (Logic.unvarify o prop_of) intro
- val (prems, concl) = Logic.strip_horn intro_t
- val frees = map fst (Term.add_frees intro_t [])
- fun rewrite prem names =
- let
- val t = (HOLogic.dest_Trueprop prem)
- val (lit, mk_lit) = case try HOLogic.dest_not t of
- SOME t => (t, HOLogic.mk_not)
- | NONE => (t, I)
- val (P, args) = (strip_comb lit)
- in
- folds_map (
- fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
- else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
- |> map (fn (resargs, (names', prems')) =>
- let
- val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
- in (prem'::prems', names') end)
- end
- val intro_ts' = folds_map rewrite prems frees
- |> maps (fn (prems', frees') =>
- rewrite concl frees'
- |> map (fn (concl'::conclprems, _) =>
- Logic.list_implies ((flat prems') @ conclprems, concl')))
- in
- map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
- end;
-
-end;