added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
authorbulwahn
Mon Mar 29 17:30:53 2010 +0200 (2010-03-29)
changeset 36034ee84eac07290
parent 36033 7106f079bd05
child 36035 d82682936c52
added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:53 2010 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val intros_of : theory -> string -> thm list
     1.5    val add_intro : thm -> theory -> theory
     1.6    val set_elim : thm -> theory -> theory
     1.7 +  val register_alternative_function : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory
     1.8 +  val alternative_function_of : theory -> string -> Predicate_Compile_Aux.mode -> string option
     1.9    val preprocess_intro : theory -> thm -> thm
    1.10    val print_stored_rules : theory -> unit
    1.11    val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit
    1.12 @@ -720,6 +722,22 @@
    1.13      PredData.map (Graph.map_node name (map_pred_data set))
    1.14    end
    1.15  
    1.16 +(* registration of alternative function names *)
    1.17 +
    1.18 +structure Alt_Names_Data = Theory_Data
    1.19 +(
    1.20 +  type T = (mode * string) list Symtab.table;
    1.21 +  val empty = Symtab.empty;
    1.22 +  val extend = I;
    1.23 +  val merge = Symtab.merge (op =);
    1.24 +);
    1.25 +
    1.26 +fun register_alternative_function pred_name mode fun_name =
    1.27 +  Alt_Names_Data.map (Symtab.insert_list (op =) (pred_name, (mode, fun_name)))
    1.28 +
    1.29 +fun alternative_function_of thy pred_name mode =
    1.30 +  AList.lookup (op =) (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode
    1.31 +
    1.32  (* datastructures and setup for generic compilation *)
    1.33  
    1.34  datatype compilation_funs = CompilationFuns of {
    1.35 @@ -1919,9 +1937,18 @@
    1.36          (t, Term Input) => SOME t
    1.37        | (t, Term Output) => NONE
    1.38        | (Const (name, T), Context mode) =>
    1.39 -        SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
    1.40 -          (ProofContext.theory_of ctxt) name mode,
    1.41 -          Comp_Mod.funT_of compilation_modifiers mode T))
    1.42 +        (case alternative_function_of (ProofContext.theory_of ctxt) name mode of
    1.43 +          SOME alt_function_name =>
    1.44 +            let
    1.45 +              val (inpTs, outpTs) = split_modeT' mode (binder_types T)
    1.46 +              val bs = map (pair "x") inpTs
    1.47 +              val bounds = map Bound (rev (0 upto (length bs) - 1))
    1.48 +              val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs)
    1.49 +            in SOME (list_abs (bs, mk_single compfuns (list_comb (f, bounds)))) end
    1.50 +        | NONE =>
    1.51 +          SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
    1.52 +            (ProofContext.theory_of ctxt) name mode,
    1.53 +            Comp_Mod.funT_of compilation_modifiers mode T)))
    1.54        | (Free (s, T), Context m) =>
    1.55          SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
    1.56        | (t, Context m) =>