src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 45461 130c90bb80b4
parent 45450 dc2236b19a3d
child 45701 615da8b8d758
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 10:40:36 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 12:10:49 2011 +0100
     1.3 @@ -66,23 +66,23 @@
     1.4    val find_split_thm : theory -> term -> thm option
     1.5    (* datastructures and setup for generic compilation *)
     1.6    datatype compilation_funs = CompilationFuns of {
     1.7 -    mk_predT : typ -> typ,
     1.8 -    dest_predT : typ -> typ,
     1.9 -    mk_bot : typ -> term,
    1.10 +    mk_monadT : typ -> typ,
    1.11 +    dest_monadT : typ -> typ,
    1.12 +    mk_empty : typ -> term,
    1.13      mk_single : term -> term,
    1.14      mk_bind : term * term -> term,
    1.15 -    mk_sup : term * term -> term,
    1.16 +    mk_plus : term * term -> term,
    1.17      mk_if : term -> term,
    1.18      mk_iterate_upto : typ -> term * term * term -> term,
    1.19      mk_not : term -> term,
    1.20      mk_map : typ -> typ -> term -> term -> term
    1.21    };
    1.22 -  val mk_predT : compilation_funs -> typ -> typ
    1.23 -  val dest_predT : compilation_funs -> typ -> typ
    1.24 -  val mk_bot : compilation_funs -> typ -> term
    1.25 +  val mk_monadT : compilation_funs -> typ -> typ
    1.26 +  val dest_monadT : compilation_funs -> typ -> typ
    1.27 +  val mk_empty : compilation_funs -> typ -> term
    1.28    val mk_single : compilation_funs -> term -> term
    1.29    val mk_bind : compilation_funs -> term * term -> term
    1.30 -  val mk_sup : compilation_funs -> term * term -> term
    1.31 +  val mk_plus : compilation_funs -> term * term -> term
    1.32    val mk_if : compilation_funs -> term -> term
    1.33    val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
    1.34    val mk_not : compilation_funs -> term -> term
    1.35 @@ -699,24 +699,24 @@
    1.36  (* datastructures and setup for generic compilation *)
    1.37  
    1.38  datatype compilation_funs = CompilationFuns of {
    1.39 -  mk_predT : typ -> typ,
    1.40 -  dest_predT : typ -> typ,
    1.41 -  mk_bot : typ -> term,
    1.42 +  mk_monadT : typ -> typ,
    1.43 +  dest_monadT : typ -> typ,
    1.44 +  mk_empty : typ -> term,
    1.45    mk_single : term -> term,
    1.46    mk_bind : term * term -> term,
    1.47 -  mk_sup : term * term -> term,
    1.48 +  mk_plus : term * term -> term,
    1.49    mk_if : term -> term,
    1.50    mk_iterate_upto : typ -> term * term * term -> term,
    1.51    mk_not : term -> term,
    1.52    mk_map : typ -> typ -> term -> term -> term
    1.53  };
    1.54  
    1.55 -fun mk_predT (CompilationFuns funs) = #mk_predT funs
    1.56 -fun dest_predT (CompilationFuns funs) = #dest_predT funs
    1.57 -fun mk_bot (CompilationFuns funs) = #mk_bot funs
    1.58 +fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
    1.59 +fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
    1.60 +fun mk_empty (CompilationFuns funs) = #mk_empty funs
    1.61  fun mk_single (CompilationFuns funs) = #mk_single funs
    1.62  fun mk_bind (CompilationFuns funs) = #mk_bind funs
    1.63 -fun mk_sup (CompilationFuns funs) = #mk_sup funs
    1.64 +fun mk_plus (CompilationFuns funs) = #mk_plus funs
    1.65  fun mk_if (CompilationFuns funs) = #mk_if funs
    1.66  fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
    1.67  fun mk_not (CompilationFuns funs) = #mk_not funs
    1.68 @@ -729,7 +729,7 @@
    1.69      val Ts = binder_types T
    1.70      val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
    1.71    in
    1.72 -    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
    1.73 +    inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
    1.74    end;
    1.75  
    1.76  (* Different options for compiler *)