# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 3085da75ed54950b02de01f89b9fd6b7ec6761b7 # Parent 1f990689349fff8849aa917d8b42bffa7d2f3749 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned diff -r 1f990689349f -r 3085da75ed54 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/MicroJava/J/Eval.thy Sat Oct 24 16:55:42 2009 +0200 @@ -40,7 +40,7 @@ ("_ \ _ -_[\]_-> _" [51,82,60,51,82] 81) and exec :: "[java_mb prog,xstate,stmt, xstate] => bool " ("_ \ _ -_-> _" [51,82,60,82] 81) - (*for G :: "java_mb prog"*) + for G :: "java_mb prog" where -- "evaluation of expressions" diff -r 1f990689349f -r 3085da75ed54 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 @@ -132,7 +132,7 @@ val th = th |> inline_equations thy |> Pred_Compile_Set.unfold_set_notation - |> AxClass.unoverload thy + (* |> AxClass.unoverload thy *) val (const, th) = if is_equationlike th then let diff -r 1f990689349f -r 3085da75ed54 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 @@ -102,9 +102,11 @@ (Free (Long_Name.base_name name ^ "P", pred_type T)) end -fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t - | mk_param lookup_pred t = - if Predicate_Compile_Aux.is_predT (fastype_of t) then +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 @@ -116,11 +118,13 @@ 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 = lookup_pred f + (*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; - + in param end + end (* creates the list of premises for every intro rule *) (* theory -> term -> (string list, term list list) *) @@ -272,7 +276,7 @@ val pred = lookup_pred t val nparams = get_nparams pred val (params, args) = chop nparams args - val params' = map (mk_param lookup_pred) params + val params' = map (mk_param thy lookup_pred) params in folds_map mk_prems' args (names', prems) |> map (fn (argvs, (names'', prems')) => @@ -318,16 +322,14 @@ 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 (@{const_name Cons}, T)) = - Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *) - | lookup_pred (Const (name, T)) = + 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)) = + | lookup_pred (Free (name, T)) = if member op = (map fst pnames) name then Free (name, transform_ho_typ T) else diff -r 1f990689349f -r 3085da75ed54 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 @@ -44,7 +44,7 @@ (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') val _ = print_intross options thy'' "Flattened introduction rules: " intross1 - val _ = "Replacing functions in introrules..." + val _ = print_step options "Replacing functions in introrules..." val intross2 = if fail_safe_mode then case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of diff -r 1f990689349f -r 3085da75ed54 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 @@ -259,82 +259,6 @@ (if null param_modes then "" else "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) -fun unify_consts thy cs intr_ts = - (let - val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); - fun varify (t, (i, ts)) = - let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t)) - in (maxidx_of_term t', t'::ts) end; - val (i, cs') = foldr varify (~1, []) cs; - val (i', intr_ts') = foldr varify (i, []) intr_ts; - val rec_consts = fold add_term_consts_2 cs' []; - val intr_consts = fold add_term_consts_2 intr_ts' []; - fun unify (cname, cT) = - let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) - in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; - val (env, _) = fold unify rec_consts (Vartab.empty, i'); - val subst = map_types (Envir.norm_type env) - in (map subst cs', map subst intr_ts') - end) handle Type.TUNIFY => - (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); - -(* how to detect polymorphic type dependencies in mutual recursive inductive predicates? *) -fun import_intros [] ctxt = ([], ctxt) - | import_intros (th :: ths) ctxt = - let - val ((_, [th']), ctxt') = Variable.import false [th] ctxt - val thy = ProofContext.theory_of ctxt' - val (pred, ([], args)) = strip_intro_concl 0 (prop_of th') - val ho_args = filter (is_predT o fastype_of) args - fun instantiate_typ th = - let - val (pred', _) = strip_intro_concl 0 (prop_of th) - val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then - error "Trying to instantiate another predicate" else () - val subst = Sign.typ_match thy - (fastype_of pred', fastype_of pred) Vartab.empty - val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T)) - (Vartab.dest subst) - in Thm.certify_instantiate (subst', []) th end; - fun instantiate_ho_args th = - let - val (_, (_, args')) = strip_intro_concl 0 (prop_of th) - val ho_args' = map dest_Var (filter (is_predT o fastype_of) args') - in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end - val ((_, ths'), ctxt1) = - Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' - in - (th' :: ths', ctxt1) - end - - -(* generation of case rules from user-given introduction rules *) - -fun mk_casesrule ctxt nparams introrules = - let - val (intros_th, ctxt1) = import_intros introrules ctxt - val intros = map prop_of intros_th - val (pred, (params, args)) = strip_intro_concl nparams (hd intros) - val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 - val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) - val (argnames, ctxt3) = Variable.variant_fixes - (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2 - val argvs = map2 (curry Free) argnames (map fastype_of args) - fun mk_case intro = - let - val (_, (_, args)) = strip_intro_concl nparams intro - val prems = Logic.strip_imp_prems intro - val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args) - val frees = (fold o fold_aterms) - (fn t as Free _ => - 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 cases = map mk_case intros - in Logic.list_implies (assm :: cases, prop) end; - - datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term | GeneratorPrem of term list * term | Generator of (string * typ); @@ -544,7 +468,82 @@ in fold print (all_modes_of thy) () end - + +(* importing introduction rules *) + +fun unify_consts thy cs intr_ts = + (let + val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); + fun varify (t, (i, ts)) = + let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t)) + in (maxidx_of_term t', t'::ts) end; + val (i, cs') = foldr varify (~1, []) cs; + val (i', intr_ts') = foldr varify (i, []) intr_ts; + val rec_consts = fold add_term_consts_2 cs' []; + val intr_consts = fold add_term_consts_2 intr_ts' []; + fun unify (cname, cT) = + let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) + in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; + val (env, _) = fold unify rec_consts (Vartab.empty, i'); + val subst = map_types (Envir.norm_type env) + in (map subst cs', map subst intr_ts') + end) handle Type.TUNIFY => + (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); + +fun import_intros _ [] ctxt = ([], ctxt) + | import_intros nparams (th :: ths) ctxt = + let + val ((_, [th']), ctxt') = Variable.import false [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 + fun instantiate_typ th = + let + val (pred', _) = strip_intro_concl 0 (prop_of th) + val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then + error "Trying to instantiate another predicate" else () + val subst = Sign.typ_match thy + (fastype_of pred', fastype_of pred) Vartab.empty + val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T)) + (Vartab.dest subst) + in Thm.certify_instantiate (subst', []) 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 ((_, ths'), ctxt1) = + Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' + in + (th' :: ths', ctxt1) + end + +(* generation of case rules from user-given introduction rules *) + +fun mk_casesrule ctxt nparams introrules = + let + val (intros_th, ctxt1) = import_intros nparams introrules ctxt + val intros = map prop_of intros_th + val (pred, (params, args)) = strip_intro_concl nparams (hd intros) + val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 + val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) + val (argnames, ctxt3) = Variable.variant_fixes + (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2 + val argvs = map2 (curry Free) argnames (map fastype_of args) + fun mk_case intro = + let + val (_, (_, args)) = strip_intro_concl nparams intro + val prems = Logic.strip_imp_prems intro + val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args) + val frees = (fold o fold_aterms) + (fn t as Free _ => + 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 cases = map mk_case intros + in Logic.list_implies (assm :: cases, prop) end; + (** preprocessing rules **) fun imp_prems_conv cv ct = diff -r 1f990689349f -r 3085da75ed54 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,7 +7,7 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred (mode: [], [1]) [show_steps, inductify] even . +code_pred (mode: [], [1]) [show_steps] even . thm odd.equation thm even.equation @@ -425,7 +425,7 @@ code_pred [inductify] splice . code_pred [inductify] List.rev . thm map.simps -code_pred [inductify, show_steps, show_intermediate_results] map . +code_pred [inductify] map . code_pred [inductify] foldr . code_pred [inductify] foldl . code_pred [inductify] filter .