# HG changeset patch # User bulwahn # Date 1269876653 -7200 # Node ID d82682936c529516cb10f68908633905898b7eff # Parent ee84eac072902fe8de342535e44c422a6eeb9c66 adding registration of functions in the function flattening diff -r ee84eac07290 -r d82682936c52 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:53 2010 +0200 @@ -46,6 +46,9 @@ | eq_mode (Bool, Bool) = true | eq_mode _ = false +fun list_fun_mode [] = Bool + | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms) + (* name: binder_modes? *) fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode' | strip_fun_mode Bool = [] diff -r ee84eac07290 -r d82682936c52 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:53 2010 +0200 @@ -736,7 +736,7 @@ Alt_Names_Data.map (Symtab.insert_list (op =) (pred_name, (mode, fun_name))) fun alternative_function_of thy pred_name mode = - AList.lookup (op =) (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode + AList.lookup eq_mode (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode (* datastructures and setup for generic compilation *) diff -r ee84eac07290 -r d82682936c52 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 29 17:30:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 29 17:30:53 2010 +0200 @@ -327,8 +327,14 @@ val thy'' = Fun_Pred.map (fold Item_Net.update (map (apfst Logic.varify_global) (distinct (op =) funs ~~ (#preds ind_result)))) thy' + fun functional_mode_of T = + list_fun_mode (replicate (length (binder_types T)) Input @ [Output]) + val thy''' = fold + (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function + predname (functional_mode_of T) name) + (prednames ~~ distinct (op =) funs) thy'' in - (specs, thy'') + (specs, thy''') end fun rewrite_intro thy intro =